Theorem pjhfo

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

	Ref	Expression
Assertion	pjhfo	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
2		foeq1	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right):\mathscr{H}\underset{onto}{⟶}H\right)$$
3	1 2	syl	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right):\mathscr{H}\underset{onto}{⟶}H\right)$$
4		foeq3	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right):\mathscr{H}\underset{onto}{⟶}H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right):\mathscr{H}\underset{onto}{⟶}if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
5		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	elimel	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	pjfoi	$$⊢{\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right):\mathscr{H}\underset{onto}{⟶}if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)$$
8	3 4 7	dedth2v	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$