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 )