Theorem pjfoi

Description: A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjfn.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjfoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$

Proof

Step	Hyp	Ref	Expression
1		pjfn.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	pjfni	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}$$
3	1	pjrni	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$
4		df-fo	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}\wedge \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H\right)$$
5	2 3 4	mpbir2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$