Proof of Theorem opphllem1
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
2 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝐷) |
3 | 1, 2 | eqeltrd 2688 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐷) |
4 | | hpg.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
5 | | hpg.i |
. . . . . . 7
⊢ 𝐼 = (Itv‘𝐺) |
6 | | opphl.l |
. . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) |
7 | | opphl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
8 | 7 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
9 | | opphllem1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
10 | 9 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
11 | | opphl.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
12 | | opphllem1.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ 𝐷) |
13 | 4, 6, 5, 7, 11, 12 | tglnpt 25244 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ 𝑃) |
14 | 13 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ∈ 𝑃) |
15 | | opphllem1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
16 | 15 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
17 | | opphllem1.y |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ≠ 𝑅) |
18 | 17 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ≠ 𝑅) |
19 | 18 | necomd 2837 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ≠ 𝐵) |
20 | | opphllem1.z |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐴)) |
21 | 20 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ (𝑅𝐼𝐴)) |
22 | 4, 5, 6, 8, 14, 10, 16, 19, 21 | btwnlng3 25316 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝑅𝐿𝐵)) |
23 | 4, 5, 6, 8, 10, 14, 16, 18, 22 | lncom 25317 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝐵𝐿𝑅)) |
24 | 11 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐷 ∈ ran 𝐿) |
25 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝐷) |
26 | 12 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ∈ 𝐷) |
27 | 4, 5, 6, 8, 10, 14, 18, 18, 24, 25, 26 | tglinethru 25331 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐷 = (𝐵𝐿𝑅)) |
28 | 23, 27 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝐷) |
29 | 3, 28 | pm2.61dane 2869 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → 𝐴 ∈ 𝐷) |
30 | | hpg.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
31 | | hpg.o |
. . . . . 6
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
32 | | opphllem1.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
33 | | opphllem1.o |
. . . . . 6
⊢ (𝜑 → 𝐴𝑂𝐶) |
34 | 4, 30, 5, 31, 6, 11, 7, 15, 32, 33 | oppne1 25433 |
. . . . 5
⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) |
35 | 34 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → ¬ 𝐴 ∈ 𝐷) |
36 | 29, 35 | pm2.65da 598 |
. . 3
⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) |
37 | 4, 30, 5, 31, 6, 11, 7, 15, 32, 33 | oppne2 25434 |
. . 3
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐷) |
38 | | opphllem1.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ 𝐷) |
39 | 4, 6, 5, 7, 11, 38 | tglnpt 25244 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ 𝑃) |
40 | | eqid 2610 |
. . . . . . 7
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
41 | | opphllem1.s |
. . . . . . 7
⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) |
42 | 4, 30, 5, 6, 40, 7,
39, 41, 15 | mirbtwn 25353 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((𝑆‘𝐴)𝐼𝐴)) |
43 | | opphllem1.n |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) |
44 | 43 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘𝐶) = 𝐴) |
45 | 4, 30, 5, 6, 40, 7,
39, 41, 32, 44 | mircom 25358 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐴) = 𝐶) |
46 | 45 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘𝐴)𝐼𝐴) = (𝐶𝐼𝐴)) |
47 | 42, 46 | eleqtrd 2690 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝐶𝐼𝐴)) |
48 | 4, 30, 5, 7, 13, 32, 15, 9, 39, 20, 47 | axtgpasch 25166 |
. . . 4
⊢ (𝜑 → ∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) |
49 | 7 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝐺 ∈ TarskiG) |
50 | 13 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑅 ∈ 𝑃) |
51 | | simplrl 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ 𝑃) |
52 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) |
53 | 52 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ (𝑀𝐼𝑅)) |
54 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑀 = 𝑅) |
55 | 54 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → (𝑀𝐼𝑅) = (𝑅𝐼𝑅)) |
56 | 53, 55 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ (𝑅𝐼𝑅)) |
57 | 4, 30, 5, 49, 50, 51, 56 | axtgbtwnid 25165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑅 = 𝑡) |
58 | 12 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑅 ∈ 𝐷) |
59 | 57, 58 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 = 𝑅) → 𝑡 ∈ 𝐷) |
60 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝐺 ∈ TarskiG) |
61 | 60 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝐺 ∈ TarskiG) |
62 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑀 ∈ 𝑃) |
63 | 62 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑀 ∈ 𝑃) |
64 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑅 ∈ 𝑃) |
65 | 64 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑅 ∈ 𝑃) |
66 | | simplrl 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ 𝑃) |
67 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑀 ≠ 𝑅) |
68 | | simplrr 797 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) |
69 | 68 | simprd 478 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ (𝑀𝐼𝑅)) |
70 | 4, 5, 6, 61, 63, 65, 66, 67, 69 | btwnlng1 25314 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ (𝑀𝐿𝑅)) |
71 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑀 ≠ 𝑅) |
72 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝐷 ∈ ran 𝐿) |
73 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑀 ∈ 𝐷) |
74 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝑅 ∈ 𝐷) |
75 | 4, 5, 6, 60, 62, 64, 71, 71, 72, 73, 74 | tglinethru 25331 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ≠ 𝑅) → 𝐷 = (𝑀𝐿𝑅)) |
76 | 75 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝐷 = (𝑀𝐿𝑅)) |
77 | 70, 76 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) ∧ 𝑀 ≠ 𝑅) → 𝑡 ∈ 𝐷) |
78 | 59, 77 | pm2.61dane 2869 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) → 𝑡 ∈ 𝐷) |
79 | | simprrl 800 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) → 𝑡 ∈ (𝐵𝐼𝐶)) |
80 | 78, 79 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)))) → (𝑡 ∈ 𝐷 ∧ 𝑡 ∈ (𝐵𝐼𝐶))) |
81 | 80 | ex 449 |
. . . . 5
⊢ (𝜑 → ((𝑡 ∈ 𝑃 ∧ (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅))) → (𝑡 ∈ 𝐷 ∧ 𝑡 ∈ (𝐵𝐼𝐶)))) |
82 | 81 | reximdv2 2997 |
. . . 4
⊢ (𝜑 → (∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝐵𝐼𝐶) ∧ 𝑡 ∈ (𝑀𝐼𝑅)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶))) |
83 | 48, 82 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶)) |
84 | 36, 37, 83 | jca31 555 |
. 2
⊢ (𝜑 → ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶))) |
85 | 4, 30, 5, 31, 9, 32 | islnopp 25431 |
. 2
⊢ (𝜑 → (𝐵𝑂𝐶 ↔ ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐶)))) |
86 | 84, 85 | mpbird 246 |
1
⊢ (𝜑 → 𝐵𝑂𝐶) |