Theorem pjpyth

Description: Pythagorean theorem for projectors. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjpyth	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {{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		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)$$
2	1	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)$$
3	2	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)$$
4	3	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$$
5		2fveq3	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)$$
6	5	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)$$
7	6	fveq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\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(\perp \left(H\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)\right)}^2$$
9	4 8	oveq12d	$$⊢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(\perp \left(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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)\right)}^2$$
10	9	eqeq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left({{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\leftrightarrow {{norm}_{ℎ}\left(A\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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)\right)}^2\right)$$
11		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
12	11	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)}^2$$
13		2fveq3	$$⊢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)$$
14	13	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$$
15		2fveq3	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
16	15	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
17	14 16	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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
18	12 17	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({{norm}_{ℎ}\left(A\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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(A\right)\right)}^2\leftrightarrow {{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2\right)$$
19		ifchhv	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
20		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
21	19 20	pjpythi	$$⊢{{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\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(\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)}^2$$
22	10 18 21	dedth2h	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {{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$$