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	$⊢ \underset{˙}{-} = dist (G)$
	motgrp.1	$⊢ φ \to G \in V$
	motco.2	$⊢ φ \to F \in (G Ismt G)$
	motco.3	$⊢ φ \to H \in (G Ismt G)$
Assertion	motco	$⊢ φ \to F \circ H \in (G Ismt G)$

Proof

Step	Hyp	Ref	Expression
1		ismot.p	$⊢ P = {Base}_{G}$
2		ismot.m	$⊢ \underset{˙}{-} = dist (G)$
3		motgrp.1	$⊢ φ \to G \in V$
4		motco.2	$⊢ φ \to F \in (G Ismt G)$
5		motco.3	$⊢ φ \to H \in (G Ismt G)$
6	1 2 3 4	motf1o	$⊢ φ \to F : P \underset{1-1 onto}{⟶} P$
7	1 2 3 5	motf1o	$⊢ φ \to H : P \underset{1-1 onto}{⟶} P$
8		f1oco	$⊢ (F : P \underset{1-1 onto}{⟶} P \land H : P \underset{1-1 onto}{⟶} P) \to (F \circ H) : P \underset{1-1 onto}{⟶} P$
9	6 7 8	syl2anc	$⊢ φ \to (F \circ H) : P \underset{1-1 onto}{⟶} P$
10		f1of	$⊢ H : P \underset{1-1 onto}{⟶} P \to H : P ⟶ P$
11	7 10	syl	$⊢ φ \to H : P ⟶ P$
12	11	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to H : P ⟶ P$
13		simprl	$⊢ (φ \land (a \in P \land b \in P)) \to a \in P$
14		fvco3	$⊢ (H : P ⟶ P \land a \in P) \to (F \circ H) (a) = F (H (a))$
15	12 13 14	syl2anc	$⊢ (φ \land (a \in P \land b \in P)) \to (F \circ H) (a) = F (H (a))$
16		simprr	$⊢ (φ \land (a \in P \land b \in P)) \to b \in P$
17		fvco3	$⊢ (H : P ⟶ P \land b \in P) \to (F \circ H) (b) = F (H (b))$
18	12 16 17	syl2anc	$⊢ (φ \land (a \in P \land b \in P)) \to (F \circ H) (b) = F (H (b))$
19	15 18	oveq12d	$⊢ (φ \land (a \in P \land b \in P)) \to (F \circ H) (a) \underset{˙}{-} (F \circ H) (b) = F (H (a)) \underset{˙}{-} F (H (b))$
20	3	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to G \in V$
21	12 13	ffvelrnd	$⊢ (φ \land (a \in P \land b \in P)) \to H (a) \in P$
22	12 16	ffvelrnd	$⊢ (φ \land (a \in P \land b \in P)) \to H (b) \in P$
23	4	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to F \in (G Ismt G)$
24	1 2 20 21 22 23	motcgr	$⊢ (φ \land (a \in P \land b \in P)) \to F (H (a)) \underset{˙}{-} F (H (b)) = H (a) \underset{˙}{-} H (b)$
25	5	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to H \in (G Ismt G)$
26	1 2 20 13 16 25	motcgr	$⊢ (φ \land (a \in P \land b \in P)) \to H (a) \underset{˙}{-} H (b) = a \underset{˙}{-} b$
27	19 24 26	3eqtrd	$⊢ (φ \land (a \in P \land b \in P)) \to (F \circ H) (a) \underset{˙}{-} (F \circ H) (b) = a \underset{˙}{-} b$
28	27	ralrimivva	$⊢ φ \to \forall a \in P \forall b \in P (F \circ H) (a) \underset{˙}{-} (F \circ H) (b) = a \underset{˙}{-} b$
29	1 2	ismot	$⊢ G \in V \to (F \circ H \in (G Ismt G) \leftrightarrow ((F \circ H) : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P (F \circ H) (a) \underset{˙}{-} (F \circ H) (b) = a \underset{˙}{-} b))$
30	3 29	syl	$⊢ φ \to (F \circ H \in (G Ismt G) \leftrightarrow ((F \circ H) : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P (F \circ H) (a) \underset{˙}{-} (F \circ H) (b) = a \underset{˙}{-} b))$
31	9 28 30	mpbir2and	$⊢ φ \to F \circ H \in (G Ismt G)$

Metamath Proof Explorer

Theorem motco

Proof