Proof of Theorem cdlemkvcl
Step | Hyp | Ref
| Expression |
1 | | cdlemk.v1 |
. 2
⊢ 𝑉 = (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) |
2 | | simp1l 1085 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝐾 ∈ HL) |
3 | | hllat 34650 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝐾 ∈ Lat) |
5 | | simp1 1061 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | | simp22 1095 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝐺 ∈ 𝑇) |
7 | | cdlemk.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
8 | | cdlemk.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
9 | 7, 8 | atbase 34576 |
. . . . . 6
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
10 | 9 | 3ad2ant3 1084 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵) |
11 | | cdlemk.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
12 | | cdlemk.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
13 | 7, 11, 12 | ltrncl 35411 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝐺‘𝑃) ∈ 𝐵) |
14 | 5, 6, 10, 13 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐵) |
15 | | simp23 1096 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝑋 ∈ 𝑇) |
16 | 7, 11, 12 | ltrncl 35411 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑋‘𝑃) ∈ 𝐵) |
17 | 5, 15, 10, 16 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐵) |
18 | | cdlemk.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
19 | 7, 18 | latjcl 17051 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑃) ∈ 𝐵 ∧ (𝑋‘𝑃) ∈ 𝐵) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) |
20 | 4, 14, 17, 19 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) |
21 | | simp21 1094 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝐹 ∈ 𝑇) |
22 | 11, 12 | ltrncnv 35432 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |
23 | 5, 21, 22 | syl2anc 693 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → ◡𝐹 ∈ 𝑇) |
24 | 11, 12 | ltrnco 36007 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝐺 ∘ ◡𝐹) ∈ 𝑇) |
25 | 5, 6, 23, 24 | syl3anc 1326 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝐺 ∘ ◡𝐹) ∈ 𝑇) |
26 | | cdlemk.r |
. . . . . 6
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
27 | 7, 11, 12, 26 | trlcl 35451 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵) |
28 | 5, 25, 27 | syl2anc 693 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵) |
29 | 11, 12 | ltrnco 36007 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝑋 ∘ ◡𝐹) ∈ 𝑇) |
30 | 5, 15, 23, 29 | syl3anc 1326 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝑋 ∘ ◡𝐹) ∈ 𝑇) |
31 | 7, 11, 12, 26 | trlcl 35451 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵) |
32 | 5, 30, 31 | syl2anc 693 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵) |
33 | 7, 18 | latjcl 17051 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵) → ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ∈ 𝐵) |
34 | 4, 28, 32, 33 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ∈ 𝐵) |
35 | | cdlemk.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
36 | 7, 35 | latmcl 17052 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵 ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ∈ 𝐵) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) ∈ 𝐵) |
37 | 4, 20, 34, 36 | syl3anc 1326 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) ∈ 𝐵) |
38 | 1, 37 | syl5eqel 2705 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → 𝑉 ∈ 𝐵) |