Theorem pjpythi

Description: Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjnorm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjnorm.2	$$⊢A\in \mathscr{H}$$
Assertion	pjpythi	$$⊢{{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		pjnorm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjnorm.2	$$⊢A\in \mathscr{H}$$
3	1 2	pjpji	$$⊢A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
4	3	fveq2i	$$⊢{norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
5	4	oveq1i	$$⊢{{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2$$
6	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
7		shococss	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to H\subseteq \perp \left(\perp \left(H\right)\right)$$
8	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
9	1 8 2	pjopythi	$$⊢H\subseteq \perp \left(\perp \left(H\right)\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2$$
10	6 7 9	mp2b	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2$$
11	5 10	eqtri	$$⊢{{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2$$