Metamath Proof Explorer


Theorem opphllem2

Description: Lemma for opphl . Lemma 9.3 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 21-Dec-2019)

Ref Expression
Hypotheses hpg.p 𝑃 = ( Base ‘ 𝐺 )
hpg.d = ( dist ‘ 𝐺 )
hpg.i 𝐼 = ( Itv ‘ 𝐺 )
hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
opphl.l 𝐿 = ( LineG ‘ 𝐺 )
opphl.d ( 𝜑𝐷 ∈ ran 𝐿 )
opphl.g ( 𝜑𝐺 ∈ TarskiG )
opphllem1.s 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
opphllem1.a ( 𝜑𝐴𝑃 )
opphllem1.b ( 𝜑𝐵𝑃 )
opphllem1.c ( 𝜑𝐶𝑃 )
opphllem1.r ( 𝜑𝑅𝐷 )
opphllem1.o ( 𝜑𝐴 𝑂 𝐶 )
opphllem1.m ( 𝜑𝑀𝐷 )
opphllem1.n ( 𝜑𝐴 = ( 𝑆𝐶 ) )
opphllem1.x ( 𝜑𝐴𝑅 )
opphllem1.y ( 𝜑𝐵𝑅 )
opphllem2.z ( 𝜑 → ( 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) )
Assertion opphllem2 ( 𝜑𝐵 𝑂 𝐶 )

Proof

Step Hyp Ref Expression
1 hpg.p 𝑃 = ( Base ‘ 𝐺 )
2 hpg.d = ( dist ‘ 𝐺 )
3 hpg.i 𝐼 = ( Itv ‘ 𝐺 )
4 hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 opphl.l 𝐿 = ( LineG ‘ 𝐺 )
6 opphl.d ( 𝜑𝐷 ∈ ran 𝐿 )
7 opphl.g ( 𝜑𝐺 ∈ TarskiG )
8 opphllem1.s 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
9 opphllem1.a ( 𝜑𝐴𝑃 )
10 opphllem1.b ( 𝜑𝐵𝑃 )
11 opphllem1.c ( 𝜑𝐶𝑃 )
12 opphllem1.r ( 𝜑𝑅𝐷 )
13 opphllem1.o ( 𝜑𝐴 𝑂 𝐶 )
14 opphllem1.m ( 𝜑𝑀𝐷 )
15 opphllem1.n ( 𝜑𝐴 = ( 𝑆𝐶 ) )
16 opphllem1.x ( 𝜑𝐴𝑅 )
17 opphllem1.y ( 𝜑𝐵𝑅 )
18 opphllem2.z ( 𝜑 → ( 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) )
19 6 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐷 ∈ ran 𝐿 )
20 7 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
21 11 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐶𝑃 )
22 10 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐵𝑃 )
23 eqid ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
24 1 5 3 7 6 14 tglnpt ( 𝜑𝑀𝑃 )
25 24 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝑀𝑃 )
26 1 2 3 5 23 20 25 8 22 mircl ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝐵 ) ∈ 𝑃 )
27 14 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝑀𝐷 )
28 12 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝑅𝐷 )
29 1 2 3 5 23 20 8 19 27 28 mirln ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝑅 ) ∈ 𝐷 )
30 simpr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
31 simplr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴 = 𝐵 ) → 𝐵𝐷 )
32 30 31 eqeltrd ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴 = 𝐵 ) → 𝐴𝐷 )
33 7 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐺 ∈ TarskiG )
34 10 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐵𝑃 )
35 1 5 3 7 6 12 tglnpt ( 𝜑𝑅𝑃 )
36 35 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝑅𝑃 )
37 9 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐴𝑃 )
38 17 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐵𝑅 )
39 38 necomd ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝑅𝐵 )
40 simpllr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) )
41 1 3 5 33 36 34 37 39 40 btwnlng1 ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐴 ∈ ( 𝑅 𝐿 𝐵 ) )
42 1 3 5 33 34 36 37 38 41 lncom ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐴 ∈ ( 𝐵 𝐿 𝑅 ) )
43 6 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐷 ∈ ran 𝐿 )
44 simplr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐵𝐷 )
45 12 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝑅𝐷 )
46 1 3 5 33 34 36 38 38 43 44 45 tglinethru ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐷 = ( 𝐵 𝐿 𝑅 ) )
47 42 46 eleqtrrd ( ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) ∧ 𝐴𝐵 ) → 𝐴𝐷 )
48 32 47 pm2.61dane ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) → 𝐴𝐷 )
49 1 2 3 4 5 6 7 9 11 13 oppne1 ( 𝜑 → ¬ 𝐴𝐷 )
50 49 ad2antrr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ 𝐵𝐷 ) → ¬ 𝐴𝐷 )
51 48 50 pm2.65da ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ¬ 𝐵𝐷 )
52 20 adantr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
53 25 adantr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → 𝑀𝑃 )
54 22 adantr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → 𝐵𝑃 )
55 1 2 3 5 23 52 53 8 54 mirmir ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → ( 𝑆 ‘ ( 𝑆𝐵 ) ) = 𝐵 )
56 19 adantr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
57 27 adantr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → 𝑀𝐷 )
58 simpr ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → ( 𝑆𝐵 ) ∈ 𝐷 )
59 1 2 3 5 23 52 8 56 57 58 mirln ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → ( 𝑆 ‘ ( 𝑆𝐵 ) ) ∈ 𝐷 )
60 55 59 eqeltrrd ( ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) ∧ ( 𝑆𝐵 ) ∈ 𝐷 ) → 𝐵𝐷 )
61 51 60 mtand ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ¬ ( 𝑆𝐵 ) ∈ 𝐷 )
62 1 2 3 5 23 20 25 8 22 mirbtwn ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝑀 ∈ ( ( 𝑆𝐵 ) 𝐼 𝐵 ) )
63 1 2 3 4 26 22 27 61 51 62 islnoppd ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝐵 ) 𝑂 𝐵 )
64 eqidd ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝐵 ) = ( 𝑆𝐵 ) )
65 nelne2 ( ( ( 𝑆𝑅 ) ∈ 𝐷 ∧ ¬ ( 𝑆𝐵 ) ∈ 𝐷 ) → ( 𝑆𝑅 ) ≠ ( 𝑆𝐵 ) )
66 29 61 65 syl2anc ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝑅 ) ≠ ( 𝑆𝐵 ) )
67 66 necomd ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝐵 ) ≠ ( 𝑆𝑅 ) )
68 1 2 3 4 5 6 7 9 11 13 oppne2 ( 𝜑 → ¬ 𝐶𝐷 )
69 68 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ¬ 𝐶𝐷 )
70 nelne2 ( ( ( 𝑆𝑅 ) ∈ 𝐷 ∧ ¬ 𝐶𝐷 ) → ( 𝑆𝑅 ) ≠ 𝐶 )
71 29 69 70 syl2anc ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝑅 ) ≠ 𝐶 )
72 71 necomd ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐶 ≠ ( 𝑆𝑅 ) )
73 15 eqcomd ( 𝜑 → ( 𝑆𝐶 ) = 𝐴 )
74 1 2 3 5 23 7 24 8 11 73 mircom ( 𝜑 → ( 𝑆𝐴 ) = 𝐶 )
75 74 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝐴 ) = 𝐶 )
76 35 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝑅𝑃 )
77 9 adantr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐴𝑃 )
78 simpr ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) )
79 1 2 3 5 23 20 25 8 76 77 22 78 mirbtwni ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → ( 𝑆𝐴 ) ∈ ( ( 𝑆𝑅 ) 𝐼 ( 𝑆𝐵 ) ) )
80 75 79 eqeltrrd ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐶 ∈ ( ( 𝑆𝑅 ) 𝐼 ( 𝑆𝐵 ) ) )
81 1 2 3 4 5 19 20 8 26 21 22 29 63 27 64 67 72 80 opphllem1 ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐶 𝑂 𝐵 )
82 1 2 3 4 5 19 20 21 22 81 oppcom ( ( 𝜑𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ) → 𝐵 𝑂 𝐶 )
83 6 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐷 ∈ ran 𝐿 )
84 7 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
85 9 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐴𝑃 )
86 10 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐵𝑃 )
87 11 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐶𝑃 )
88 12 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝑅𝐷 )
89 13 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐴 𝑂 𝐶 )
90 14 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝑀𝐷 )
91 15 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐴 = ( 𝑆𝐶 ) )
92 16 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐴𝑅 )
93 17 adantr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐵𝑅 )
94 simpr ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) )
95 1 2 3 4 5 83 84 8 85 86 87 88 89 90 91 92 93 94 opphllem1 ( ( 𝜑𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) → 𝐵 𝑂 𝐶 )
96 82 95 18 mpjaodan ( 𝜑𝐵 𝑂 𝐶 )