Metamath Proof Explorer

Theorem pjhfo

Description: A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjhfo 
|- ( H e. CH -> ( projh ` H ) : ~H -onto-> 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 foeq1 
 |-  ( ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) -> ( ( projh ` H ) : ~H -onto-> H <-> ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> H ) )
3 1 2 syl 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` H ) : ~H -onto-> H <-> ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> H ) )
4 foeq3 
 |-  ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> H <-> ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> if ( H e. CH , H , 0H ) ) )
5 h0elch 
 |-  0H e. CH
6 5 elimel 
 |-  if ( H e. CH , H , 0H ) e. CH
7 6 pjfoi 
 |-  ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> if ( H e. CH , H , 0H )
8 3 4 7 dedth2v 
 |-  ( H e. CH -> ( projh ` H ) : ~H -onto-> H )