Metamath Proof Explorer

Theorem mirauto

Description: Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-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 )
mirauto.m 
|- M = ( S ` T )
mirauto.x 
|- X = ( M ` A )
mirauto.y 
|- Y = ( M ` B )
mirauto.z 
|- Z = ( M ` C )
mirauto.0 
|- ( ph -> T e. P )
mirauto.1 
|- ( ph -> A e. P )
mirauto.2 
|- ( ph -> B e. P )
mirauto.3 
|- ( ph -> C e. P )
mirauto.4 
|- ( ph -> ( ( S ` A ) ` B ) = C )
Assertion mirauto 
|- ( ph -> ( ( S ` X ) ` Y ) = Z )

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 mirauto.m 
 |-  M = ( S ` T )
8 mirauto.x 
 |-  X = ( M ` A )
9 mirauto.y 
 |-  Y = ( M ` B )
10 mirauto.z 
 |-  Z = ( M ` C )
11 mirauto.0 
 |-  ( ph -> T e. P )
12 mirauto.1 
 |-  ( ph -> A e. P )
13 mirauto.2 
 |-  ( ph -> B e. P )
14 mirauto.3 
 |-  ( ph -> C e. P )
15 mirauto.4 
 |-  ( ph -> ( ( S ` A ) ` B ) = C )
16 1 2 3 4 5 6 11 7 mirf 
 |-  ( ph -> M : P --> P )
17 16 12 ffvelrnd 
 |-  ( ph -> ( M ` A ) e. P )
18 8 17 eqeltrid 
 |-  ( ph -> X e. P )
19 eqid 
 |-  ( S ` X ) = ( S ` X )
20 16 13 ffvelrnd 
 |-  ( ph -> ( M ` B ) e. P )
21 9 20 eqeltrid 
 |-  ( ph -> Y e. P )
22 16 14 ffvelrnd 
 |-  ( ph -> ( M ` C ) e. P )
23 10 22 eqeltrid 
 |-  ( ph -> Z e. P )
24 15 14 eqeltrd 
 |-  ( ph -> ( ( S ` A ) ` B ) e. P )
25 eqid 
 |-  ( S ` A ) = ( S ` A )
26 1 2 3 4 5 6 12 25 13 mircgr 
 |-  ( ph -> ( A .- ( ( S ` A ) ` B ) ) = ( A .- B ) )
27 1 2 3 4 5 6 11 7 12 24 12 13 26 mircgrs 
 |-  ( ph -> ( ( M ` A ) .- ( M ` ( ( S ` A ) ` B ) ) ) = ( ( M ` A ) .- ( M ` B ) ) )
28 8 a1i 
 |-  ( ph -> X = ( M ` A ) )
29 15 fveq2d 
 |-  ( ph -> ( M ` ( ( S ` A ) ` B ) ) = ( M ` C ) )
30 10 29 eqtr4id 
 |-  ( ph -> Z = ( M ` ( ( S ` A ) ` B ) ) )
31 28 30 oveq12d 
 |-  ( ph -> ( X .- Z ) = ( ( M ` A ) .- ( M ` ( ( S ` A ) ` B ) ) ) )
32 8 9 oveq12i 
 |-  ( X .- Y ) = ( ( M ` A ) .- ( M ` B ) )
33 32 a1i 
 |-  ( ph -> ( X .- Y ) = ( ( M ` A ) .- ( M ` B ) ) )
34 27 31 33 3eqtr4d 
 |-  ( ph -> ( X .- Z ) = ( X .- Y ) )
35 1 2 3 4 5 6 12 25 13 mirbtwn 
 |-  ( ph -> A e. ( ( ( S ` A ) ` B ) I B ) )
36 15 oveq1d 
 |-  ( ph -> ( ( ( S ` A ) ` B ) I B ) = ( C I B ) )
37 35 36 eleqtrd 
 |-  ( ph -> A e. ( C I B ) )
38 1 2 3 4 5 6 11 7 14 12 13 37 mirbtwni 
 |-  ( ph -> ( M ` A ) e. ( ( M ` C ) I ( M ` B ) ) )
39 10 9 oveq12i 
 |-  ( Z I Y ) = ( ( M ` C ) I ( M ` B ) )
40 38 8 39 3eltr4g 
 |-  ( ph -> X e. ( Z I Y ) )
41 1 2 3 4 5 6 18 19 21 23 34 40 ismir 
 |-  ( ph -> Z = ( ( S ` X ) ` Y ) )
42 41 eqcomd 
 |-  ( ph -> ( ( S ` X ) ` Y ) = Z )