Proof of Theorem pmodlem1
Step | Hyp | Ref
| Expression |
1 | | simpl11 1136 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝐾 ∈ HL) |
2 | | simpl12 1137 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑋 ⊆ 𝐴) |
3 | | simpl13 1138 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑌 ⊆ 𝐴) |
4 | | ssinss1 3841 |
. . . . 5
⊢ (𝑌 ⊆ 𝐴 → (𝑌 ∩ 𝑍) ⊆ 𝐴) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → (𝑌 ∩ 𝑍) ⊆ 𝐴) |
6 | | pmodlem.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
7 | | pmodlem.p |
. . . . 5
⊢ + =
(+𝑃‘𝐾) |
8 | 6, 7 | sspadd1 35101 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ (𝑌 ∩ 𝑍) ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + (𝑌 ∩ 𝑍))) |
9 | 1, 2, 5, 8 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑋 ⊆ (𝑋 + (𝑌 ∩ 𝑍))) |
10 | | simpr 477 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑝 = 𝑞) |
11 | | simpl31 1142 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑞 ∈ 𝑋) |
12 | 10, 11 | eqeltrd 2701 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑝 ∈ 𝑋) |
13 | 9, 12 | sseldd 3604 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 = 𝑞) → 𝑝 ∈ (𝑋 + (𝑌 ∩ 𝑍))) |
14 | | simpl11 1136 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝐾 ∈ HL) |
15 | | hllat 34650 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
16 | 14, 15 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝐾 ∈ Lat) |
17 | | simpl12 1137 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑋 ⊆ 𝐴) |
18 | | simpl13 1138 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑌 ⊆ 𝐴) |
19 | 18, 4 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → (𝑌 ∩ 𝑍) ⊆ 𝐴) |
20 | | simpl31 1142 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑞 ∈ 𝑋) |
21 | | simpl32 1143 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑟 ∈ 𝑌) |
22 | | simpl21 1139 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑍 ∈ 𝑆) |
23 | | simpl22 1140 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑋 ⊆ 𝑍) |
24 | | simpl23 1141 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑝 ∈ 𝑍) |
25 | | pmodlem.s |
. . . . . . . . . 10
⊢ 𝑆 = (PSubSp‘𝐾) |
26 | 6, 25 | psubssat 35040 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑍 ∈ 𝑆) → 𝑍 ⊆ 𝐴) |
27 | 14, 22, 26 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑍 ⊆ 𝐴) |
28 | 27, 24 | sseldd 3604 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑝 ∈ 𝐴) |
29 | 18, 21 | sseldd 3604 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑟 ∈ 𝐴) |
30 | 17, 20 | sseldd 3604 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑞 ∈ 𝐴) |
31 | 28, 29, 30 | 3jca 1242 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) |
32 | | simpr 477 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑝 ≠ 𝑞) |
33 | | simpl33 1144 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑝 ≤ (𝑞 ∨ 𝑟)) |
34 | | pmodlem.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
35 | | pmodlem.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
36 | 34, 35, 6 | hlatexch1 34681 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ≠ 𝑞) → (𝑝 ≤ (𝑞 ∨ 𝑟) → 𝑟 ≤ (𝑞 ∨ 𝑝))) |
37 | 36 | imp 445 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ≠ 𝑞) ∧ 𝑝 ≤ (𝑞 ∨ 𝑟)) → 𝑟 ≤ (𝑞 ∨ 𝑝)) |
38 | 14, 31, 32, 33, 37 | syl31anc 1329 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑟 ≤ (𝑞 ∨ 𝑝)) |
39 | | simp31 1097 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑞 ∈ 𝑋) |
40 | 39 | snssd 4340 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → {𝑞} ⊆ 𝑋) |
41 | | simp22 1095 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑋 ⊆ 𝑍) |
42 | 40, 41 | sstrd 3613 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → {𝑞} ⊆ 𝑍) |
43 | | simp23 1096 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑝 ∈ 𝑍) |
44 | 43 | snssd 4340 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → {𝑝} ⊆ 𝑍) |
45 | | simp11 1091 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝐾 ∈ HL) |
46 | | simp12 1092 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑋 ⊆ 𝐴) |
47 | 46, 39 | sseldd 3604 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑞 ∈ 𝐴) |
48 | 47 | snssd 4340 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → {𝑞} ⊆ 𝐴) |
49 | | simp21 1094 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑍 ∈ 𝑆) |
50 | 45, 49, 26 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑍 ⊆ 𝐴) |
51 | 50, 43 | sseldd 3604 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑝 ∈ 𝐴) |
52 | 51 | snssd 4340 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → {𝑝} ⊆ 𝐴) |
53 | 6, 25, 7 | paddss 35131 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ ({𝑞} ⊆ 𝐴 ∧ {𝑝} ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆)) → (({𝑞} ⊆ 𝑍 ∧ {𝑝} ⊆ 𝑍) ↔ ({𝑞} + {𝑝}) ⊆ 𝑍)) |
54 | 45, 48, 52, 49, 53 | syl13anc 1328 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → (({𝑞} ⊆ 𝑍 ∧ {𝑝} ⊆ 𝑍) ↔ ({𝑞} + {𝑝}) ⊆ 𝑍)) |
55 | 42, 44, 54 | mpbi2and 956 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → ({𝑞} + {𝑝}) ⊆ 𝑍) |
56 | | simp33 1099 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑟 ≤ (𝑞 ∨ 𝑝)) |
57 | 45, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝐾 ∈ Lat) |
58 | | simp13 1093 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑌 ⊆ 𝐴) |
59 | | simp32 1098 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑟 ∈ 𝑌) |
60 | 58, 59 | sseldd 3604 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑟 ∈ 𝐴) |
61 | 34, 35, 6, 7 | elpadd2at2 35093 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑞 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → (𝑟 ∈ ({𝑞} + {𝑝}) ↔ 𝑟 ≤ (𝑞 ∨ 𝑝))) |
62 | 57, 47, 51, 60, 61 | syl13anc 1328 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → (𝑟 ∈ ({𝑞} + {𝑝}) ↔ 𝑟 ≤ (𝑞 ∨ 𝑝))) |
63 | 56, 62 | mpbird 247 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑟 ∈ ({𝑞} + {𝑝})) |
64 | 55, 63 | sseldd 3604 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑟 ≤ (𝑞 ∨ 𝑝))) → 𝑟 ∈ 𝑍) |
65 | 14, 17, 18, 22, 23, 24, 20, 21, 38, 64 | syl333anc 1358 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑟 ∈ 𝑍) |
66 | 21, 65 | elind 3798 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑟 ∈ (𝑌 ∩ 𝑍)) |
67 | 34, 35, 6, 7 | elpaddri 35088 |
. . 3
⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ (𝑌 ∩ 𝑍) ⊆ 𝐴) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 ∩ 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) → 𝑝 ∈ (𝑋 + (𝑌 ∩ 𝑍))) |
68 | 16, 17, 19, 20, 66, 28, 33, 67 | syl322anc 1354 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) ∧ 𝑝 ≠ 𝑞) → 𝑝 ∈ (𝑋 + (𝑌 ∩ 𝑍))) |
69 | 13, 68 | pm2.61dane 2881 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) → 𝑝 ∈ (𝑋 + (𝑌 ∩ 𝑍))) |