Proof of Theorem tglineneq
Step | Hyp | Ref
| Expression |
1 | | tglineintmo.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | tglineintmo.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
3 | | tglineintmo.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
4 | | tglineintmo.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | | tglineinteq.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
6 | | tglineinteq.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
7 | | tglineinteq.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
8 | | tglineinteq.e |
. . . . . 6
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | ncolne1 25944 |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
10 | 1, 2, 3, 4, 5, 6, 9 | tglinerflx1 25952 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵)) |
11 | 10 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐴 ∈ (𝐴𝐿𝐵)) |
12 | | simplr 785 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 = 𝐷) |
13 | 4 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐺 ∈ TarskiG) |
14 | 7 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ∈ 𝑃) |
15 | | tglineinteq.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
16 | 15 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐷 ∈ 𝑃) |
17 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐴 ∈ (𝐶𝐿𝐷)) |
18 | 1, 3, 2, 13, 14, 16, 17 | tglngne 25869 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) |
19 | 18 | adantlr 706 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) |
20 | 19 | neneqd 3004 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → ¬ 𝐶 = 𝐷) |
21 | 12, 20 | pm2.65da 851 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → ¬ 𝐴 ∈ (𝐶𝐿𝐷)) |
22 | | nelne1 3095 |
. . 3
⊢ ((𝐴 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 ∈ (𝐶𝐿𝐷)) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |
23 | 11, 21, 22 | syl2anc 579 |
. 2
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |
24 | 4 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐺 ∈ TarskiG) |
25 | 6 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐵 ∈ 𝑃) |
26 | 7 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ 𝑃) |
27 | 5 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ∈ 𝑃) |
28 | | pm2.46 911 |
. . . . . . . . 9
⊢ (¬
(𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶) → ¬ 𝐵 = 𝐶) |
29 | 8, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 = 𝐶) |
30 | 29 | neqned 3006 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
31 | 30 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐵 ≠ 𝐶) |
32 | 15 | ad2antrr 717 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐷 ∈ 𝑃) |
33 | | simplr 785 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) |
34 | 1, 2, 3, 24, 26, 32, 33 | tglinerflx1 25952 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ (𝐶𝐿𝐷)) |
35 | | simpr 479 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) |
36 | 34, 35 | eleqtrrd 2909 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ (𝐴𝐿𝐵)) |
37 | 1, 3, 2, 24, 27, 25, 36 | tglngne 25869 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ≠ 𝐵) |
38 | 1, 2, 3, 24, 25, 26, 27, 31, 36, 37 | lnrot1 25942 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ∈ (𝐵𝐿𝐶)) |
39 | 38 | orcd 904 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
40 | 8 | ad2antrr 717 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
41 | 39, 40 | pm2.65da 851 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐷) → ¬ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) |
42 | 41 | neqned 3006 |
. 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐷) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |
43 | 23, 42 | pm2.61dane 3086 |
1
⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |