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	⊢ 0ℋ ∈ Cℋ
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→ 𝐻 )