# Metamath Proof Explorer

## Theorem pjch

Description: Projection of a vector in the projection subspace. Lemma 4.4(ii) of Beran p. 111. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion pjch ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to \left({A}\in {H}↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\right)$

### Proof

Step Hyp Ref Expression
1 eleq2 ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\to \left({A}\in {H}↔{A}\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)$
2 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)$
3 2 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)$
4 3 eqeq1d ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left({A}\right)={A}\right)$
5 1 4 bibi12d ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\to \left(\left({A}\in {H}↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\right)↔\left({A}\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left({A}\right)={A}\right)\right)$
6 eleq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)$
7 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
8 id ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
9 7 8 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left({A}\right)={A}↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
10 6 9 bibi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({A}\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left({A}\right)={A}\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
11 ifchhv ${⊢}if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\in {\mathbf{C}}_{ℋ}$
12 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
13 11 12 pjchi ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},ℋ\right)\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
14 5 10 13 dedth2h ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to \left({A}\in {H}↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\right)$