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	$⊢ \underset{˙}{-} = dist (G)$
	motgrp.1	$⊢ φ \to G \in V$
	motgrp.i	$⊢ I = \{⟨{Base}_{ndx}, G Ismt G⟩, ⟨+_{ndx}, (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g)⟩\}$
	motplusg.1	$⊢ φ \to F \in (G Ismt G)$
	motplusg.2	$⊢ φ \to H \in (G Ismt G)$
Assertion	motplusg	$⊢ φ \to F +_{I} H = F \circ H$

Step	Hyp	Ref	Expression
1		ismot.p	$⊢ P = {Base}_{G}$
2		ismot.m	$⊢ \underset{˙}{-} = dist (G)$
3		motgrp.1	$⊢ φ \to G \in V$
4		motgrp.i	$⊢ I = \{⟨{Base}_{ndx}, G Ismt G⟩, ⟨+_{ndx}, (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g)⟩\}$
5		motplusg.1	$⊢ φ \to F \in (G Ismt G)$
6		motplusg.2	$⊢ φ \to H \in (G Ismt G)$
7		coexg	$⊢ (F \in (G Ismt G) \land H \in (G Ismt G)) \to F \circ H \in V$
8	5 6 7	syl2anc	$⊢ φ \to F \circ H \in V$
9		coeq1	$⊢ a = F \to a \circ b = F \circ b$
10		coeq2	$⊢ b = H \to F \circ b = F \circ H$
11		ovex	$⊢ G Ismt G \in V$
12	11 11	mpoex	$⊢ (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g) \in V$
13	4	grpplusg	$⊢ (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g) \in V \to (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g) = +_{I}$
14	12 13	ax-mp	$⊢ (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g) = +_{I}$
15		coeq1	$⊢ f = a \to f \circ g = a \circ g$
16		coeq2	$⊢ g = b \to a \circ g = a \circ b$
17	15 16	cbvmpov	$⊢ (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g) = (a \in (G Ismt G), b \in (G Ismt G) ⟼ a \circ b)$
18	14 17	eqtr3i	$⊢ +_{I} = (a \in (G Ismt G), b \in (G Ismt G) ⟼ a \circ b)$
19	9 10 18	ovmpog	$⊢ (F \in (G Ismt G) \land H \in (G Ismt G) \land F \circ H \in V) \to F +_{I} H = F \circ H$
20	5 6 8 19	syl3anc	$⊢ φ \to F +_{I} H = F \circ H$

Metamath Proof Explorer