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	⊢ ( 𝐻 ∈ Cℋ → ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) )
2	1 1	coeq12d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ∘ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) )
3	2 1	eqeq12d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ∘ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) )
4		h0elch	⊢ 0ℋ ∈ Cℋ
5	4	elimel	⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ∈ Cℋ
6	5	pjidmcoi	⊢ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ∘ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) )
7	3 6	dedth	⊢ ( 𝐻 ∈ Cℋ → ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )