no goals
ι : Type u_3
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.514897
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace { x // x ∈ F i }
hFortho : OrthogonalFamily 𝕜 (fun i => { x // x ∈ F i }) fun i => subtypeₗᵢ (F i)
hFtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), F i)
⊢ ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (subtypeₗᵢ (F i)).toLinearMap)
simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal