Proof of Theorem opphllem2
Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | hpg.d |
. . 3
⊢ − =
(dist‘𝐺) |
3 | | hpg.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
4 | | hpg.o |
. . 3
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
5 | | opphl.l |
. . 3
⊢ 𝐿 = (LineG‘𝐺) |
6 | | opphl.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
7 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐷 ∈ ran 𝐿) |
8 | | opphl.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐺 ∈ TarskiG) |
10 | | opphllem1.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐶 ∈ 𝑃) |
12 | | opphllem1.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐵 ∈ 𝑃) |
14 | | opphllem1.s |
. . . 4
⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) |
15 | | eqid 2610 |
. . . . 5
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
16 | | opphllem1.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝐷) |
17 | 1, 5, 3, 8, 6, 16 | tglnpt 25244 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ 𝑃) |
18 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝑀 ∈ 𝑃) |
19 | 1, 2, 3, 5, 15, 9,
18, 14, 13 | mircl 25356 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝐵) ∈ 𝑃) |
20 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝑀 ∈ 𝐷) |
21 | | opphllem1.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ 𝐷) |
22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝑅 ∈ 𝐷) |
23 | 1, 2, 3, 5, 15, 9,
14, 7, 20, 22 | mirln 25371 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝑅) ∈ 𝐷) |
24 | 9 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → 𝐺 ∈ TarskiG) |
25 | 18 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → 𝑀 ∈ 𝑃) |
26 | 13 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → 𝐵 ∈ 𝑃) |
27 | 1, 2, 3, 5, 15, 24, 25, 14, 26 | mirmir 25357 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → (𝑆‘(𝑆‘𝐵)) = 𝐵) |
28 | 7 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → 𝐷 ∈ ran 𝐿) |
29 | 20 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → 𝑀 ∈ 𝐷) |
30 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → (𝑆‘𝐵) ∈ 𝐷) |
31 | 1, 2, 3, 5, 15, 24, 14, 28, 29, 30 | mirln 25371 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → (𝑆‘(𝑆‘𝐵)) ∈ 𝐷) |
32 | 27, 31 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → 𝐵 ∈ 𝐷) |
33 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
34 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝐷) |
35 | 33, 34 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐷) |
36 | 8 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
37 | 12 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
38 | 1, 5, 3, 8, 6, 21 | tglnpt 25244 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ 𝑃) |
39 | 38 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ∈ 𝑃) |
40 | | opphllem1.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
41 | 40 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
42 | | opphllem1.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ≠ 𝑅) |
43 | 42 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ≠ 𝑅) |
44 | 43 | necomd 2837 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ≠ 𝐵) |
45 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝑅𝐼𝐵)) |
46 | 1, 3, 5, 36, 39, 37, 41, 44, 45 | btwnlng1 25314 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝑅𝐿𝐵)) |
47 | 1, 3, 5, 36, 37, 39, 41, 43, 46 | lncom 25317 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝐵𝐿𝑅)) |
48 | 6 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐷 ∈ ran 𝐿) |
49 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝐷) |
50 | 21 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝑅 ∈ 𝐷) |
51 | 1, 3, 5, 36, 37, 39, 43, 43, 48, 49, 50 | tglinethru 25331 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐷 = (𝐵𝐿𝑅)) |
52 | 47, 51 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝐷) |
53 | 35, 52 | pm2.61dane 2869 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) → 𝐴 ∈ 𝐷) |
54 | | opphllem1.o |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴𝑂𝐶) |
55 | 1, 2, 3, 4, 5, 6, 8, 40, 10, 54 | oppne1 25433 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) |
56 | 55 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ 𝐵 ∈ 𝐷) → ¬ 𝐴 ∈ 𝐷) |
57 | 53, 56 | pm2.65da 598 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ¬ 𝐵 ∈ 𝐷) |
58 | 57 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) ∧ (𝑆‘𝐵) ∈ 𝐷) → ¬ 𝐵 ∈ 𝐷) |
59 | 32, 58 | pm2.65da 598 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ¬ (𝑆‘𝐵) ∈ 𝐷) |
60 | 57 | idi 2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ¬ 𝐵 ∈ 𝐷) |
61 | 1, 2, 3, 5, 15, 9,
18, 14, 13 | mirbtwn 25353 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝑀 ∈ ((𝑆‘𝐵)𝐼𝐵)) |
62 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑡 = 𝑀 → (𝑡 ∈ ((𝑆‘𝐵)𝐼𝐵) ↔ 𝑀 ∈ ((𝑆‘𝐵)𝐼𝐵))) |
63 | 62 | rspcev 3282 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝐷 ∧ 𝑀 ∈ ((𝑆‘𝐵)𝐼𝐵)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ ((𝑆‘𝐵)𝐼𝐵)) |
64 | 20, 61, 63 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ ((𝑆‘𝐵)𝐼𝐵)) |
65 | 59, 60, 64 | jca31 555 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ((¬ (𝑆‘𝐵) ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ ((𝑆‘𝐵)𝐼𝐵))) |
66 | 1, 2, 3, 4, 19, 13 | islnopp 25431 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ((𝑆‘𝐵)𝑂𝐵 ↔ ((¬ (𝑆‘𝐵) ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ ((𝑆‘𝐵)𝐼𝐵)))) |
67 | 65, 66 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝐵)𝑂𝐵) |
68 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝐵) = (𝑆‘𝐵)) |
69 | | nelne2 2879 |
. . . . . 6
⊢ (((𝑆‘𝑅) ∈ 𝐷 ∧ ¬ (𝑆‘𝐵) ∈ 𝐷) → (𝑆‘𝑅) ≠ (𝑆‘𝐵)) |
70 | 23, 59, 69 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝑅) ≠ (𝑆‘𝐵)) |
71 | 70 | necomd 2837 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝐵) ≠ (𝑆‘𝑅)) |
72 | 1, 2, 3, 4, 5, 6, 8, 40, 10, 54 | oppne2 25434 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐷) |
73 | 72 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → ¬ 𝐶 ∈ 𝐷) |
74 | | nelne2 2879 |
. . . . . 6
⊢ (((𝑆‘𝑅) ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) → (𝑆‘𝑅) ≠ 𝐶) |
75 | 23, 73, 74 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝑅) ≠ 𝐶) |
76 | 75 | necomd 2837 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐶 ≠ (𝑆‘𝑅)) |
77 | | opphllem1.n |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) |
78 | 77 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐶) = 𝐴) |
79 | 1, 2, 3, 5, 15, 8,
17, 14, 10, 78 | mircom 25358 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐴) = 𝐶) |
80 | 79 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝐴) = 𝐶) |
81 | 38 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝑅 ∈ 𝑃) |
82 | 40 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐴 ∈ 𝑃) |
83 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐴 ∈ (𝑅𝐼𝐵)) |
84 | 1, 2, 3, 5, 15, 9,
18, 14, 81, 82, 13, 83 | mirbtwni 25366 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → (𝑆‘𝐴) ∈ ((𝑆‘𝑅)𝐼(𝑆‘𝐵))) |
85 | 80, 84 | eqeltrrd 2689 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐶 ∈ ((𝑆‘𝑅)𝐼(𝑆‘𝐵))) |
86 | 1, 2, 3, 4, 5, 7, 9, 14, 19, 11, 13, 23, 67, 20, 68, 71, 76, 85 | opphllem1 25439 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐶𝑂𝐵) |
87 | 1, 2, 3, 4, 5, 7, 9, 11, 13, 86 | oppcom 25436 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (𝑅𝐼𝐵)) → 𝐵𝑂𝐶) |
88 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐷 ∈ ran 𝐿) |
89 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐺 ∈ TarskiG) |
90 | 40 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐴 ∈ 𝑃) |
91 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐵 ∈ 𝑃) |
92 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐶 ∈ 𝑃) |
93 | 21 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝑅 ∈ 𝐷) |
94 | 54 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐴𝑂𝐶) |
95 | 16 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝑀 ∈ 𝐷) |
96 | 77 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐴 = (𝑆‘𝐶)) |
97 | | opphllem1.x |
. . . 4
⊢ (𝜑 → 𝐴 ≠ 𝑅) |
98 | 97 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐴 ≠ 𝑅) |
99 | 42 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐵 ≠ 𝑅) |
100 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐵 ∈ (𝑅𝐼𝐴)) |
101 | 1, 2, 3, 4, 5, 88,
89, 14, 90, 91, 92, 93, 94, 95, 96, 98, 99, 100 | opphllem1 25439 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (𝑅𝐼𝐴)) → 𝐵𝑂𝐶) |
102 | | opphllem2.z |
. 2
⊢ (𝜑 → (𝐴 ∈ (𝑅𝐼𝐵) ∨ 𝐵 ∈ (𝑅𝐼𝐴))) |
103 | 87, 101, 102 | mpjaodan 823 |
1
⊢ (𝜑 → 𝐵𝑂𝐶) |