Metamath Proof Explorer

Theorem motcgrg

Description: Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses ismot.p 
|- P = ( Base ` G )
ismot.m 
|- .- = ( dist ` G )
motgrp.1 
|- ( ph -> G e. V )
motgrp.i 
|- I = { <. ( Base ` ndx ) , ( G Ismt G ) >. , <. ( +g ` ndx ) , ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) >. }
motcgrg.r 
|- .~ = ( cgrG ` G )
motcgrg.t 
|- ( ph -> T e. Word P )
motcgrg.f 
|- ( ph -> F e. ( G Ismt G ) )
Assertion motcgrg 
|- ( ph -> ( F o. T ) .~ T )

Proof

Step Hyp Ref Expression
1 ismot.p 
 |-  P = ( Base ` G )
2 ismot.m 
 |-  .- = ( dist ` G )
3 motgrp.1 
 |-  ( ph -> G e. V )
4 motgrp.i 
 |-  I = { <. ( Base ` ndx ) , ( G Ismt G ) >. , <. ( +g ` ndx ) , ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) >. }
5 motcgrg.r 
 |-  .~ = ( cgrG ` G )
6 motcgrg.t 
 |-  ( ph -> T e. Word P )
7 motcgrg.f 
 |-  ( ph -> F e. ( G Ismt G ) )
8 simpr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> T : ( 0 ..^ n ) --> P )
9 8 adantr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> T : ( 0 ..^ n ) --> P )
10 simprl 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> a e. dom ( F o. T ) )
11 1 2 3 7 motf1o 
 |-  ( ph -> F : P -1-1-onto-> P )
12 f1of 
 |-  ( F : P -1-1-onto-> P -> F : P --> P )
13 11 12 syl 
 |-  ( ph -> F : P --> P )
14 13 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> F : P --> P )
15 fco 
 |-  ( ( F : P --> P /\ T : ( 0 ..^ n ) --> P ) -> ( F o. T ) : ( 0 ..^ n ) --> P )
16 14 8 15 syl2anc 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> ( F o. T ) : ( 0 ..^ n ) --> P )
17 16 adantr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( F o. T ) : ( 0 ..^ n ) --> P )
18 17 fdmd 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> dom ( F o. T ) = ( 0 ..^ n ) )
19 10 18 eleqtrd 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> a e. ( 0 ..^ n ) )
20 fvco3 
 |-  ( ( T : ( 0 ..^ n ) --> P /\ a e. ( 0 ..^ n ) ) -> ( ( F o. T ) ` a ) = ( F ` ( T ` a ) ) )
21 9 19 20 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( ( F o. T ) ` a ) = ( F ` ( T ` a ) ) )
22 simprr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> b e. dom ( F o. T ) )
23 22 18 eleqtrd 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> b e. ( 0 ..^ n ) )
24 fvco3 
 |-  ( ( T : ( 0 ..^ n ) --> P /\ b e. ( 0 ..^ n ) ) -> ( ( F o. T ) ` b ) = ( F ` ( T ` b ) ) )
25 9 23 24 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( ( F o. T ) ` b ) = ( F ` ( T ` b ) ) )
26 21 25 oveq12d 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( ( ( F o. T ) ` a ) .- ( ( F o. T ) ` b ) ) = ( ( F ` ( T ` a ) ) .- ( F ` ( T ` b ) ) ) )
27 3 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> G e. V )
28 27 adantr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> G e. V )
29 9 19 ffvelrnd 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( T ` a ) e. P )
30 9 23 ffvelrnd 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( T ` b ) e. P )
31 7 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> F e. ( G Ismt G ) )
32 1 2 28 29 30 31 motcgr 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( ( F ` ( T ` a ) ) .- ( F ` ( T ` b ) ) ) = ( ( T ` a ) .- ( T ` b ) ) )
33 26 32 eqtrd 
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) /\ ( a e. dom ( F o. T ) /\ b e. dom ( F o. T ) ) ) -> ( ( ( F o. T ) ` a ) .- ( ( F o. T ) ` b ) ) = ( ( T ` a ) .- ( T ` b ) ) )
34 33 ralrimivva 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> A. a e. dom ( F o. T ) A. b e. dom ( F o. T ) ( ( ( F o. T ) ` a ) .- ( ( F o. T ) ` b ) ) = ( ( T ` a ) .- ( T ` b ) ) )
35 fzo0ssnn0 
 |-  ( 0 ..^ n ) C_ NN0
36 nn0ssre 
 |-  NN0 C_ RR
37 35 36 sstri 
 |-  ( 0 ..^ n ) C_ RR
38 37 a1i 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> ( 0 ..^ n ) C_ RR )
39 1 2 5 27 38 16 8 iscgrgd 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> ( ( F o. T ) .~ T <-> A. a e. dom ( F o. T ) A. b e. dom ( F o. T ) ( ( ( F o. T ) ` a ) .- ( ( F o. T ) ` b ) ) = ( ( T ` a ) .- ( T ` b ) ) ) )
40 34 39 mpbird 
 |-  ( ( ( ph /\ n e. NN0 ) /\ T : ( 0 ..^ n ) --> P ) -> ( F o. T ) .~ T )
41 iswrd 
 |-  ( T e. Word P <-> E. n e. NN0 T : ( 0 ..^ n ) --> P )
42 6 41 sylib 
 |-  ( ph -> E. n e. NN0 T : ( 0 ..^ n ) --> P )
43 40 42 r19.29a 
 |-  ( ph -> ( F o. T ) .~ T )