Proof of Theorem oppne3
Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
2 | | eqid 2778 |
. . . . . 6
⊢
(dist‘𝐺) =
(dist‘𝐺) |
3 | | hpg.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
4 | | opphl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | ad3antrrr 720 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG) |
6 | | oppcom.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
7 | 6 | ad3antrrr 720 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃) |
8 | | opphl.l |
. . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) |
9 | | opphl.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
10 | 9 | ad3antrrr 720 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐷 ∈ ran 𝐿) |
11 | | simplr 759 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ 𝐷) |
12 | 1, 8, 3, 5, 10, 11 | tglnpt 25917 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ 𝑃) |
13 | | simpr 479 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ (𝐴𝐼𝐵)) |
14 | | simpllr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐴 = 𝐵) |
15 | 14 | oveq2d 6940 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → (𝐴𝐼𝐴) = (𝐴𝐼𝐵)) |
16 | 13, 15 | eleqtrrd 2862 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ (𝐴𝐼𝐴)) |
17 | 1, 2, 3, 5, 7, 12,
16 | axtgbtwnid 25834 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐴 = 𝑡) |
18 | 17, 11 | eqeltrd 2859 |
. . . 4
⊢ ((((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝐷) |
19 | | oppcom.o |
. . . . . . 7
⊢ (𝜑 → 𝐴𝑂𝐵) |
20 | | hpg.d |
. . . . . . . 8
⊢ − =
(dist‘𝐺) |
21 | | hpg.o |
. . . . . . . 8
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
22 | | oppcom.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
23 | 1, 20, 3, 21, 6, 22 | islnopp 26104 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)))) |
24 | 19, 23 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))) |
25 | 24 | simprd 491 |
. . . . 5
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)) |
26 | 25 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)) |
27 | 18, 26 | r19.29a 3264 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐷) |
28 | 1, 20, 3, 21, 8, 9,
4, 6, 22, 19 | oppne1 26106 |
. . . 4
⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) |
29 | 28 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ¬ 𝐴 ∈ 𝐷) |
30 | 27, 29 | pm2.65da 807 |
. 2
⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
31 | 30 | neqned 2976 |
1
⊢ (𝜑 → 𝐴 ≠ 𝐵) |