Metamath Proof Explorer

Theorem motco

Description: The composition of two motions is a motion. (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 ) )
motco.3 
|- ( ph -> H e. ( G Ismt G ) )
Assertion motco 
|- ( ph -> ( F o. H ) e. ( G Ismt G ) )

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 motco.3 
 |-  ( ph -> H e. ( G Ismt G ) )
6 1 2 3 4 motf1o 
 |-  ( ph -> F : P -1-1-onto-> P )
7 1 2 3 5 motf1o 
 |-  ( ph -> H : P -1-1-onto-> P )
8 f1oco 
 |-  ( ( F : P -1-1-onto-> P /\ H : P -1-1-onto-> P ) -> ( F o. H ) : P -1-1-onto-> P )
9 6 7 8 syl2anc 
 |-  ( ph -> ( F o. H ) : P -1-1-onto-> P )
10 f1of 
 |-  ( H : P -1-1-onto-> P -> H : P --> P )
11 7 10 syl 
 |-  ( ph -> H : P --> P )
12 11 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> H : P --> P )
13 simprl 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> a e. P )
14 fvco3 
 |-  ( ( H : P --> P /\ a e. P ) -> ( ( F o. H ) ` a ) = ( F ` ( H ` a ) ) )
15 12 13 14 syl2anc 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F o. H ) ` a ) = ( F ` ( H ` a ) ) )
16 simprr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> b e. P )
17 fvco3 
 |-  ( ( H : P --> P /\ b e. P ) -> ( ( F o. H ) ` b ) = ( F ` ( H ` b ) ) )
18 12 16 17 syl2anc 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F o. H ) ` b ) = ( F ` ( H ` b ) ) )
19 15 18 oveq12d 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( ( F ` ( H ` a ) ) .- ( F ` ( H ` b ) ) ) )
20 3 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> G e. V )
21 12 13 ffvelrnd 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( H ` a ) e. P )
22 12 16 ffvelrnd 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( H ` b ) e. P )
23 4 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> F e. ( G Ismt G ) )
24 1 2 20 21 22 23 motcgr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( F ` ( H ` a ) ) .- ( F ` ( H ` b ) ) ) = ( ( H ` a ) .- ( H ` b ) ) )
25 5 adantr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> H e. ( G Ismt G ) )
26 1 2 20 13 16 25 motcgr 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( H ` a ) .- ( H ` b ) ) = ( a .- b ) )
27 19 24 26 3eqtrd 
 |-  ( ( ph /\ ( a e. P /\ b e. P ) ) -> ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) )
28 27 ralrimivva 
 |-  ( ph -> A. a e. P A. b e. P ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) )
29 1 2 ismot 
 |-  ( G e. V -> ( ( F o. H ) e. ( G Ismt G ) <-> ( ( F o. H ) : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) ) ) )
30 3 29 syl 
 |-  ( ph -> ( ( F o. H ) e. ( G Ismt G ) <-> ( ( F o. H ) : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( ( F o. H ) ` a ) .- ( ( F o. H ) ` b ) ) = ( a .- b ) ) ) )
31 9 28 30 mpbir2and 
 |-  ( ph -> ( F o. H ) e. ( G Ismt G ) )