motcgrg

Description: Property of a motion: distances are preserved. (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)⟩\}$
	motcgrg.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	motcgrg.t	$⊢ φ \to T \in Word P$
	motcgrg.f	$⊢ φ \to F \in (G Ismt G)$
Assertion	motcgrg	$⊢ φ \to (F \circ T) \underset{˙}{\sim} T$

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		motgrp.i	$⊢ I = \{⟨{Base}_{ndx}, G Ismt G⟩, ⟨+_{ndx}, (f \in (G Ismt G), g \in (G Ismt G) ⟼ f \circ g)⟩\}$
5		motcgrg.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
6		motcgrg.t	$⊢ φ \to T \in Word P$
7		motcgrg.f	$⊢ φ \to F \in (G Ismt G)$
8		simpr	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to T : (0 ..^n) ⟶ P$
9	8	adantr	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to T : (0 ..^n) ⟶ P$
10		simprl	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to a \in dom (F \circ T)$
11	1 2 3 7	motf1o	$⊢ φ \to F : P \underset{1-1 onto}{⟶} P$
12		f1of	$⊢ F : P \underset{1-1 onto}{⟶} P \to F : P ⟶ P$
13	11 12	syl	$⊢ φ \to F : P ⟶ P$
14	13	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to F : P ⟶ P$
15		fco	$⊢ (F : P ⟶ P \land T : (0 ..^n) ⟶ P) \to (F \circ T) : (0 ..^n) ⟶ P$
16	14 8 15	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to (F \circ T) : (0 ..^n) ⟶ P$
17	16	adantr	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to (F \circ T) : (0 ..^n) ⟶ P$
18	17	fdmd	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to dom (F \circ T) = (0 ..^n)$
19	10 18	eleqtrd	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to a \in (0 ..^n)$
20		fvco3	$⊢ (T : (0 ..^n) ⟶ P \land a \in (0 ..^n)) \to (F \circ T) (a) = F (T (a))$
21	9 19 20	syl2anc	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to (F \circ T) (a) = F (T (a))$
22		simprr	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to b \in dom (F \circ T)$
23	22 18	eleqtrd	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to b \in (0 ..^n)$
24		fvco3	$⊢ (T : (0 ..^n) ⟶ P \land b \in (0 ..^n)) \to (F \circ T) (b) = F (T (b))$
25	9 23 24	syl2anc	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to (F \circ T) (b) = F (T (b))$
26	21 25	oveq12d	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to (F \circ T) (a) \underset{˙}{-} (F \circ T) (b) = F (T (a)) \underset{˙}{-} F (T (b))$
27	3	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to G \in V$
28	27	adantr	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to G \in V$
29	9 19	ffvelrnd	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to T (a) \in P$
30	9 23	ffvelrnd	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to T (b) \in P$
31	7	ad3antrrr	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to F \in (G Ismt G)$
32	1 2 28 29 30 31	motcgr	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to F (T (a)) \underset{˙}{-} F (T (b)) = T (a) \underset{˙}{-} T (b)$
33	26 32	eqtrd	$⊢ (((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \land (a \in dom (F \circ T) \land b \in dom (F \circ T))) \to (F \circ T) (a) \underset{˙}{-} (F \circ T) (b) = T (a) \underset{˙}{-} T (b)$
34	33	ralrimivva	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to \forall a \in dom (F \circ T) \forall b \in dom (F \circ T) (F \circ T) (a) \underset{˙}{-} (F \circ T) (b) = T (a) \underset{˙}{-} T (b)$
35		fzo0ssnn0	$⊢ (0 ..^n) \subseteq ℕ_{0}$
36		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
37	35 36	sstri	$⊢ (0 ..^n) \subseteq ℝ$
38	37	a1i	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to (0 ..^n) \subseteq ℝ$
39	1 2 5 27 38 16 8	iscgrgd	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to ((F \circ T) \underset{˙}{\sim} T \leftrightarrow \forall a \in dom (F \circ T) \forall b \in dom (F \circ T) (F \circ T) (a) \underset{˙}{-} (F \circ T) (b) = T (a) \underset{˙}{-} T (b))$
40	34 39	mpbird	$⊢ ((φ \land n \in ℕ_{0}) \land T : (0 ..^n) ⟶ P) \to (F \circ T) \underset{˙}{\sim} T$
41		iswrd	$⊢ T \in Word P \leftrightarrow \exists n \in ℕ_{0} T : (0 ..^n) ⟶ P$
42	6 41	sylib	$⊢ φ \to \exists n \in ℕ_{0} T : (0 ..^n) ⟶ P$
43	40 42	r19.29a	$⊢ φ \to (F \circ T) \underset{˙}{\sim} T$

Metamath Proof Explorer

Theorem motcgrg

Proof