Proof of Theorem opphllem1
Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | hpg.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
3 | | hpg.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
4 | | hpg.o |
. . . . 5
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
5 | | opphl.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
6 | | opphl.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
7 | | opphl.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
8 | | opphllem1.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
9 | | opphllem1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
10 | | opphllem1.o |
. . . . 5
⊢ (𝜑 → 𝐴𝑂𝐶) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | oppne1 26832 |
. . . 4
⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) |
12 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
13 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝐷) |
14 | 12, 13 | eqeltrd 2838 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐷) |
15 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
16 | | opphllem1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
17 | 16 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
18 | | opphllem1.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ 𝐷) |
19 | 1, 5, 3, 7, 6, 18 | tglnpt 26640 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ 𝑃) |
20 | 19 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ∈ 𝑃) |
21 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
22 | | opphllem1.y |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ≠ 𝑅) |
23 | 22 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ≠ 𝑅) |
24 | 23 | necomd 2996 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ≠ 𝐵) |
25 | | opphllem1.z |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐴)) |
26 | 25 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ (𝑅𝐼𝐴)) |
27 | 1, 3, 5, 15, 20, 17, 21, 24, 26 | btwnlng3 26712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝑅𝐿𝐵)) |
28 | 1, 3, 5, 15, 17, 20, 21, 23, 27 | lncom 26713 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝐵𝐿𝑅)) |
29 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐷 ∈ ran 𝐿) |
30 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝐷) |
31 | 18 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ∈ 𝐷) |
32 | 1, 3, 5, 15, 17, 20, 23, 23, 29, 30, 31 | tglinethru 26727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐷 = (𝐵𝐿𝑅)) |
33 | 28, 32 | eleqtrrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝐷) |
34 | 14, 33 | pm2.61dane 3029 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → 𝐴 ∈ 𝐷) |
35 | 11, 34 | mtand 816 |
. . 3
⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) |
36 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | oppne2 26833 |
. . 3
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐷) |
37 | | opphllem1.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ 𝐷) |
38 | 1, 5, 3, 7, 6, 37 | tglnpt 26640 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ 𝑃) |
39 | | eqid 2737 |
. . . . . . 7
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
40 | | opphllem1.s |
. . . . . . 7
⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) |
41 | 1, 2, 3, 5, 39, 7,
38, 40, 8 | mirbtwn 26749 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((𝑆‘𝐴)𝐼𝐴)) |
42 | | opphllem1.n |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) |
43 | 42 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘𝐶) = 𝐴) |
44 | 1, 2, 3, 5, 39, 7,
38, 40, 9, 43 | mircom 26754 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐴) = 𝐶) |
45 | 44 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘𝐴)𝐼𝐴) = (𝐶𝐼𝐴)) |
46 | 41, 45 | eleqtrd 2840 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝐶𝐼𝐴)) |
47 | 1, 2, 3, 7, 19, 9,
8, 16, 38, 25, 46 | axtgpasch 26558 |
. . . 4
⊢ (𝜑 → ∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) |
48 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝐺 ∈ TarskiG) |
49 | 19 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑅 ∈ 𝑃) |
50 | | simplrl 777 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ 𝑃) |
51 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) |
52 | 51 | simprd 499 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ (𝑀𝐼𝑅)) |
53 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑀 = 𝑅) |
54 | 53 | oveq1d 7228 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → (𝑀𝐼𝑅) = (𝑅𝐼𝑅)) |
55 | 52, 54 | eleqtrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ (𝑅𝐼𝑅)) |
56 | 1, 2, 3, 48, 49, 50, 55 | axtgbtwnid 26557 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑅 = 𝑡) |
57 | 18 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑅 ∈ 𝐷) |
58 | 56, 57 | eqeltrrd 2839 |
. . . . 5
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ 𝐷) |
59 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝐺 ∈ TarskiG) |
60 | 38 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑀 ∈ 𝑃) |
61 | 19 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑅 ∈ 𝑃) |
62 | | simplrl 777 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ 𝑃) |
63 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑀 ≠ 𝑅) |
64 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) |
65 | 64 | simprd 499 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ (𝑀𝐼𝑅)) |
66 | 1, 3, 5, 59, 60, 61, 62, 63, 65 | btwnlng1 26710 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ (𝑀𝐿𝑅)) |
67 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝐺 ∈ TarskiG) |
68 | 38 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑀 ∈ 𝑃) |
69 | 19 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑅 ∈ 𝑃) |
70 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑀 ≠ 𝑅) |
71 | 6 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝐷 ∈ ran 𝐿) |
72 | 37 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑀 ∈ 𝐷) |
73 | 18 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑅 ∈ 𝐷) |
74 | 1, 3, 5, 67, 68, 69, 70, 70, 71, 72, 73 | tglinethru 26727 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝐷 = (𝑀𝐿𝑅)) |
75 | 74 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝐷 = (𝑀𝐿𝑅)) |
76 | 66, 75 | eleqtrrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ 𝐷) |
77 | 58, 76 | pm2.61dane 3029 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) → 𝑡 ∈ 𝐷) |
78 | | simprrl 781 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) → 𝑡 ∈ (𝐵𝐼𝐶)) |
79 | 47, 77, 78 | reximssdv 3195 |
. . 3
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶)) |
80 | 35, 36, 79 | jca31 518 |
. 2
⊢ (𝜑 → ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶))) |
81 | 1, 2, 3, 4, 16, 9 | islnopp 26830 |
. 2
⊢ (𝜑 → (𝐵𝑂𝐶 ↔ ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶)))) |
82 | 80, 81 | mpbird 260 |
1
⊢ (𝜑 → 𝐵𝑂𝐶) |