This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latjass

Description: Lattice join is associative. Lemma 2.2 in MegPav2002 p. 362. ( chjass analog.) (Contributed by NM, 17-Sep-2011)

Ref Expression
Hypotheses latjass.b 
|- B = ( Base ` K )
latjass.j 
|- .\/ = ( join ` K )
Assertion latjass 
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( X .\/ ( Y .\/ Z ) ) )

Proof

Step Hyp Ref Expression
1 latjass.b 
 |-  B = ( Base ` K )
2 latjass.j 
 |-  .\/ = ( join ` K )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 simpl 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
5 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
6 5 3adant3r3 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ Y ) e. B )
7 simpr3 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
8 1 2 latjcl 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( ( X .\/ Y ) .\/ Z ) e. B )
9 4 6 7 8 syl3anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) e. B )
10 simpr1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
11 1 2 latjcl 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y .\/ Z ) e. B )
12 11 3adant3r1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ Z ) e. B )
13 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( X .\/ ( Y .\/ Z ) ) e. B )
14 4 10 12 13 syl3anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) e. B )
15 1 3 2 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> X ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
16 4 10 12 15 syl3anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
17 simpr2 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
18 1 3 2 latlej1 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> Y ( le ` K ) ( Y .\/ Z ) )
19 18 3adant3r1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y ( le ` K ) ( Y .\/ Z ) )
20 1 3 2 latlej2 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( Y .\/ Z ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
21 4 10 12 20 syl3anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ Z ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
22 1 3 4 17 12 14 19 21 lattrd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
23 1 3 2 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ ( X .\/ ( Y .\/ Z ) ) e. B ) ) -> ( ( X ( le ` K ) ( X .\/ ( Y .\/ Z ) ) /\ Y ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) <-> ( X .\/ Y ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) )
24 4 10 17 14 23 syl13anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ( le ` K ) ( X .\/ ( Y .\/ Z ) ) /\ Y ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) <-> ( X .\/ Y ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) )
25 16 22 24 mpbi2and 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ Y ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
26 1 3 2 latlej2 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> Z ( le ` K ) ( Y .\/ Z ) )
27 26 3adant3r1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z ( le ` K ) ( Y .\/ Z ) )
28 1 3 4 7 12 14 27 21 lattrd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
29 1 3 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( X .\/ Y ) e. B /\ Z e. B /\ ( X .\/ ( Y .\/ Z ) ) e. B ) ) -> ( ( ( X .\/ Y ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) /\ Z ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) <-> ( ( X .\/ Y ) .\/ Z ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) )
30 4 6 7 14 29 syl13anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( X .\/ Y ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) /\ Z ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) <-> ( ( X .\/ Y ) .\/ Z ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) ) )
31 25 28 30 mpbi2and 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) ( le ` K ) ( X .\/ ( Y .\/ Z ) ) )
32 1 3 2 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )
33 32 3adant3r3 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X ( le ` K ) ( X .\/ Y ) )
34 1 3 2 latlej1 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( X .\/ Y ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
35 4 6 7 34 syl3anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ Y ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
36 1 3 4 10 6 9 33 35 lattrd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
37 1 3 2 latlej2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y ( le ` K ) ( X .\/ Y ) )
38 37 3adant3r3 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y ( le ` K ) ( X .\/ Y ) )
39 1 3 4 17 6 9 38 35 lattrd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
40 1 3 2 latlej2 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> Z ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
41 4 6 7 40 syl3anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
42 1 3 2 latjle12 
 |-  ( ( K e. Lat /\ ( Y e. B /\ Z e. B /\ ( ( X .\/ Y ) .\/ Z ) e. B ) ) -> ( ( Y ( le ` K ) ( ( X .\/ Y ) .\/ Z ) /\ Z ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) <-> ( Y .\/ Z ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) )
43 4 17 7 9 42 syl13anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y ( le ` K ) ( ( X .\/ Y ) .\/ Z ) /\ Z ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) <-> ( Y .\/ Z ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) )
44 39 41 43 mpbi2and 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ Z ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
45 1 3 2 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ ( Y .\/ Z ) e. B /\ ( ( X .\/ Y ) .\/ Z ) e. B ) ) -> ( ( X ( le ` K ) ( ( X .\/ Y ) .\/ Z ) /\ ( Y .\/ Z ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) <-> ( X .\/ ( Y .\/ Z ) ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) )
46 4 10 12 9 45 syl13anc 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ( le ` K ) ( ( X .\/ Y ) .\/ Z ) /\ ( Y .\/ Z ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) <-> ( X .\/ ( Y .\/ Z ) ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) ) )
47 36 44 46 mpbi2and 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) ( le ` K ) ( ( X .\/ Y ) .\/ Z ) )
48 1 3 4 9 14 31 47 latasymd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( X .\/ ( Y .\/ Z ) ) )