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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismot.m ⊢ − = ( dist ‘ 𝐺 )
motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
motco.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
motco.3 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) )
Assertion motco ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐺 Ismt 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ismot.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismot.m ⊢ − = ( dist ‘ 𝐺 )
3 motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 motco.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
5 motco.3 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) )
6 1 2 3 4 motf1o ⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 )
7 1 2 3 5 motf1o ⊢ ( 𝜑 → 𝐻 : 𝑃 –1-1-onto→ 𝑃 )
8 f1oco ⊢ ( ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ 𝐻 : 𝑃 –1-1-onto→ 𝑃 ) → ( 𝐹 ∘ 𝐻 ) : 𝑃 –1-1-onto→ 𝑃 )
9 6 7 8 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : 𝑃 –1-1-onto→ 𝑃 )
10 f1of ⊢ ( 𝐻 : 𝑃 –1-1-onto→ 𝑃 → 𝐻 : 𝑃 ⟶ 𝑃 )
11 7 10 syl ⊢ ( 𝜑 → 𝐻 : 𝑃 ⟶ 𝑃 )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐻 : 𝑃 ⟶ 𝑃 )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝑎 ∈ 𝑃 )
14 fvco3 ⊢ ( ( 𝐻 : 𝑃 ⟶ 𝑃 ∧ 𝑎 ∈ 𝑃 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑎 ) ) )
15 12 13 14 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑎 ) ) )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝑏 ∈ 𝑃 )
17 fvco3 ⊢ ( ( 𝐻 : 𝑃 ⟶ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑏 ) ) )
18 12 16 17 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑏 ) ) )
19 15 18 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑎 ) ) − ( 𝐹 ‘ ( 𝐻 ‘ 𝑏 ) ) ) )
20 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐺 ∈ 𝑉 )
21 12 13 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( 𝐻 ‘ 𝑎 ) ∈ 𝑃 )
22 12 16 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( 𝐻 ‘ 𝑏 ) ∈ 𝑃 )
23 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
24 1 2 20 21 22 23 motcgr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐹 ‘ ( 𝐻 ‘ 𝑎 ) ) − ( 𝐹 ‘ ( 𝐻 ‘ 𝑏 ) ) ) = ( ( 𝐻 ‘ 𝑎 ) − ( 𝐻 ‘ 𝑏 ) ) )
25 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) )
26 1 2 20 13 16 25 motcgr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐻 ‘ 𝑎 ) − ( 𝐻 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
27 19 24 26 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
28 27 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
29 1 2 ismot ⊢ ( 𝐺 ∈ 𝑉 → ( ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( ( 𝐹 ∘ 𝐻 ) : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
30 3 29 syl ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( ( 𝐹 ∘ 𝐻 ) : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
31 9 28 30 mpbir2and ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐺 Ismt 𝐺 ) )