Proof of Theorem dalem4
Step | Hyp | Ref
| Expression |
1 | | dalema.ph |
. . . . 5
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
2 | | dalemc.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
3 | | dalemc.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
4 | | dalemc.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 1, 2, 3, 4 | dalemswapyz 37670 |
. . . 4
⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (𝐶 ≤ (𝑆 ∨ 𝑃) ∧ 𝐶 ≤ (𝑇 ∨ 𝑄) ∧ 𝐶 ≤ (𝑈 ∨ 𝑅))))) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ≠ 𝑇) → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (𝐶 ≤ (𝑆 ∨ 𝑃) ∧ 𝐶 ≤ (𝑇 ∨ 𝑄) ∧ 𝐶 ≤ (𝑈 ∨ 𝑅))))) |
7 | | dalem3.d |
. . . . . 6
⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) |
8 | 1 | dalemkelat 37638 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Lat) |
9 | 1, 3, 4 | dalempjqeb 37659 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
10 | 1, 3, 4 | dalemsjteb 37660 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
11 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
12 | | dalem3.m |
. . . . . . . 8
⊢ ∧ =
(meet‘𝐾) |
13 | 11, 12 | latmcom 18181 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄))) |
14 | 8, 9, 10, 13 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄))) |
15 | 7, 14 | eqtrid 2790 |
. . . . 5
⊢ (𝜑 → 𝐷 = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄))) |
16 | 15 | neeq1d 3003 |
. . . 4
⊢ (𝜑 → (𝐷 ≠ 𝑇 ↔ ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≠ 𝑇)) |
17 | 16 | biimpa 477 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ≠ 𝑇) → ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≠ 𝑇) |
18 | | biid 260 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (𝐶 ≤ (𝑆 ∨ 𝑃) ∧ 𝐶 ≤ (𝑇 ∨ 𝑄) ∧ 𝐶 ≤ (𝑈 ∨ 𝑅)))) ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (𝐶 ≤ (𝑆 ∨ 𝑃) ∧ 𝐶 ≤ (𝑇 ∨ 𝑄) ∧ 𝐶 ≤ (𝑈 ∨ 𝑅))))) |
19 | | dalem3.o |
. . . 4
⊢ 𝑂 = (LPlanes‘𝐾) |
20 | | dalem3.z |
. . . 4
⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) |
21 | | dalem3.y |
. . . 4
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
22 | | eqid 2738 |
. . . 4
⊢ ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) |
23 | | eqid 2738 |
. . . 4
⊢ ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)) = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)) |
24 | 18, 2, 3, 4, 12, 19, 20, 21, 22, 23 | dalem3 37678 |
. . 3
⊢
(((((𝐾 ∈ HL
∧ 𝐶 ∈
(Base‘𝐾)) ∧
(𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (𝐶 ≤ (𝑆 ∨ 𝑃) ∧ 𝐶 ≤ (𝑇 ∨ 𝑄) ∧ 𝐶 ≤ (𝑈 ∨ 𝑅)))) ∧ ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≠ 𝑇) → ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≠ ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅))) |
25 | 6, 17, 24 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ 𝐷 ≠ 𝑇) → ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≠ ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅))) |
26 | 15 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝐷 ≠ 𝑇) → 𝐷 = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄))) |
27 | | dalem3.e |
. . . 4
⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) |
28 | 1 | dalemkehl 37637 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ HL) |
29 | 1 | dalemqea 37641 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
30 | 1 | dalemrea 37642 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ 𝐴) |
31 | 11, 3, 4 | hlatjcl 37381 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
32 | 28, 29, 30, 31 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
33 | 1, 3, 4 | dalemtjueb 37661 |
. . . . 5
⊢ (𝜑 → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) |
34 | 11, 12 | latmcom 18181 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅))) |
35 | 8, 32, 33, 34 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅))) |
36 | 27, 35 | eqtrid 2790 |
. . 3
⊢ (𝜑 → 𝐸 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅))) |
37 | 36 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝐷 ≠ 𝑇) → 𝐸 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅))) |
38 | 25, 26, 37 | 3netr4d 3021 |
1
⊢ ((𝜑 ∧ 𝐷 ≠ 𝑇) → 𝐷 ≠ 𝐸) |