# Metamath Proof Explorer

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