Metamath Proof Explorer

Theorem cm2j

Description: A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of Beran p. 49. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cm2j 
|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> A C_H ( B vH C ) )

Proof

Step Hyp Ref Expression
1 cmcm 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> B C_H A ) )
2 cmbr 
 |-  ( ( B e. CH /\ A e. CH ) -> ( B C_H A <-> B = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) ) )
3 2 ancoms 
 |-  ( ( A e. CH /\ B e. CH ) -> ( B C_H A <-> B = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) ) )
4 1 3 bitrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> B = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) ) )
5 4 biimpa 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ A C_H B ) -> B = ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) )
6 incom 
 |-  ( B i^i A ) = ( A i^i B )
7 incom 
 |-  ( B i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i B )
8 6 7 oveq12i 
 |-  ( ( B i^i A ) vH ( B i^i ( _|_ ` A ) ) ) = ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) )
9 5 8 eqtrdi 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ A C_H B ) -> B = ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) )
10 9 3adantl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_H B ) -> B = ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) )
11 10 adantrr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> B = ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) )
12 cmcm 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A C_H C <-> C C_H A ) )
13 cmbr 
 |-  ( ( C e. CH /\ A e. CH ) -> ( C C_H A <-> C = ( ( C i^i A ) vH ( C i^i ( _|_ ` A ) ) ) ) )
14 13 ancoms 
 |-  ( ( A e. CH /\ C e. CH ) -> ( C C_H A <-> C = ( ( C i^i A ) vH ( C i^i ( _|_ ` A ) ) ) ) )
15 12 14 bitrd 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A C_H C <-> C = ( ( C i^i A ) vH ( C i^i ( _|_ ` A ) ) ) ) )
16 15 biimpa 
 |-  ( ( ( A e. CH /\ C e. CH ) /\ A C_H C ) -> C = ( ( C i^i A ) vH ( C i^i ( _|_ ` A ) ) ) )
17 incom 
 |-  ( C i^i A ) = ( A i^i C )
18 incom 
 |-  ( C i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i C )
19 17 18 oveq12i 
 |-  ( ( C i^i A ) vH ( C i^i ( _|_ ` A ) ) ) = ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) )
20 16 19 eqtrdi 
 |-  ( ( ( A e. CH /\ C e. CH ) /\ A C_H C ) -> C = ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) )
21 20 3adantl2 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_H C ) -> C = ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) )
22 21 adantrl 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> C = ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) )
23 11 22 oveq12d 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( B vH C ) = ( ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) vH ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) ) )
24 chincl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
25 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
26 chincl 
 |-  ( ( ( _|_ ` A ) e. CH /\ B e. CH ) -> ( ( _|_ ` A ) i^i B ) e. CH )
27 25 26 sylan 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` A ) i^i B ) e. CH )
28 24 27 jca 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( A i^i B ) e. CH /\ ( ( _|_ ` A ) i^i B ) e. CH ) )
29 chincl 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A i^i C ) e. CH )
30 chincl 
 |-  ( ( ( _|_ ` A ) e. CH /\ C e. CH ) -> ( ( _|_ ` A ) i^i C ) e. CH )
31 25 30 sylan 
 |-  ( ( A e. CH /\ C e. CH ) -> ( ( _|_ ` A ) i^i C ) e. CH )
32 29 31 jca 
 |-  ( ( A e. CH /\ C e. CH ) -> ( ( A i^i C ) e. CH /\ ( ( _|_ ` A ) i^i C ) e. CH ) )
33 chj4 
 |-  ( ( ( ( A i^i B ) e. CH /\ ( ( _|_ ` A ) i^i B ) e. CH ) /\ ( ( A i^i C ) e. CH /\ ( ( _|_ ` A ) i^i C ) e. CH ) ) -> ( ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) vH ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) ) = ( ( ( A i^i B ) vH ( A i^i C ) ) vH ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) ) )
34 28 32 33 syl2an 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) vH ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) ) = ( ( ( A i^i B ) vH ( A i^i C ) ) vH ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) ) )
35 34 3impdi 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) vH ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) ) = ( ( ( A i^i B ) vH ( A i^i C ) ) vH ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) ) )
36 35 adantr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( ( A i^i B ) vH ( ( _|_ ` A ) i^i B ) ) vH ( ( A i^i C ) vH ( ( _|_ ` A ) i^i C ) ) ) = ( ( ( A i^i B ) vH ( A i^i C ) ) vH ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) ) )
37 incom 
 |-  ( A i^i ( B vH C ) ) = ( ( B vH C ) i^i A )
38 fh1 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A i^i C ) ) )
39 37 38 syl5reqr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) = ( ( B vH C ) i^i A ) )
40 incom 
 |-  ( ( _|_ ` A ) i^i ( B vH C ) ) = ( ( B vH C ) i^i ( _|_ ` A ) )
41 25 3anim1i 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( _|_ ` A ) e. CH /\ B e. CH /\ C e. CH ) )
42 41 adantr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( _|_ ` A ) e. CH /\ B e. CH /\ C e. CH ) )
43 cmcm3 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> ( _|_ ` A ) C_H B ) )
44 43 3adant3 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A C_H B <-> ( _|_ ` A ) C_H B ) )
45 cmcm3 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A C_H C <-> ( _|_ ` A ) C_H C ) )
46 45 3adant2 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A C_H C <-> ( _|_ ` A ) C_H C ) )
47 44 46 anbi12d 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_H B /\ A C_H C ) <-> ( ( _|_ ` A ) C_H B /\ ( _|_ ` A ) C_H C ) ) )
48 47 biimpa 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( _|_ ` A ) C_H B /\ ( _|_ ` A ) C_H C ) )
49 fh1 
 |-  ( ( ( ( _|_ ` A ) e. CH /\ B e. CH /\ C e. CH ) /\ ( ( _|_ ` A ) C_H B /\ ( _|_ ` A ) C_H C ) ) -> ( ( _|_ ` A ) i^i ( B vH C ) ) = ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) )
50 42 48 49 syl2anc 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( _|_ ` A ) i^i ( B vH C ) ) = ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) )
51 40 50 syl5reqr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) = ( ( B vH C ) i^i ( _|_ ` A ) ) )
52 39 51 oveq12d 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( ( A i^i B ) vH ( A i^i C ) ) vH ( ( ( _|_ ` A ) i^i B ) vH ( ( _|_ ` A ) i^i C ) ) ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) )
53 23 36 52 3eqtrd 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) )
54 53 ex 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_H B /\ A C_H C ) -> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) ) )
55 chjcl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
56 cmcm 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A C_H ( B vH C ) <-> ( B vH C ) C_H A ) )
57 cmbr 
 |-  ( ( ( B vH C ) e. CH /\ A e. CH ) -> ( ( B vH C ) C_H A <-> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) ) )
58 57 ancoms 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( ( B vH C ) C_H A <-> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) ) )
59 56 58 bitrd 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A C_H ( B vH C ) <-> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) ) )
60 55 59 sylan2 
 |-  ( ( A e. CH /\ ( B e. CH /\ C e. CH ) ) -> ( A C_H ( B vH C ) <-> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) ) )
61 60 3impb 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A C_H ( B vH C ) <-> ( B vH C ) = ( ( ( B vH C ) i^i A ) vH ( ( B vH C ) i^i ( _|_ ` A ) ) ) ) )
62 54 61 sylibrd 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_H B /\ A C_H C ) -> A C_H ( B vH C ) ) )
63 62 imp 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> A C_H ( B vH C ) )