| Step | Hyp | Ref
| Expression |
| 1 | | hllat 39364 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
| 2 | 1 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝐾 ∈ Lat) |
| 3 | | simp21 1207 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝑋 ⊆ 𝐴) |
| 4 | | simp1 1137 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝐾 ∈ HL) |
| 5 | | simp22 1208 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝑌 ⊆ 𝐴) |
| 6 | | simp23 1209 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝑍 ⊆ 𝐴) |
| 7 | | paddasslem.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 8 | | paddasslem.p |
. . . . . 6
⊢ + =
(+𝑃‘𝐾) |
| 9 | 7, 8 | paddssat 39816 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 + 𝑍) ⊆ 𝐴) |
| 10 | 4, 5, 6, 9 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑌 + 𝑍) ⊆ 𝐴) |
| 11 | | simp3l 1202 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅)) |
| 12 | | paddasslem.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
| 13 | | paddasslem.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
| 14 | 12, 13, 7, 8 | elpaddn0 39802 |
. . . 4
⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ (𝑌 + 𝑍) ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅)) → (𝑝 ∈ (𝑋 + (𝑌 + 𝑍)) ↔ (𝑝 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟)))) |
| 15 | 2, 3, 10, 11, 14 | syl31anc 1375 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑝 ∈ (𝑋 + (𝑌 + 𝑍)) ↔ (𝑝 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟)))) |
| 16 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) → (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) |
| 17 | 12, 13, 7, 8 | paddasslem15 39836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) |
| 18 | 16, 17 | syl3anl3 1416 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) |
| 19 | 18 | 3exp2 1355 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑝 ∈ 𝐴 → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) → (𝑝 ≤ (𝑥 ∨ 𝑟) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))))) |
| 20 | 19 | imp 406 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) ∧ 𝑝 ∈ 𝐴) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) → (𝑝 ≤ (𝑥 ∨ 𝑟) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)))) |
| 21 | 20 | rexlimdvv 3212 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) ∧ 𝑝 ∈ 𝐴) → (∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))) |
| 22 | 21 | expimpd 453 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → ((𝑝 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟)) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))) |
| 23 | 15, 22 | sylbid 240 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑝 ∈ (𝑋 + (𝑌 + 𝑍)) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))) |
| 24 | 23 | ssrdv 3989 |
1
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)) |