Proof of Theorem cdlemefrs29pre00
Step | Hyp | Ref
| Expression |
1 | | anass 470 |
. 2
⊢ (((¬
𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) ↔ (¬ 𝑠 ≤ 𝑊 ∧ (𝜑 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅))) |
2 | | simpl3 1194 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → 𝜓) |
3 | | cdlemefrs29.eq |
. . . . . . 7
⊢ (𝑠 = 𝑅 → (𝜑 ↔ 𝜓)) |
4 | 3 | pm5.32ri 577 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 = 𝑅) ↔ (𝜓 ∧ 𝑠 = 𝑅)) |
5 | 4 | baibr 538 |
. . . . 5
⊢ (𝜓 → (𝑠 = 𝑅 ↔ (𝜑 ∧ 𝑠 = 𝑅))) |
6 | 2, 5 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → (𝑠 = 𝑅 ↔ (𝜑 ∧ 𝑠 = 𝑅))) |
7 | | cdlemefrs29.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝐾) |
8 | | cdlemefrs29.m |
. . . . . . . . . 10
⊢ ∧ =
(meet‘𝐾) |
9 | | eqid 2733 |
. . . . . . . . . 10
⊢
(0.‘𝐾) =
(0.‘𝐾) |
10 | | cdlemefrs29.a |
. . . . . . . . . 10
⊢ 𝐴 = (Atoms‘𝐾) |
11 | | cdlemefrs29.h |
. . . . . . . . . 10
⊢ 𝐻 = (LHyp‘𝐾) |
12 | 7, 8, 9, 10, 11 | lhpmat 38890 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑅 ∧ 𝑊) = (0.‘𝐾)) |
13 | 12 | 3adant3 1133 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) → (𝑅 ∧ 𝑊) = (0.‘𝐾)) |
14 | 13 | adantr 482 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → (𝑅 ∧ 𝑊) = (0.‘𝐾)) |
15 | 14 | oveq2d 7422 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → (𝑠 ∨ (𝑅 ∧ 𝑊)) = (𝑠 ∨ (0.‘𝐾))) |
16 | | simpl1l 1225 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → 𝐾 ∈ HL) |
17 | | hlol 38220 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → 𝐾 ∈ OL) |
19 | | cdlemefrs29.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐾) |
20 | 19, 10 | atbase 38148 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐴 → 𝑠 ∈ 𝐵) |
21 | 20 | adantl 483 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐵) |
22 | | cdlemefrs29.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
23 | 19, 22, 9 | olj01 38084 |
. . . . . . 7
⊢ ((𝐾 ∈ OL ∧ 𝑠 ∈ 𝐵) → (𝑠 ∨ (0.‘𝐾)) = 𝑠) |
24 | 18, 21, 23 | syl2anc 585 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → (𝑠 ∨ (0.‘𝐾)) = 𝑠) |
25 | 15, 24 | eqtrd 2773 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑠) |
26 | 25 | eqeq1d 2735 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 ↔ 𝑠 = 𝑅)) |
27 | 26 | anbi2d 630 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → ((𝜑 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) ↔ (𝜑 ∧ 𝑠 = 𝑅))) |
28 | 6, 26, 27 | 3bitr4d 311 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → ((𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅 ↔ (𝜑 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅))) |
29 | 28 | anbi2d 630 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) ↔ (¬ 𝑠 ≤ 𝑊 ∧ (𝜑 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅)))) |
30 | 1, 29 | bitr4id 290 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝜓) ∧ 𝑠 ∈ 𝐴) → (((¬ 𝑠 ≤ 𝑊 ∧ 𝜑) ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅) ↔ (¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑅 ∧ 𝑊)) = 𝑅))) |