Proof of Theorem dalem23
Step | Hyp | Ref
| Expression |
1 | | dalem23.g |
. 2
⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) |
2 | | dalem.ph |
. . . . . . . 8
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
3 | 2 | dalemkehl 37374 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ HL) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ HL) |
5 | | dalem.ps |
. . . . . . . 8
⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) |
6 | 5 | dalemccea 37434 |
. . . . . . 7
⊢ (𝜓 → 𝑐 ∈ 𝐴) |
7 | 6 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑐 ∈ 𝐴) |
8 | 2 | dalempea 37377 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
9 | 8 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑃 ∈ 𝐴) |
10 | 5 | dalemddea 37435 |
. . . . . . 7
⊢ (𝜓 → 𝑑 ∈ 𝐴) |
11 | 10 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑑 ∈ 𝐴) |
12 | 2 | dalemsea 37380 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
13 | 12 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑆 ∈ 𝐴) |
14 | | dalem.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
15 | | dalem.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
16 | 14, 15 | hlatj4 37125 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑐 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑑 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑐 ∨ 𝑃) ∨ (𝑑 ∨ 𝑆)) = ((𝑐 ∨ 𝑑) ∨ (𝑃 ∨ 𝑆))) |
17 | 4, 7, 9, 11, 13, 16 | syl122anc 1381 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑐 ∨ 𝑃) ∨ (𝑑 ∨ 𝑆)) = ((𝑐 ∨ 𝑑) ∨ (𝑃 ∨ 𝑆))) |
18 | 17 | 3adant2 1133 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝑐 ∨ 𝑃) ∨ (𝑑 ∨ 𝑆)) = ((𝑐 ∨ 𝑑) ∨ (𝑃 ∨ 𝑆))) |
19 | | dalem.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
20 | | dalem23.o |
. . . . 5
⊢ 𝑂 = (LPlanes‘𝐾) |
21 | | dalem23.y |
. . . . 5
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
22 | | dalem23.z |
. . . . 5
⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) |
23 | 2, 19, 14, 15, 5, 20, 21, 22 | dalem22 37446 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝑐 ∨ 𝑑) ∨ (𝑃 ∨ 𝑆)) ∈ 𝑂) |
24 | 18, 23 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝑐 ∨ 𝑃) ∨ (𝑑 ∨ 𝑆)) ∈ 𝑂) |
25 | 3 | 3ad2ant1 1135 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐾 ∈ HL) |
26 | 2, 19, 14, 15, 20, 21 | dalemply 37405 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ≤ 𝑌) |
27 | 5 | dalem-ccly 37436 |
. . . . . . . 8
⊢ (𝜓 → ¬ 𝑐 ≤ 𝑌) |
28 | | nbrne2 5073 |
. . . . . . . 8
⊢ ((𝑃 ≤ 𝑌 ∧ ¬ 𝑐 ≤ 𝑌) → 𝑃 ≠ 𝑐) |
29 | 26, 27, 28 | syl2an 599 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑃 ≠ 𝑐) |
30 | 29 | necomd 2996 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑐 ≠ 𝑃) |
31 | | eqid 2737 |
. . . . . . 7
⊢
(LLines‘𝐾) =
(LLines‘𝐾) |
32 | 14, 15, 31 | llni2 37263 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑐 ≠ 𝑃) → (𝑐 ∨ 𝑃) ∈ (LLines‘𝐾)) |
33 | 4, 7, 9, 30, 32 | syl31anc 1375 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑐 ∨ 𝑃) ∈ (LLines‘𝐾)) |
34 | 33 | 3adant2 1133 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑐 ∨ 𝑃) ∈ (LLines‘𝐾)) |
35 | 10 | 3ad2ant3 1137 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑑 ∈ 𝐴) |
36 | 12 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑆 ∈ 𝐴) |
37 | 2, 19, 14, 15, 22 | dalemsly 37406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝑆 ≤ 𝑌) |
38 | 37 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑆 ≤ 𝑌) |
39 | 5 | dalem-ddly 37437 |
. . . . . . . 8
⊢ (𝜓 → ¬ 𝑑 ≤ 𝑌) |
40 | 39 | 3ad2ant3 1137 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑑 ≤ 𝑌) |
41 | | nbrne2 5073 |
. . . . . . 7
⊢ ((𝑆 ≤ 𝑌 ∧ ¬ 𝑑 ≤ 𝑌) → 𝑆 ≠ 𝑑) |
42 | 38, 40, 41 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑆 ≠ 𝑑) |
43 | 42 | necomd 2996 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑑 ≠ 𝑆) |
44 | 14, 15, 31 | llni2 37263 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑑 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ 𝑑 ≠ 𝑆) → (𝑑 ∨ 𝑆) ∈ (LLines‘𝐾)) |
45 | 25, 35, 36, 43, 44 | syl31anc 1375 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝑑 ∨ 𝑆) ∈ (LLines‘𝐾)) |
46 | | dalem23.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
47 | 14, 46, 15, 31, 20 | 2llnmj 37311 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑐 ∨ 𝑃) ∈ (LLines‘𝐾) ∧ (𝑑 ∨ 𝑆) ∈ (LLines‘𝐾)) → (((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) ∈ 𝐴 ↔ ((𝑐 ∨ 𝑃) ∨ (𝑑 ∨ 𝑆)) ∈ 𝑂)) |
48 | 25, 34, 45, 47 | syl3anc 1373 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) ∈ 𝐴 ↔ ((𝑐 ∨ 𝑃) ∨ (𝑑 ∨ 𝑆)) ∈ 𝑂)) |
49 | 24, 48 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) ∈ 𝐴) |
50 | 1, 49 | eqeltrid 2842 |
1
⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ∈ 𝐴) |