Metamath Proof Explorer

Theorem ismidb

Description: Property of the midpoint. (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 )
midcl.1 
|- ( ph -> A e. P )
midcl.2 
|- ( ph -> B e. P )
ismidb.s 
|- S = ( pInvG ` G )
ismidb.m 
|- ( ph -> M e. P )
Assertion ismidb 
|- ( ph -> ( B = ( ( S ` M ) ` A ) <-> ( A ( midG ` G ) B ) = M ) )

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 midcl.1 
 |-  ( ph -> A e. P )
7 midcl.2 
 |-  ( ph -> B e. P )
8 ismidb.s 
 |-  S = ( pInvG ` G )
9 ismidb.m 
 |-  ( ph -> M e. P )
10 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
11 1 2 3 10 4 8 6 7 5 mideu 
 |-  ( ph -> E! m e. P B = ( ( S ` m ) ` A ) )
12 fveq2 
 |-  ( m = M -> ( S ` m ) = ( S ` M ) )
13 12 fveq1d 
 |-  ( m = M -> ( ( S ` m ) ` A ) = ( ( S ` M ) ` A ) )
14 13 eqeq2d 
 |-  ( m = M -> ( B = ( ( S ` m ) ` A ) <-> B = ( ( S ` M ) ` A ) ) )
15 14 riota2 
 |-  ( ( M e. P /\ E! m e. P B = ( ( S ` m ) ` A ) ) -> ( B = ( ( S ` M ) ` A ) <-> ( iota_ m e. P B = ( ( S ` m ) ` A ) ) = M ) )
16 9 11 15 syl2anc 
 |-  ( ph -> ( B = ( ( S ` M ) ` A ) <-> ( iota_ m e. P B = ( ( S ` m ) ` A ) ) = M ) )
17 df-mid 
 |-  midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) ) )
18 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
19 18 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
20 fveq2 
 |-  ( g = G -> ( pInvG ` g ) = ( pInvG ` G ) )
21 20 8 eqtr4di 
 |-  ( g = G -> ( pInvG ` g ) = S )
22 21 fveq1d 
 |-  ( g = G -> ( ( pInvG ` g ) ` m ) = ( S ` m ) )
23 22 fveq1d 
 |-  ( g = G -> ( ( ( pInvG ` g ) ` m ) ` a ) = ( ( S ` m ) ` a ) )
24 23 eqeq2d 
 |-  ( g = G -> ( b = ( ( ( pInvG ` g ) ` m ) ` a ) <-> b = ( ( S ` m ) ` a ) ) )
25 19 24 riotaeqbidv 
 |-  ( g = G -> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) = ( iota_ m e. P b = ( ( S ` m ) ` a ) ) )
26 19 19 25 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 = ( ( S ` m ) ` a ) ) ) )
27 4 elexd 
 |-  ( ph -> G e. _V )
28 1 fvexi 
 |-  P e. _V
29 28 28 mpoex 
 |-  ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( S ` m ) ` a ) ) ) e. _V
30 29 a1i 
 |-  ( ph -> ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( S ` m ) ` a ) ) ) e. _V )
31 17 26 27 30 fvmptd3 
 |-  ( ph -> ( midG ` G ) = ( a e. P , b e. P |-> ( iota_ m e. P b = ( ( S ` m ) ` a ) ) ) )
32 simprr 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> b = B )
33 simprl 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> a = A )
34 33 fveq2d 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ( ( S ` m ) ` a ) = ( ( S ` m ) ` A ) )
35 32 34 eqeq12d 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ( b = ( ( S ` m ) ` a ) <-> B = ( ( S ` m ) ` A ) ) )
36 35 riotabidv 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ( iota_ m e. P b = ( ( S ` m ) ` a ) ) = ( iota_ m e. P B = ( ( S ` m ) ` A ) ) )
37 riotacl 
 |-  ( E! m e. P B = ( ( S ` m ) ` A ) -> ( iota_ m e. P B = ( ( S ` m ) ` A ) ) e. P )
38 11 37 syl 
 |-  ( ph -> ( iota_ m e. P B = ( ( S ` m ) ` A ) ) e. P )
39 31 36 6 7 38 ovmpod 
 |-  ( ph -> ( A ( midG ` G ) B ) = ( iota_ m e. P B = ( ( S ` m ) ` A ) ) )
40 39 eqeq1d 
 |-  ( ph -> ( ( A ( midG ` G ) B ) = M <-> ( iota_ m e. P B = ( ( S ` m ) ` A ) ) = M ) )
41 16 40 bitr4d 
 |-  ( ph -> ( B = ( ( S ` M ) ` A ) <-> ( A ( midG ` G ) B ) = M ) )