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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ismot.m	⊢ − = ( dist ‘ 𝐺 )
Assertion	ismot	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ismot.m	⊢ − = ( dist ‘ 𝐺 )
3	1 1 2 2	isismt	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
4	3	anidms	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )