# Metamath Proof Explorer

## Theorem pjidmco

Description: A projection operator is idempotent. Property (ii) of Beran p. 109. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)$
2 1 1 coeq12d ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)$
3 2 1 eqeq12d ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)\right)$
4 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
5 4 elimel ${⊢}if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
6 5 pjidmcoi ${⊢}{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)$
7 3 6 dedth ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)$