# Metamath Proof Explorer

## 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}}_{ℎ}↔\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)$

### Proof

Step Hyp Ref Expression
1 pjmfn ${⊢}{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{ℋ}$
2 fvelrnb ${⊢}{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{ℋ}\to \left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}↔\exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left({x}\right)={T}\right)$
3 1 2 ax-mp ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}↔\exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left({x}\right)={T}$
4 pjhmop ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {\mathrm{proj}}_{ℎ}\left({x}\right)\in \mathrm{HrmOp}$
5 pjidmco ${⊢}{x}\in {\mathbf{C}}_{ℋ}\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}}_{ℋ}\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}↔{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)↔{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)↔\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\right)$
12 6 11 syl5ibcom ${⊢}{x}\in {\mathbf{C}}_{ℋ}\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}}_{ℋ}\phantom{\rule{.4em}{0ex}}{\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}}_{ℋ}$
17 fnfvelrn ${⊢}\left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{ℋ}\wedge \mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}\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}}_{ℎ}↔\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)$