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 e. CH -> ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) )
2 1 1 coeq12d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` H ) o. ( projh ` H ) ) = ( ( projh ` if ( H e. CH , H , 0H ) ) o. ( projh ` if ( H e. CH , H , 0H ) ) ) )
3 2 1 eqeq12d 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H ) <-> ( ( projh ` if ( H e. CH , H , 0H ) ) o. ( projh ` if ( H e. CH , H , 0H ) ) ) = ( projh ` if ( H e. CH , H , 0H ) ) ) )
4 h0elch 
 |-  0H e. CH
5 4 elimel 
 |-  if ( H e. CH , H , 0H ) e. CH
6 5 pjidmcoi 
 |-  ( ( projh ` if ( H e. CH , H , 0H ) ) o. ( projh ` if ( H e. CH , H , 0H ) ) ) = ( projh ` if ( H e. CH , H , 0H ) )
7 3 6 dedth 
 |-  ( H e. CH -> ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H ) )