Metamath Proof Explorer


Theorem motgrp

Description: The motions of a geometry form a group with respect to function composition, called the Isometry group. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses ismot.p P=BaseG
ismot.m -˙=distG
motgrp.1 φGV
motgrp.i I=BasendxGIsmtG+ndxfGIsmtG,gGIsmtGfg
Assertion motgrp φIGrp

Proof

Step Hyp Ref Expression
1 ismot.p P=BaseG
2 ismot.m -˙=distG
3 motgrp.1 φGV
4 motgrp.i I=BasendxGIsmtG+ndxfGIsmtG,gGIsmtGfg
5 ovex GIsmtGV
6 4 grpbase GIsmtGVGIsmtG=BaseI
7 5 6 mp1i φGIsmtG=BaseI
8 eqidd φ+I=+I
9 3 3ad2ant1 φfGIsmtGgGIsmtGGV
10 simp2 φfGIsmtGgGIsmtGfGIsmtG
11 simp3 φfGIsmtGgGIsmtGgGIsmtG
12 1 2 9 4 10 11 motplusg φfGIsmtGgGIsmtGf+Ig=fg
13 1 2 9 10 11 motco φfGIsmtGgGIsmtGfgGIsmtG
14 12 13 eqeltrd φfGIsmtGgGIsmtGf+IgGIsmtG
15 coass fgh=fgh
16 12 3adant3r3 φfGIsmtGgGIsmtGhGIsmtGf+Ig=fg
17 16 oveq1d φfGIsmtGgGIsmtGhGIsmtGf+Ig+Ih=fg+Ih
18 3 adantr φfGIsmtGgGIsmtGhGIsmtGGV
19 13 3adant3r3 φfGIsmtGgGIsmtGhGIsmtGfgGIsmtG
20 simpr3 φfGIsmtGgGIsmtGhGIsmtGhGIsmtG
21 1 2 18 4 19 20 motplusg φfGIsmtGgGIsmtGhGIsmtGfg+Ih=fgh
22 17 21 eqtrd φfGIsmtGgGIsmtGhGIsmtGf+Ig+Ih=fgh
23 simpr2 φfGIsmtGgGIsmtGhGIsmtGgGIsmtG
24 1 2 18 4 23 20 motplusg φfGIsmtGgGIsmtGhGIsmtGg+Ih=gh
25 24 oveq2d φfGIsmtGgGIsmtGhGIsmtGf+Ig+Ih=f+Igh
26 simpr1 φfGIsmtGgGIsmtGhGIsmtGfGIsmtG
27 1 2 18 23 20 motco φfGIsmtGgGIsmtGhGIsmtGghGIsmtG
28 1 2 18 4 26 27 motplusg φfGIsmtGgGIsmtGhGIsmtGf+Igh=fgh
29 25 28 eqtrd φfGIsmtGgGIsmtGhGIsmtGf+Ig+Ih=fgh
30 15 22 29 3eqtr4a φfGIsmtGgGIsmtGhGIsmtGf+Ig+Ih=f+Ig+Ih
31 1 2 3 idmot φIPGIsmtG
32 3 adantr φfGIsmtGGV
33 31 adantr φfGIsmtGIPGIsmtG
34 simpr φfGIsmtGfGIsmtG
35 1 2 32 4 33 34 motplusg φfGIsmtGIP+If=IPf
36 1 2 ismot GVfGIsmtGf:P1-1 ontoPaPbPfa-˙fb=a-˙b
37 36 simprbda GVfGIsmtGf:P1-1 ontoP
38 3 37 sylan φfGIsmtGf:P1-1 ontoP
39 f1of f:P1-1 ontoPf:PP
40 fcoi2 f:PPIPf=f
41 38 39 40 3syl φfGIsmtGIPf=f
42 35 41 eqtrd φfGIsmtGIP+If=f
43 1 2 32 34 cnvmot φfGIsmtGf-1GIsmtG
44 1 2 32 4 43 34 motplusg φfGIsmtGf-1+If=f-1f
45 f1ococnv1 f:P1-1 ontoPf-1f=IP
46 38 45 syl φfGIsmtGf-1f=IP
47 44 46 eqtrd φfGIsmtGf-1+If=IP
48 7 8 14 30 31 42 43 47 isgrpd φIGrp