Proof of Theorem tglineneq
Step | Hyp | Ref
| Expression |
1 | | tglineintmo.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | tglineintmo.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
3 | | tglineintmo.l |
. . . 4
⊢ 𝐿 = (LineG‘𝐺) |
4 | | tglineintmo.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | | tglineinteq.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
6 | | tglineinteq.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
7 | | tglineinteq.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
8 | | tglineinteq.e |
. . . . 5
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | ncolne1 26986 |
. . . 4
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
10 | 1, 2, 3, 4, 5, 6, 9 | tglinerflx1 26994 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵)) |
11 | | simplr 766 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 = 𝐷) |
12 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐺 ∈ TarskiG) |
13 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ∈ 𝑃) |
14 | | tglineinteq.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐷 ∈ 𝑃) |
16 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐴 ∈ (𝐶𝐿𝐷)) |
17 | 1, 3, 2, 12, 13, 15, 16 | tglngne 26911 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) |
18 | 17 | adantlr 712 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) |
19 | 18 | neneqd 2948 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → ¬ 𝐶 = 𝐷) |
20 | 11, 19 | pm2.65da 814 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → ¬ 𝐴 ∈ (𝐶𝐿𝐷)) |
21 | | nelne1 3041 |
. . 3
⊢ ((𝐴 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 ∈ (𝐶𝐿𝐷)) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |
22 | 10, 20, 21 | syl2an2r 682 |
. 2
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |
23 | 4 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐺 ∈ TarskiG) |
24 | 6 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐵 ∈ 𝑃) |
25 | 7 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ 𝑃) |
26 | 5 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ∈ 𝑃) |
27 | | pm2.46 880 |
. . . . . . . . 9
⊢ (¬
(𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶) → ¬ 𝐵 = 𝐶) |
28 | 8, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 = 𝐶) |
29 | 28 | neqned 2950 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
30 | 29 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐵 ≠ 𝐶) |
31 | 14 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐷 ∈ 𝑃) |
32 | | simplr 766 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) |
33 | 1, 2, 3, 23, 25, 31, 32 | tglinerflx1 26994 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ (𝐶𝐿𝐷)) |
34 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) |
35 | 33, 34 | eleqtrrd 2842 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ (𝐴𝐿𝐵)) |
36 | 1, 3, 2, 23, 26, 24, 35 | tglngne 26911 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ≠ 𝐵) |
37 | 1, 2, 3, 23, 24, 25, 26, 30, 35, 36 | lnrot1 26984 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ∈ (𝐵𝐿𝐶)) |
38 | 37 | orcd 870 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
39 | 8 | ad2antrr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
40 | 38, 39 | pm2.65da 814 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐷) → ¬ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) |
41 | 40 | neqned 2950 |
. 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐷) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |
42 | 22, 41 | pm2.61dane 3032 |
1
⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |