theorem A {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E) : K.orthogonalProjection ↑(K.orthogonalProjection v) = K.orthogonalProjection v

Projecting on U and then on U again is the same as projecting on U once.

theorem B {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (u v : E) : inner 𝕜 (↑(K.orthogonalProjection u)) v = inner 𝕜 u ↑(K.orthogonalProjection v)