Theorem motf1o

Description: Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	ismot.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ismot.m	⊢ − = ( dist ‘ 𝐺 )
	motgrp.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	motco.2	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
Assertion	motf1o	⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ismot.m	⊢ − = ( dist ‘ 𝐺 )
3		motgrp.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4		motco.2	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
5	1 2	ismot	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
7	4 6	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) )
8	7	simpld	⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 )