Metamath Proof Explorer


Theorem motcl

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

Ref Expression
Hypotheses ismot.p P=BaseG
ismot.m -˙=distG
motgrp.1 φGV
motco.2 φFGIsmtG
motcl.a φAP
Assertion motcl φFAP

Proof

Step Hyp Ref Expression
1 ismot.p P=BaseG
2 ismot.m -˙=distG
3 motgrp.1 φGV
4 motco.2 φFGIsmtG
5 motcl.a φAP
6 1 2 3 4 motf1o φF:P1-1 ontoP
7 f1of F:P1-1 ontoPF:PP
8 6 7 syl φF:PP
9 8 5 ffvelcdmd φFAP