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 ⊢ ( 𝜑 → 𝐵 𝑂 𝐶 )