Metamath Proof Explorer


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𝑃 )