Theorem pjrn

Description: The range of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjrn	⊢ ( 𝐻 ∈ Cℋ → ran ( projℎ ‘ 𝐻 ) = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		pjhfo	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 )
2		forn	⊢ ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 → ran ( projℎ ‘ 𝐻 ) = 𝐻 )
3	1 2	syl	⊢ ( 𝐻 ∈ Cℋ → ran ( projℎ ‘ 𝐻 ) = 𝐻 )