𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ orthogonalProjection U = ↑adjoint (Submodule.subtypeL U)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ↑adjoint (Submodule.subtypeL U) = orthogonalProjection U
symm
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ∀ (x : E) (y : (fun x => { x // x ∈ U }) x),
    inner (↑(orthogonalProjection U) x) y = inner x (↑(Submodule.subtypeL U) y)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ orthogonalProjection U = ↑adjoint (Submodule.subtypeL U)
rw [eq_adjoint_iff]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
x : E
u : { x // x ∈ U }
⊢ inner (↑(orthogonalProjection U) x) u = inner x (↑(Submodule.subtypeL U) u)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ∀ (x : E) (y : (fun x => { x // x ∈ U }) x),
    inner (↑(orthogonalProjection U) x) y = inner x (↑(Submodule.subtypeL U) y)
intro x u
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
x : E
u : { x // x ∈ U }
⊢ inner x ↑u = inner x (↑(Submodule.subtypeL U) u)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
x : E
u : { x // x ∈ U }
⊢ inner (↑(orthogonalProjection U) x) u = inner x (↑(Submodule.subtypeL U) u)
rw [U.coe_inner, inner_orthogonalProjection_left_eq_right,
  orthogonalProjection_mem_subspace_eq_self]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.852407
G : Type ?u.852410
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
x : E
u : { x // x ∈ U }
⊢ inner x ↑u = inner x (↑(Submodule.subtypeL U) u)
rfl