Metamath Proof Explorer


Theorem krippenlem

Description: Lemma for krippen . We can assume krippen.7 "without loss of generality". (Contributed by Thierry Arnoux, 12-Aug-2019)

Ref Expression
Hypotheses mirval.p P = Base G
mirval.d - ˙ = dist G
mirval.i I = Itv G
mirval.l L = Line 𝒢 G
mirval.s S = pInv 𝒢 G
mirval.g φ G 𝒢 Tarski
krippen.m M = S X
krippen.n N = S Y
krippen.a φ A P
krippen.b φ B P
krippen.c φ C P
krippen.e φ E P
krippen.f φ F P
krippen.x φ X P
krippen.y φ Y P
krippen.1 φ C A I E
krippen.2 φ C B I F
krippen.3 φ C - ˙ A = C - ˙ B
krippen.4 φ C - ˙ E = C - ˙ F
krippen.5 φ B = M A
krippen.6 φ F = N E
krippen.l ˙ = 𝒢 G
krippen.7 φ C - ˙ A ˙ C - ˙ E
Assertion krippenlem φ C X I Y

Proof

Step Hyp Ref Expression
1 mirval.p P = Base G
2 mirval.d - ˙ = dist G
3 mirval.i I = Itv G
4 mirval.l L = Line 𝒢 G
5 mirval.s S = pInv 𝒢 G
6 mirval.g φ G 𝒢 Tarski
7 krippen.m M = S X
8 krippen.n N = S Y
9 krippen.a φ A P
10 krippen.b φ B P
11 krippen.c φ C P
12 krippen.e φ E P
13 krippen.f φ F P
14 krippen.x φ X P
15 krippen.y φ Y P
16 krippen.1 φ C A I E
17 krippen.2 φ C B I F
18 krippen.3 φ C - ˙ A = C - ˙ B
19 krippen.4 φ C - ˙ E = C - ˙ F
20 krippen.5 φ B = M A
21 krippen.6 φ F = N E
22 krippen.l ˙ = 𝒢 G
23 krippen.7 φ C - ˙ A ˙ C - ˙ E
24 16 adantr φ E = C C A I E
25 6 adantr φ E = C G 𝒢 Tarski
26 11 adantr φ E = C C P
27 9 adantr φ E = C A P
28 10 adantr φ E = C B P
29 18 adantr φ E = C C - ˙ A = C - ˙ B
30 23 adantr φ E = C C - ˙ A ˙ C - ˙ E
31 simpr φ E = C E = C
32 31 oveq2d φ E = C C - ˙ E = C - ˙ C
33 30 32 breqtrd φ E = C C - ˙ A ˙ C - ˙ C
34 1 2 3 22 25 26 27 26 28 33 legeq φ E = C C = A
35 1 2 3 25 26 27 26 28 29 34 tgcgreq φ E = C C = B
36 20 adantr φ E = C B = M A
37 35 34 36 3eqtr3rd φ E = C M A = A
38 14 adantr φ E = C X P
39 1 2 3 4 5 25 38 7 27 mirinv φ E = C M A = A X = A
40 37 39 mpbid φ E = C X = A
41 13 adantr φ E = C F P
42 19 adantr φ E = C C - ˙ E = C - ˙ F
43 42 32 eqtr3d φ E = C C - ˙ F = C - ˙ C
44 1 2 3 25 26 41 26 43 axtgcgrid φ E = C C = F
45 21 adantr φ E = C F = N E
46 31 44 45 3eqtrrd φ E = C N E = E
47 15 adantr φ E = C Y P
48 12 adantr φ E = C E P
49 1 2 3 4 5 25 47 8 48 mirinv φ E = C N E = E Y = E
50 46 49 mpbid φ E = C Y = E
51 40 50 oveq12d φ E = C X I Y = A I E
52 24 51 eleqtrrd φ E = C C X I Y
53 6 adantr φ E C G 𝒢 Tarski
54 53 ad2antrr φ E C q P q S C Y I C q A I B G 𝒢 Tarski
55 11 adantr φ E C C P
56 eqid S C = S C
57 1 2 3 4 5 53 55 56 mirf φ E C S C : P P
58 15 adantr φ E C Y P
59 57 58 ffvelrnd φ E C S C Y P
60 59 ad2antrr φ E C q P q S C Y I C q A I B S C Y P
61 simplr φ E C q P q S C Y I C q A I B q P
62 55 ad2antrr φ E C q P q S C Y I C q A I B C P
63 58 ad2antrr φ E C q P q S C Y I C q A I B Y P
64 simprl φ E C q P q S C Y I C q A I B q S C Y I C
65 1 2 3 4 5 6 11 56 15 mirbtwn φ C S C Y I Y
66 65 ad3antrrr φ E C q P q S C Y I C q A I B C S C Y I Y
67 1 2 3 54 60 61 62 63 64 66 tgbtwnexch3 φ E C q P q S C Y I C q A I B C q I Y
68 14 ad3antrrr φ E C q P q S C Y I C q A I B X P
69 9 adantr φ E C A P
70 69 ad2antrr φ E C q P q S C Y I C q A I B A P
71 10 adantr φ E C B P
72 71 ad2antrr φ E C q P q S C Y I C q A I B B P
73 eqid S q = S q
74 12 adantr φ E C E P
75 57 74 ffvelrnd φ E C S C E P
76 13 adantr φ E C F P
77 57 76 ffvelrnd φ E C S C F P
78 6 ad2antrr φ E C A = C G 𝒢 Tarski
79 9 ad2antrr φ E C A = C A P
80 75 adantr φ E C A = C S C E P
81 1 2 3 78 79 80 tgbtwntriv1 φ E C A = C A A I S C E
82 simpr φ E C A = C A = C
83 82 oveq1d φ E C A = C A I S C E = C I S C E
84 81 83 eleqtrd φ E C A = C A C I S C E
85 6 ad2antrr φ E C A C G 𝒢 Tarski
86 9 ad2antrr φ E C A C A P
87 75 adantr φ E C A C S C E P
88 11 ad2antrr φ E C A C C P
89 12 ad2antrr φ E C A C E P
90 simplr φ E C A C E C
91 1 2 3 6 9 11 12 16 tgbtwncom φ C E I A
92 91 ad2antrr φ E C A C C E I A
93 1 2 3 4 5 85 88 56 89 mirbtwn φ E C A C C S C E I E
94 1 2 3 85 87 88 89 93 tgbtwncom φ E C A C C E I S C E
95 1 3 85 89 88 86 87 90 92 94 tgbtwnconn2 φ E C A C A C I S C E S C E C I A
96 23 adantr φ E C C - ˙ A ˙ C - ˙ E
97 1 2 3 4 5 53 55 56 74 mircgr φ E C C - ˙ S C E = C - ˙ E
98 96 97 breqtrrd φ E C C - ˙ A ˙ C - ˙ S C E
99 98 adantr φ E C A C C - ˙ A ˙ C - ˙ S C E
100 1 2 3 22 85 86 87 88 86 95 99 legbtwn φ E C A C A C I S C E
101 84 100 pm2.61dane φ E C A C I S C E
102 1 2 3 53 55 69 75 101 tgbtwncom φ E C A S C E I C
103 6 ad2antrr φ E C B = C G 𝒢 Tarski
104 10 ad2antrr φ E C B = C B P
105 77 adantr φ E C B = C S C F P
106 1 2 3 103 104 105 tgbtwntriv1 φ E C B = C B B I S C F
107 simpr φ E C B = C B = C
108 107 oveq1d φ E C B = C B I S C F = C I S C F
109 106 108 eleqtrd φ E C B = C B C I S C F
110 6 ad2antrr φ E C B C G 𝒢 Tarski
111 10 ad2antrr φ E C B C B P
112 77 adantr φ E C B C S C F P
113 11 ad2antrr φ E C B C C P
114 13 ad2antrr φ E C B C F P
115 6 adantr φ F = C G 𝒢 Tarski
116 11 adantr φ F = C C P
117 12 adantr φ F = C E P
118 19 adantr φ F = C C - ˙ E = C - ˙ F
119 simpr φ F = C F = C
120 119 oveq2d φ F = C C - ˙ F = C - ˙ C
121 118 120 eqtrd φ F = C C - ˙ E = C - ˙ C
122 1 2 3 115 116 117 116 121 axtgcgrid φ F = C C = E
123 122 eqcomd φ F = C E = C
124 123 adantlr φ E C F = C E = C
125 simplr φ E C F = C E C
126 125 neneqd φ E C F = C ¬ E = C
127 124 126 pm2.65da φ E C ¬ F = C
128 127 neqned φ E C F C
129 128 adantr φ E C B C F C
130 1 2 3 6 10 11 13 17 tgbtwncom φ C F I B
131 130 ad2antrr φ E C B C C F I B
132 1 2 3 4 5 110 113 56 114 mirbtwn φ E C B C C S C F I F
133 1 2 3 110 112 113 114 132 tgbtwncom φ E C B C C F I S C F
134 1 3 110 114 113 111 112 129 131 133 tgbtwnconn2 φ E C B C B C I S C F S C F C I B
135 23 18 19 3brtr3d φ C - ˙ B ˙ C - ˙ F
136 135 adantr φ E C C - ˙ B ˙ C - ˙ F
137 1 2 3 4 5 53 55 56 76 mircgr φ E C C - ˙ S C F = C - ˙ F
138 136 137 breqtrrd φ E C C - ˙ B ˙ C - ˙ S C F
139 138 adantr φ E C B C C - ˙ B ˙ C - ˙ S C F
140 1 2 3 22 110 111 112 113 111 134 139 legbtwn φ E C B C B C I S C F
141 109 140 pm2.61dane φ E C B C I S C F
142 1 2 3 53 55 71 77 141 tgbtwncom φ E C B S C F I C
143 19 adantr φ E C C - ˙ E = C - ˙ F
144 143 97 137 3eqtr4d φ E C C - ˙ S C E = C - ˙ S C F
145 1 2 3 53 55 75 55 77 144 tgcgrcomlr φ E C S C E - ˙ C = S C F - ˙ C
146 18 adantr φ E C C - ˙ A = C - ˙ B
147 1 2 3 53 55 69 55 71 146 tgcgrcomlr φ E C A - ˙ C = B - ˙ C
148 eqid S S C Y = S S C Y
149 1 2 3 4 5 53 59 148 75 mircgr φ E C S C Y - ˙ S S C Y S C E = S C Y - ˙ S C E
150 eqid S C Y = S C Y
151 eqid S C E = S C E
152 eqid S C F = S C F
153 21 adantr φ E C F = N E
154 8 fveq1i N E = S Y E
155 153 154 eqtr2di φ E C S Y E = F
156 1 2 3 4 5 53 56 150 151 152 55 58 74 76 155 mirauto φ E C S S C Y S C E = S C F
157 156 oveq2d φ E C S C Y - ˙ S S C Y S C E = S C Y - ˙ S C F
158 149 157 eqtr3d φ E C S C Y - ˙ S C E = S C Y - ˙ S C F
159 1 2 3 53 59 75 59 77 158 tgcgrcomlr φ E C S C E - ˙ S C Y = S C F - ˙ S C Y
160 eqidd φ E C C - ˙ S C Y = C - ˙ S C Y
161 1 2 3 53 75 69 55 59 77 71 55 59 102 142 145 147 159 160 tgifscgr φ E C A - ˙ S C Y = B - ˙ S C Y
162 1 2 3 53 69 59 71 59 161 tgcgrcomlr φ E C S C Y - ˙ A = S C Y - ˙ B
163 162 ad3antrrr φ E C q P q S C Y I C q A I B S C Y = C S C Y - ˙ A = S C Y - ˙ B
164 54 adantr φ E C q P q S C Y I C q A I B S C Y = C G 𝒢 Tarski
165 60 adantr φ E C q P q S C Y I C q A I B S C Y = C S C Y P
166 61 adantr φ E C q P q S C Y I C q A I B S C Y = C q P
167 64 adantr φ E C q P q S C Y I C q A I B S C Y = C q S C Y I C
168 simpr φ E C q P q S C Y I C q A I B S C Y = C S C Y = C
169 168 oveq2d φ E C q P q S C Y I C q A I B S C Y = C S C Y I S C Y = S C Y I C
170 167 169 eleqtrrd φ E C q P q S C Y I C q A I B S C Y = C q S C Y I S C Y
171 1 2 3 164 165 166 170 axtgbtwnid φ E C q P q S C Y I C q A I B S C Y = C S C Y = q
172 171 oveq1d φ E C q P q S C Y I C q A I B S C Y = C S C Y - ˙ A = q - ˙ A
173 171 oveq1d φ E C q P q S C Y I C q A I B S C Y = C S C Y - ˙ B = q - ˙ B
174 163 172 173 3eqtr3d φ E C q P q S C Y I C q A I B S C Y = C q - ˙ A = q - ˙ B
175 53 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C G 𝒢 Tarski
176 59 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C S C Y P
177 55 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C C P
178 61 adantr φ E C q P q S C Y I C q A I B S C Y C q P
179 eqid 𝒢 G = 𝒢 G
180 69 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C A P
181 71 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C B P
182 simpr φ E C q P q S C Y I C q A I B S C Y C S C Y C
183 60 adantr φ E C q P q S C Y I C q A I B S C Y C S C Y P
184 64 adantr φ E C q P q S C Y I C q A I B S C Y C q S C Y I C
185 1 4 3 175 183 178 177 184 btwncolg3 φ E C q P q S C Y I C q A I B S C Y C C S C Y L q S C Y = q
186 162 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C S C Y - ˙ A = S C Y - ˙ B
187 146 ad3antrrr φ E C q P q S C Y I C q A I B S C Y C C - ˙ A = C - ˙ B
188 1 4 3 175 176 177 178 179 180 181 2 182 185 186 187 lncgr φ E C q P q S C Y I C q A I B S C Y C q - ˙ A = q - ˙ B
189 174 188 pm2.61dane φ E C q P q S C Y I C q A I B q - ˙ A = q - ˙ B
190 189 eqcomd φ E C q P q S C Y I C q A I B q - ˙ B = q - ˙ A
191 simprr φ E C q P q S C Y I C q A I B q A I B
192 1 2 3 54 70 61 72 191 tgbtwncom φ E C q P q S C Y I C q A I B q B I A
193 1 2 3 4 5 54 61 73 70 72 190 192 ismir φ E C q P q S C Y I C q A I B B = S q A
194 193 eqcomd φ E C q P q S C Y I C q A I B S q A = B
195 20 ad3antrrr φ E C q P q S C Y I C q A I B B = M A
196 7 fveq1i M A = S X A
197 195 196 eqtr2di φ E C q P q S C Y I C q A I B S X A = B
198 1 2 3 4 5 54 61 68 70 72 194 197 miduniq φ E C q P q S C Y I C q A I B q = X
199 198 oveq1d φ E C q P q S C Y I C q A I B q I Y = X I Y
200 67 199 eleqtrd φ E C q P q S C Y I C q A I B C X I Y
201 1 2 3 4 5 53 58 8 74 mirbtwn φ E C Y N E I E
202 153 oveq1d φ E C F I E = N E I E
203 201 202 eleqtrrd φ E C Y F I E
204 1 2 3 53 76 58 74 203 tgbtwncom φ E C Y E I F
205 1 2 3 4 5 53 55 56 74 58 76 204 mirbtwni φ E C S C Y S C E I S C F
206 1 2 3 53 75 69 55 77 71 59 102 142 205 tgtrisegint φ E C q P q S C Y I C q A I B
207 200 206 r19.29a φ E C C X I Y
208 52 207 pm2.61dane φ C X I Y