Theorem pjhf

Description: The mapping of a projection. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhf	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{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		fof	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶H$$
3	1 2	syl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶H$$
4		chss	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to H\subseteq \mathscr{H}$$
5	3 4	fssd	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$