# Metamath Proof Explorer

## Theorem pjid

Description: The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {H}\right)\to {H}\in {\mathbf{C}}_{ℋ}$
2 chel ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {H}\right)\to {A}\in ℋ$
3 1 2 jca ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {H}\right)\to \left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)$
4 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)$
5 4 biimpa ${⊢}\left(\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\wedge {A}\in {H}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}$
6 3 5 sylancom ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {H}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}$