isga

Description: The predicate "is a (left) group action." The group G is said to act on the base set Y of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element g of G is a permutation of the elements of Y (see gapm ). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	isga.1	$⊢ X = {Base}_{G}$
	isga.2	$⊢ \underset{˙}{+} = +_{G}$
	isga.3	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	isga	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \leftrightarrow ((G \in Grp \land Y \in V) \land (\underset{˙}{\oplus} : X \times Y ⟶ Y \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))))$

Proof

Step	Hyp	Ref	Expression
1		isga.1	$⊢ X = {Base}_{G}$
2		isga.2	$⊢ \underset{˙}{+} = +_{G}$
3		isga.3	$⊢ \underset{˙}{0} = 0_{G}$
4		df-ga	$⊢ GrpAct = (g \in Grp, s \in V ⟼ ⦋ {Base}_{g} / b ⦌ \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\})$
5	4	elmpocl	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \to (G \in Grp \land Y \in V)$
6		fvexd	$⊢ (g = G \land s = Y) \to {Base}_{g} \in V$
7		simplr	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to s = Y$
8		id	$⊢ b = {Base}_{g} \to b = {Base}_{g}$
9		simpl	$⊢ (g = G \land s = Y) \to g = G$
10	9	fveq2d	$⊢ (g = G \land s = Y) \to {Base}_{g} = {Base}_{G}$
11	10 1	eqtr4di	$⊢ (g = G \land s = Y) \to {Base}_{g} = X$
12	8 11	sylan9eqr	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to b = X$
13	12 7	xpeq12d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to b \times s = X \times Y$
14	7 13	oveq12d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to s^{(b \times s)} = Y^{(X \times Y)}$
15		simpll	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to g = G$
16	15	fveq2d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to 0_{g} = 0_{G}$
17	16 3	eqtr4di	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to 0_{g} = \underset{˙}{0}$
18	17	oveq1d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to 0_{g} m x = \underset{˙}{0} m x$
19	18	eqeq1d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to (0_{g} m x = x \leftrightarrow \underset{˙}{0} m x = x)$
20	15	fveq2d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to +_{g} = +_{G}$
21	20 2	eqtr4di	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to +_{g} = \underset{˙}{+}$
22	21	oveqd	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to y +_{g} z = y \underset{˙}{+} z$
23	22	oveq1d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to (y +_{g} z) m x = (y \underset{˙}{+} z) m x$
24	23	eqeq1d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to ((y +_{g} z) m x = y m (z m x) \leftrightarrow (y \underset{˙}{+} z) m x = y m (z m x))$
25	12 24	raleqbidv	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to (\forall z \in b (y +_{g} z) m x = y m (z m x) \leftrightarrow \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))$
26	12 25	raleqbidv	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to (\forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x) \leftrightarrow \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))$
27	19 26	anbi12d	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to ((0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x)) \leftrightarrow (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x)))$
28	7 27	raleqbidv	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to (\forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x)) \leftrightarrow \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x)))$
29	14 28	rabeqbidv	$⊢ ((g = G \land s = Y) \land b = {Base}_{g}) \to \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\} = \{m \in (Y^{(X \times Y)}) \| \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))\}$
30	6 29	csbied	$⊢ (g = G \land s = Y) \to ⦋ {Base}_{g} / b ⦌ \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\} = \{m \in (Y^{(X \times Y)}) \| \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))\}$
31		ovex	$⊢ Y^{(X \times Y)} \in V$
32	31	rabex	$⊢ \{m \in (Y^{(X \times Y)}) \| \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))\} \in V$
33	30 4 32	ovmpoa	$⊢ (G \in Grp \land Y \in V) \to G GrpAct Y = \{m \in (Y^{(X \times Y)}) \| \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))\}$
34	33	eleq2d	$⊢ (G \in Grp \land Y \in V) \to (\underset{˙}{\oplus} \in (G GrpAct Y) \leftrightarrow \underset{˙}{\oplus} \in \{m \in (Y^{(X \times Y)}) \| \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))\})$
35		oveq	$⊢ m = \underset{˙}{\oplus} \to \underset{˙}{0} m x = \underset{˙}{0} \underset{˙}{\oplus} x$
36	35	eqeq1d	$⊢ m = \underset{˙}{\oplus} \to (\underset{˙}{0} m x = x \leftrightarrow \underset{˙}{0} \underset{˙}{\oplus} x = x)$
37		oveq	$⊢ m = \underset{˙}{\oplus} \to (y \underset{˙}{+} z) m x = (y \underset{˙}{+} z) \underset{˙}{\oplus} x$
38		oveq	$⊢ m = \underset{˙}{\oplus} \to y m (z m x) = y \underset{˙}{\oplus} (z m x)$
39		oveq	$⊢ m = \underset{˙}{\oplus} \to z m x = z \underset{˙}{\oplus} x$
40	39	oveq2d	$⊢ m = \underset{˙}{\oplus} \to y \underset{˙}{\oplus} (z m x) = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)$
41	38 40	eqtrd	$⊢ m = \underset{˙}{\oplus} \to y m (z m x) = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)$
42	37 41	eqeq12d	$⊢ m = \underset{˙}{\oplus} \to ((y \underset{˙}{+} z) m x = y m (z m x) \leftrightarrow (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))$
43	42	2ralbidv	$⊢ m = \underset{˙}{\oplus} \to (\forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x) \leftrightarrow \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))$
44	36 43	anbi12d	$⊢ m = \underset{˙}{\oplus} \to ((\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x)) \leftrightarrow (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)))$
45	44	ralbidv	$⊢ m = \underset{˙}{\oplus} \to (\forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x)) \leftrightarrow \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)))$
46	45	elrab	$⊢ \underset{˙}{\oplus} \in \{m \in (Y^{(X \times Y)}) \| \forall x \in Y (\underset{˙}{0} m x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) m x = y m (z m x))\} \leftrightarrow (\underset{˙}{\oplus} \in (Y^{(X \times Y)}) \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)))$
47	34 46	bitrdi	$⊢ (G \in Grp \land Y \in V) \to (\underset{˙}{\oplus} \in (G GrpAct Y) \leftrightarrow (\underset{˙}{\oplus} \in (Y^{(X \times Y)}) \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))))$
48		simpr	$⊢ (G \in Grp \land Y \in V) \to Y \in V$
49	1	fvexi	$⊢ X \in V$
50		xpexg	$⊢ (X \in V \land Y \in V) \to X \times Y \in V$
51	49 48 50	sylancr	$⊢ (G \in Grp \land Y \in V) \to X \times Y \in V$
52	48 51	elmapd	$⊢ (G \in Grp \land Y \in V) \to (\underset{˙}{\oplus} \in (Y^{(X \times Y)}) \leftrightarrow \underset{˙}{\oplus} : X \times Y ⟶ Y)$
53	52	anbi1d	$⊢ (G \in Grp \land Y \in V) \to ((\underset{˙}{\oplus} \in (Y^{(X \times Y)}) \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))) \leftrightarrow (\underset{˙}{\oplus} : X \times Y ⟶ Y \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))))$
54	47 53	bitrd	$⊢ (G \in Grp \land Y \in V) \to (\underset{˙}{\oplus} \in (G GrpAct Y) \leftrightarrow (\underset{˙}{\oplus} : X \times Y ⟶ Y \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))))$
55	5 54	biadanii	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \leftrightarrow ((G \in Grp \land Y \in V) \land (\underset{˙}{\oplus} : X \times Y ⟶ Y \land \forall x \in Y (\underset{˙}{0} \underset{˙}{\oplus} x = x \land \forall y \in X \forall z \in X (y \underset{˙}{+} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x))))$

Metamath Proof Explorer

Theorem isga

Proof