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 
|- G e. CH
pjclem1.2 
|- H e. CH
Assertion pjcmul1i 
|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) <-> ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh )

Proof

Step Hyp Ref Expression
1 pjclem1.1 
 |-  G e. CH
2 pjclem1.2 
 |-  H e. CH
3 1 2 pjclem4 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )
4 pjmfn 
 |-  projh Fn CH
5 1 2 chincli 
 |-  ( G i^i H ) e. CH
6 fnfvelrn 
 |-  ( ( projh Fn CH /\ ( G i^i H ) e. CH ) -> ( projh ` ( G i^i H ) ) e. ran projh )
7 4 5 6 mp2an 
 |-  ( projh ` ( G i^i H ) ) e. ran projh
8 3 7 eqeltrdi 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh )
9 pjadj2 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh -> ( adjh ` ( ( projh ` G ) o. ( projh ` H ) ) ) = ( ( projh ` G ) o. ( projh ` H ) ) )
10 1 pjbdlni 
 |-  ( projh ` G ) e. BndLinOp
11 2 pjbdlni 
 |-  ( projh ` H ) e. BndLinOp
12 10 11 adjcoi 
 |-  ( adjh ` ( ( projh ` G ) o. ( projh ` H ) ) ) = ( ( adjh ` ( projh ` H ) ) o. ( adjh ` ( projh ` G ) ) )
13 pjadj3 
 |-  ( H e. CH -> ( adjh ` ( projh ` H ) ) = ( projh ` H ) )
14 2 13 ax-mp 
 |-  ( adjh ` ( projh ` H ) ) = ( projh ` H )
15 pjadj3 
 |-  ( G e. CH -> ( adjh ` ( projh ` G ) ) = ( projh ` G ) )
16 1 15 ax-mp 
 |-  ( adjh ` ( projh ` G ) ) = ( projh ` G )
17 14 16 coeq12i 
 |-  ( ( adjh ` ( projh ` H ) ) o. ( adjh ` ( projh ` G ) ) ) = ( ( projh ` H ) o. ( projh ` G ) )
18 12 17 eqtri 
 |-  ( adjh ` ( ( projh ` G ) o. ( projh ` H ) ) ) = ( ( projh ` H ) o. ( projh ` G ) )
19 9 18 eqtr3di 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh -> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )
20 8 19 impbii 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) <-> ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh )