R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 = ⊥
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 = ⊥
rw [← Finset.coe_singleton]
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 = ⊥
refine' eq_bot_iff.2 fun y h ↦ _
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
rcases mem_span_finset.1 h.1 with ⟨μ, rfl⟩
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
replace h := h.2 x (by simp [Submodule.mem_span] : x ∈ Submodule.span K₁ ({x} : Finset V₁))
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
rw [Finset.sum_singleton] at h ⊢
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥

case hμzero
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
suffices hμzero : μ x = 0
case hμzero
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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
case hμzero
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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
rw [isOrtho_def, map_smulₛₗ, smul_eq_mul] at h
no goals
case hμzero
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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
exact Or.elim (zero_eq_mul.mp h.symm)
    (fun y ↦ by simpa using y)
    (fun hfalse ↦ False.elim $ hx hfalse)
no goals
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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}
simp [Submodule.mem_span]
no goals
case intro
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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 ∈ ⊥
rw [hμzero, zero_smul, Submodule.mem_bot]
no goals
R : Type ?u.235358
R₁ : Type ?u.235361
R₂ : Type ?u.235364
R₃ : Type ?u.235367
M : Type ?u.235370
M₁ : Type ?u.235373
M₂ : Type ?u.235376
Mₗ₁ : Type ?u.235379
Mₗ₁' : Type ?u.235382
Mₗ₂ : Type ?u.235385
Mₗ₂' : Type ?u.235388
K : Type u_2
K₁ : Type u_1
K₂ : Type ?u.235397
V : Type ?u.235400
V₁ : Type u_3
V₂ : Type ?u.235406
n : Type ?u.235409
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
simpa using y