Theorem pjopyth

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

	Ref	Expression
Assertion	pjopyth	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge G\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(H\subseteq \perp \left(G\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left(H\subseteq \perp \left(G\right)\leftrightarrow if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\right)$$
2		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)$$
3	2	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)$$
4	3	oveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)$$
5	4	fveq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
6	5	oveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2$$
7	3	fveq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)$$
8	7	oveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2$$
9	8	oveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {{norm}_{ℎ}\left({\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(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2$$
10	6 9	eqeq12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)$$
11	1 10	imbi12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left(\left(H\subseteq \perp \left(G\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)\leftrightarrow \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)\right)$$
12		fveq2	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \perp \left(G\right)=\perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)$$
13	12	sseq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\leftrightarrow if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\right)$$
14		fveq2	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)$$
15	14	fveq1d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)$$
16	15	oveq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)$$
17	16	fveq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)$$
18	17	oveq1d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2$$
19	15	fveq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)$$
20	19	oveq1d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2$$
21	20	oveq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2$$
22	18 21	eqeq12d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2\right)$$
23	13 22	imbi12d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \left(\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)\leftrightarrow \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2\right)\right)$$
24		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
25		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
26	24 25	oveq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
27	26	fveq2d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
28	27	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
29	24	fveq2d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
30	29	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
31	25	fveq2d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
32	31	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
33	30 32	oveq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
34	28 33	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2\right)$$
35	34	imbi2d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)}^2\right)\leftrightarrow \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2\right)\right)$$
36		ifchhv	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
37		ifchhv	$$⊢if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
38		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
39	36 37 38	pjopythi	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
40	11 23 35 39	dedth3h	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge G\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(H\subseteq \perp \left(G\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)$$