Theorem ismot

Description: Property of being an isometry mapping to the same space. In geometry, this is also called a motion. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	ismot.p	|- P = ( Base ` G )
	ismot.m	|- .- = ( dist ` G )
Assertion	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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	|- P = ( Base ` G )
2		ismot.m	|- .- = ( dist ` G )
3	1 1 2 2	isismt	|- ( ( G e. V /\ 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 ) ) ) )
4	3	anidms	|- ( 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 ) ) ) )