Metamath Proof Explorer


Theorem motcl

Description: Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses ismot.p 𝑃 = ( Base ‘ 𝐺 )
ismot.m = ( dist ‘ 𝐺 )
motgrp.1 ( 𝜑𝐺𝑉 )
motco.2 ( 𝜑𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
motcl.a ( 𝜑𝐴𝑃 )
Assertion motcl ( 𝜑 → ( 𝐹𝐴 ) ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 ismot.p 𝑃 = ( Base ‘ 𝐺 )
2 ismot.m = ( dist ‘ 𝐺 )
3 motgrp.1 ( 𝜑𝐺𝑉 )
4 motco.2 ( 𝜑𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
5 motcl.a ( 𝜑𝐴𝑃 )
6 1 2 3 4 motf1o ( 𝜑𝐹 : 𝑃1-1-onto𝑃 )
7 f1of ( 𝐹 : 𝑃1-1-onto𝑃𝐹 : 𝑃𝑃 )
8 6 7 syl ( 𝜑𝐹 : 𝑃𝑃 )
9 8 5 ffvelrnd ( 𝜑 → ( 𝐹𝐴 ) ∈ 𝑃 )