Metamath Proof Explorer


Theorem ismidb

Description: Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses ismid.p P=BaseG
ismid.d -˙=distG
ismid.i I=ItvG
ismid.g φG𝒢Tarski
ismid.1 φGDim𝒢2
midcl.1 φAP
midcl.2 φBP
ismidb.s S=pInv𝒢G
ismidb.m φMP
Assertion ismidb φB=SMAAmid𝒢GB=M

Proof

Step Hyp Ref Expression
1 ismid.p P=BaseG
2 ismid.d -˙=distG
3 ismid.i I=ItvG
4 ismid.g φG𝒢Tarski
5 ismid.1 φGDim𝒢2
6 midcl.1 φAP
7 midcl.2 φBP
8 ismidb.s S=pInv𝒢G
9 ismidb.m φMP
10 eqid Line𝒢G=Line𝒢G
11 1 2 3 10 4 8 6 7 5 mideu φ∃!mPB=SmA
12 fveq2 m=MSm=SM
13 12 fveq1d m=MSmA=SMA
14 13 eqeq2d m=MB=SmAB=SMA
15 14 riota2 MP∃!mPB=SmAB=SMAιmP|B=SmA=M
16 9 11 15 syl2anc φB=SMAιmP|B=SmA=M
17 df-mid mid𝒢=gVaBaseg,bBasegιmBaseg|b=pInv𝒢gma
18 fveq2 g=GBaseg=BaseG
19 18 1 eqtr4di g=GBaseg=P
20 fveq2 g=GpInv𝒢g=pInv𝒢G
21 20 8 eqtr4di g=GpInv𝒢g=S
22 21 fveq1d g=GpInv𝒢gm=Sm
23 22 fveq1d g=GpInv𝒢gma=Sma
24 23 eqeq2d g=Gb=pInv𝒢gmab=Sma
25 19 24 riotaeqbidv g=GιmBaseg|b=pInv𝒢gma=ιmP|b=Sma
26 19 19 25 mpoeq123dv g=GaBaseg,bBasegιmBaseg|b=pInv𝒢gma=aP,bPιmP|b=Sma
27 4 elexd φGV
28 1 fvexi PV
29 28 28 mpoex aP,bPιmP|b=SmaV
30 29 a1i φaP,bPιmP|b=SmaV
31 17 26 27 30 fvmptd3 φmid𝒢G=aP,bPιmP|b=Sma
32 simprr φa=Ab=Bb=B
33 simprl φa=Ab=Ba=A
34 33 fveq2d φa=Ab=BSma=SmA
35 32 34 eqeq12d φa=Ab=Bb=SmaB=SmA
36 35 riotabidv φa=Ab=BιmP|b=Sma=ιmP|B=SmA
37 riotacl ∃!mPB=SmAιmP|B=SmAP
38 11 37 syl φιmP|B=SmAP
39 31 36 6 7 38 ovmpod φAmid𝒢GB=ιmP|B=SmA
40 39 eqeq1d φAmid𝒢GB=MιmP|B=SmA=M
41 16 40 bitr4d φB=SMAAmid𝒢GB=M