Metamath Proof Explorer


Theorem opphllem

Description: Lemma 8.24 of Schwabhauser p. 66. This is used later for mideulem and later for opphl . (Contributed by Thierry Arnoux, 21-Dec-2019)

Ref Expression
Hypotheses colperpex.p P = Base G
colperpex.d - ˙ = dist G
colperpex.i I = Itv G
colperpex.l L = Line 𝒢 G
colperpex.g φ G 𝒢 Tarski
mideu.s S = pInv 𝒢 G
mideu.1 φ A P
mideu.2 φ B P
mideulem.1 φ A B
mideulem.2 φ Q P
mideulem.3 φ O P
mideulem.4 φ T P
mideulem.5 φ A L B 𝒢 G Q L B
mideulem.6 φ A L B 𝒢 G A L O
mideulem.7 φ T A L B
mideulem.8 φ T Q I O
opphllem.1 φ R P
opphllem.2 φ R B I Q
opphllem.3 φ A - ˙ O = B - ˙ R
Assertion opphllem φ x P B = S x A O = S x R

Proof

Step Hyp Ref Expression
1 colperpex.p P = Base G
2 colperpex.d - ˙ = dist G
3 colperpex.i I = Itv G
4 colperpex.l L = Line 𝒢 G
5 colperpex.g φ G 𝒢 Tarski
6 mideu.s S = pInv 𝒢 G
7 mideu.1 φ A P
8 mideu.2 φ B P
9 mideulem.1 φ A B
10 mideulem.2 φ Q P
11 mideulem.3 φ O P
12 mideulem.4 φ T P
13 mideulem.5 φ A L B 𝒢 G Q L B
14 mideulem.6 φ A L B 𝒢 G A L O
15 mideulem.7 φ T A L B
16 mideulem.8 φ T Q I O
17 opphllem.1 φ R P
18 opphllem.2 φ R B I Q
19 opphllem.3 φ A - ˙ O = B - ˙ R
20 5 adantr φ x P x T I B x R I O G 𝒢 Tarski
21 eqid S x = S x
22 8 adantr φ x P x T I B x R I O B P
23 11 adantr φ x P x T I B x R I O O P
24 7 adantr φ x P x T I B x R I O A P
25 17 adantr φ x P x T I B x R I O R P
26 simprl φ x P x T I B x R I O x P
27 9 necomd φ B A
28 27 neneqd φ ¬ B = A
29 28 adantr φ O B L A ¬ B = A
30 4 5 14 perpln2 φ A L O ran L
31 1 3 4 5 7 11 30 tglnne φ A O
32 31 necomd φ O A
33 32 neneqd φ ¬ O = A
34 33 adantr φ O B L A ¬ O = A
35 29 34 jca φ O B L A ¬ B = A ¬ O = A
36 5 adantr φ O B L A G 𝒢 Tarski
37 8 adantr φ O B L A B P
38 7 adantr φ O B L A A P
39 11 adantr φ O B L A O P
40 1 3 4 5 8 7 27 tglinerflx2 φ A B L A
41 1 3 4 5 7 8 9 tglinecom φ A L B = B L A
42 41 14 eqbrtrrd φ B L A 𝒢 G A L O
43 1 2 3 4 5 8 7 40 11 42 perprag φ ⟨“ BAO ”⟩ 𝒢 G
44 43 adantr φ O B L A ⟨“ BAO ”⟩ 𝒢 G
45 simpr φ O B L A O B L A
46 45 orcd φ O B L A O B L A B = A
47 1 2 3 4 6 36 37 38 39 44 46 ragflat3 φ O B L A B = A O = A
48 oran B = A O = A ¬ ¬ B = A ¬ O = A
49 47 48 sylib φ O B L A ¬ ¬ B = A ¬ O = A
50 35 49 pm2.65da φ ¬ O B L A
51 50 adantr φ x P x T I B x R I O ¬ O B L A
52 41 adantr φ x P x T I B x R I O A L B = B L A
53 51 52 neleqtrrd φ x P x T I B x R I O ¬ O A L B
54 9 adantr φ x P x T I B x R I O A B
55 54 neneqd φ x P x T I B x R I O ¬ A = B
56 53 55 jca φ x P x T I B x R I O ¬ O A L B ¬ A = B
57 pm4.56 ¬ O A L B ¬ A = B ¬ O A L B A = B
58 56 57 sylib φ x P x T I B x R I O ¬ O A L B A = B
59 1 4 3 20 24 22 23 58 ncolrot2 φ x P x T I B x R I O ¬ B O L A O = A
60 simprrr φ x P x T I B x R I O x R I O
61 1 2 3 20 25 26 23 60 tgbtwncom φ x P x T I B x R I O x O I R
62 12 adantr φ x P x T I B x R I O T P
63 15 adantr φ x P x T I B x R I O T A L B
64 simprrl φ x P x T I B x R I O x T I B
65 1 3 4 20 62 24 22 26 63 64 coltr3 φ x P x T I B x R I O x A L B
66 50 41 neleqtrrd φ ¬ O A L B
67 66 adantr φ x P x T I B x R I O ¬ O A L B
68 nelne2 x A L B ¬ O A L B x O
69 65 67 68 syl2anc φ x P x T I B x R I O x O
70 1 2 3 20 23 26 25 61 69 tgbtwnne φ x P x T I B x R I O O R
71 1 2 3 4 6 5 8 7 11 israg φ ⟨“ BAO ”⟩ 𝒢 G B - ˙ O = B - ˙ S A O
72 43 71 mpbid φ B - ˙ O = B - ˙ S A O
73 72 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B - ˙ O = B - ˙ S A O
74 5 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R G 𝒢 Tarski
75 eqid S A = S A
76 1 2 3 4 6 20 24 75 23 mircl φ x P x T I B x R I O S A O P
77 76 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R S A O P
78 7 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A P
79 11 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R O P
80 17 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R R P
81 8 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B P
82 simplr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R s P
83 1 2 3 4 6 74 78 75 79 mirbtwn φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A S A O I O
84 eqid S B = S B
85 1 2 3 4 6 74 81 84 82 mirbtwn φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B S B s I s
86 simpr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s R = S m s
87 74 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s G 𝒢 Tarski
88 78 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s A P
89 81 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s B P
90 54 ad4antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s A B
91 10 ad5antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s Q P
92 79 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s O P
93 62 ad4antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s T P
94 13 ad5antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s A L B 𝒢 G Q L B
95 14 ad5antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s A L B 𝒢 G A L O
96 63 ad4antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s T A L B
97 16 ad5antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s T Q I O
98 80 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s R P
99 18 ad5antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s R B I Q
100 19 ad5antr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s A - ˙ O = B - ˙ R
101 26 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x P
102 101 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x P
103 simp-5r φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x P x T I B x R I O
104 103 simprd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x T I B x R I O
105 104 simpld φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x T I B
106 104 simprd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x R I O
107 82 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s s P
108 simpllr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x S A O I s x - ˙ s = x - ˙ R
109 108 simpld φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x S A O I s
110 simprr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x - ˙ s = x - ˙ R
111 110 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s x - ˙ s = x - ˙ R
112 simplr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s m P
113 1 2 3 4 87 6 88 89 90 91 92 93 94 95 96 97 98 99 100 102 105 106 107 109 111 112 86 mideulem2 φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s B = m
114 113 eqcomd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s m = B
115 114 fveq2d φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s S m = S B
116 115 fveq1d φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s S m s = S B s
117 86 116 eqtrd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s R = S B s
118 eqid S m = S m
119 1 2 3 4 6 74 118 82 80 101 110 midexlem φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R m P R = S m s
120 117 119 r19.29a φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R R = S B s
121 120 oveq1d φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R R I s = S B s I s
122 85 121 eleqtrrd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B R I s
123 1 2 3 4 6 74 78 75 79 mircgr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A - ˙ S A O = A - ˙ O
124 19 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A - ˙ O = B - ˙ R
125 123 124 eqtrd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A - ˙ S A O = B - ˙ R
126 1 2 3 74 78 77 81 80 125 tgcgrcomlr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R S A O - ˙ A = R - ˙ B
127 120 oveq2d φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B - ˙ R = B - ˙ S B s
128 1 2 3 4 6 74 81 84 82 mircgr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B - ˙ S B s = B - ˙ s
129 124 127 128 3eqtrd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A - ˙ O = B - ˙ s
130 1 2 3 74 77 78 79 80 81 82 83 122 126 129 tgcgrextend φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R S A O - ˙ O = R - ˙ s
131 1 2 3 74 77 80 axtgcgrrflx φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R S A O - ˙ R = R - ˙ S A O
132 1 2 3 74 79 80 axtgcgrrflx φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R O - ˙ R = R - ˙ O
133 60 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x R I O
134 simprl φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x S A O I s
135 1 2 3 74 77 101 82 134 tgbtwncom φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x s I S A O
136 1 2 3 74 101 82 101 80 110 tgcgrcomlr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R s - ˙ x = R - ˙ x
137 136 eqcomd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R R - ˙ x = s - ˙ x
138 43 ad3antrrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R ⟨“ BAO ”⟩ 𝒢 G
139 54 necomd φ x P x T I B x R I O B A
140 139 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B A
141 65 ad2antrr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x A L B
142 141 orcd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x A L B A = B
143 1 4 3 74 78 81 101 142 colcom φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x B L A B = A
144 1 4 3 74 81 78 101 143 colrot1 φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B A L x A = x
145 1 2 3 4 6 74 81 78 79 101 138 140 144 ragcol φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R ⟨“ xAO ”⟩ 𝒢 G
146 1 2 3 4 6 74 101 78 79 israg φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R ⟨“ xAO ”⟩ 𝒢 G x - ˙ O = x - ˙ S A O
147 145 146 mpbid φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R x - ˙ O = x - ˙ S A O
148 1 2 3 74 80 101 79 82 101 77 133 135 137 147 tgcgrextend φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R R - ˙ O = s - ˙ S A O
149 132 148 eqtrd φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R O - ˙ R = s - ˙ S A O
150 1 2 3 74 77 78 79 80 80 81 82 77 83 122 130 129 131 149 tgifscgr φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R A - ˙ R = B - ˙ S A O
151 73 150 eqtr4d φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R B - ˙ O = A - ˙ R
152 1 2 3 20 76 26 26 25 axtgsegcon φ x P x T I B x R I O s P x S A O I s x - ˙ s = x - ˙ R
153 151 152 r19.29a φ x P x T I B x R I O B - ˙ O = A - ˙ R
154 19 adantr φ x P x T I B x R I O A - ˙ O = B - ˙ R
155 1 2 3 20 24 23 22 25 154 tgcgrcomlr φ x P x T I B x R I O O - ˙ A = R - ˙ B
156 143 152 r19.29a φ x P x T I B x R I O x B L A B = A
157 1 4 3 20 23 25 26 61 btwncolg1 φ x P x T I B x R I O x O L R O = R
158 1 2 3 4 6 20 21 22 23 24 25 26 59 70 153 155 156 157 symquadlem φ x P x T I B x R I O B = S x A
159 1 2 3 4 6 20 26 21 24 mirbtwn φ x P x T I B x R I O x S x A I A
160 158 oveq1d φ x P x T I B x R I O B I A = S x A I A
161 159 160 eleqtrrd φ x P x T I B x R I O x B I A
162 1 2 3 20 22 26 24 161 tgbtwncom φ x P x T I B x R I O x A I B
163 1 2 3 20 24 22 axtgcgrrflx φ x P x T I B x R I O A - ˙ B = B - ˙ A
164 158 oveq2d φ x P x T I B x R I O x - ˙ B = x - ˙ S x A
165 1 2 3 4 6 20 26 21 24 mircgr φ x P x T I B x R I O x - ˙ S x A = x - ˙ A
166 164 165 eqtrd φ x P x T I B x R I O x - ˙ B = x - ˙ A
167 1 2 3 20 24 26 22 23 22 26 24 25 162 161 163 166 154 153 tgifscgr φ x P x T I B x R I O x - ˙ O = x - ˙ R
168 1 2 3 4 6 20 26 21 25 23 167 61 ismir φ x P x T I B x R I O O = S x R
169 158 168 jca φ x P x T I B x R I O B = S x A O = S x R
170 1 2 3 5 10 12 11 16 tgbtwncom φ T O I Q
171 1 2 3 5 11 8 10 12 17 170 18 axtgpasch φ x P x T I B x R I O
172 169 171 reximddv φ x P B = S x A O = S x R