Proof of Theorem cdlemk9
Step | Hyp | Ref
| Expression |
1 | | cdlemk.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
2 | | cdlemk.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | cdlemk.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
4 | | cdlemk.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | cdlemk.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | cdlemk.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
7 | | cdlemk.r |
. . . 4
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
8 | | cdlemk.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | cdlemk8 38831 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) = ((𝐺‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
10 | 9 | oveq1d 7283 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (((𝐺‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) ∧ 𝑊)) |
11 | | simp1 1134 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
12 | 2, 4, 5, 6 | ltrnel 38132 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∈ 𝐴 ∧ ¬ (𝐺‘𝑃) ≤ 𝑊)) |
13 | 12 | 3adant2r 1177 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∈ 𝐴 ∧ ¬ (𝐺‘𝑃) ≤ 𝑊)) |
14 | | eqid 2739 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
15 | 2, 8, 14, 4, 5 | lhpmat 38023 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑃) ∈ 𝐴 ∧ ¬ (𝐺‘𝑃) ≤ 𝑊)) → ((𝐺‘𝑃) ∧ 𝑊) = (0.‘𝐾)) |
16 | 11, 13, 15 | syl2anc 583 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∧ 𝑊) = (0.‘𝐾)) |
17 | 16 | oveq1d 7283 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∧ 𝑊) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) = ((0.‘𝐾) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
18 | | simp1l 1195 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL) |
19 | | simp2l 1197 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
20 | | simp3l 1199 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴) |
21 | 2, 4, 5, 6 | ltrnat 38133 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴) |
22 | 11, 19, 20, 21 | syl3anc 1369 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝑃) ∈ 𝐴) |
23 | | simp2r 1198 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇) |
24 | 5, 6 | ltrncnv 38139 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → ◡𝐺 ∈ 𝑇) |
25 | 11, 19, 24 | syl2anc 583 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ◡𝐺 ∈ 𝑇) |
26 | 5, 6 | ltrnco 38712 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ◡𝐺 ∈ 𝑇) → (𝑋 ∘ ◡𝐺) ∈ 𝑇) |
27 | 11, 23, 25, 26 | syl3anc 1369 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ◡𝐺) ∈ 𝑇) |
28 | 1, 5, 6, 7 | trlcl 38157 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐺) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐵) |
29 | 11, 27, 28 | syl2anc 583 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐵) |
30 | | simp1r 1196 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
31 | 1, 5 | lhpbase 37991 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
32 | 30, 31 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵) |
33 | 2, 5, 6, 7 | trlle 38177 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐺) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ◡𝐺)) ≤ 𝑊) |
34 | 11, 27, 33 | syl2anc 583 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐺)) ≤ 𝑊) |
35 | 1, 2, 3, 8, 4 | atmod4i2 37860 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ((𝐺‘𝑃) ∈ 𝐴 ∧ (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ (𝑅‘(𝑋 ∘ ◡𝐺)) ≤ 𝑊) → (((𝐺‘𝑃) ∧ 𝑊) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) = (((𝐺‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) ∧ 𝑊)) |
36 | 18, 22, 29, 32, 34, 35 | syl131anc 1381 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∧ 𝑊) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) = (((𝐺‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) ∧ 𝑊)) |
37 | | hlol 37354 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
38 | 18, 37 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ OL) |
39 | 1, 3, 14 | olj02 37219 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐵) → ((0.‘𝐾) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) = (𝑅‘(𝑋 ∘ ◡𝐺))) |
40 | 38, 29, 39 | syl2anc 583 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((0.‘𝐾) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) = (𝑅‘(𝑋 ∘ ◡𝐺))) |
41 | 17, 36, 40 | 3eqtr3d 2787 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ◡𝐺))) |
42 | 10, 41 | eqtrd 2779 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ◡𝐺))) |