Metamath Proof Explorer

Theorem cmcmlem

Description: Commutation is symmetric. Theorem 3.4 of Beran p. 45. (Contributed by NM, 3-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 
|- A e. CH
pjoml2.2 
|- B e. CH
Assertion cmcmlem 
|- ( A C_H B -> B C_H A )

Proof

Step Hyp Ref Expression
1 pjoml2.1 
 |-  A e. CH
2 pjoml2.2 
 |-  B e. CH
3 1 choccli 
 |-  ( _|_ ` A ) e. CH
4 2 3 chub2i 
 |-  B C_ ( ( _|_ ` A ) vH B )
5 sseqin2 
 |-  ( B C_ ( ( _|_ ` A ) vH B ) <-> ( ( ( _|_ ` A ) vH B ) i^i B ) = B )
6 4 5 mpbi 
 |-  ( ( ( _|_ ` A ) vH B ) i^i B ) = B
7 6 ineq2i 
 |-  ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( ( _|_ ` A ) vH B ) i^i B ) ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i B )
8 inass 
 |-  ( ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH B ) ) i^i B ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( ( _|_ ` A ) vH B ) i^i B ) )
9 1 2 chdmm1i 
 |-  ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) )
10 9 ineq1i 
 |-  ( ( _|_ ` ( A i^i B ) ) i^i B ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i B )
11 7 8 10 3eqtr4ri 
 |-  ( ( _|_ ` ( A i^i B ) ) i^i B ) = ( ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH B ) ) i^i B )
12 1 2 chdmj4i 
 |-  ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i B )
13 1 2 chdmj2i 
 |-  ( _|_ ` ( ( _|_ ` A ) vH B ) ) = ( A i^i ( _|_ ` B ) )
14 12 13 oveq12i 
 |-  ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) )
15 14 eqeq2i 
 |-  ( A = ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
16 15 biimpri 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> A = ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) )
17 16 fveq2d 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> ( _|_ ` A ) = ( _|_ ` ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) ) )
18 2 choccli 
 |-  ( _|_ ` B ) e. CH
19 3 18 chjcli 
 |-  ( ( _|_ ` A ) vH ( _|_ ` B ) ) e. CH
20 3 2 chjcli 
 |-  ( ( _|_ ` A ) vH B ) e. CH
21 19 20 chdmj4i 
 |-  ( _|_ ` ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH B ) )
22 17 21 eqtr2di 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH B ) ) = ( _|_ ` A ) )
23 22 ineq1d 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> ( ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH B ) ) i^i B ) = ( ( _|_ ` A ) i^i B ) )
24 11 23 eqtrid 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> ( ( _|_ ` ( A i^i B ) ) i^i B ) = ( ( _|_ ` A ) i^i B ) )
25 24 oveq2d 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> ( ( A i^i B ) vH ( ( _|_ ` ( A i^i B ) ) i^i B ) ) = ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) )
26 inss2 
 |-  ( A i^i B ) C_ B
27 1 2 chincli 
 |-  ( A i^i B ) e. CH
28 27 2 pjoml2i 
 |-  ( ( A i^i B ) C_ B -> ( ( A i^i B ) vH ( ( _|_ ` ( A i^i B ) ) i^i B ) ) = B )
29 26 28 ax-mp 
 |-  ( ( A i^i B ) vH ( ( _|_ ` ( A i^i B ) ) i^i B ) ) = B
30 incom 
 |-  ( A i^i B ) = ( B i^i A )
31 incom 
 |-  ( ( _|_ ` A ) i^i B ) = ( B i^i ( _|_ ` A ) )
32 30 31 oveq12i 
 |-  ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) )
33 25 29 32 3eqtr3g 
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) -> B = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) )
34 1 2 cmbri 
 |-  ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
35 2 1 cmbri 
 |-  ( B C_H A <-> B = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) )
36 33 34 35 3imtr4i 
 |-  ( A C_H B -> B C_H A )