Proof of Theorem cdleme20yOLD
Step | Hyp | Ref
| Expression |
1 | | simp3r 1083 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ¬ 𝑅 ≤ (𝑆 ∨ 𝑇)) |
2 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ HL) |
3 | | simp22 1088 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝑆 ∈ 𝐴) |
4 | | simp23 1089 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝑇 ∈ 𝐴) |
5 | | cdleme20z.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
6 | | cdleme20z.a |
. . . . . . . . 9
⊢ 𝐴 = (Atoms‘𝐾) |
7 | 5, 6 | hlatjcom 33672 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) = (𝑇 ∨ 𝑆)) |
8 | 2, 3, 4, 7 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → (𝑆 ∨ 𝑇) = (𝑇 ∨ 𝑆)) |
9 | 8 | breq2d 4595 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → (𝑅 ≤ (𝑆 ∨ 𝑇) ↔ 𝑅 ≤ (𝑇 ∨ 𝑆))) |
10 | 1, 9 | mtbid 313 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ¬ 𝑅 ≤ (𝑇 ∨ 𝑆)) |
11 | | hlcvl 33664 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) |
12 | 11 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ CvLat) |
13 | | simp21 1087 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝑅 ∈ 𝐴) |
14 | | simp3l 1082 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝑆 ≠ 𝑇) |
15 | | cdleme20z.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
16 | 15, 5, 6 | cvlatexch1 33641 |
. . . . . 6
⊢ ((𝐾 ∈ CvLat ∧ (𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ 𝑆 ≠ 𝑇) → (𝑆 ≤ (𝑇 ∨ 𝑅) → 𝑅 ≤ (𝑇 ∨ 𝑆))) |
17 | 12, 3, 13, 4, 14, 16 | syl131anc 1331 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → (𝑆 ≤ (𝑇 ∨ 𝑅) → 𝑅 ≤ (𝑇 ∨ 𝑆))) |
18 | 10, 17 | mtod 188 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ¬ 𝑆 ≤ (𝑇 ∨ 𝑅)) |
19 | | hlatl 33665 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
20 | 19 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ AtLat) |
21 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
22 | 21, 5, 6 | hlatjcl 33671 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑇 ∨ 𝑅) ∈ (Base‘𝐾)) |
23 | 2, 4, 13, 22 | syl3anc 1318 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → (𝑇 ∨ 𝑅) ∈ (Base‘𝐾)) |
24 | | cdleme20z.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
25 | | eqid 2610 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
26 | 21, 15, 24, 25, 6 | atnle 33622 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑆 ∈ 𝐴 ∧ (𝑇 ∨ 𝑅) ∈ (Base‘𝐾)) → (¬ 𝑆 ≤ (𝑇 ∨ 𝑅) ↔ (𝑆 ∧ (𝑇 ∨ 𝑅)) = (0.‘𝐾))) |
27 | 20, 3, 23, 26 | syl3anc 1318 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → (¬ 𝑆 ≤ (𝑇 ∨ 𝑅) ↔ (𝑆 ∧ (𝑇 ∨ 𝑅)) = (0.‘𝐾))) |
28 | 18, 27 | mpbid 221 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → (𝑆 ∧ (𝑇 ∨ 𝑅)) = (0.‘𝐾)) |
29 | 28 | oveq1d 6564 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ((𝑆 ∧ (𝑇 ∨ 𝑅)) ∨ 𝑅) = ((0.‘𝐾) ∨ 𝑅)) |
30 | 21, 6 | atbase 33594 |
. . . 4
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
31 | 13, 30 | syl 17 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝑅 ∈ (Base‘𝐾)) |
32 | 15, 5, 6 | hlatlej2 33680 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → 𝑅 ≤ (𝑇 ∨ 𝑅)) |
33 | 2, 4, 13, 32 | syl3anc 1318 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝑅 ≤ (𝑇 ∨ 𝑅)) |
34 | 21, 15, 5, 24, 6 | atmod4i2 34171 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑅) ∈ (Base‘𝐾)) ∧ 𝑅 ≤ (𝑇 ∨ 𝑅)) → ((𝑆 ∧ (𝑇 ∨ 𝑅)) ∨ 𝑅) = ((𝑆 ∨ 𝑅) ∧ (𝑇 ∨ 𝑅))) |
35 | 2, 3, 31, 23, 33, 34 | syl131anc 1331 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ((𝑆 ∧ (𝑇 ∨ 𝑅)) ∨ 𝑅) = ((𝑆 ∨ 𝑅) ∧ (𝑇 ∨ 𝑅))) |
36 | | hlol 33666 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
37 | 36 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ OL) |
38 | 21, 5, 25 | olj02 33531 |
. . 3
⊢ ((𝐾 ∈ OL ∧ 𝑅 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑅) = 𝑅) |
39 | 37, 31, 38 | syl2anc 691 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ((0.‘𝐾) ∨ 𝑅) = 𝑅) |
40 | 29, 35, 39 | 3eqtr3d 2652 |
1
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ (𝑆 ∨ 𝑇))) → ((𝑆 ∨ 𝑅) ∧ (𝑇 ∨ 𝑅)) = 𝑅) |