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	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$

Proof

Step	Hyp	Ref	Expression
1		pjhfo	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$
2		forn	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$
3	1 2	syl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$