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 TranprojTHrmOpTT=T

Proof

Step Hyp Ref Expression
1 pjmfn projFnC
2 fvelrnb projFnCTranprojxCprojx=T
3 1 2 ax-mp TranprojxCprojx=T
4 pjhmop xCprojxHrmOp
5 pjidmco xCprojxprojx=projx
6 4 5 jca xCprojxHrmOpprojxprojx=projx
7 eleq1 projx=TprojxHrmOpTHrmOp
8 id projx=Tprojx=T
9 8 8 coeq12d projx=Tprojxprojx=TT
10 9 8 eqeq12d projx=Tprojxprojx=projxTT=T
11 7 10 anbi12d projx=TprojxHrmOpprojxprojx=projxTHrmOpTT=T
12 6 11 syl5ibcom xCprojx=TTHrmOpTT=T
13 12 rexlimiv xCprojx=TTHrmOpTT=T
14 3 13 sylbi TranprojTHrmOpTT=T
15 hmopidmpj THrmOpTT=TT=projranT
16 hmopidmch THrmOpTT=TranTC
17 fnfvelrn projFnCranTCprojranTranproj
18 1 16 17 sylancr THrmOpTT=TprojranTranproj
19 15 18 eqeltrd THrmOpTT=TTranproj
20 14 19 impbii TranprojTHrmOpTT=T