𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
⊢ orthogonalProjectionFn K u = v
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
have hvs : orthogonalProjectionFn K u - v ∈ K :=
  Submodule.sub_mem K (orthogonalProjectionFn_mem u) hvm
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
have huo : ⟪u - orthogonalProjectionFn K u, orthogonalProjectionFn K u - v⟫ = 0 :=
  orthogonalProjectionFn_inner_eq_zero u _ hvs
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
huv : inner (u - v) (orthogonalProjectionFn K u - v) = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
have huv : ⟪u - v, orthogonalProjectionFn K u - v⟫ = 0 := hvo _ hvs
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
huv : inner (u - v) (orthogonalProjectionFn K u - v) = 0
houv : inner (u - v - (u - orthogonalProjectionFn K u)) (orthogonalProjectionFn K u - v) = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
huv : inner (u - v) (orthogonalProjectionFn K u - v) = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
have houv : ⟪u - v - (u - orthogonalProjectionFn K u), orthogonalProjectionFn K u - v⟫ = 0 := by
  rw [inner_sub_left, huo, huv, sub_zero]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
huv : inner (u - v) (orthogonalProjectionFn K u - v) = 0
houv : inner (u - v - (u - orthogonalProjectionFn K u)) (orthogonalProjectionFn K u - v) = 0
⊢ inner (orthogonalProjectionFn K u - v) (orthogonalProjectionFn K u - v) = 0
rwa [sub_sub_sub_cancel_left] at houv
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.457095
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u v : E
hvm : v ∈ K
hvo : ∀ (w : E), w ∈ K → inner (u - v) w = 0
hvs : orthogonalProjectionFn K u - v ∈ K
huo : inner (u - orthogonalProjectionFn K u) (orthogonalProjectionFn K u - v) = 0
huv : inner (u - v) (orthogonalProjectionFn K u - v) = 0
⊢ inner (u - v - (u - orthogonalProjectionFn K u)) (orthogonalProjectionFn K u - v) = 0
rw [inner_sub_left, huo, huv, sub_zero]