Proof of Theorem cdleme42c
Step | Hyp | Ref
| Expression |
1 | | simp2r 1081 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ¬ 𝑅 ≤ 𝑊) |
2 | | simp1l 1078 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ HL) |
3 | | hllat 33668 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ Lat) |
5 | | simp2l 1080 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑅 ∈ 𝐴) |
6 | | cdleme42.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
7 | | cdleme42.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
8 | 6, 7 | atbase 33594 |
. . . . 5
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵) |
9 | 5, 8 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑅 ∈ 𝐵) |
10 | | cdleme42.v |
. . . . 5
⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) |
11 | | simp3l 1082 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ∈ 𝐴) |
12 | | cdleme42.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
13 | 6, 12, 7 | hlatjcl 33671 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ 𝐵) |
14 | 2, 5, 11, 13 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) ∈ 𝐵) |
15 | | simp1r 1079 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
16 | | cdleme42.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
17 | 6, 16 | lhpbase 34302 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
18 | 15, 17 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑊 ∈ 𝐵) |
19 | | cdleme42.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
20 | 6, 19 | latmcl 16875 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐵) |
21 | 4, 14, 18, 20 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐵) |
22 | 10, 21 | syl5eqel 2692 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑉 ∈ 𝐵) |
23 | | cdleme42.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
24 | 6, 23, 12 | latjle12 16885 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑅 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) ↔ (𝑅 ∨ 𝑉) ≤ 𝑊)) |
25 | 4, 9, 22, 18, 24 | syl13anc 1320 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑅 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) ↔ (𝑅 ∨ 𝑉) ≤ 𝑊)) |
26 | | simpl 472 |
. . 3
⊢ ((𝑅 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) → 𝑅 ≤ 𝑊) |
27 | 25, 26 | syl6bir 243 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑅 ∨ 𝑉) ≤ 𝑊 → 𝑅 ≤ 𝑊)) |
28 | 1, 27 | mtod 188 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ¬ (𝑅 ∨ 𝑉) ≤ 𝑊) |