Step |
Hyp |
Ref |
Expression |
1 |
|
dalawlem.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
dalawlem.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
dalawlem.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
dalawlem.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
6 |
|
simp11 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝐾 ∈ HL ) |
7 |
6
|
hllatd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝐾 ∈ Lat ) |
8 |
|
simp21 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 ) |
9 |
|
simp22 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 ) |
10 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) |
11 |
6 8 9 10
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) |
12 |
|
simp31 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 ) |
13 |
|
simp32 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ∈ 𝐴 ) |
14 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
15 |
6 12 13 14
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
16 |
5 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
17 |
7 11 15 16
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
18 |
5 4
|
atbase |
⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) ) |
19 |
12 18
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) ) |
20 |
5 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
21 |
7 11 19 20
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
22 |
5 4
|
atbase |
⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) ) |
23 |
13 22
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) ) |
24 |
5 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
25 |
7 21 23 24
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
26 |
5 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
27 |
7 25 19 26
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
28 |
5 4
|
atbase |
⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) ) |
29 |
9 28
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) ) |
30 |
|
simp33 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑈 ∈ 𝐴 ) |
31 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) |
32 |
6 13 30 31
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) |
33 |
5 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ) |
34 |
7 29 32 33
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ) |
35 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
36 |
6 30 12 35
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
37 |
5 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
38 |
7 34 36 37
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
39 |
5 1 2
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) |
40 |
7 11 19 39
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) |
41 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
42 |
6 13 12 41
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑇 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
43 |
5 1 3
|
latmlem1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ) ) |
44 |
7 11 21 42 43
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ) ) |
45 |
40 44
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ) |
46 |
2 4
|
hlatjcom |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑆 ) ) |
47 |
6 12 13 46
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑆 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑆 ) ) |
48 |
47
|
oveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ) |
49 |
5 1 2
|
latlej2 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) |
50 |
7 11 19 49
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) |
51 |
5 1 2 3 4
|
atmod2i2 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑇 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ) |
52 |
6 13 21 19 50 51
|
syl131anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑇 ∨ 𝑆 ) ) ) |
53 |
45 48 52
|
3brtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ) |
54 |
|
hlol |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL ) |
55 |
6 54
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝐾 ∈ OL ) |
56 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
57 |
6 8 12 56
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
58 |
5 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
59 |
7 29 57 58
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
60 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
61 |
6 9 13 60
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) |
62 |
5 3
|
latmassOLD |
⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∧ 𝑇 ) = ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( ( 𝑄 ∨ 𝑇 ) ∧ 𝑇 ) ) ) |
63 |
55 59 61 23 62
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∧ 𝑇 ) = ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( ( 𝑄 ∨ 𝑇 ) ∧ 𝑇 ) ) ) |
64 |
2 4
|
hlatjass |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑆 ) ) ) |
65 |
6 8 9 12 64
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑆 ) ) ) |
66 |
2 4
|
hlatj12 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑆 ) ) = ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ) |
67 |
6 8 9 12 66
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑆 ) ) = ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ) |
68 |
65 67
|
eqtr2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) |
69 |
1 2 4
|
hlatlej2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → 𝑇 ≤ ( 𝑄 ∨ 𝑇 ) ) |
70 |
6 9 13 69
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ≤ ( 𝑄 ∨ 𝑇 ) ) |
71 |
5 1 3
|
latleeqm2 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑇 ≤ ( 𝑄 ∨ 𝑇 ) ↔ ( ( 𝑄 ∨ 𝑇 ) ∧ 𝑇 ) = 𝑇 ) ) |
72 |
7 23 61 71
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑇 ≤ ( 𝑄 ∨ 𝑇 ) ↔ ( ( 𝑄 ∨ 𝑇 ) ∧ 𝑇 ) = 𝑇 ) ) |
73 |
70 72
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ 𝑇 ) = 𝑇 ) |
74 |
68 73
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( ( 𝑄 ∨ 𝑇 ) ∧ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) |
75 |
63 74
|
eqtr2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) = ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∧ 𝑇 ) ) |
76 |
1 2 4
|
hlatlej1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑄 ∨ 𝑇 ) ) |
77 |
6 9 13 76
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ≤ ( 𝑄 ∨ 𝑇 ) ) |
78 |
5 1 2 3 4
|
atmod1i1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑄 ≤ ( 𝑄 ∨ 𝑇 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) = ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) |
79 |
6 9 57 61 77 78
|
syl131anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) = ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) |
80 |
1 2 4
|
hlatlej2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑈 ∨ 𝑄 ) ) |
81 |
6 30 9 80
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ≤ ( 𝑈 ∨ 𝑄 ) ) |
82 |
|
simp13 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) |
83 |
|
simp12 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 = 𝑅 ) |
84 |
83
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑈 ) = ( 𝑅 ∨ 𝑈 ) ) |
85 |
2 4
|
hlatjcom |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑈 ) = ( 𝑈 ∨ 𝑄 ) ) |
86 |
6 9 30 85
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑈 ) = ( 𝑈 ∨ 𝑄 ) ) |
87 |
84 86
|
eqtr3d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑈 ) = ( 𝑈 ∨ 𝑄 ) ) |
88 |
82 87
|
breqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) |
89 |
5 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
90 |
7 57 61 89
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
91 |
5 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) |
92 |
6 30 9 91
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑈 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) |
93 |
5 1 2
|
latjle12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ≤ ( 𝑈 ∨ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) ↔ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) ) |
94 |
7 29 90 92 93
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ≤ ( 𝑈 ∨ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) ↔ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) ) |
95 |
81 88 94
|
mpbi2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) |
96 |
79 95
|
eqbrtrrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑄 ) ) |
97 |
1 2 4
|
hlatlej1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → 𝑇 ≤ ( 𝑇 ∨ 𝑈 ) ) |
98 |
6 13 30 97
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ≤ ( 𝑇 ∨ 𝑈 ) ) |
99 |
5 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
100 |
7 59 61 99
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ) |
101 |
5 1 3
|
latmlem12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑇 ∨ 𝑈 ) ) → ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∧ 𝑇 ) ≤ ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) ) |
102 |
7 100 92 23 32 101
|
syl122anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑈 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑇 ∨ 𝑈 ) ) → ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∧ 𝑇 ) ≤ ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) ) |
103 |
96 98 102
|
mp2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∧ 𝑇 ) ≤ ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) |
104 |
75 103
|
eqbrtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) |
105 |
1 2 4
|
hlatlej2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ≤ ( 𝑇 ∨ 𝑈 ) ) |
106 |
6 13 30 105
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑈 ≤ ( 𝑇 ∨ 𝑈 ) ) |
107 |
5 1 2 3 4
|
atmod1i1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑈 ≤ ( 𝑇 ∨ 𝑈 ) ) → ( 𝑈 ∨ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ) = ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) |
108 |
6 30 29 32 106 107
|
syl131anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑈 ∨ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ) = ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) |
109 |
5 4
|
atbase |
⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) ) |
110 |
30 109
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) ) |
111 |
5 2
|
latjcom |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑈 ∨ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ) = ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ) |
112 |
7 110 34 111
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑈 ∨ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ) = ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ) |
113 |
108 112
|
eqtr3d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑈 ∨ 𝑄 ) ∧ ( 𝑇 ∨ 𝑈 ) ) = ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ) |
114 |
104 113
|
breqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ) |
115 |
5 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) |
116 |
7 34 110 115
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) |
117 |
5 1 2
|
latjlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ≤ ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∨ 𝑆 ) ) ) |
118 |
7 25 116 19 117
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ≤ ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∨ 𝑆 ) ) ) |
119 |
114 118
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ≤ ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∨ 𝑆 ) ) |
120 |
5 2
|
latjass |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∨ 𝑆 ) = ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ) |
121 |
7 34 110 19 120
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ 𝑈 ) ∨ 𝑆 ) = ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ) |
122 |
119 121
|
breqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∨ 𝑆 ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ) |
123 |
5 1 7 17 27 38 53 122
|
lattrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ) |
124 |
5 1 3
|
latmle1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) |
125 |
7 11 15 124
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) |
126 |
5 1 3
|
latlem12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) |
127 |
7 17 38 11 126
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) |
128 |
123 125 127
|
mpbi2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) |
129 |
5 4
|
atbase |
⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
130 |
8 129
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
131 |
5 1 2 3
|
latmlej12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) |
132 |
7 29 32 130 131
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) |
133 |
5 1 2 3 4
|
llnmod1i2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑈 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) = ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) |
134 |
6 34 11 30 12 132 133
|
syl321anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑈 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) = ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) |
135 |
2 4
|
hlatjidm |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 ) |
136 |
6 9 135
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 ) |
137 |
83
|
oveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑅 ) ) |
138 |
136 137
|
eqtr3d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 = ( 𝑄 ∨ 𝑅 ) ) |
139 |
138
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) = ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ) |
140 |
5 3
|
latmcom |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑈 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) |
141 |
7 36 11 140
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑈 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) |
142 |
2 4
|
hlatjcom |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) ) |
143 |
6 8 9 142
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) ) |
144 |
83
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑃 ) ) |
145 |
143 144
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑃 ) ) |
146 |
145
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑈 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) |
147 |
141 146
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑈 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) |
148 |
139 147
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑈 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) = ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) |
149 |
134 148
|
eqtr3d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) |
150 |
128 149
|
breqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) |