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 ( 𝐻C → ( proj𝐻 ) : ℋ –onto𝐻 )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝐻 = if ( 𝐻C , 𝐻 , 0 ) → ( proj𝐻 ) = ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) )
2 foeq1 ( ( proj𝐻 ) = ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) → ( ( proj𝐻 ) : ℋ –onto𝐻 ↔ ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) : ℋ –onto𝐻 ) )
3 1 2 syl ( 𝐻 = if ( 𝐻C , 𝐻 , 0 ) → ( ( proj𝐻 ) : ℋ –onto𝐻 ↔ ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) : ℋ –onto𝐻 ) )
4 foeq3 ( 𝐻 = if ( 𝐻C , 𝐻 , 0 ) → ( ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) : ℋ –onto𝐻 ↔ ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) : ℋ –onto→ if ( 𝐻C , 𝐻 , 0 ) ) )
5 h0elch 0C
6 5 elimel if ( 𝐻C , 𝐻 , 0 ) ∈ C
7 6 pjfoi ( proj ‘ if ( 𝐻C , 𝐻 , 0 ) ) : ℋ –onto→ if ( 𝐻C , 𝐻 , 0 )
8 3 4 7 dedth2v ( 𝐻C → ( proj𝐻 ) : ℋ –onto𝐻 )