Metamath Proof Explorer

Theorem cmbr3i

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 
|- A e. CH
pjoml2.2 
|- B e. CH
Assertion cmbr3i 
|- ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) )

Proof

Step Hyp Ref Expression
1 pjoml2.1 
 |-  A e. CH
2 pjoml2.2 
 |-  B e. CH
3 1 2 cmcmi 
 |-  ( A C_H B <-> B C_H A )
4 2 1 cmbr2i 
 |-  ( B C_H A <-> B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) )
5 3 4 bitri 
 |-  ( A C_H B <-> B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) )
6 ineq2 
 |-  ( B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) -> ( A i^i B ) = ( A i^i ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) )
7 inass 
 |-  ( ( A i^i ( B vH A ) ) i^i ( B vH ( _|_ ` A ) ) ) = ( A i^i ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) )
8 2 1 chjcomi 
 |-  ( B vH A ) = ( A vH B )
9 8 ineq2i 
 |-  ( A i^i ( B vH A ) ) = ( A i^i ( A vH B ) )
10 1 2 chabs2i 
 |-  ( A i^i ( A vH B ) ) = A
11 9 10 eqtri 
 |-  ( A i^i ( B vH A ) ) = A
12 1 choccli 
 |-  ( _|_ ` A ) e. CH
13 2 12 chjcomi 
 |-  ( B vH ( _|_ ` A ) ) = ( ( _|_ ` A ) vH B )
14 11 13 ineq12i 
 |-  ( ( A i^i ( B vH A ) ) i^i ( B vH ( _|_ ` A ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) )
15 7 14 eqtr3i 
 |-  ( A i^i ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) )
16 6 15 eqtr2di 
 |-  ( B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) -> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) )
17 5 16 sylbi 
 |-  ( A C_H B -> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) )
18 inss1 
 |-  ( A i^i ( _|_ ` B ) ) C_ A
19 2 choccli 
 |-  ( _|_ ` B ) e. CH
20 1 19 chincli 
 |-  ( A i^i ( _|_ ` B ) ) e. CH
21 20 1 pjoml2i 
 |-  ( ( A i^i ( _|_ ` B ) ) C_ A -> ( ( A i^i ( _|_ ` B ) ) vH ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) ) = A )
22 18 21 ax-mp 
 |-  ( ( A i^i ( _|_ ` B ) ) vH ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) ) = A
23 20 choccli 
 |-  ( _|_ ` ( A i^i ( _|_ ` B ) ) ) e. CH
24 23 1 chincli 
 |-  ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) e. CH
25 20 24 chjcomi 
 |-  ( ( A i^i ( _|_ ` B ) ) vH ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) ) = ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) )
26 22 25 eqtr3i 
 |-  A = ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) )
27 1 2 chdmm3i 
 |-  ( _|_ ` ( A i^i ( _|_ ` B ) ) ) = ( ( _|_ ` A ) vH B )
28 27 ineq2i 
 |-  ( A i^i ( _|_ ` ( A i^i ( _|_ ` B ) ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) )
29 incom 
 |-  ( A i^i ( _|_ ` ( A i^i ( _|_ ` B ) ) ) ) = ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A )
30 28 29 eqtr3i 
 |-  ( A i^i ( ( _|_ ` A ) vH B ) ) = ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A )
31 30 eqeq1i 
 |-  ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) <-> ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) = ( A i^i B ) )
32 oveq1 
 |-  ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) = ( A i^i B ) -> ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
33 31 32 sylbi 
 |-  ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
34 26 33 syl5eq 
 |-  ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
35 1 2 cmbri 
 |-  ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
36 34 35 sylibr 
 |-  ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> A C_H B )
37 17 36 impbii 
 |-  ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) )