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

Theorem midex 24771
 Description: Existence of the midpoint, part Theorem 8.22 of [Schwabhauser] p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p
colperpex.d
colperpex.i Itv
colperpex.l LineG
colperpex.g TarskiG
mideu.s pInvG
mideu.1
mideu.2
mideu.3 DimTarskiG
Assertion
Ref Expression
midex
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem midex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mideu.1 . . . 4
21adantr 467 . . 3
3 colperpex.p . . . . 5
4 colperpex.d . . . . 5
5 colperpex.i . . . . 5 Itv
6 colperpex.l . . . . 5 LineG
7 mideu.s . . . . 5 pInvG
8 colperpex.g . . . . . 6 TarskiG
98adantr 467 . . . . 5 TarskiG
10 eqid 2423 . . . . 5
113, 4, 5, 6, 7, 9, 2, 10mircinv 24705 . . . 4
12 simpr 463 . . . 4
1311, 12eqtr2d 2465 . . 3
14 fveq2 5879 . . . . . 6
1514fveq1d 5881 . . . . 5
1615eqeq2d 2437 . . . 4
1716rspcev 3183 . . 3
182, 13, 17syl2anc 666 . 2
198adantr 467 . . . . . . . 8 TarskiG
2019ad2antrr 731 . . . . . . 7 ⟂G TarskiG
2120ad4antr 737 . . . . . 6 ⟂G ⟂G ≤G TarskiG
221adantr 467 . . . . . . . 8
2322ad2antrr 731 . . . . . . 7 ⟂G
2423ad4antr 737 . . . . . 6 ⟂G ⟂G ≤G
25 mideu.2 . . . . . . . . 9
2625adantr 467 . . . . . . . 8
2726ad2antrr 731 . . . . . . 7 ⟂G
2827ad4antr 737 . . . . . 6 ⟂G ⟂G ≤G
29 simpr 463 . . . . . . . 8
3029ad2antrr 731 . . . . . . 7 ⟂G
3130ad4antr 737 . . . . . 6 ⟂G ⟂G ≤G
32 simplr 761 . . . . . . 7 ⟂G
3332ad4antr 737 . . . . . 6 ⟂G ⟂G ≤G
34 simp-4r 776 . . . . . 6 ⟂G ⟂G ≤G
35 simpllr 768 . . . . . 6 ⟂G ⟂G ≤G
36 simp-5r 778 . . . . . . . . 9 ⟂G ⟂G ≤G ⟂G
376, 21, 36perpln1 24747 . . . . . . . 8 ⟂G ⟂G ≤G
383, 5, 6, 21, 24, 28, 31tgelrnln 24667 . . . . . . . 8 ⟂G ⟂G ≤G
393, 4, 5, 6, 21, 37, 38, 36perpcom 24750 . . . . . . 7 ⟂G ⟂G ≤G ⟂G
403, 5, 6, 21, 28, 33, 37tglnne 24665 . . . . . . . 8 ⟂G ⟂G ≤G
413, 5, 6, 21, 28, 33, 40tglinecom 24672 . . . . . . 7 ⟂G ⟂G ≤G
4239, 41breqtrd 4446 . . . . . 6 ⟂G ⟂G ≤G ⟂G
43 simplr 761 . . . . . . . . 9 ⟂G ⟂G ≤G ⟂G
4443simpld 461 . . . . . . . 8 ⟂G ⟂G ≤G ⟂G
456, 21, 44perpln1 24747 . . . . . . 7 ⟂G ⟂G ≤G
463, 4, 5, 6, 21, 45, 38, 44perpcom 24750 . . . . . 6 ⟂G ⟂G ≤G ⟂G
4731neneqd 2626 . . . . . . 7 ⟂G ⟂G ≤G
4843simprd 465 . . . . . . . . . 10 ⟂G ⟂G ≤G
4948simpld 461 . . . . . . . . 9 ⟂G ⟂G ≤G
5049orcomd 390 . . . . . . . 8 ⟂G ⟂G ≤G
5150ord 379 . . . . . . 7 ⟂G ⟂G ≤G
5247, 51mpd 15 . . . . . 6 ⟂G ⟂G ≤G
5348simprd 465 . . . . . 6 ⟂G ⟂G ≤G
54 simpr 463 . . . . . 6 ⟂G ⟂G ≤G ≤G
553, 4, 5, 6, 21, 7, 24, 28, 31, 33, 34, 35, 42, 46, 52, 53, 54mideulem 24770 . . . . 5 ⟂G ⟂G ≤G
5620ad4antr 737 . . . . . . . . 9 ⟂G ⟂G ≤G TarskiG
5756adantr 467 . . . . . . . 8 ⟂G ⟂G ≤G TarskiG
58 simprl 763 . . . . . . . 8 ⟂G ⟂G ≤G
59 eqid 2423 . . . . . . . 8
6027ad4antr 737 . . . . . . . . 9 ⟂G ⟂G ≤G
6160adantr 467 . . . . . . . 8 ⟂G ⟂G ≤G
62 simprr 765 . . . . . . . . 9 ⟂G ⟂G ≤G
6362eqcomd 2431 . . . . . . . 8 ⟂G ⟂G ≤G
643, 4, 5, 6, 7, 57, 58, 59, 61, 63mircom 24700 . . . . . . 7 ⟂G ⟂G ≤G
6564eqcomd 2431 . . . . . 6 ⟂G ⟂G ≤G
6623ad4antr 737 . . . . . . 7 ⟂G ⟂G ≤G
6730ad4antr 737 . . . . . . . 8 ⟂G ⟂G ≤G
6867necomd 2696 . . . . . . 7 ⟂G ⟂G ≤G
69 simp-4r 776 . . . . . . 7 ⟂G ⟂G ≤G
7032ad4antr 737 . . . . . . 7 ⟂G ⟂G ≤G
71 simpllr 768 . . . . . . 7 ⟂G ⟂G ≤G
72 simplr 761 . . . . . . . . . . . . . 14 ⟂G ⟂G ≤G ⟂G
7372simpld 461 . . . . . . . . . . . . 13 ⟂G ⟂G ≤G ⟂G
746, 56, 73perpln1 24747 . . . . . . . . . . . 12 ⟂G ⟂G ≤G
753, 5, 6, 56, 66, 69, 74tglnne 24665 . . . . . . . . . . 11 ⟂G ⟂G ≤G
763, 5, 6, 56, 66, 69, 75tglinecom 24672 . . . . . . . . . 10 ⟂G ⟂G ≤G
7776eqcomd 2431 . . . . . . . . 9 ⟂G ⟂G ≤G
7877, 74eqeltrd 2511 . . . . . . . 8 ⟂G ⟂G ≤G
793, 5, 6, 56, 60, 66, 68tgelrnln 24667 . . . . . . . 8 ⟂G ⟂G ≤G
803, 5, 6, 56, 66, 60, 67tglinecom 24672 . . . . . . . . 9 ⟂G ⟂G ≤G
8173, 76, 803brtr3d 4451 . . . . . . . 8 ⟂G ⟂G ≤G ⟂G
823, 4, 5, 6, 56, 78, 79, 81perpcom 24750 . . . . . . 7 ⟂G ⟂G ≤G ⟂G
83 simp-5r 778 . . . . . . . . 9 ⟂G ⟂G ≤G ⟂G
846, 56, 83perpln1 24747 . . . . . . . 8 ⟂G ⟂G ≤G
8583, 80breqtrd 4446 . . . . . . . 8 ⟂G ⟂G ≤G ⟂G
863, 4, 5, 6, 56, 84, 79, 85perpcom 24750 . . . . . . 7 ⟂G ⟂G ≤G ⟂G
8767neneqd 2626 . . . . . . . . 9 ⟂G ⟂G ≤G
8872simprd 465 . . . . . . . . . . . 12 ⟂G ⟂G ≤G
8988simpld 461 . . . . . . . . . . 11 ⟂G ⟂G ≤G
9089orcomd 390 . . . . . . . . . 10 ⟂G ⟂G ≤G
9190ord 379 . . . . . . . . 9 ⟂G ⟂G ≤G
9287, 91mpd 15 . . . . . . . 8 ⟂G ⟂G ≤G
9392, 80eleqtrd 2513 . . . . . . 7 ⟂G ⟂G ≤G
9488simprd 465 . . . . . . . 8 ⟂G ⟂G ≤G
953, 4, 5, 56, 70, 71, 69, 94tgbtwncom 24524 . . . . . . 7 ⟂G ⟂G ≤G
96 simpr 463 . . . . . . 7 ⟂G ⟂G ≤G ≤G
973, 4, 5, 6, 56, 7, 60, 66, 68, 69, 70, 71, 82, 86, 93, 95, 96mideulem 24770 . . . . . 6 ⟂G ⟂G ≤G
9865, 97reximddv 2902 . . . . 5 ⟂G ⟂G ≤G
99 eqid 2423 . . . . . 6 ≤G ≤G
10020ad3antrrr 735 . . . . . 6 ⟂G ⟂G TarskiG
10123ad3antrrr 735 . . . . . 6 ⟂G ⟂G
102 simpllr 768 . . . . . 6 ⟂G ⟂G
10327ad3antrrr 735 . . . . . 6 ⟂G ⟂G
10432ad3antrrr 735 . . . . . 6 ⟂G ⟂G
1053, 4, 5, 99, 100, 101, 102, 103, 104legtrid 24628 . . . . 5 ⟂G ⟂G ≤G ≤G
10655, 98, 105mpjaodan 794 . . . 4 ⟂G ⟂G
107 mideu.3 . . . . . . . 8 DimTarskiG
108107adantr 467 . . . . . . 7 DimTarskiG
109108ad2antrr 731 . . . . . 6 ⟂G DimTarskiG
1103, 4, 5, 6, 20, 23, 27, 32, 30, 109colperpex 24767 . . . . 5 ⟂G ⟂G
111 r19.42v 2984 . . . . . 6 ⟂G ⟂G
112111rexbii 2928 . . . . 5 ⟂G ⟂G
113110, 112sylibr 216 . . . 4 ⟂G ⟂G
114106, 113r19.29vva 2973 . . 3 ⟂G
11529necomd 2696 . . . . 5
1163, 4, 5, 6, 19, 26, 22, 22, 115, 108colperpex 24767 . . . 4 ⟂G
117 simprl 763 . . . . . . 7 ⟂G ⟂G
1183, 5, 6, 19, 22, 26, 29tglinecom 24672 . . . . . . . 8
119118adantr 467 . . . . . . 7 ⟂G
120117, 119breqtrrd 4448 . . . . . 6 ⟂G ⟂G
121120ex 436 . . . . 5 ⟂G ⟂G
122121reximdv 2900 . . . 4 ⟂G ⟂G
123116, 122mpd 15 . . 3 ⟂G
124114, 123r19.29a 2971 . 2
12518, 124pm2.61dane 2743 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 370   wa 371   wceq 1438   wcel 1869   wne 2619  wrex 2777   class class class wbr 4421   crn 4852  cfv 5599  (class class class)co 6303  c2 10661  cbs 15114  cds 15192  TarskiGcstrkg 24470  DimTarskiG≥cstrkgld 24474  Itvcitv 24476  LineGclng 24477  ≤Gcleg 24619  pInvGcmir 24689  ⟂Gcperpg 24732 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-card 8376  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-nn 10612  df-2 10670  df-3 10671  df-n0 10872  df-z 10940  df-uz 11162  df-fz 11787  df-fzo 11918  df-hash 12517  df-word 12662  df-concat 12664  df-s1 12665  df-s2 12940  df-s3 12941  df-trkgc 24488  df-trkgb 24489  df-trkgcb 24490  df-trkgld 24492  df-trkg 24493  df-cgrg 24548  df-leg 24620  df-mir 24690  df-rag 24731  df-perpg 24733 This theorem is referenced by:  mideu  24772  opphllem5  24785  opphl  24788
 Copyright terms: Public domain W3C validator