Metamath Proof Explorer

Theorem midf

Description: Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses ismid.p 
|- P = ( Base ` G )
ismid.d 
|- .- = ( dist ` G )
ismid.i 
|- I = ( Itv ` G )
ismid.g 
|- ( ph -> G e. TarskiG )
ismid.1 
|- ( ph -> G TarskiGDim>= 2 )
Assertion midf 
|- ( ph -> ( midG ` G ) : ( P X. P ) --> P )

Proof

Step Hyp Ref Expression
1 ismid.p 
 |-  P = ( Base ` G )
2 ismid.d 
 |-  .- = ( dist ` G )
3 ismid.i 
 |-  I = ( Itv ` G )
4 ismid.g 
 |-  ( ph -> G e. TarskiG )
5 ismid.1 
 |-  ( ph -> G TarskiGDim>= 2 )
6 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
7 4 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> G e. TarskiG )
8 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
9 simprl 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> a e. P )
10 simprr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> b e. P )
11 5 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> G TarskiGDim>= 2 )
12 1 2 3 6 7 8 9 10 11 mideu 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> E! m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) )
13 12 ralrimivva 
 |-  ( ph -> A. a e. P A. b e. P E! m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) )
14 riotacl 
 |-  ( E! m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) -> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) e. P )
15 14 2ralimi 
 |-  ( A. a e. P A. b e. P E! m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) -> A. a e. P A. b e. P ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) e. P )
16 13 15 syl 
 |-  ( ph -> A. a e. P A. b e. P ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) e. P )
17 eqid 
 |-  ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) = ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) )
18 17 fmpo 
 |-  ( A. a e. P A. b e. P ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) e. P <-> ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) : ( P X. P ) --> P )
19 16 18 sylib 
 |-  ( ph -> ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) : ( P X. P ) --> P )
20 df-mid 
 |-  midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) ) )
21 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
22 21 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
23 fveq2 
 |-  ( g = G -> ( pInvG ` g ) = ( pInvG ` G ) )
24 23 fveq1d 
 |-  ( g = G -> ( ( pInvG ` g ) ` m ) = ( ( pInvG ` G ) ` m ) )
25 24 fveq1d 
 |-  ( g = G -> ( ( ( pInvG ` g ) ` m ) ` a ) = ( ( ( pInvG ` G ) ` m ) ` a ) )
26 25 eqeq2d 
 |-  ( g = G -> ( b = ( ( ( pInvG ` g ) ` m ) ` a ) <-> b = ( ( ( pInvG ` G ) ` m ) ` a ) ) )
27 22 26 riotaeqbidv 
 |-  ( g = G -> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) = ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) )
28 22 22 27 mpoeq123dv 
 |-  ( g = G -> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) ) = ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) )
29 4 elexd 
 |-  ( ph -> G e. _V )
30 1 fvexi 
 |-  P e. _V
31 30 30 mpoex 
 |-  ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) e. _V
32 31 a1i 
 |-  ( ph -> ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) e. _V )
33 20 28 29 32 fvmptd3 
 |-  ( ph -> ( midG ` G ) = ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) )
34 33 feq1d 
 |-  ( ph -> ( ( midG ` G ) : ( P X. P ) --> P <-> ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( ( pInvG ` G ) ` m ) ` a ) ) ) : ( P X. P ) --> P ) )
35 19 34 mpbird 
 |-  ( ph -> ( midG ` G ) : ( P X. P ) --> P )