[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
x : M₂
⊢ IsOrtho B 0 x
[PROOFSTEP]
dsimp only [IsOrtho]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
x : M₂
⊢ ↑(↑B 0) x = 0
[PROOFSTEP]
rw [map_zero B, zero_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
x y : M₁
⊢ IsOrtho B x y ↔ IsOrtho (flip B) y x
[PROOFSTEP]
simp_rw [isOrtho_def, flip_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ IsOrthoᵢ B v ↔ IsOrthoᵢ (flip B) v
[PROOFSTEP]
simp_rw [isOrthoᵢ_def]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0) ↔ ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0) → ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
[PROOFSTEP]
intro h i j hij
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0) → ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
[PROOFSTEP]
intro h i j hij
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑(flip B) (v i)) (v j) = 0
[PROOFSTEP]
rw [flip_apply]
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v j)) (v i) = 0
[PROOFSTEP]
exact h j i (Ne.symm hij)
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v i)) (v j) = 0
[PROOFSTEP]
simp_rw [flip_apply] at h 
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v j)) (v i) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v i)) (v j) = 0
[PROOFSTEP]
exact h j i (Ne.symm hij)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ IsOrtho B x y ↔ IsOrtho B (a • x) y
[PROOFSTEP]
dsimp only [IsOrtho]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ ↑(↑B x) y = 0 ↔ ↑(↑B (a • x)) y = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ ↑(↑B x) y = 0 → ↑(↑B (a • x)) y = 0
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ ↑(↑B (a • x)) y = 0 → ↑(↑B x) y = 0
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : ↑(↑B x) y = 0
⊢ ↑(↑B (a • x)) y = 0
[PROOFSTEP]
rw [map_smulₛₗ₂, H, smul_zero]
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : ↑(↑B (a • x)) y = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
rw [map_smulₛₗ₂, smul_eq_zero] at H 
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : ↑I₁ a = 0 ∨ ↑(↑B x) y = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
cases' H with H H
[GOAL]
case mpr.inl
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : ↑I₁ a = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
rw [map_eq_zero I₁] at H 
[GOAL]
case mpr.inl
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : a = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
trivial
[GOAL]
case mpr.inr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : ↑(↑B x) y = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
exact H
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
⊢ IsOrtho B x y ↔ IsOrtho B x (a • y)
[PROOFSTEP]
dsimp only [IsOrtho]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
⊢ ↑(↑B x) y = 0 ↔ ↑(↑B x) (a • y) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
⊢ ↑(↑B x) y = 0 → ↑(↑B x) (a • y) = 0
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
⊢ ↑(↑B x) (a • y) = 0 → ↑(↑B x) y = 0
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : ↑(↑B x) y = 0
⊢ ↑(↑B x) (a • y) = 0
[PROOFSTEP]
rw [map_smulₛₗ, H, smul_zero]
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : ↑(↑B x) (a • y) = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
rw [map_smulₛₗ, smul_eq_zero] at H 
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : ↑I₂ a = 0 ∨ ↑(↑B x) y = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
cases' H with H H
[GOAL]
case mpr.inl
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : ↑I₂ a = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
simp at H 
[GOAL]
case mpr.inl
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : a = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
exfalso
[GOAL]
case mpr.inl.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : a = 0
⊢ False
[PROOFSTEP]
exact ha H
[GOAL]
case mpr.inr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
H : ↑(↑B x) y = 0
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
exact H
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
⊢ LinearIndependent K₁ v
[PROOFSTEP]
classical
rw [linearIndependent_iff']
intro s w hs i hi
have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
have hsum : (s.sum fun j : n ↦ I₁ (w j) * B (v j) (v i)) = I₁ (w i) * B (v i) (v i) :=
  by
  apply Finset.sum_eq_single_of_mem i hi
  intro j _hj hij
  rw [isOrthoᵢ_def.1 hv₁ _ _ hij, mul_zero]
simp_rw [B.map_sum₂, map_smulₛₗ₂, smul_eq_mul, hsum] at this 
apply (map_eq_zero I₁).mp
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
⊢ LinearIndependent K₁ v
[PROOFSTEP]
rw [linearIndependent_iff']
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
⊢ ∀ (s : Finset n) (g : n → K₁), ∑ i in s, g i • v i = 0 → ∀ (i : n), i ∈ s → g i = 0
[PROOFSTEP]
intro s w hs i hi
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
⊢ w i = 0
[PROOFSTEP]
have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
⊢ ↑(↑B (∑ i in s, w i • v i)) (v i) = 0
[PROOFSTEP]
rw [hs, map_zero, zero_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
this : ↑(↑B (∑ i in s, w i • v i)) (v i) = 0
⊢ w i = 0
[PROOFSTEP]
have hsum : (s.sum fun j : n ↦ I₁ (w j) * B (v j) (v i)) = I₁ (w i) * B (v i) (v i) :=
  by
  apply Finset.sum_eq_single_of_mem i hi
  intro j _hj hij
  rw [isOrthoᵢ_def.1 hv₁ _ _ hij, mul_zero]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
this : ↑(↑B (∑ i in s, w i • v i)) (v i) = 0
⊢ ∑ j in s, ↑I₁ (w j) * ↑(↑B (v j)) (v i) = ↑I₁ (w i) * ↑(↑B (v i)) (v i)
[PROOFSTEP]
apply Finset.sum_eq_single_of_mem i hi
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
this : ↑(↑B (∑ i in s, w i • v i)) (v i) = 0
⊢ ∀ (b : n), b ∈ s → b ≠ i → ↑I₁ (w b) * ↑(↑B (v b)) (v i) = 0
[PROOFSTEP]
intro j _hj hij
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
this : ↑(↑B (∑ i in s, w i • v i)) (v i) = 0
j : n
_hj : j ∈ s
hij : j ≠ i
⊢ ↑I₁ (w j) * ↑(↑B (v j)) (v i) = 0
[PROOFSTEP]
rw [isOrthoᵢ_def.1 hv₁ _ _ hij, mul_zero]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
this : ↑(↑B (∑ i in s, w i • v i)) (v i) = 0
hsum : ∑ j in s, ↑I₁ (w j) * ↑(↑B (v j)) (v i) = ↑I₁ (w i) * ↑(↑B (v i)) (v i)
⊢ w i = 0
[PROOFSTEP]
simp_rw [B.map_sum₂, map_smulₛₗ₂, smul_eq_mul, hsum] at this 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
hsum : ∑ j in s, ↑I₁ (w j) * ↑(↑B (v j)) (v i) = ↑I₁ (w i) * ↑(↑B (v i)) (v i)
this : ↑I₁ (w i) * ↑(↑B (v i)) (v i) = 0
⊢ w i = 0
[PROOFSTEP]
apply (map_eq_zero I₁).mp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : Field K
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
I₁' : K₁ →+* K
J₁ J₂ : K →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K
v : n → V₁
hv₁ : IsOrthoᵢ B v
hv₂ : ∀ (i : n), ¬IsOrtho B (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i in s, w i • v i = 0
i : n
hi : i ∈ s
hsum : ∑ j in s, ↑I₁ (w j) * ↑(↑B (v j)) (v i) = ↑I₁ (w i) * ↑(↑B (v i)) (v i)
this : ↑I₁ (w i) * ↑(↑B (v i)) (v i) = 0
⊢ ↑I₁ (w i) = 0
[PROOFSTEP]
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
p : Submodule R₁ M₁
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑(↑(domRestrict₁₂ B p p) x✝¹) x✝ = 0 → ↑(↑(domRestrict₁₂ B p p) x✝) x✝¹ = 0
[PROOFSTEP]
simp_rw [domRestrict₁₂_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
p : Submodule R₁ M₁
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑(↑B ↑x✝¹) ↑x✝ = 0 → ↑(↑B ↑x✝) ↑x✝¹ = 0
[PROOFSTEP]
exact H _ _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
⊢ ker (flip B) = ⊥
[PROOFSTEP]
refine' ker_eq_bot'.mpr fun _ hx ↦ ker_eq_bot'.mp h _ _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
x✝ : M₁
hx : ↑(flip B) x✝ = 0
⊢ ↑B x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker B = ⊥
x✝¹ : M₁
hx : ↑(flip B) x✝¹ = 0
x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = ↑0 x✝
[PROOFSTEP]
exact H _ _ (LinearMap.congr_fun hx _)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
⊢ ker B = ⊥ ↔ ker (flip B) = ⊥
[PROOFSTEP]
refine' ⟨ker_flip_eq_bot H, fun h ↦ _⟩
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker (flip B) = ⊥
⊢ ker B = ⊥
[PROOFSTEP]
exact (congr_arg _ B.flip_flip.symm).trans (ker_flip_eq_bot (flip_isRefl_iff.mpr H) h)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
x y : M
H1 : ↑(↑B x) y = 0
⊢ ↑(↑B y) x = 0
[PROOFSTEP]
rw [← H.eq]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
x y : M
H1 : ↑(↑B x) y = 0
⊢ ↑I (↑(↑B x) y) = 0
[PROOFSTEP]
simp [H1]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
p : Submodule R M
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑I (↑(↑(domRestrict₁₂ B p p) x✝¹) x✝) = ↑(↑(domRestrict₁₂ B p p) x✝) x✝¹
[PROOFSTEP]
simp_rw [domRestrict₁₂_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : IsSymm B
p : Submodule R M
x✝¹ x✝ : { x // x ∈ p }
⊢ ↑I (↑(↑B ↑x✝¹) ↑x✝) = ↑(↑B ↑x✝) ↑x✝¹
[PROOFSTEP]
exact H _ _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
⊢ IsSymm B ↔ B = flip B
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
⊢ IsSymm B → B = flip B
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
⊢ B = flip B → IsSymm B
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : IsSymm B
⊢ B = flip B
[PROOFSTEP]
ext
[GOAL]
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : IsSymm B
x✝¹ x✝ : M
⊢ ↑(↑B x✝¹) x✝ = ↑(↑(flip B) x✝¹) x✝
[PROOFSTEP]
rw [← h, flip_apply, RingHom.id_apply]
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
⊢ IsSymm B
[PROOFSTEP]
intro x y
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
x y : M
⊢ ↑(RingHom.id R) (↑(↑B x) y) = ↑(↑B y) x
[PROOFSTEP]
conv_lhs => rw [h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
x y : M
| ↑(RingHom.id R) (↑(↑B x) y)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
x y : M
| ↑(RingHom.id R) (↑(↑B x) y)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B✝ : M →ₛₗ[I] M →ₗ[R] R
B : M →ₗ[R] M →ₗ[R] R
h : B = flip B
x y : M
| ↑(RingHom.id R) (↑(↑B x) y)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
⊢ -↑(↑B x) y = ↑(↑B y) x
[PROOFSTEP]
have H1 : B (y + x) (y + x) = 0 := self_eq_zero H (y + x)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : ↑(↑B (y + x)) (y + x) = 0
⊢ -↑(↑B x) y = ↑(↑B y) x
[PROOFSTEP]
simp [map_add, self_eq_zero H] at H1 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : ↑(↑B x) y + ↑(↑B y) x = 0
⊢ -↑(↑B x) y = ↑(↑B y) x
[PROOFSTEP]
rw [add_eq_zero_iff_neg_eq] at H1 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
H1 : -↑(↑B x) y = ↑(↑B y) x
⊢ -↑(↑B x) y = ↑(↑B y) x
[PROOFSTEP]
exact H1
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
⊢ IsRefl B
[PROOFSTEP]
intro x y h
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H : IsAlt B
x y : M₁
h : ↑(↑B x) y = 0
⊢ ↑(↑B y) x = 0
[PROOFSTEP]
rw [← neg H, h, neg_zero]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ IsAlt B ↔ B = -flip B
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ IsAlt B → B = -flip B
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B = -flip B → IsAlt B
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
⊢ B = -flip B
[PROOFSTEP]
ext
[GOAL]
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
x✝¹ x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = ↑(↑(-flip B) x✝¹) x✝
[PROOFSTEP]
simp_rw [neg_apply, flip_apply]
[GOAL]
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
x✝¹ x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = -↑(↑B x✝) x✝¹
[PROOFSTEP]
exact (h.neg _ _).symm
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
⊢ IsAlt B
[PROOFSTEP]
intro x
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
⊢ ↑(↑B x) x = 0
[PROOFSTEP]
let h' := congr_fun₂ h x x
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
h' : ↑(↑B x) x = ↑(↑(-flip B) x) x := congr_fun₂ h x x
⊢ ↑(↑B x) x = 0
[PROOFSTEP]
simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h' 
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
h' : ↑(↑B x) x + ↑(↑B x) x = 0
⊢ ↑(↑B x) x = 0
[PROOFSTEP]
exact add_self_eq_zero.mp h'
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n✝ : Type u_18
inst✝³ : CommRing R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
N : Submodule R₁ M₁
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
a✝ b✝ : M₁
hx : a✝ ∈ {m | ∀ (n : M₁), n ∈ N → LinearMap.IsOrtho B n m}
hy : b✝ ∈ {m | ∀ (n : M₁), n ∈ N → LinearMap.IsOrtho B n m}
n : M₁
hn : n ∈ N
⊢ LinearMap.IsOrtho B n (a✝ + b✝)
[PROOFSTEP]
rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn, zero_add]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n✝ : Type u_18
inst✝³ : CommRing R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
N : Submodule R₁ M₁
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
c : R₁
x : M₁
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {m | ∀ (n : M₁), n ∈ N → LinearMap.IsOrtho B n m},
              add_mem' :=
                (_ :
                  ∀ {a b : M₁},
                    a ∈ {m | ∀ (n : M₁), n ∈ N → LinearMap.IsOrtho B n m} →
                      b ∈ {m | ∀ (n : M₁), n ∈ N → LinearMap.IsOrtho B n m} →
                        ∀ (n : M₁), n ∈ N → LinearMap.IsOrtho B n (a + b)) },
          zero_mem' := (_ : ∀ (x : M₁), x ∈ N → LinearMap.IsOrtho B x 0) }.toAddSubsemigroup.carrier
n : M₁
hn : n ∈ N
⊢ LinearMap.IsOrtho B n (c • x)
[PROOFSTEP]
rw [LinearMap.IsOrtho, LinearMap.map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
⊢ Submodule.span K₁ {x} ⊓ Submodule.orthogonalBilin (Submodule.span K₁ {x}) B = ⊥
[PROOFSTEP]
rw [← Finset.coe_singleton]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
⊢ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin (Submodule.span K₁ ↑{x}) B = ⊥
[PROOFSTEP]
refine' eq_bot_iff.2 fun y h ↦ _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
y : V₁
h : y ∈ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin (Submodule.span K₁ ↑{x}) B
⊢ y ∈ ⊥
[PROOFSTEP]
rcases mem_span_finset.1 h.1 with ⟨μ, rfl⟩
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : ∑ i in {x}, μ i • i ∈ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin (Submodule.span K₁ ↑{x}) B
⊢ ∑ i in {x}, μ i • i ∈ ⊥
[PROOFSTEP]
replace h := h.2 x (by simp [Submodule.mem_span] : x ∈ Submodule.span K₁ ({ x } : Finset V₁))
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : ∑ i in {x}, μ i • i ∈ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin (Submodule.span K₁ ↑{x}) B
⊢ x ∈ Submodule.span K₁ ↑{x}
[PROOFSTEP]
simp [Submodule.mem_span]
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : IsOrtho B x (∑ i in {x}, μ i • i)
⊢ ∑ i in {x}, μ i • i ∈ ⊥
[PROOFSTEP]
rw [Finset.sum_singleton] at h ⊢
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : IsOrtho B x (μ x • x)
⊢ μ x • x ∈ ⊥
[PROOFSTEP]
suffices hμzero : μ x = 0
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : IsOrtho B x (μ x • x)
hμzero : μ x = 0
⊢ μ x • x ∈ ⊥
[PROOFSTEP]
rw [hμzero, zero_smul, Submodule.mem_bot]
[GOAL]
case hμzero
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : IsOrtho B x (μ x • x)
⊢ μ x = 0
[PROOFSTEP]
rw [isOrtho_def, map_smulₛₗ, smul_eq_mul] at h 
[GOAL]
case hμzero
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : ↑J₁' (μ x) * ↑(↑B x) x = 0
⊢ μ x = 0
[PROOFSTEP]
exact Or.elim (zero_eq_mul.mp h.symm) (fun y ↦ by simpa using y) (fun hfalse ↦ False.elim $ hx hfalse)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K
x : V₁
hx : ¬IsOrtho B x x
μ : V₁ → K₁
h : ↑J₁' (μ x) * ↑(↑B x) x = 0
y : ↑J₁' (μ x) = 0
⊢ μ x = 0
[PROOFSTEP]
simpa using y
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x : V
⊢ Submodule.orthogonalBilin (Submodule.span K {x}) B = ker (↑B x)
[PROOFSTEP]
ext y
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x y : V
⊢ y ∈ Submodule.orthogonalBilin (Submodule.span K {x}) B ↔ y ∈ ker (↑B x)
[PROOFSTEP]
simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y) ↔ ↑(↑B x) y = 0
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y) → ↑(↑B x) y = 0
[PROOFSTEP]
exact fun h ↦ h x ⟨1, one_smul _ _⟩
[GOAL]
case h.mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x y : V
⊢ ↑(↑B x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → IsOrtho B n y
[PROOFSTEP]
rintro h _ ⟨z, rfl⟩
[GOAL]
case h.mpr.intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x y : V
h : ↑(↑B x) y = 0
z : K
⊢ IsOrtho B (z • x) y
[PROOFSTEP]
rw [isOrtho_def, map_smulₛₗ₂, smul_eq_zero]
[GOAL]
case h.mpr.intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₛₗ[J] K
x y : V
h : ↑(↑B x) y = 0
z : K
⊢ ↑(RingHom.id K) z = 0 ∨ ↑(↑B x) y = 0
[PROOFSTEP]
exact Or.intro_right _ h
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ Submodule.orthogonalBilin (Submodule.span K {x}) B = ⊤
[PROOFSTEP]
rw [orthogonal_span_singleton_eq_to_lin_ker]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ ker (↑B x) = ⊤
[PROOFSTEP]
exact (B x).span_singleton_sup_ker_eq_top hx
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
⊢ IsAdjointPair B B' f g ↔ comp B' f = compl₂ B g
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
⊢ IsAdjointPair B B' f g → comp B' f = compl₂ B g
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
⊢ comp B' f = compl₂ B g → IsAdjointPair B B' f g
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
⊢ comp B' f = compl₂ B g
[PROOFSTEP]
ext x y
[GOAL]
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
x : M
y : M₁
⊢ ↑(↑(comp B' f) x) y = ↑(↑(compl₂ B g) x) y
[PROOFSTEP]
rw [comp_apply, compl₂_apply]
[GOAL]
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
x : M
y : M₁
⊢ ↑(↑B' (↑f x)) y = ↑(↑B x) (↑g y)
[PROOFSTEP]
exact h x y
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : comp B' f = compl₂ B g
⊢ IsAdjointPair B B' f g
[PROOFSTEP]
intro _ _
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : comp B' f = compl₂ B g
x✝ : M
y✝ : M₁
⊢ ↑(↑B' (↑f x✝)) y✝ = ↑(↑B x✝) (↑g y✝)
[PROOFSTEP]
rw [← compl₂_apply, ← comp_apply, h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
x✝¹ : M
x✝ : M₁
⊢ ↑(↑B' (↑0 x✝¹)) x✝ = ↑(↑B x✝¹) (↑0 x✝)
[PROOFSTEP]
simp only [zero_apply, map_zero]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
h' : IsAdjointPair B B' f' g'
x : M
x✝ : M₁
⊢ ↑(↑B' (↑(f + f') x)) x✝ = ↑(↑B x) (↑(g + g') x✝)
[PROOFSTEP]
rw [f.add_apply, g.add_apply, B'.map_add₂, (B x).map_add, h, h']
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f'✝ : M →ₗ[R] M₁
g g'✝ : M₁ →ₗ[R] M
f' : M₁ →ₗ[R] M₂
g' : M₂ →ₗ[R] M₁
h : IsAdjointPair B B' f g
h' : IsAdjointPair B' B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ ↑(↑B'' (↑(LinearMap.comp f' f) x✝¹)) x✝ = ↑(↑B x✝¹) (↑(LinearMap.comp g g') x✝)
[PROOFSTEP]
rw [LinearMap.comp_apply, LinearMap.comp_apply, h', h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
B' : M₁ →ₗ[R] M₁ →ₗ[R] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
h' : IsAdjointPair B B' f' g'
x : M
x✝ : M₁
⊢ ↑(↑B' (↑(f - f') x)) x✝ = ↑(↑B x) (↑(g - g') x✝)
[PROOFSTEP]
rw [f.sub_apply, g.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
B' : M₁ →ₗ[R] M₁ →ₗ[R] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
c : R
h : IsAdjointPair B B' f g
x✝¹ : M
x✝ : M₁
⊢ ↑(↑B' (↑(c • f) x✝¹)) x✝ = ↑(↑B x✝¹) (↑(c • g) x✝)
[PROOFSTEP]
simp [h _]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
⊢ IsPairSelfAdjoint B F f ↔
    IsPairSelfAdjoint (compl₁₂ B ↑e ↑e) (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f)
[PROOFSTEP]
have hₗ :
  (F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).comp (e.symm.conj f) =
    (F.comp f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) :=
  by
  ext
  simp only [LinearEquiv.symm_conj_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply, LinearEquiv.apply_symm_apply,
    Function.comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
⊢ comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (comp F f) ↑e ↑e
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
x✝¹ x✝ : M₁
⊢ ↑(↑(comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f)) x✝¹) x✝ =
    ↑(↑(compl₁₂ (comp F f) ↑e ↑e) x✝¹) x✝
[PROOFSTEP]
simp only [LinearEquiv.symm_conj_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply, LinearEquiv.apply_symm_apply,
  Function.comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
hₗ : comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (comp F f) ↑e ↑e
⊢ IsPairSelfAdjoint B F f ↔
    IsPairSelfAdjoint (compl₁₂ B ↑e ↑e) (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f)
[PROOFSTEP]
have hᵣ :
  (B.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).compl₂ (e.symm.conj f) =
    (B.compl₂ f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) :=
  by
  ext
  simp only [LinearEquiv.symm_conj_apply, compl₂_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply,
    LinearEquiv.apply_symm_apply, Function.comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
hₗ : comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (comp F f) ↑e ↑e
⊢ compl₂ (compl₁₂ B ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (compl₂ B f) ↑e ↑e
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
hₗ : comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (comp F f) ↑e ↑e
x✝¹ x✝ : M₁
⊢ ↑(↑(compl₂ (compl₁₂ B ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f)) x✝¹) x✝ =
    ↑(↑(compl₁₂ (compl₂ B f) ↑e ↑e) x✝¹) x✝
[PROOFSTEP]
simp only [LinearEquiv.symm_conj_apply, compl₂_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply,
  LinearEquiv.apply_symm_apply, Function.comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
hₗ : comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (comp F f) ↑e ↑e
hᵣ : compl₂ (compl₁₂ B ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (compl₂ B f) ↑e ↑e
⊢ IsPairSelfAdjoint B F f ↔
    IsPairSelfAdjoint (compl₁₂ B ↑e ↑e) (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f)
[PROOFSTEP]
have he : Function.Surjective (⇑(↑e : M₁ →ₗ[R] M) : M₁ → M) := e.surjective
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
e : M₁ ≃ₗ[R] M
f : Module.End R M
hₗ : comp (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (comp F f) ↑e ↑e
hᵣ : compl₂ (compl₁₂ B ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f) = compl₁₂ (compl₂ B f) ↑e ↑e
he : Function.Surjective ↑↑e
⊢ IsPairSelfAdjoint B F f ↔
    IsPairSelfAdjoint (compl₁₂ B ↑e ↑e) (compl₁₂ F ↑e ↑e) (↑(LinearEquiv.conj (LinearEquiv.symm e)) f)
[PROOFSTEP]
simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
f : Module.End R M
⊢ (∀ (x y : M), ↑(↑B (↑f x)) y = ↑(↑B x) (↑(-f) y)) ↔ ∀ (x y : M), ↑(↑B (↑f x)) y = ↑(↑(-B) x) (↑f y)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
f : Module.End R M
⊢ f ∈ skewAdjointSubmodule B ↔ IsSkewAdjoint B f
[PROOFSTEP]
rw [isSkewAdjoint_iff_neg_self_adjoint]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
f : Module.End R M
⊢ f ∈ skewAdjointSubmodule B ↔ IsAdjointPair (-B) B f f
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft B
⊢ SeparatingLeft (↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B)
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft B
x : Mₗ₁'
hx : ∀ (y : Mₗ₂'), ↑(↑(↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B) x) y = 0
⊢ x = 0
[PROOFSTEP]
rw [← e₁.symm.map_eq_zero_iff]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft B
x : Mₗ₁'
hx : ∀ (y : Mₗ₂'), ↑(↑(↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B) x) y = 0
⊢ ↑(LinearEquiv.symm e₁) x = 0
[PROOFSTEP]
refine' h (e₁.symm x) fun y ↦ _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft B
x : Mₗ₁'
hx : ∀ (y : Mₗ₂'), ↑(↑(↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B) x) y = 0
y : Mₗ₂
⊢ ↑(↑B (↑(LinearEquiv.symm e₁) x)) y = 0
[PROOFSTEP]
specialize hx (e₂ y)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft B
x : Mₗ₁'
y : Mₗ₂
hx : ↑(↑(↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B) x) (↑e₂ y) = 0
⊢ ↑(↑B (↑(LinearEquiv.symm e₁) x)) y = 0
[PROOFSTEP]
simp only [LinearEquiv.arrowCongr_apply, LinearEquiv.symm_apply_apply, LinearEquiv.map_eq_zero_iff] at hx 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft B
x : Mₗ₁'
y : Mₗ₂
hx : ↑(↑B (↑(LinearEquiv.symm e₁) x)) y = 0
⊢ ↑(↑B (↑(LinearEquiv.symm e₁) x)) y = 0
[PROOFSTEP]
exact hx
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft (↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B)
⊢ SeparatingLeft B
[PROOFSTEP]
convert h.congr e₁.symm e₂.symm
[GOAL]
case h.e'_15
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft (↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B)
⊢ B =
    ↑(LinearEquiv.arrowCongr (LinearEquiv.symm e₁)
          (LinearEquiv.arrowCongr (LinearEquiv.symm e₂) (LinearEquiv.refl R R)))
      (↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B)
[PROOFSTEP]
ext x y
[GOAL]
case h.e'_15.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring R₁
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : SeparatingLeft (↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B)
x : Mₗ₁
y : Mₗ₂
⊢ ↑(↑B x) y =
    ↑(↑(↑(LinearEquiv.arrowCongr (LinearEquiv.symm e₁)
                  (LinearEquiv.arrowCongr (LinearEquiv.symm e₂) (LinearEquiv.refl R R)))
              (↑(LinearEquiv.arrowCongr e₁ (LinearEquiv.arrowCongr e₂ (LinearEquiv.refl R R))) B))
          x)
      y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ SeparatingLeft (flip B) ↔ SeparatingRight B
[PROOFSTEP]
rw [← flip_separatingRight, flip_flip]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ SeparatingLeft B ↔ ∀ (x : M₁), ↑B x = 0 → x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ SeparatingLeft B → ∀ (x : M₁), ↑B x = 0 → x = 0
[PROOFSTEP]
intro h x hB
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ (∀ (x : M₁), ↑B x = 0 → x = 0) → SeparatingLeft B
[PROOFSTEP]
intro h x hB
[GOAL]
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : SeparatingLeft B
x : M₁
hB : ↑B x = 0
⊢ x = 0
[PROOFSTEP]
simpa only [hB, zero_apply, eq_self_iff_true, forall_const] using h x
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
⊢ x = 0
[PROOFSTEP]
have h' : B x = 0 := by
  ext
  rw [zero_apply]
  exact hB _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
⊢ ↑B x = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
x✝ : M₂
⊢ ↑(↑B x) x✝ = ↑0 x✝
[PROOFSTEP]
rw [zero_apply]
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
x✝ : M₂
⊢ ↑(↑B x) x✝ = 0
[PROOFSTEP]
exact hB _
[GOAL]
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
h' : ↑B x = 0
⊢ x = 0
[PROOFSTEP]
exact h x h'
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ SeparatingRight B ↔ ∀ (y : M₂), ↑(flip B) y = 0 → y = 0
[PROOFSTEP]
rw [← flip_separatingLeft, separatingLeft_iff_linear_nontrivial]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ SeparatingRight B ↔ ker (flip B) = ⊥
[PROOFSTEP]
rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ Nondegenerate B
[PROOFSTEP]
refine' ⟨hB', _⟩
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ SeparatingRight B
[PROOFSTEP]
rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ ker B = ⊥
[PROOFSTEP]
rwa [← separatingLeft_iff_ker_eq_bot]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ Nondegenerate B
[PROOFSTEP]
refine' ⟨_, hB'⟩
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ SeparatingLeft B
[PROOFSTEP]
rw [separatingLeft_iff_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mpr]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ ker (flip B) = ⊥
[PROOFSTEP]
rwa [← separatingRight_iff_flip_ker_eq_bot]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
⊢ Nondegenerate (domRestrict₁₂ B W W)
[PROOFSTEP]
refine' (hB.domRestrict W).nondegenerate_of_separatingLeft _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
⊢ SeparatingLeft (domRestrict₁₂ B W W)
[PROOFSTEP]
rintro ⟨x, hx⟩ b₁
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
⊢ { val := x, property := hx } = 0
[PROOFSTEP]
rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R]
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
⊢ x ∈ ⊥
[PROOFSTEP]
refine' hW.le_bot ⟨hx, fun y hy ↦ _⟩
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
y : M
hy : y ∈ W
⊢ IsOrtho B y x
[PROOFSTEP]
specialize b₁ ⟨y, hy⟩
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) { val := y, property := hy } = 0
⊢ IsOrtho B y x
[PROOFSTEP]
simp_rw [domRestrict₁₂_apply] at b₁ 
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑B x) y = 0
⊢ IsOrtho B y x
[PROOFSTEP]
rw [hB.ortho_comm]
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑B x) y = 0
⊢ IsOrtho B x y
[PROOFSTEP]
exact b₁
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
[PROOFSTEP]
intro ho
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
⊢ False
[PROOFSTEP]
refine' v.ne_zero i (hB (v i) fun m ↦ _)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
m : M
⊢ ↑(↑B (↑v i)) m = 0
[PROOFSTEP]
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ↑(↑B (↑v i)) (↑(LinearEquiv.symm v.repr) vi) = 0
[PROOFSTEP]
rw [Basis.repr_symm_apply, Finsupp.total_apply, Finsupp.sum, map_sum]
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∑ i_1 in vi.support, ↑(↑B (↑v i)) (↑vi i_1 • ↑v i_1) = 0
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∀ (x : n), x ∈ vi.support → ↑(↑B (↑v i)) (↑vi x • ↑v x) = 0
[PROOFSTEP]
rintro j -
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑(↑B (↑v i)) (↑vi j • ↑v j) = 0
[PROOFSTEP]
rw [map_smulₛₗ]
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑I' (↑vi j) • ↑(↑B (↑v i)) (↑v j) = 0
[PROOFSTEP]
suffices : B (v i) (v j) = 0
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
this : ↑(↑B (↑v i)) (↑v j) = 0
⊢ ↑I' (↑vi j) • ↑(↑B (↑v i)) (↑v j) = 0
[PROOFSTEP]
rw [this, smul_eq_mul, mul_zero]
[GOAL]
case this
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑(↑B (↑v i)) (↑v j) = 0
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case this.inl
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ↑(↑B (↑v i)) (↑v i) = 0
[PROOFSTEP]
exact ho
[GOAL]
case this.inr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ ↑(↑B (↑v i)) (↑v j) = 0
[PROOFSTEP]
exact h hij
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
[PROOFSTEP]
rw [isOrthoᵢ_flip] at h 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ (flip B) ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
[PROOFSTEP]
rw [isOrtho_flip]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ (flip B) ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho (flip B) (↑v i) (↑v i)
[PROOFSTEP]
exact h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingLeft B
[PROOFSTEP]
intro m hB
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
m : M
hB : ∀ (y : M), ↑(↑B m) y = 0
⊢ m = 0
[PROOFSTEP]
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
⊢ ↑(LinearEquiv.symm v.repr) vi = 0
[PROOFSTEP]
rw [LinearEquiv.map_eq_zero_iff]
[GOAL]
case intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
⊢ vi = 0
[PROOFSTEP]
ext i
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
i : n
⊢ ↑vi i = ↑0 i
[PROOFSTEP]
rw [Finsupp.zero_apply]
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
i : n
⊢ ↑vi i = 0
[PROOFSTEP]
specialize hB (v i)
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) (↑v i) = 0
⊢ ↑vi i = 0
[PROOFSTEP]
simp_rw [Basis.repr_symm_apply, Finsupp.total_apply, Finsupp.sum, map_sum₂, map_smulₛₗ₂, smul_eq_mul] at hB 
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ↑vi i = 0
[PROOFSTEP]
rw [Finset.sum_eq_single i] at hB 
[GOAL]
case intro.h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
⊢ ↑vi i = 0
[PROOFSTEP]
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (h i) hB
[GOAL]
case intro.h.h₀
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ∀ (b : n), b ∈ vi.support → b ≠ i → ↑(RingHom.id R) (↑vi b) * ↑(↑B (↑v b)) (↑v i) = 0
[PROOFSTEP]
intro j _hj hij
[GOAL]
case intro.h.h₀
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
j : n
_hj : j ∈ vi.support
hij : j ≠ i
⊢ ↑(RingHom.id R) (↑vi j) * ↑(↑B (↑v j)) (↑v i) = 0
[PROOFSTEP]
replace hij : B (v j) (v i) = 0 := hO hij
[GOAL]
case intro.h.h₀
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
j : n
_hj : j ∈ vi.support
hij : ↑(↑B (↑v j)) (↑v i) = 0
⊢ ↑(RingHom.id R) (↑vi j) * ↑(↑B (↑v j)) (↑v i) = 0
[PROOFSTEP]
rw [hij, RingHom.id_apply, mul_zero]
[GOAL]
case intro.h.h₁
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ¬i ∈ vi.support → ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
[PROOFSTEP]
intro hi
[GOAL]
case intro.h.h₁
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
hi : ¬i ∈ vi.support
⊢ ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
[PROOFSTEP]
replace hi : vi i = 0 := Finsupp.not_mem_support_iff.mp hi
[GOAL]
case intro.h.h₁
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
hi : ↑vi i = 0
⊢ ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
[PROOFSTEP]
rw [hi, RingHom.id_apply, zero_mul]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingRight B
[PROOFSTEP]
rw [isOrthoᵢ_flip] at hO 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingRight B
[PROOFSTEP]
rw [← flip_separatingLeft]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingLeft (flip B)
[PROOFSTEP]
refine' IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ _
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
i : n
⊢ ¬IsOrtho (flip B) (↑v i) (↑v i)
[PROOFSTEP]
rw [isOrtho_flip]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
Mₗ₁ : Type u_8
Mₗ₁' : Type u_9
Mₗ₂ : Type u_10
Mₗ₂' : Type u_11
K : Type u_12
K₁ : Type u_13
K₂ : Type u_14
V : Type u_15
V₁ : Type u_16
V₂ : Type u_17
n : Type u_18
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
i : n
⊢ ¬IsOrtho (flip (flip B)) (↑v i) (↑v i)
[PROOFSTEP]
exact h i
