Metamath Proof Explorer


Theorem mirmir2

Description: Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019)

Ref Expression
Hypotheses mirval.p
|- P = ( Base ` G )
mirval.d
|- .- = ( dist ` G )
mirval.i
|- I = ( Itv ` G )
mirval.l
|- L = ( LineG ` G )
mirval.s
|- S = ( pInvG ` G )
mirval.g
|- ( ph -> G e. TarskiG )
mirval.a
|- ( ph -> A e. P )
mirfv.m
|- M = ( S ` A )
miriso.1
|- ( ph -> X e. P )
miriso.2
|- ( ph -> Y e. P )
Assertion mirmir2
|- ( ph -> ( M ` ( ( S ` Y ) ` X ) ) = ( ( S ` ( M ` Y ) ) ` ( M ` X ) ) )

Proof

Step Hyp Ref Expression
1 mirval.p
 |-  P = ( Base ` G )
2 mirval.d
 |-  .- = ( dist ` G )
3 mirval.i
 |-  I = ( Itv ` G )
4 mirval.l
 |-  L = ( LineG ` G )
5 mirval.s
 |-  S = ( pInvG ` G )
6 mirval.g
 |-  ( ph -> G e. TarskiG )
7 mirval.a
 |-  ( ph -> A e. P )
8 mirfv.m
 |-  M = ( S ` A )
9 miriso.1
 |-  ( ph -> X e. P )
10 miriso.2
 |-  ( ph -> Y e. P )
11 1 2 3 4 5 6 7 8 10 mircl
 |-  ( ph -> ( M ` Y ) e. P )
12 eqid
 |-  ( S ` ( M ` Y ) ) = ( S ` ( M ` Y ) )
13 1 2 3 4 5 6 7 8 9 mircl
 |-  ( ph -> ( M ` X ) e. P )
14 eqid
 |-  ( S ` Y ) = ( S ` Y )
15 1 2 3 4 5 6 10 14 9 mircl
 |-  ( ph -> ( ( S ` Y ) ` X ) e. P )
16 1 2 3 4 5 6 7 8 15 mircl
 |-  ( ph -> ( M ` ( ( S ` Y ) ` X ) ) e. P )
17 1 2 3 4 5 6 10 14 9 mircgr
 |-  ( ph -> ( Y .- ( ( S ` Y ) ` X ) ) = ( Y .- X ) )
18 1 2 3 4 5 6 7 8 10 15 10 9 17 mircgrs
 |-  ( ph -> ( ( M ` Y ) .- ( M ` ( ( S ` Y ) ` X ) ) ) = ( ( M ` Y ) .- ( M ` X ) ) )
19 1 2 3 4 5 6 10 14 9 mirbtwn
 |-  ( ph -> Y e. ( ( ( S ` Y ) ` X ) I X ) )
20 1 2 3 4 5 6 7 8 15 10 9 19 mirbtwni
 |-  ( ph -> ( M ` Y ) e. ( ( M ` ( ( S ` Y ) ` X ) ) I ( M ` X ) ) )
21 1 2 3 4 5 6 11 12 13 16 18 20 ismir
 |-  ( ph -> ( M ` ( ( S ` Y ) ` X ) ) = ( ( S ` ( M ` Y ) ) ` ( M ` X ) ) )