Step |
Hyp |
Ref |
Expression |
1 |
|
4at.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
4at.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
4at.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
simp11 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝐾 ∈ HL ) |
5 |
|
simp12 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑃 ∈ 𝐴 ) |
6 |
|
simp13 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑇 ∈ 𝐴 ) |
7 |
4
|
hllatd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝐾 ∈ Lat ) |
8 |
|
simp21 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑈 ∈ 𝐴 ) |
9 |
|
simp22 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑉 ∈ 𝐴 ) |
10 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
11 |
10 2 3
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) |
12 |
4 8 9 11
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) |
13 |
|
simp23 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑊 ∈ 𝐴 ) |
14 |
10 3
|
atbase |
⊢ ( 𝑊 ∈ 𝐴 → 𝑊 ∈ ( Base ‘ 𝐾 ) ) |
15 |
13 14
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) ) |
16 |
10 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) |
17 |
7 12 15 16
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) |
18 |
|
simp3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) |
19 |
10 1 2 3
|
hlexchb2 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ↔ ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) ) |
20 |
4 5 6 17 18 19
|
syl131anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ↔ ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) ) |
21 |
1 2 3
|
4atlem4a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) |
22 |
4 6 8 9 13 21
|
syl32anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) |
23 |
22
|
breq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ 𝑃 ≤ ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) ) |
24 |
1 2 3
|
4atlem4a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) |
25 |
4 5 8 9 13 24
|
syl32anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) |
26 |
25 22
|
eqeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) ) |
27 |
20 23 26
|
3bitr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) |