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 ) )