Metamath Proof Explorer

Theorem mirmid

Description: Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-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 )
mirmid.s 
|- S = ( ( pInvG ` G ) ` M )
mirmid.x 
|- ( ph -> M e. P )
Assertion mirmid 
|- ( ph -> ( ( S ` A ) ( midG ` G ) ( S ` B ) ) = ( S ` ( A ( midG ` G ) B ) ) )

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 mirmid.s 
 |-  S = ( ( pInvG ` G ) ` M )
9 mirmid.x 
 |-  ( ph -> M e. P )
10 eqidd 
 |-  ( ph -> ( A ( midG ` G ) B ) = ( A ( midG ` G ) B ) )
11 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
12 1 2 3 4 5 6 7 midcl 
 |-  ( ph -> ( A ( midG ` G ) B ) e. P )
13 1 2 3 4 5 6 7 11 12 ismidb 
 |-  ( ph -> ( B = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) <-> ( A ( midG ` G ) B ) = ( A ( midG ` G ) B ) ) )
14 10 13 mpbird 
 |-  ( ph -> B = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) )
15 14 fveq2d 
 |-  ( ph -> ( S ` B ) = ( S ` ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) ) )
16 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
17 1 2 3 16 11 4 9 8 6 12 mirmir2 
 |-  ( ph -> ( S ` ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) ) = ( ( ( pInvG ` G ) ` ( S ` ( A ( midG ` G ) B ) ) ) ` ( S ` A ) ) )
18 15 17 eqtrd 
 |-  ( ph -> ( S ` B ) = ( ( ( pInvG ` G ) ` ( S ` ( A ( midG ` G ) B ) ) ) ` ( S ` A ) ) )
19 1 2 3 16 11 4 9 8 6 mircl 
 |-  ( ph -> ( S ` A ) e. P )
20 1 2 3 16 11 4 9 8 7 mircl 
 |-  ( ph -> ( S ` B ) e. P )
21 1 2 3 16 11 4 9 8 12 mircl 
 |-  ( ph -> ( S ` ( A ( midG ` G ) B ) ) e. P )
22 1 2 3 4 5 19 20 11 21 ismidb 
 |-  ( ph -> ( ( S ` B ) = ( ( ( pInvG ` G ) ` ( S ` ( A ( midG ` G ) B ) ) ) ` ( S ` A ) ) <-> ( ( S ` A ) ( midG ` G ) ( S ` B ) ) = ( S ` ( A ( midG ` G ) B ) ) ) )
23 18 22 mpbid 
 |-  ( ph -> ( ( S ` A ) ( midG ` G ) ( S ` B ) ) = ( S ` ( A ( midG ` G ) B ) ) )