Proof of Theorem dalem57
Step | Hyp | Ref
| Expression |
1 | | dalem.ph |
. . . . . . 7
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
2 | | dalem.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
3 | | dalem.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
4 | | dalem.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | dalem.ps |
. . . . . . 7
⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) |
6 | | dalem57.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
7 | | dalem57.o |
. . . . . . 7
⊢ 𝑂 = (LPlanes‘𝐾) |
8 | | dalem57.y |
. . . . . . 7
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
9 | | dalem57.z |
. . . . . . 7
⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) |
10 | | dalem57.g |
. . . . . . 7
⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) |
11 | | dalem57.h |
. . . . . . 7
⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) |
12 | | dalem57.i |
. . . . . . 7
⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) |
13 | | dalem57.b1 |
. . . . . . 7
⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | dalem55 37396 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) = ((𝐺 ∨ 𝐻) ∧ 𝐵)) |
15 | 1 | dalemkelat 37293 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Lat) |
16 | 15 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ Lat) |
17 | 1 | dalemkehl 37292 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ HL) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ HL) |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | dalem23 37365 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ∈ 𝐴) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11 | dalem29 37370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐻 ∈ 𝐴) |
21 | | eqid 2739 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
22 | 21, 3, 4 | hlatjcl 37036 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝐺 ∨ 𝐻) ∈ (Base‘𝐾)) |
23 | 18, 19, 20, 22 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐺 ∨ 𝐻) ∈ (Base‘𝐾)) |
24 | 1, 3, 4 | dalempjqeb 37314 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
25 | 24 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
26 | 21, 2, 6 | latmle2 17815 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝐺 ∨ 𝐻) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) ≤ (𝑃 ∨ 𝑄)) |
27 | 16, 23, 25, 26 | syl3anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) ≤ (𝑃 ∨ 𝑄)) |
28 | 14, 27 | eqbrtrrd 5064 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ (𝑃 ∨ 𝑄)) |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | dalem56 37397 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑆 ∨ 𝑇)) = ((𝐺 ∨ 𝐻) ∧ 𝐵)) |
30 | 1, 3, 4 | dalemsjteb 37315 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
31 | 30 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
32 | 21, 2, 6 | latmle2 17815 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝐺 ∨ 𝐻) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝐺 ∨ 𝐻) ∧ (𝑆 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇)) |
33 | 16, 23, 31, 32 | syl3anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑆 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇)) |
34 | 29, 33 | eqbrtrrd 5064 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ (𝑆 ∨ 𝑇)) |
35 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | dalem54 37395 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ 𝐴) |
36 | 21, 4 | atbase 36958 |
. . . . . . 7
⊢ (((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ 𝐴 → ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ (Base‘𝐾)) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ (Base‘𝐾)) |
38 | 21, 2, 6 | latlem12 17816 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))) → ((((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ (𝑆 ∨ 𝑇)) ↔ ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)))) |
39 | 16, 37, 25, 31, 38 | syl13anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ (𝑆 ∨ 𝑇)) ↔ ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)))) |
40 | 28, 34, 39 | mpbi2and 712 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))) |
41 | | dalem57.d |
. . . 4
⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) |
42 | 40, 41 | breqtrrdi 5082 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ 𝐷) |
43 | | hlatl 37029 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
44 | 18, 43 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ AtLat) |
45 | 1, 2, 3, 4, 6, 7, 8, 9, 41 | dalemdea 37331 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝐴) |
46 | 45 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐷 ∈ 𝐴) |
47 | 2, 4 | atcmp 36980 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ 𝐷 ↔ ((𝐺 ∨ 𝐻) ∧ 𝐵) = 𝐷)) |
48 | 44, 35, 46, 47 | syl3anc 1372 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ 𝐷 ↔ ((𝐺 ∨ 𝐻) ∧ 𝐵) = 𝐷)) |
49 | 42, 48 | mpbid 235 |
. 2
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) = 𝐷) |
50 | | eqid 2739 |
. . . . 5
⊢
(LLines‘𝐾) =
(LLines‘𝐾) |
51 | 1, 2, 3, 4, 5, 6, 50, 7, 8, 9,
10, 11, 12, 13 | dalem53 37394 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐵 ∈ (LLines‘𝐾)) |
52 | 21, 50 | llnbase 37178 |
. . . 4
⊢ (𝐵 ∈ (LLines‘𝐾) → 𝐵 ∈ (Base‘𝐾)) |
53 | 51, 52 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐵 ∈ (Base‘𝐾)) |
54 | 21, 2, 6 | latmle2 17815 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ (𝐺 ∨ 𝐻) ∈ (Base‘𝐾) ∧ 𝐵 ∈ (Base‘𝐾)) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ 𝐵) |
55 | 16, 23, 53, 54 | syl3anc 1372 |
. 2
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ≤ 𝐵) |
56 | 49, 55 | eqbrtrrd 5064 |
1
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐷 ≤ 𝐵) |