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}}_{\mathscr{H}}\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}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
2	1 1	coeq12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
3	2 1	eqeq12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\right)$$
4		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	elimel	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	pjidmcoi	$$⊢{\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
7	3 6	dedth	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$