Theorem motcl

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

	Ref	Expression
Hypotheses	ismot.p	|- P = ( Base ` G )
	ismot.m	|- .- = ( dist ` G )
	motgrp.1	|- ( ph -> G e. V )
	motco.2	|- ( ph -> F e. ( G Ismt G ) )
	motcl.a	|- ( ph -> A e. P )
Assertion	motcl	|- ( ph -> ( F ` A ) e. P )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	|- P = ( Base ` G )
2		ismot.m	|- .- = ( dist ` G )
3		motgrp.1	|- ( ph -> G e. V )
4		motco.2	|- ( ph -> F e. ( G Ismt G ) )
5		motcl.a	|- ( ph -> A e. P )
6	1 2 3 4	motf1o	|- ( ph -> F : P -1-1-onto-> P )
7		f1of	|- ( F : P -1-1-onto-> P -> F : P --> P )
8	6 7	syl	|- ( ph -> F : P --> P )
9	8 5	ffvelrnd	|- ( ph -> ( F ` A ) e. P )