Theorem dfpjop

Description: Definition of projection operator in Hughes p. 47, except that we do not need linearity to be explicit by virtue of hmoplin . (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	dfpjop	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjmfn	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$
2		fvelrnb	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\to \left(T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \exists x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)=T\right)$$
3	1 2	ax-mp	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \exists x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)=T$$
4		pjhmop	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(x\right)\in \mathrm{HrmOp}$$
5		pjidmco	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(x\right)\circ {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(x\right)$$
6	4 5	jca	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left({\mathrm{proj}}_{ℎ}\left(x\right)\in \mathrm{HrmOp}\wedge {\mathrm{proj}}_{ℎ}\left(x\right)\circ {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(x\right)\right)$$
7		eleq1	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)=T\to \left({\mathrm{proj}}_{ℎ}\left(x\right)\in \mathrm{HrmOp}\leftrightarrow T\in \mathrm{HrmOp}\right)$$
8		id	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)=T\to {\mathrm{proj}}_{ℎ}\left(x\right)=T$$
9	8 8	coeq12d	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)=T\to {\mathrm{proj}}_{ℎ}\left(x\right)\circ {\mathrm{proj}}_{ℎ}\left(x\right)=T\circ T$$
10	9 8	eqeq12d	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)=T\to \left({\mathrm{proj}}_{ℎ}\left(x\right)\circ {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(x\right)\leftrightarrow T\circ T=T\right)$$
11	7 10	anbi12d	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)=T\to \left(\left({\mathrm{proj}}_{ℎ}\left(x\right)\in \mathrm{HrmOp}\wedge {\mathrm{proj}}_{ℎ}\left(x\right)\circ {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(x\right)\right)\leftrightarrow \left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\right)$$
12	6 11	syl5ibcom	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left({\mathrm{proj}}_{ℎ}\left(x\right)=T\to \left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\right)$$
13	12	rexlimiv	$$⊢\exists x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)=T\to \left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)$$
14	3 13	sylbi	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)$$
15		hmopidmpj	$$⊢\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\to T={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)$$
16		hmopidmch	$$⊢\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\to \mathrm{ran}T\in {\mathbf{C}}_{\mathscr{H}}$$
17		fnfvelrn	$$⊢\left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\wedge \mathrm{ran}T\in {\mathbf{C}}_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
18	1 16 17	sylancr	$$⊢\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\to {\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
19	15 18	eqeltrd	$$⊢\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\to T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
20	14 19	impbii	$$⊢T\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)$$