Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmiisolem Structured version   Unicode version

Theorem lmiisolem 24378
 Description: Lemma for lmiiso 24379 (Contributed by Thierry Arnoux, 14-Dec-2019.)
Hypotheses
Ref Expression
ismid.p
ismid.d
ismid.i Itv
ismid.g TarskiG
ismid.1 DimTarskiG
lmif.m lInvG
lmif.l LineG
lmif.d
lmiiso.1
lmiiso.2
lmiisolem.s pInvG
lmiisolem.z midGmidGmidG
Assertion
Ref Expression
lmiisolem

Proof of Theorem lmiisolem
StepHypRef Expression
1 ismid.p . . . . . . . 8
2 ismid.d . . . . . . . 8
3 ismid.i . . . . . . . 8 Itv
4 ismid.g . . . . . . . . 9 TarskiG
54adantr 465 . . . . . . . 8 TarskiG
6 lmiisolem.z . . . . . . . . . 10 midGmidGmidG
7 ismid.1 . . . . . . . . . . 11 DimTarskiG
8 lmiiso.1 . . . . . . . . . . . 12
9 lmif.m . . . . . . . . . . . . 13 lInvG
10 lmif.l . . . . . . . . . . . . 13 LineG
11 lmif.d . . . . . . . . . . . . 13
121, 2, 3, 4, 7, 9, 10, 11, 8lmicl 24369 . . . . . . . . . . . 12
131, 2, 3, 4, 7, 8, 12midcl 24360 . . . . . . . . . . 11 midG
14 lmiiso.2 . . . . . . . . . . . 12
151, 2, 3, 4, 7, 9, 10, 11, 14lmicl 24369 . . . . . . . . . . . 12
161, 2, 3, 4, 7, 14, 15midcl 24360 . . . . . . . . . . 11 midG
171, 2, 3, 4, 7, 13, 16midcl 24360 . . . . . . . . . 10 midGmidGmidG
186, 17syl5eqel 2549 . . . . . . . . 9
1918adantr 465 . . . . . . . 8
20 eqid 2457 . . . . . . . . . 10 pInvG pInvG
21 lmiisolem.s . . . . . . . . . 10 pInvG
221, 2, 3, 10, 20, 4, 18, 21, 8mircl 24259 . . . . . . . . 9
2322adantr 465 . . . . . . . 8
248adantr 465 . . . . . . . 8
251, 2, 3, 10, 20, 5, 19, 21, 24mircgr 24255 . . . . . . . 8
26 simpr 461 . . . . . . . . 9
2726eqcomd 2465 . . . . . . . 8
281, 2, 3, 5, 19, 23, 19, 24, 25, 27tgcgreq 24090 . . . . . . 7
29 simpr 461 . . . . . . . . . . . . 13 midG midG midG midG
3029oveq2d 6312 . . . . . . . . . . . 12 midG midG midGmidGmidG midGmidGmidG
3130, 6syl6reqr 2517 . . . . . . . . . . 11 midG midG midGmidGmidG
324adantr 465 . . . . . . . . . . . 12 midG midG TarskiG
337adantr 465 . . . . . . . . . . . 12 midG midG DimTarskiG
3413adantr 465 . . . . . . . . . . . 12 midG midG midG
351, 2, 3, 32, 33, 34, 34midid 24364 . . . . . . . . . . 11 midG midG midGmidGmidG midG
3631, 35eqtrd 2498 . . . . . . . . . 10 midG midG midG
37 eqidd 2458 . . . . . . . . . . . . 13
381, 2, 3, 4, 7, 9, 10, 11, 8, 12islmib 24370 . . . . . . . . . . . . 13 midG ⟂G
3937, 38mpbid 210 . . . . . . . . . . . 12 midG ⟂G
4039simpld 459 . . . . . . . . . . 11 midG
4140adantr 465 . . . . . . . . . 10 midG midG midG
4236, 41eqeltrd 2545 . . . . . . . . 9 midG midG
434adantr 465 . . . . . . . . . . 11 midG midG TarskiG
4413adantr 465 . . . . . . . . . . 11 midG midG midG
4516adantr 465 . . . . . . . . . . 11 midG midG midG
4618adantr 465 . . . . . . . . . . 11 midG midG
47 simpr 461 . . . . . . . . . . 11 midG midG midG midG
481, 2, 3, 4, 7, 13, 16midbtwn 24362 . . . . . . . . . . . . 13 midGmidGmidG midGmidG
496, 48syl5eqel 2549 . . . . . . . . . . . 12 midGmidG
5049adantr 465 . . . . . . . . . . 11 midG midG midGmidG
511, 3, 10, 43, 44, 45, 46, 47, 50btwnlng1 24216 . . . . . . . . . 10 midG midG midGmidG
5211adantr 465 . . . . . . . . . . 11 midG midG
5340adantr 465 . . . . . . . . . . 11 midG midG midG
54 eqidd 2458 . . . . . . . . . . . . . 14
551, 2, 3, 4, 7, 9, 10, 11, 14, 15islmib 24370 . . . . . . . . . . . . . 14 midG ⟂G
5654, 55mpbid 210 . . . . . . . . . . . . 13 midG ⟂G
5756simpld 459 . . . . . . . . . . . 12 midG
5857adantr 465 . . . . . . . . . . 11 midG midG midG
591, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58tglinethru 24233 . . . . . . . . . 10 midG midG midGmidG
6051, 59eleqtrrd 2548 . . . . . . . . 9 midG midG
6142, 60pm2.61dane 2775 . . . . . . . 8
6261adantr 465 . . . . . . 7
6328, 62eqeltrrd 2546 . . . . . 6
641, 2, 3, 4, 7, 9, 10, 11, 8lmiinv 24375 . . . . . . 7
6564biimpar 485 . . . . . 6
6663, 65syldan 470 . . . . 5
6766, 28eqtr4d 2501 . . . 4
6867oveq1d 6311 . . 3
69 eqidd 2458 . . . . . . . . 9
704adantr 465 . . . . . . . . . 10 TarskiG
7114adantr 465 . . . . . . . . . 10
7216adantr 465 . . . . . . . . . 10 midG
731, 2, 3, 4, 7, 14, 15midbtwn 24362 . . . . . . . . . . . 12 midG
7473adantr 465 . . . . . . . . . . 11 midG
75 simpr 461 . . . . . . . . . . . 12
7675oveq2d 6312 . . . . . . . . . . 11
7774, 76eleqtrrd 2548 . . . . . . . . . 10 midG
781, 2, 3, 70, 71, 72, 77axtgbtwnid 24080 . . . . . . . . 9 midG
79 eqidd 2458 . . . . . . . . 9
8069, 78, 79s3eqd 12840 . . . . . . . 8 midG
811, 2, 3, 10, 20, 4, 18, 14, 14ragtrivb 24296 . . . . . . . . 9 ∟G
8281adantr 465 . . . . . . . 8 ∟G
8380, 82eqeltrrd 2546 . . . . . . 7 midG ∟G
844adantr 465 . . . . . . . 8 TarskiG
8561adantr 465 . . . . . . . 8
8657adantr 465 . . . . . . . 8 midG
8714adantr 465 . . . . . . . 8
88 df-ne 2654 . . . . . . . . . 10
8956simprd 463 . . . . . . . . . . . 12 ⟂G
9089orcomd 388 . . . . . . . . . . 11 ⟂G
9190orcanai 913 . . . . . . . . . 10 ⟂G
9288, 91sylan2b 475 . . . . . . . . 9 ⟂G
9315adantr 465 . . . . . . . . . . 11
94 simpr 461 . . . . . . . . . . 11
9516adantr 465 . . . . . . . . . . 11 midG
964adantr 465 . . . . . . . . . . . . . . 15 midG TarskiG
9714adantr 465 . . . . . . . . . . . . . . 15 midG
9815adantr 465 . . . . . . . . . . . . . . 15 midG
997adantr 465 . . . . . . . . . . . . . . . . 17 midG DimTarskiG
100 simpr 461 . . . . . . . . . . . . . . . . 17 midG midG
1011, 2, 3, 96, 99, 97, 98, 100midcgr 24363 . . . . . . . . . . . . . . . 16 midG
102101eqcomd 2465 . . . . . . . . . . . . . . 15 midG
1031, 2, 3, 96, 97, 98, 97, 102axtgcgrid 24077 . . . . . . . . . . . . . 14 midG
104103ex 434 . . . . . . . . . . . . 13 midG
105104necon3d 2681 . . . . . . . . . . . 12 midG
106105imp 429 . . . . . . . . . . 11 midG
10773adantr 465 . . . . . . . . . . . 12 midG
1081, 3, 10, 84, 87, 93, 95, 94, 107btwnlng1 24216 . . . . . . . . . . 11 midG
1091, 3, 10, 84, 87, 93, 94, 95, 106, 108tglineelsb2 24229 . . . . . . . . . 10 midG
1101, 3, 10, 84, 95, 87, 106tglinecom 24232 . . . . . . . . . 10 midG midG
111109, 110eqtr4d 2501 . . . . . . . . 9 midG
11292, 111breqtrd 4480 . . . . . . . 8 ⟂GmidG
1131, 2, 3, 10, 84, 85, 86, 87, 112perpdrag 24319 . . . . . . 7 midG ∟G
11483, 113pm2.61dane 2775 . . . . . 6 midG ∟G
1151, 2, 3, 10, 20, 4, 18, 16, 14israg 24291 . . . . . 6 midG ∟G pInvGmidG
116114, 115mpbid 210 . . . . 5 pInvGmidG
117 eqidd 2458 . . . . . . 7 midG midG
1181, 2, 3, 4, 7, 14, 15, 20, 16ismidb 24361 . . . . . . 7 pInvGmidG midG midG
119117, 118mpbird 232 . . . . . 6 pInvGmidG
120119oveq2d 6312 . . . . 5 pInvGmidG
121116, 120eqtr4d 2501 . . . 4
12328oveq1d 6311 . . 3
12468, 122, 1233eqtr2d 2504 . 2
1254adantr 465 . . . 4 TarskiG
12622adantr 465 . . . 4
12718adantr 465 . . . 4
1288adantr 465 . . . 4
1291, 2, 3, 10, 20, 4, 18, 21, 12mircl 24259 . . . . 5
130129adantr 465 . . . 4
13112adantr 465 . . . 4
13214adantr 465 . . . 4
13315adantr 465 . . . 4
134 simpr 461 . . . 4
1351, 2, 3, 10, 20, 125, 127, 21, 128mirbtwn 24256 . . . 4
1361, 2, 3, 10, 20, 125, 127, 21, 131mirbtwn 24256 . . . 4
137 eqidd 2458 . . . . . . . . . . . 12
1384adantr 465 . . . . . . . . . . . . 13 TarskiG
1398adantr 465 . . . . . . . . . . . . 13
14013adantr 465 . . . . . . . . . . . . 13 midG
1411, 2, 3, 4, 7, 8, 12midbtwn 24362 . . . . . . . . . . . . . . 15 midG
142141adantr 465 . . . . . . . . . . . . . 14 midG
143 simpr 461 . . . . . . . . . . . . . . 15
144143oveq2d 6312 . . . . . . . . . . . . . 14
145142, 144eleqtrrd 2548 . . . . . . . . . . . . 13 midG
1461, 2, 3, 138, 139, 140, 145axtgbtwnid 24080 . . . . . . . . . . . 12 midG
147 eqidd 2458 . . . . . . . . . . . 12
148137, 146, 147s3eqd 12840 . . . . . . . . . . 11 midG
1491, 2, 3, 10, 20, 4, 18, 8, 8ragtrivb 24296 . . . . . . . . . . . 12 ∟G
150149adantr 465 . . . . . . . . . . 11 ∟G
151148, 150eqeltrrd 2546 . . . . . . . . . 10 midG ∟G
1524adantr 465 . . . . . . . . . . 11 TarskiG
15361adantr 465 . . . . . . . . . . 11
15440adantr 465 . . . . . . . . . . 11 midG
1558adantr 465 . . . . . . . . . . 11
156 df-ne 2654 . . . . . . . . . . . . 13
15739simprd 463 . . . . . . . . . . . . . . 15 ⟂G
158157orcomd 388 . . . . . . . . . . . . . 14 ⟂G
159158orcanai 913 . . . . . . . . . . . . 13 ⟂G
160156, 159sylan2b 475 . . . . . . . . . . . 12 ⟂G
16112adantr 465 . . . . . . . . . . . . . 14
162 simpr 461 . . . . . . . . . . . . . 14
16313adantr 465 . . . . . . . . . . . . . 14 midG
1644adantr 465 . . . . . . . . . . . . . . . . . 18 midG TarskiG
1658adantr 465 . . . . . . . . . . . . . . . . . 18 midG
16612adantr 465 . . . . . . . . . . . . . . . . . 18 midG
1677adantr 465 . . . . . . . . . . . . . . . . . . . 20 midG DimTarskiG
168 simpr 461 . . . . . . . . . . . . . . . . . . . 20 midG midG
1691, 2, 3, 164, 167, 165, 166, 168midcgr 24363 . . . . . . . . . . . . . . . . . . 19 midG
170169eqcomd 2465 . . . . . . . . . . . . . . . . . 18 midG
1711, 2, 3, 164, 165, 166, 165, 170axtgcgrid 24077 . . . . . . . . . . . . . . . . 17 midG
172171ex 434 . . . . . . . . . . . . . . . 16 midG
173172necon3d 2681 . . . . . . . . . . . . . . 15 midG
174173imp 429 . . . . . . . . . . . . . 14 midG
175141adantr 465 . . . . . . . . . . . . . . 15 midG
1761, 3, 10, 152, 155, 161, 163, 162, 175btwnlng1 24216 . . . . . . . . . . . . . 14 midG
1771, 3, 10, 152, 155, 161, 162, 163, 174, 176tglineelsb2 24229 . . . . . . . . . . . . 13 midG
1781, 3, 10, 152, 163, 155, 174tglinecom 24232 . . . . . . . . . . . . 13 midG midG
179177, 178eqtr4d 2501 . . . . . . . . . . . 12 midG
180160, 179breqtrd 4480 . . . . . . . . . . 11 ⟂GmidG
1811, 2, 3, 10, 152, 153, 154, 155, 180perpdrag 24319 . . . . . . . . . 10 midG ∟G
182151, 181pm2.61dane 2775 . . . . . . . . 9 midG ∟G
1831, 2, 3, 10, 20, 4, 18, 13, 8israg 24291 . . . . . . . . 9 midG ∟G pInvGmidG
184182, 183mpbid 210 . . . . . . . 8 pInvGmidG
185 eqidd 2458 . . . . . . . . . 10 midG midG
1861, 2, 3, 4, 7, 8, 12, 20, 13ismidb 24361 . . . . . . . . . 10 pInvGmidG midG midG
187185, 186mpbird 232 . . . . . . . . 9 pInvGmidG
188187oveq2d 6312 . . . . . . . 8 pInvGmidG
189184, 188eqtr4d 2501 . . . . . . 7
1901, 2, 3, 10, 20, 4, 18, 21, 8mircgr 24255 . . . . . . 7
1911, 2, 3, 10, 20, 4, 18, 21, 12mircgr 24255 . . . . . . 7
192189, 190, 1913eqtr4d 2508 . . . . . 6
193192adantr 465 . . . . 5
1941, 2, 3, 125, 127, 126, 127, 130, 193tgcgrcomlr 24088 . . . 4
195189adantr 465 . . . 4
19621fveq1i 5873 . . . . . . . . . 10 midG pInvGmidG
1971, 2, 3, 4, 7, 8, 12, 21, 18mirmid 24366 . . . . . . . . . 10 midG midG
1986eqcomi 2470 . . . . . . . . . . 11 midGmidGmidG
1991, 2, 3, 4, 7, 13, 16, 20, 18ismidb 24361 . . . . . . . . . . 11 midG pInvGmidG midGmidGmidG
200198, 199mpbiri 233 . . . . . . . . . 10 midG pInvGmidG
201196, 197, 2003eqtr4a 2524 . . . . . . . . 9 midG midG
2021, 2, 3, 4, 7, 22, 129, 20, 16ismidb 24361 . . . . . . . . 9 pInvGmidG midG midG
203201, 202mpbird 232 . . . . . . . 8 pInvGmidG
204119, 203oveq12d 6314 . . . . . . 7 pInvGmidG pInvGmidG
205 eqid 2457 . . . . . . . 8 pInvGmidG pInvGmidG
2061, 2, 3, 10, 20, 4, 16, 205, 14, 22miriso 24267 . . . . . . 7 pInvGmidG pInvGmidG
207204, 206eqtr2d 2499 . . . . . 6
208207adantr 465 . . . . 5
2091, 2, 3, 125, 132, 126, 133, 130, 208tgcgrcomlr 24088 . . . 4
210121adantr 465 . . . 4
2111, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210axtg5seg 24079 . . 3
212211eqcomd 2465 . 2
213124, 212pm2.61dane 2775 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 368   wa 369   wceq 1395   wcel 1819   wne 2652   class class class wbr 4456   crn 5009  cfv 5594  (class class class)co 6296  c2 10606  cs3 12819  cbs 14735  cds 14812  TarskiGcstrkg 24042  DimTarskiG≥cstrkgld 24046  Itvcitv 24049  LineGclng 24050  pInvGcmir 24250  ∟Gcrag 24287  ⟂Gcperpg 24289  midGcmid 24355  lInvGclmi 24356 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-3 10616  df-n0 10817  df-z 10886  df-uz 11107  df-fz 11698  df-fzo 11822  df-hash 12409  df-word 12546  df-concat 12548  df-s1 12549  df-s2 12825  df-s3 12826  df-trkgc 24061  df-trkgb 24062  df-trkgcb 24063  df-trkgld 24065  df-trkg 24067  df-cgrg 24120  df-leg 24187  df-mir 24251  df-rag 24288  df-perpg 24290  df-mid 24357  df-lmi 24358 This theorem is referenced by:  lmiiso  24379
 Copyright terms: Public domain W3C validator