Proof of Theorem paddasslem12
Step | Hyp | Ref
| Expression |
1 | | simpl1l 1225 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝐾 ∈ HL) |
2 | | simpl21 1252 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑋 ⊆ 𝐴) |
3 | | simpl22 1253 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑌 ⊆ 𝐴) |
4 | | paddasslem.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | paddasslem.p |
. . . . . 6
⊢ + =
(+𝑃‘𝐾) |
6 | 4, 5 | paddssat 37473 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴) |
7 | 1, 2, 3, 6 | syl3anc 1372 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑋 + 𝑌) ⊆ 𝐴) |
8 | | simpl23 1254 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑍 ⊆ 𝐴) |
9 | 1, 7, 8 | 3jca 1129 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) |
10 | 4, 5 | sspadd2 37475 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴) → 𝑌 ⊆ (𝑋 + 𝑌)) |
11 | 1, 3, 2, 10 | syl3anc 1372 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑌 ⊆ (𝑋 + 𝑌)) |
12 | 4, 5 | paddss1 37476 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 ⊆ (𝑋 + 𝑌) → (𝑌 + 𝑍) ⊆ ((𝑋 + 𝑌) + 𝑍))) |
13 | 9, 11, 12 | sylc 65 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑌 + 𝑍) ⊆ ((𝑋 + 𝑌) + 𝑍)) |
14 | 1 | hllatd 37023 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝐾 ∈ Lat) |
15 | | simprll 779 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ∈ 𝑌) |
16 | | simprlr 780 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑧 ∈ 𝑍) |
17 | | simpl3l 1229 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ 𝐴) |
18 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐾) =
(Base‘𝐾) |
19 | | paddasslem.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
20 | 18, 4 | atbase 36948 |
. . . . 5
⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾)) |
21 | 17, 20 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ (Base‘𝐾)) |
22 | 3, 15 | sseldd 3878 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ∈ 𝐴) |
23 | 18, 4 | atbase 36948 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ (Base‘𝐾)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ∈ (Base‘𝐾)) |
25 | | simpl3r 1230 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑟 ∈ 𝐴) |
26 | 18, 4 | atbase 36948 |
. . . . . 6
⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾)) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑟 ∈ (Base‘𝐾)) |
28 | | paddasslem.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
29 | 18, 28 | latjcl 17779 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → (𝑦 ∨ 𝑟) ∈ (Base‘𝐾)) |
30 | 14, 24, 27, 29 | syl3anc 1372 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑦 ∨ 𝑟) ∈ (Base‘𝐾)) |
31 | 8, 16 | sseldd 3878 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑧 ∈ 𝐴) |
32 | 18, 4 | atbase 36948 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (Base‘𝐾)) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑧 ∈ (Base‘𝐾)) |
34 | 18, 28 | latjcl 17779 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑦 ∨ 𝑧) ∈ (Base‘𝐾)) |
35 | 14, 24, 33, 34 | syl3anc 1372 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑦 ∨ 𝑧) ∈ (Base‘𝐾)) |
36 | | simpl1r 1226 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑥 = 𝑦) |
37 | | simprrl 781 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ≤ (𝑥 ∨ 𝑟)) |
38 | | oveq1 7179 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∨ 𝑟) = (𝑦 ∨ 𝑟)) |
39 | 38 | breq2d 5042 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑝 ≤ (𝑥 ∨ 𝑟) ↔ 𝑝 ≤ (𝑦 ∨ 𝑟))) |
40 | 39 | biimpa 480 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝑝 ≤ (𝑥 ∨ 𝑟)) → 𝑝 ≤ (𝑦 ∨ 𝑟)) |
41 | 36, 37, 40 | syl2anc 587 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ≤ (𝑦 ∨ 𝑟)) |
42 | 18, 19, 28 | latlej1 17788 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑦 ≤ (𝑦 ∨ 𝑧)) |
43 | 14, 24, 33, 42 | syl3anc 1372 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑦 ≤ (𝑦 ∨ 𝑧)) |
44 | | simprrr 782 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑟 ≤ (𝑦 ∨ 𝑧)) |
45 | 18, 19, 28 | latjle12 17790 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾) ∧ (𝑦 ∨ 𝑧) ∈ (Base‘𝐾))) → ((𝑦 ≤ (𝑦 ∨ 𝑧) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ↔ (𝑦 ∨ 𝑟) ≤ (𝑦 ∨ 𝑧))) |
46 | 14, 24, 27, 35, 45 | syl13anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → ((𝑦 ≤ (𝑦 ∨ 𝑧) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ↔ (𝑦 ∨ 𝑟) ≤ (𝑦 ∨ 𝑧))) |
47 | 43, 44, 46 | mpbi2and 712 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → (𝑦 ∨ 𝑟) ≤ (𝑦 ∨ 𝑧)) |
48 | 18, 19, 14, 21, 30, 35, 41, 47 | lattrd 17786 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ≤ (𝑦 ∨ 𝑧)) |
49 | 19, 28, 4, 5 | elpaddri 37461 |
. . 3
⊢ (((𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝 ≤ (𝑦 ∨ 𝑧))) → 𝑝 ∈ (𝑌 + 𝑍)) |
50 | 14, 3, 8, 15, 16, 17, 48, 49 | syl322anc 1399 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ (𝑌 + 𝑍)) |
51 | 13, 50 | sseldd 3878 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)) |