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 = ( Base ` G )
ismot.m 
|- .- = ( dist ` G )
motgrp.1 
|- ( ph -> G e. V )
motgrp.i 
|- I = { <. ( Base ` ndx ) , ( G Ismt G ) >. , <. ( +g ` ndx ) , ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) >. }
Assertion motgrp 
|- ( ph -> I e. Grp )

Proof

Step Hyp Ref Expression
1 ismot.p 
 |-  P = ( Base ` G )
2 ismot.m 
 |-  .- = ( dist ` G )
3 motgrp.1 
 |-  ( ph -> G e. V )
4 motgrp.i 
 |-  I = { <. ( Base ` ndx ) , ( G Ismt G ) >. , <. ( +g ` ndx ) , ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) >. }
5 ovex 
 |-  ( G Ismt G ) e. _V
6 4 grpbase 
 |-  ( ( G Ismt G ) e. _V -> ( G Ismt G ) = ( Base ` I ) )
7 5 6 mp1i 
 |-  ( ph -> ( G Ismt G ) = ( Base ` I ) )
8 eqidd 
 |-  ( ph -> ( +g ` I ) = ( +g ` I ) )
9 3 3ad2ant1 
 |-  ( ( ph /\ f e. ( G Ismt G ) /\ g e. ( G Ismt G ) ) -> G e. V )
10 simp2 
 |-  ( ( ph /\ f e. ( G Ismt G ) /\ g e. ( G Ismt G ) ) -> f e. ( G Ismt G ) )
11 simp3 
 |-  ( ( ph /\ f e. ( G Ismt G ) /\ g e. ( G Ismt G ) ) -> g e. ( G Ismt G ) )
12 1 2 9 4 10 11 motplusg 
 |-  ( ( ph /\ f e. ( G Ismt G ) /\ g e. ( G Ismt G ) ) -> ( f ( +g ` I ) g ) = ( f o. g ) )
13 1 2 9 10 11 motco 
 |-  ( ( ph /\ f e. ( G Ismt G ) /\ g e. ( G Ismt G ) ) -> ( f o. g ) e. ( G Ismt G ) )
14 12 13 eqeltrd 
 |-  ( ( ph /\ f e. ( G Ismt G ) /\ g e. ( G Ismt G ) ) -> ( f ( +g ` I ) g ) e. ( G Ismt G ) )
15 coass 
 |-  ( ( f o. g ) o. h ) = ( f o. ( g o. h ) )
16 12 3adant3r3 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( f ( +g ` I ) g ) = ( f o. g ) )
17 16 oveq1d 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( ( f ( +g ` I ) g ) ( +g ` I ) h ) = ( ( f o. g ) ( +g ` I ) h ) )
18 3 adantr 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> G e. V )
19 13 3adant3r3 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( f o. g ) e. ( G Ismt G ) )
20 simpr3 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> h e. ( G Ismt G ) )
21 1 2 18 4 19 20 motplusg 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( ( f o. g ) ( +g ` I ) h ) = ( ( f o. g ) o. h ) )
22 17 21 eqtrd 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( ( f ( +g ` I ) g ) ( +g ` I ) h ) = ( ( f o. g ) o. h ) )
23 simpr2 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> g e. ( G Ismt G ) )
24 1 2 18 4 23 20 motplusg 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( g ( +g ` I ) h ) = ( g o. h ) )
25 24 oveq2d 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( f ( +g ` I ) ( g ( +g ` I ) h ) ) = ( f ( +g ` I ) ( g o. h ) ) )
26 simpr1 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> f e. ( G Ismt G ) )
27 1 2 18 23 20 motco 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( g o. h ) e. ( G Ismt G ) )
28 1 2 18 4 26 27 motplusg 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( f ( +g ` I ) ( g o. h ) ) = ( f o. ( g o. h ) ) )
29 25 28 eqtrd 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( f ( +g ` I ) ( g ( +g ` I ) h ) ) = ( f o. ( g o. h ) ) )
30 15 22 29 3eqtr4a 
 |-  ( ( ph /\ ( f e. ( G Ismt G ) /\ g e. ( G Ismt G ) /\ h e. ( G Ismt G ) ) ) -> ( ( f ( +g ` I ) g ) ( +g ` I ) h ) = ( f ( +g ` I ) ( g ( +g ` I ) h ) ) )
31 1 2 3 idmot 
 |-  ( ph -> ( _I |` P ) e. ( G Ismt G ) )
32 3 adantr 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> G e. V )
33 31 adantr 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( _I |` P ) e. ( G Ismt G ) )
34 simpr 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> f e. ( G Ismt G ) )
35 1 2 32 4 33 34 motplusg 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( ( _I |` P ) ( +g ` I ) f ) = ( ( _I |` P ) o. f ) )
36 1 2 ismot 
 |-  ( G e. V -> ( f e. ( G Ismt G ) <-> ( f : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( f ` a ) .- ( f ` b ) ) = ( a .- b ) ) ) )
37 36 simprbda 
 |-  ( ( G e. V /\ f e. ( G Ismt G ) ) -> f : P -1-1-onto-> P )
38 3 37 sylan 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> f : P -1-1-onto-> P )
39 f1of 
 |-  ( f : P -1-1-onto-> P -> f : P --> P )
40 fcoi2 
 |-  ( f : P --> P -> ( ( _I |` P ) o. f ) = f )
41 38 39 40 3syl 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( ( _I |` P ) o. f ) = f )
42 35 41 eqtrd 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( ( _I |` P ) ( +g ` I ) f ) = f )
43 1 2 32 34 cnvmot 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> `' f e. ( G Ismt G ) )
44 1 2 32 4 43 34 motplusg 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( `' f ( +g ` I ) f ) = ( `' f o. f ) )
45 f1ococnv1 
 |-  ( f : P -1-1-onto-> P -> ( `' f o. f ) = ( _I |` P ) )
46 38 45 syl 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( `' f o. f ) = ( _I |` P ) )
47 44 46 eqtrd 
 |-  ( ( ph /\ f e. ( G Ismt G ) ) -> ( `' f ( +g ` I ) f ) = ( _I |` P ) )
48 7 8 14 30 31 42 43 47 isgrpd 
 |-  ( ph -> I e. Grp )