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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
latjass.j ⊢ ∨ = ( join ‘ 𝐾 )
Assertion latjass ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) = ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latjass.j ⊢ ∨ = ( join ‘ 𝐾 )
3 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 simpl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
5 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
6 5 3adant3r3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
7 simpr3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
8 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∈ 𝐵 )
9 4 6 7 8 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∈ 𝐵 )
10 simpr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 )
12 11 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 )
13 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 )
14 4 10 12 13 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 )
15 1 3 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
16 4 10 12 15 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
17 simpr2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
18 1 3 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑌 ∨ 𝑍 ) )
19 18 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑌 ∨ 𝑍 ) )
20 1 3 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) → ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
21 4 10 12 20 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
22 1 3 4 17 12 14 19 21 lattrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
23 1 3 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∧ 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) ↔ ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) )
24 4 10 17 14 23 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∧ 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) ↔ ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) )
25 16 22 24 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
26 1 3 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ( le ‘ 𝐾 ) ( 𝑌 ∨ 𝑍 ) )
27 26 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ( le ‘ 𝐾 ) ( 𝑌 ∨ 𝑍 ) )
28 1 3 4 7 12 14 27 21 lattrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
29 1 3 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 ) ) → ( ( ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∧ 𝑍 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) ↔ ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) )
30 4 6 7 14 29 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ∧ 𝑍 ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) ↔ ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ) )
31 25 28 30 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ( le ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
32 1 3 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
33 32 3adant3r3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
34 1 3 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
35 4 6 7 34 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
36 1 3 4 10 6 9 33 35 lattrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
37 1 3 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
38 37 3adant3r3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
39 1 3 4 17 6 9 38 35 lattrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
40 1 3 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
41 4 6 7 40 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
42 1 3 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑌 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∧ 𝑍 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) ↔ ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) )
43 4 17 7 9 42 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∧ 𝑍 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) ↔ ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) )
44 39 41 43 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
45 1 3 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ∧ ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∧ ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) ↔ ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) )
46 4 10 12 9 45 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ∧ ( 𝑌 ∨ 𝑍 ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) ↔ ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) ) )
47 36 44 46 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) ( le ‘ 𝐾 ) ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) )
48 1 3 4 9 14 31 47 latasymd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) = ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )