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 ) )