Metamath Proof Explorer

Theorem motplusg

Description: The operation for motions is their composition. (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 ) ) >. }
motplusg.1 
|- ( ph -> F e. ( G Ismt G ) )
motplusg.2 
|- ( ph -> H e. ( G Ismt G ) )
Assertion motplusg 
|- ( ph -> ( F ( +g ` I ) H ) = ( F o. H ) )

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 motplusg.1 
 |-  ( ph -> F e. ( G Ismt G ) )
6 motplusg.2 
 |-  ( ph -> H e. ( G Ismt G ) )
7 coexg 
 |-  ( ( F e. ( G Ismt G ) /\ H e. ( G Ismt G ) ) -> ( F o. H ) e. _V )
8 5 6 7 syl2anc 
 |-  ( ph -> ( F o. H ) e. _V )
9 coeq1 
 |-  ( a = F -> ( a o. b ) = ( F o. b ) )
10 coeq2 
 |-  ( b = H -> ( F o. b ) = ( F o. H ) )
11 ovex 
 |-  ( G Ismt G ) e. _V
12 11 11 mpoex 
 |-  ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) e. _V
13 4 grpplusg 
 |-  ( ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) e. _V -> ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) = ( +g ` I ) )
14 12 13 ax-mp 
 |-  ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) = ( +g ` I )
15 coeq1 
 |-  ( f = a -> ( f o. g ) = ( a o. g ) )
16 coeq2 
 |-  ( g = b -> ( a o. g ) = ( a o. b ) )
17 15 16 cbvmpov 
 |-  ( f e. ( G Ismt G ) , g e. ( G Ismt G ) |-> ( f o. g ) ) = ( a e. ( G Ismt G ) , b e. ( G Ismt G ) |-> ( a o. b ) )
18 14 17 eqtr3i 
 |-  ( +g ` I ) = ( a e. ( G Ismt G ) , b e. ( G Ismt G ) |-> ( a o. b ) )
19 9 10 18 ovmpog 
 |-  ( ( F e. ( G Ismt G ) /\ H e. ( G Ismt G ) /\ ( F o. H ) e. _V ) -> ( F ( +g ` I ) H ) = ( F o. H ) )
20 5 6 8 19 syl3anc 
 |-  ( ph -> ( F ( +g ` I ) H ) = ( F o. H ) )