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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismot.m ⊢ − = ( dist ‘ 𝐺 )
motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
motgrp.i ⊢ 𝐼 = { ⟨ ( Base ‘ ndx ) , ( 𝐺 Ismt 𝐺 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ }
motplusg.1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
motplusg.2 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) )
Assertion motplusg ( 𝜑 → ( 𝐹 ( +g ‘ 𝐼 ) 𝐻 ) = ( 𝐹 ∘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ismot.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismot.m ⊢ − = ( dist ‘ 𝐺 )
3 motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 motgrp.i ⊢ 𝐼 = { ⟨ ( Base ‘ ndx ) , ( 𝐺 Ismt 𝐺 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ }
5 motplusg.1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
6 motplusg.2 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) )
7 coexg ⊢ ( ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ∧ 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) ) → ( 𝐹 ∘ 𝐻 ) ∈ V )
8 5 6 7 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ V )
9 coeq1 ⊢ ( 𝑎 = 𝐹 → ( 𝑎 ∘ 𝑏 ) = ( 𝐹 ∘ 𝑏 ) )
10 coeq2 ⊢ ( 𝑏 = 𝐻 → ( 𝐹 ∘ 𝑏 ) = ( 𝐹 ∘ 𝐻 ) )
11 ovex ⊢ ( 𝐺 Ismt 𝐺 ) ∈ V
12 11 11 mpoex ⊢ ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V
13 4 grpplusg ⊢ ( ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V → ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ 𝐼 ) )
14 12 13 ax-mp ⊢ ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ 𝐼 )
15 coeq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ∘ 𝑔 ) = ( 𝑎 ∘ 𝑔 ) )
16 coeq2 ⊢ ( 𝑔 = 𝑏 → ( 𝑎 ∘ 𝑔 ) = ( 𝑎 ∘ 𝑏 ) )
17 15 16 cbvmpov ⊢ ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑎 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑏 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑎 ∘ 𝑏 ) )
18 14 17 eqtr3i ⊢ ( +g ‘ 𝐼 ) = ( 𝑎 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑏 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑎 ∘ 𝑏 ) )
19 9 10 18 ovmpog ⊢ ( ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ∧ 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) ∧ ( 𝐹 ∘ 𝐻 ) ∈ V ) → ( 𝐹 ( +g ‘ 𝐼 ) 𝐻 ) = ( 𝐹 ∘ 𝐻 ) )
20 5 6 8 19 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( +g ‘ 𝐼 ) 𝐻 ) = ( 𝐹 ∘ 𝐻 ) )