Metamath Proof Explorer

Theorem opphllem1

Description: Lemma for opphl . (Contributed by Thierry Arnoux, 20-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 ⊢ ( 𝜑 → 𝐵 ≠ 𝑅 )
opphllem1.z ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) )
Assertion opphllem1 ( 𝜑 → 𝐵 𝑂 𝐶 )

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 opphllem1.z ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) )
19 1 2 3 4 5 6 7 9 11 13 oppne1 ⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
20 simpr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
21 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝐷 )
22 20 21 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝐷 )
23 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
24 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
25 1 5 3 7 6 12 tglnpt ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑅 ∈ 𝑃 )
27 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
28 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 𝑅 )
29 28 necomd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑅 ≠ 𝐵 )
30 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) )
31 1 3 5 23 26 24 27 29 30 btwnlng3 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( 𝑅 𝐿 𝐵 ) )
32 1 3 5 23 24 26 27 28 31 lncom ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐿 𝑅 ) )
33 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐷 ∈ ran 𝐿 )
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝐷 )
35 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑅 ∈ 𝐷 )
36 1 3 5 23 24 26 28 28 33 34 35 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐷 = ( 𝐵 𝐿 𝑅 ) )
37 32 36 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝐷 )
38 22 37 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
39 19 38 mtand ⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐷 )
40 1 2 3 4 5 6 7 9 11 13 oppne2 ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐷 )
41 1 5 3 7 6 14 tglnpt ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
42 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
43 1 2 3 5 42 7 41 8 9 mirbtwn ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑆 ‘ 𝐴 ) 𝐼 𝐴 ) )
44 15 eqcomd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = 𝐴 )
45 1 2 3 5 42 7 41 8 11 44 mircom ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = 𝐶 )
46 45 oveq1d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) 𝐼 𝐴 ) = ( 𝐶 𝐼 𝐴 ) )
47 43 46 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐶 𝐼 𝐴 ) )
48 1 2 3 7 25 11 9 10 41 18 47 axtgpasch ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) )
49 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝐺 ∈ TarskiG )
50 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑅 ∈ 𝑃 )
51 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑡 ∈ 𝑃 )
52 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) )
53 52 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) )
54 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑀 = 𝑅 )
55 54 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → ( 𝑀 𝐼 𝑅 ) = ( 𝑅 𝐼 𝑅 ) )
56 53 55 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑡 ∈ ( 𝑅 𝐼 𝑅 ) )
57 1 2 3 49 50 51 56 axtgbtwnid ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑅 = 𝑡 )
58 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑅 ∈ 𝐷 )
59 57 58 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 = 𝑅 ) → 𝑡 ∈ 𝐷 )
60 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝐺 ∈ TarskiG )
61 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑀 ∈ 𝑃 )
62 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑅 ∈ 𝑃 )
63 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑡 ∈ 𝑃 )
64 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑀 ≠ 𝑅 )
65 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) )
66 65 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) )
67 1 3 5 60 61 62 63 64 66 btwnlng1 ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑡 ∈ ( 𝑀 𝐿 𝑅 ) )
68 7 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝐺 ∈ TarskiG )
69 41 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝑀 ∈ 𝑃 )
70 25 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝑅 ∈ 𝑃 )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝑀 ≠ 𝑅 )
72 6 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝐷 ∈ ran 𝐿 )
73 14 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝑀 ∈ 𝐷 )
74 12 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝑅 ∈ 𝐷 )
75 1 3 5 68 69 70 71 71 72 73 74 tglinethru ⊢ ( ( 𝜑 ∧ 𝑀 ≠ 𝑅 ) → 𝐷 = ( 𝑀 𝐿 𝑅 ) )
76 75 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝐷 = ( 𝑀 𝐿 𝑅 ) )
77 67 76 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) ∧ 𝑀 ≠ 𝑅 ) → 𝑡 ∈ 𝐷 )
78 59 77 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) → 𝑡 ∈ 𝐷 )
79 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑃 ∧ ( 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝑀 𝐼 𝑅 ) ) ) ) → 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) )
80 48 78 79 reximssdv ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) )
81 39 40 80 jca31 ⊢ ( 𝜑 → ( ( ¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ) )
82 1 2 3 4 10 11 islnopp ⊢ ( 𝜑 → ( 𝐵 𝑂 𝐶 ↔ ( ( ¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) ) ) )
83 81 82 mpbird ⊢ ( 𝜑 → 𝐵 𝑂 𝐶 )