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 28633 | . . . 4
⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| 10 | 1, 2, 3, 4, 5, 6, 9 | tglinerflx1 28641 | . . 3
⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵)) | 
| 11 |  | simplr 769 | . . . 4
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 = 𝐷) | 
| 12 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐺 ∈ TarskiG) | 
| 13 | 7 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ∈ 𝑃) | 
| 14 |  | tglineinteq.d | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐷 ∈ 𝑃) | 
| 16 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐴 ∈ (𝐶𝐿𝐷)) | 
| 17 | 1, 3, 2, 12, 13, 15, 16 | tglngne 28558 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) | 
| 18 | 17 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) | 
| 19 | 18 | neneqd 2945 | . . . 4
⊢ (((𝜑 ∧ 𝐶 = 𝐷) ∧ 𝐴 ∈ (𝐶𝐿𝐷)) → ¬ 𝐶 = 𝐷) | 
| 20 | 11, 19 | pm2.65da 817 | . . 3
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → ¬ 𝐴 ∈ (𝐶𝐿𝐷)) | 
| 21 |  | nelne1 3039 | . . 3
⊢ ((𝐴 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 ∈ (𝐶𝐿𝐷)) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) | 
| 22 | 10, 20, 21 | syl2an2r 685 | . 2
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) | 
| 23 | 4 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐺 ∈ TarskiG) | 
| 24 | 6 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐵 ∈ 𝑃) | 
| 25 | 7 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ 𝑃) | 
| 26 | 5 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ∈ 𝑃) | 
| 27 |  | pm2.46 883 | . . . . . . . . 9
⊢ (¬
(𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶) → ¬ 𝐵 = 𝐶) | 
| 28 | 8, 27 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 = 𝐶) | 
| 29 | 28 | neqned 2947 | . . . . . . 7
⊢ (𝜑 → 𝐵 ≠ 𝐶) | 
| 30 | 29 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐵 ≠ 𝐶) | 
| 31 | 14 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐷 ∈ 𝑃) | 
| 32 |  | simplr 769 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ≠ 𝐷) | 
| 33 | 1, 2, 3, 23, 25, 31, 32 | tglinerflx1 28641 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ (𝐶𝐿𝐷)) | 
| 34 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) | 
| 35 | 33, 34 | eleqtrrd 2844 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐶 ∈ (𝐴𝐿𝐵)) | 
| 36 | 1, 3, 2, 23, 26, 24, 35 | tglngne 28558 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ≠ 𝐵) | 
| 37 | 1, 2, 3, 23, 24, 25, 26, 30, 35, 36 | lnrot1 28631 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → 𝐴 ∈ (𝐵𝐿𝐶)) | 
| 38 | 37 | orcd 874 | . . . 4
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 39 | 8 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 40 | 38, 39 | pm2.65da 817 | . . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐷) → ¬ (𝐴𝐿𝐵) = (𝐶𝐿𝐷)) | 
| 41 | 40 | neqned 2947 | . 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐷) → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) | 
| 42 | 22, 41 | pm2.61dane 3029 | 1
⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) |