motgrp

Description: The motions of a geometry form a group with respect to function composition, called the Isometry group. (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)⟩\}$
Assertion	motgrp	$⊢ φ \to I \in Grp$

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		ovex	$⊢ G Ismt G \in V$
6	4	grpbase	$⊢ G Ismt G \in V \to G Ismt G = {Base}_{I}$
7	5 6	mp1i	$⊢ φ \to G Ismt G = {Base}_{I}$
8		eqidd	$⊢ φ \to +_{I} = +_{I}$
9	3	3ad2ant1	$⊢ (φ \land f \in (G Ismt G) \land g \in (G Ismt G)) \to G \in V$
10		simp2	$⊢ (φ \land f \in (G Ismt G) \land g \in (G Ismt G)) \to f \in (G Ismt G)$
11		simp3	$⊢ (φ \land f \in (G Ismt G) \land g \in (G Ismt G)) \to g \in (G Ismt G)$
12	1 2 9 4 10 11	motplusg	$⊢ (φ \land f \in (G Ismt G) \land g \in (G Ismt G)) \to f +_{I} g = f \circ g$
13	1 2 9 10 11	motco	$⊢ (φ \land f \in (G Ismt G) \land g \in (G Ismt G)) \to f \circ g \in (G Ismt G)$
14	12 13	eqeltrd	$⊢ (φ \land f \in (G Ismt G) \land g \in (G Ismt G)) \to f +_{I} g \in (G Ismt G)$
15		coass	$⊢ (f \circ g) \circ h = f \circ (g \circ h)$
16	12	3adant3r3	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to f +_{I} g = f \circ g$
17	16	oveq1d	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to (f +_{I} g) +_{I} h = (f \circ g) +_{I} h$
18	3	adantr	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to G \in V$
19	13	3adant3r3	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to f \circ g \in (G Ismt G)$
20		simpr3	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to h \in (G Ismt G)$
21	1 2 18 4 19 20	motplusg	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to (f \circ g) +_{I} h = (f \circ g) \circ h$
22	17 21	eqtrd	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to (f +_{I} g) +_{I} h = (f \circ g) \circ h$
23		simpr2	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to g \in (G Ismt G)$
24	1 2 18 4 23 20	motplusg	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to g +_{I} h = g \circ h$
25	24	oveq2d	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to f +_{I} (g +_{I} h) = f +_{I} (g \circ h)$
26		simpr1	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to f \in (G Ismt G)$
27	1 2 18 23 20	motco	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to g \circ h \in (G Ismt G)$
28	1 2 18 4 26 27	motplusg	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to f +_{I} (g \circ h) = f \circ (g \circ h)$
29	25 28	eqtrd	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to f +_{I} (g +_{I} h) = f \circ (g \circ h)$
30	15 22 29	3eqtr4a	$⊢ (φ \land (f \in (G Ismt G) \land g \in (G Ismt G) \land h \in (G Ismt G))) \to (f +_{I} g) +_{I} h = f +_{I} (g +_{I} h)$
31	1 2 3	idmot	$⊢ φ \to {I ↾}_{P} \in (G Ismt G)$
32	3	adantr	$⊢ (φ \land f \in (G Ismt G)) \to G \in V$
33	31	adantr	$⊢ (φ \land f \in (G Ismt G)) \to {I ↾}_{P} \in (G Ismt G)$
34		simpr	$⊢ (φ \land f \in (G Ismt G)) \to f \in (G Ismt G)$
35	1 2 32 4 33 34	motplusg	$⊢ (φ \land f \in (G Ismt G)) \to ({I ↾}_{P}) +_{I} f = ({I ↾}_{P}) \circ f$
36	1 2	ismot	$⊢ G \in V \to (f \in (G Ismt G) \leftrightarrow (f : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P f (a) \underset{˙}{-} f (b) = a \underset{˙}{-} b))$
37	36	simprbda	$⊢ (G \in V \land f \in (G Ismt G)) \to f : P \underset{1-1 onto}{⟶} P$
38	3 37	sylan	$⊢ (φ \land f \in (G Ismt G)) \to f : P \underset{1-1 onto}{⟶} P$
39		f1of	$⊢ f : P \underset{1-1 onto}{⟶} P \to f : P ⟶ P$
40		fcoi2	$⊢ f : P ⟶ P \to ({I ↾}_{P}) \circ f = f$
41	38 39 40	3syl	$⊢ (φ \land f \in (G Ismt G)) \to ({I ↾}_{P}) \circ f = f$
42	35 41	eqtrd	$⊢ (φ \land f \in (G Ismt G)) \to ({I ↾}_{P}) +_{I} f = f$
43	1 2 32 34	cnvmot	$⊢ (φ \land f \in (G Ismt G)) \to f^{-1} \in (G Ismt G)$
44	1 2 32 4 43 34	motplusg	$⊢ (φ \land f \in (G Ismt G)) \to f^{-1} +_{I} f = f^{-1} \circ f$
45		f1ococnv1	$⊢ f : P \underset{1-1 onto}{⟶} P \to f^{-1} \circ f = {I ↾}_{P}$
46	38 45	syl	$⊢ (φ \land f \in (G Ismt G)) \to f^{-1} \circ f = {I ↾}_{P}$
47	44 46	eqtrd	$⊢ (φ \land f \in (G Ismt G)) \to f^{-1} +_{I} f = {I ↾}_{P}$
48	7 8 14 30 31 42 43 47	isgrpd	$⊢ φ \to I \in Grp$

Metamath Proof Explorer

Theorem motgrp

Proof