𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ↑b = Subtype.val
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ↑b = Subtype.val
haveI := proper_isROrC 𝕜 (span 𝕜 v)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ (span 𝕜 v)ᗮ = ⊥ ↔ ∃ b, ↑b = Subtype.val
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ↑b = Subtype.val
rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hv]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ↑b = Subtype.val
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ (span 𝕜 v)ᗮ = ⊥ ↔ ∃ b, ↑b = Subtype.val
rw [Submodule.orthogonal_eq_bot_iff]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ↑b = Subtype.val
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ↑b = Subtype.val
have hv_coe : range ((↑) : v → E) = v := by simp
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ → ∃ b, ↑b = Subtype.val

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ↑b = Subtype.val) → span 𝕜 v = ⊤
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ↑b = Subtype.val
constructor
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
⊢ Set.range Subtype.val = v
simp
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
h : span 𝕜 v = ⊤
⊢ ⊤ ≤ span 𝕜 (Set.range Subtype.val)
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ → ∃ b, ↑b = Subtype.val
refine' fun h => ⟨Basis.mk hv.linearIndependent _, Basis.coe_mk _ _⟩
no goals
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
h : span 𝕜 v = ⊤
⊢ ⊤ ≤ span 𝕜 (Set.range Subtype.val)
convert h.ge
case mpr.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
h : Basis (↑v) 𝕜 E
coe_h : ↑h = Subtype.val
⊢ span 𝕜 v = ⊤
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ↑b = Subtype.val) → span 𝕜 v = ⊤
rintro ⟨h, coe_h⟩
no goals
case mpr.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1127153
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
this : ProperSpace { x // x ∈ span 𝕜 v }
hv_coe : Set.range Subtype.val = v
h : Basis (↑v) 𝕜 E
coe_h : ↑h = Subtype.val
⊢ span 𝕜 v = ⊤
rw [← h.span_eq, coe_h, hv_coe]