Metamath Proof Explorer

Theorem cnvmot

Description: The converse of a motion is a motion. (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 )
motco.2 
|- ( ph -> F e. ( G Ismt G ) )
Assertion cnvmot 
|- ( ph -> `' F e. ( G Ismt G ) )

Proof

Step Hyp Ref Expression
1 ismot.p 
 |-  P = ( Base ` G )
2 ismot.m 
 |-  .- = ( dist ` G )
3 motgrp.1 
 |-  ( ph -> G e. V )
4 motco.2 
 |-  ( ph -> F e. ( G Ismt G ) )
5 1 2 3 4 motf1o 
 |-  ( ph -> F : P -1-1-onto-> P )
6 f1ocnv 
 |-  ( F : P -1-1-onto-> P -> `' F : P -1-1-onto-> P )
7 5 6 syl 
 |-  ( ph -> `' F : P -1-1-onto-> P )
8 3 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> G e. V )
9 f1of 
 |-  ( `' F : P -1-1-onto-> P -> `' F : P --> P )
10 7 9 syl 
 |-  ( ph -> `' F : P --> P )
11 10 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> `' F : P --> P )
12 simprl 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> a e. P )
13 11 12 ffvelrnd 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( `' F ` a ) e. P )
14 simprr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> b e. P )
15 11 14 ffvelrnd 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( `' F ` b ) e. P )
16 4 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> F e. ( G Ismt G ) )
17 1 2 8 13 15 16 motcgr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F ` ( `' F ` a ) ) .- ( F ` ( `' F ` b ) ) ) = ( ( `' F ` a ) .- ( `' F ` b ) ) )
18 f1ocnvfv2 
 |-  ( ( F : P -1-1-onto-> P /\ a e. P ) -> ( F ` ( `' F ` a ) ) = a )
19 5 12 18 syl2an2r 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( F ` ( `' F ` a ) ) = a )
20 f1ocnvfv2 
 |-  ( ( F : P -1-1-onto-> P /\ b e. P ) -> ( F ` ( `' F ` b ) ) = b )
21 5 14 20 syl2an2r 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( F ` ( `' F ` b ) ) = b )
22 19 21 oveq12d 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F ` ( `' F ` a ) ) .- ( F ` ( `' F ` b ) ) ) = ( a .- b ) )
23 17 22 eqtr3d 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( `' F ` a ) .- ( `' F ` b ) ) = ( a .- b ) )
24 23 ralrimivva 
 |-  ( ph -> A. a e. P A. b e. P ( ( `' F ` a ) .- ( `' F ` b ) ) = ( a .- b ) )
25 1 2 ismot 
 |-  ( G e. V -> ( `' F e. ( G Ismt G ) <-> ( `' F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( `' F ` a ) .- ( `' F ` b ) ) = ( a .- b ) ) ) )
26 3 25 syl 
 |-  ( ph -> ( `' F e. ( G Ismt G ) <-> ( `' F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( `' F ` a ) .- ( `' F ` b ) ) = ( a .- b ) ) ) )
27 7 24 26 mpbir2and 
 |-  ( ph -> `' F e. ( G Ismt G ) )