gaid

Description: The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

		Ref	Expression
	Hypothesis	gaid.1	$⊢ X = {Base}_{G}$
	Assertion	gaid	$⊢ (G \in Grp \land S \in V) \to {2^{nd} ↾}_{(X \times S)} \in (G GrpAct S)$

Proof

Step	Hyp	Ref	Expression
1		gaid.1	$⊢ X = {Base}_{G}$
2		elex	$⊢ S \in V \to S \in V$
3	2	anim2i	$⊢ (G \in Grp \land S \in V) \to (G \in Grp \land S \in V)$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	1 4	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
6	5	adantr	$⊢ (G \in Grp \land S \in V) \to 0_{G} \in X$
7		ovres	$⊢ (0_{G} \in X \land x \in S) \to 0_{G} ({2^{nd} ↾}_{(X \times S)}) x = 0_{G} 2^{nd} x$
8		df-ov	$⊢ 0_{G} 2^{nd} x = 2^{nd} (⟨0_{G}, x⟩)$
9		fvex	$⊢ 0_{G} \in V$
10		vex	$⊢ x \in V$
11	9 10	op2nd	$⊢ 2^{nd} (⟨0_{G}, x⟩) = x$
12	8 11	eqtri	$⊢ 0_{G} 2^{nd} x = x$
13	7 12	eqtrdi	$⊢ (0_{G} \in X \land x \in S) \to 0_{G} ({2^{nd} ↾}_{(X \times S)}) x = x$
14	6 13	sylan	$⊢ ((G \in Grp \land S \in V) \land x \in S) \to 0_{G} ({2^{nd} ↾}_{(X \times S)}) x = x$
15		simprl	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to y \in X$
16		simplr	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to x \in S$
17		ovres	$⊢ (y \in X \land x \in S) \to y ({2^{nd} ↾}_{(X \times S)}) x = y 2^{nd} x$
18		df-ov	$⊢ y 2^{nd} x = 2^{nd} (⟨y, x⟩)$
19		vex	$⊢ y \in V$
20	19 10	op2nd	$⊢ 2^{nd} (⟨y, x⟩) = x$
21	18 20	eqtri	$⊢ y 2^{nd} x = x$
22	17 21	eqtrdi	$⊢ (y \in X \land x \in S) \to y ({2^{nd} ↾}_{(X \times S)}) x = x$
23	15 16 22	syl2anc	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to y ({2^{nd} ↾}_{(X \times S)}) x = x$
24		simprr	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to z \in X$
25		ovres	$⊢ (z \in X \land x \in S) \to z ({2^{nd} ↾}_{(X \times S)}) x = z 2^{nd} x$
26		df-ov	$⊢ z 2^{nd} x = 2^{nd} (⟨z, x⟩)$
27		vex	$⊢ z \in V$
28	27 10	op2nd	$⊢ 2^{nd} (⟨z, x⟩) = x$
29	26 28	eqtri	$⊢ z 2^{nd} x = x$
30	25 29	eqtrdi	$⊢ (z \in X \land x \in S) \to z ({2^{nd} ↾}_{(X \times S)}) x = x$
31	24 16 30	syl2anc	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to z ({2^{nd} ↾}_{(X \times S)}) x = x$
32	31	oveq2d	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x) = y ({2^{nd} ↾}_{(X \times S)}) x$
33		eqid	$⊢ +_{G} = +_{G}$
34	1 33	grpcl	$⊢ (G \in Grp \land y \in X \land z \in X) \to y +_{G} z \in X$
35	34	3expb	$⊢ (G \in Grp \land (y \in X \land z \in X)) \to y +_{G} z \in X$
36	35	ad4ant14	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to y +_{G} z \in X$
37		ovres	$⊢ (y +_{G} z \in X \land x \in S) \to (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = (y +_{G} z) 2^{nd} x$
38		df-ov	$⊢ (y +_{G} z) 2^{nd} x = 2^{nd} (⟨y +_{G} z, x⟩)$
39		ovex	$⊢ y +_{G} z \in V$
40	39 10	op2nd	$⊢ 2^{nd} (⟨y +_{G} z, x⟩) = x$
41	38 40	eqtri	$⊢ (y +_{G} z) 2^{nd} x = x$
42	37 41	eqtrdi	$⊢ (y +_{G} z \in X \land x \in S) \to (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = x$
43	36 16 42	syl2anc	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = x$
44	23 32 43	3eqtr4rd	$⊢ (((G \in Grp \land S \in V) \land x \in S) \land (y \in X \land z \in X)) \to (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x)$
45	44	ralrimivva	$⊢ ((G \in Grp \land S \in V) \land x \in S) \to \forall y \in X \forall z \in X (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x)$
46	14 45	jca	$⊢ ((G \in Grp \land S \in V) \land x \in S) \to (0_{G} ({2^{nd} ↾}_{(X \times S)}) x = x \land \forall y \in X \forall z \in X (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x))$
47	46	ralrimiva	$⊢ (G \in Grp \land S \in V) \to \forall x \in S (0_{G} ({2^{nd} ↾}_{(X \times S)}) x = x \land \forall y \in X \forall z \in X (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x))$
48		f2ndres	$⊢ ({2^{nd} ↾}_{(X \times S)}) : X \times S ⟶ S$
49	47 48	jctil	$⊢ (G \in Grp \land S \in V) \to (({2^{nd} ↾}_{(X \times S)}) : X \times S ⟶ S \land \forall x \in S (0_{G} ({2^{nd} ↾}_{(X \times S)}) x = x \land \forall y \in X \forall z \in X (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x)))$
50	1 33 4	isga	$⊢ {2^{nd} ↾}_{(X \times S)} \in (G GrpAct S) \leftrightarrow ((G \in Grp \land S \in V) \land (({2^{nd} ↾}_{(X \times S)}) : X \times S ⟶ S \land \forall x \in S (0_{G} ({2^{nd} ↾}_{(X \times S)}) x = x \land \forall y \in X \forall z \in X (y +_{G} z) ({2^{nd} ↾}_{(X \times S)}) x = y ({2^{nd} ↾}_{(X \times S)}) (z ({2^{nd} ↾}_{(X \times S)}) x))))$
51	3 49 50	sylanbrc	$⊢ (G \in Grp \land S \in V) \to {2^{nd} ↾}_{(X \times S)} \in (G GrpAct S)$

Metamath Proof Explorer

Theorem gaid

Proof