Theorem pjopythi

Description: Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoi0.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoi0.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoi0.3	$$⊢A\in \mathscr{H}$$
Assertion	pjopythi	$$⊢G\subseteq \perp \left(H\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		pjoi0.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjoi0.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjoi0.3	$$⊢A\in \mathscr{H}$$
4	1 2 3	pjoi0i	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0$$
5	1 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
6	2 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
7	5 6	normpythi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
8	4 7	syl	$$⊢G\subseteq \perp \left(H\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$