Theorem pjfi

Description: The mapping of a projection. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjfn.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{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	1	chssii	$$⊢H\subseteq \mathscr{H}$$
5	3 4	eqsstri	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\subseteq \mathscr{H}$$
6		df-f	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}\wedge \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\subseteq \mathscr{H}\right)$$
7	2 5 6	mpbir2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$