Metamath Proof Explorer


Theorem pjcmul1i

Description: A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of AkhiezerGlazman p. 65. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 GC
pjclem1.2 HC
Assertion pjcmul1i projGprojH=projHprojGprojGprojHranproj

Proof

Step Hyp Ref Expression
1 pjclem1.1 GC
2 pjclem1.2 HC
3 1 2 pjclem4 projGprojH=projHprojGprojGprojH=projGH
4 pjmfn projFnC
5 1 2 chincli GHC
6 fnfvelrn projFnCGHCprojGHranproj
7 4 5 6 mp2an projGHranproj
8 3 7 eqeltrdi projGprojH=projHprojGprojGprojHranproj
9 pjadj2 projGprojHranprojadjhprojGprojH=projGprojH
10 1 pjbdlni projGBndLinOp
11 2 pjbdlni projHBndLinOp
12 10 11 adjcoi adjhprojGprojH=adjhprojHadjhprojG
13 pjadj3 HCadjhprojH=projH
14 2 13 ax-mp adjhprojH=projH
15 pjadj3 GCadjhprojG=projG
16 1 15 ax-mp adjhprojG=projG
17 14 16 coeq12i adjhprojHadjhprojG=projHprojG
18 12 17 eqtri adjhprojGprojH=projHprojG
19 9 18 eqtr3di projGprojHranprojprojGprojH=projHprojG
20 8 19 impbii projGprojH=projHprojGprojGprojHranproj