gasubg

Description: The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015)

		Ref	Expression
	Hypothesis	gasubg.1	$⊢ H = G ↾_{𝑠} S$
	Assertion	gasubg	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to {\underset{˙}{\oplus} ↾}_{(S \times Y)} \in (H GrpAct Y)$

Proof

Step	Hyp	Ref	Expression
1		gasubg.1	$⊢ H = G ↾_{𝑠} S$
2		gaset	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \to Y \in V$
3	1	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$
4	2 3	anim12ci	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to (H \in Grp \land Y \in V)$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	5	gaf	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \to \underset{˙}{\oplus} : {Base}_{G} \times Y ⟶ Y$
7	6	adantr	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to \underset{˙}{\oplus} : {Base}_{G} \times Y ⟶ Y$
8		simpr	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to S \in SubGrp (G)$
9	5	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
10	8 9	syl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to S \subseteq {Base}_{G}$
11		xpss1	$⊢ S \subseteq {Base}_{G} \to S \times Y \subseteq {Base}_{G} \times Y$
12	10 11	syl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to S \times Y \subseteq {Base}_{G} \times Y$
13	7 12	fssresd	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) : S \times Y ⟶ Y$
14	1	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
15	8 14	syl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to S = {Base}_{H}$
16	15	xpeq1d	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to S \times Y = {Base}_{H} \times Y$
17	16	feq2d	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to (({\underset{˙}{\oplus} ↾}_{(S \times Y)}) : S \times Y ⟶ Y \leftrightarrow ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) : {Base}_{H} \times Y ⟶ Y)$
18	13 17	mpbid	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) : {Base}_{H} \times Y ⟶ Y$
19	8	adantr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to S \in SubGrp (G)$
20		eqid	$⊢ 0_{G} = 0_{G}$
21	20	subg0cl	$⊢ S \in SubGrp (G) \to 0_{G} \in S$
22	19 21	syl	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to 0_{G} \in S$
23		simpr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to x \in Y$
24		ovres	$⊢ (0_{G} \in S \land x \in Y) \to 0_{G} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = 0_{G} \underset{˙}{\oplus} x$
25	22 23 24	syl2anc	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to 0_{G} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = 0_{G} \underset{˙}{\oplus} x$
26	1 20	subg0	$⊢ S \in SubGrp (G) \to 0_{G} = 0_{H}$
27	19 26	syl	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to 0_{G} = 0_{H}$
28	27	oveq1d	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to 0_{G} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = 0_{H} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x$
29	20	gagrpid	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land x \in Y) \to 0_{G} \underset{˙}{\oplus} x = x$
30	29	adantlr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to 0_{G} \underset{˙}{\oplus} x = x$
31	25 28 30	3eqtr3d	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to 0_{H} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = x$
32		eqimss2	$⊢ S = {Base}_{H} \to {Base}_{H} \subseteq S$
33	15 32	syl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to {Base}_{H} \subseteq S$
34	33	adantr	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to {Base}_{H} \subseteq S$
35	34	sselda	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land y \in {Base}_{H}) \to y \in S$
36	34	sselda	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land z \in {Base}_{H}) \to z \in S$
37	35 36	anim12dan	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in {Base}_{H} \land z \in {Base}_{H})) \to (y \in S \land z \in S)$
38		simprl	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y \in S$
39	7	ad2antrr	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to \underset{˙}{\oplus} : {Base}_{G} \times Y ⟶ Y$
40	9	ad3antlr	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to S \subseteq {Base}_{G}$
41		simprr	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to z \in S$
42	40 41	sseldd	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to z \in {Base}_{G}$
43	23	adantr	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to x \in Y$
44	39 42 43	fovcdmd	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to z \underset{˙}{\oplus} x \in Y$
45		ovres	$⊢ (y \in S \land z \underset{˙}{\oplus} x \in Y) \to y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z \underset{˙}{\oplus} x) = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)$
46	38 44 45	syl2anc	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z \underset{˙}{\oplus} x) = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)$
47		ovres	$⊢ (z \in S \land x \in Y) \to z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = z \underset{˙}{\oplus} x$
48	41 43 47	syl2anc	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = z \underset{˙}{\oplus} x$
49	48	oveq2d	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x) = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z \underset{˙}{\oplus} x)$
50		simplll	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to \underset{˙}{\oplus} \in (G GrpAct Y)$
51	40 38	sseldd	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y \in {Base}_{G}$
52		eqid	$⊢ +_{G} = +_{G}$
53	5 52	gaass	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land (y \in {Base}_{G} \land z \in {Base}_{G} \land x \in Y)) \to (y +_{G} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)$
54	50 51 42 43 53	syl13anc	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to (y +_{G} z) \underset{˙}{\oplus} x = y \underset{˙}{\oplus} (z \underset{˙}{\oplus} x)$
55	46 49 54	3eqtr4d	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x) = (y +_{G} z) \underset{˙}{\oplus} x$
56	52	subgcl	$⊢ (S \in SubGrp (G) \land y \in S \land z \in S) \to y +_{G} z \in S$
57	56	3expb	$⊢ (S \in SubGrp (G) \land (y \in S \land z \in S)) \to y +_{G} z \in S$
58	19 57	sylan	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y +_{G} z \in S$
59		ovres	$⊢ (y +_{G} z \in S \land x \in Y) \to (y +_{G} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = (y +_{G} z) \underset{˙}{\oplus} x$
60	58 43 59	syl2anc	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to (y +_{G} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = (y +_{G} z) \underset{˙}{\oplus} x$
61	1 52	ressplusg	$⊢ S \in SubGrp (G) \to +_{G} = +_{H}$
62	61	ad3antlr	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to +_{G} = +_{H}$
63	62	oveqd	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to y +_{G} z = y +_{H} z$
64	63	oveq1d	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to (y +_{G} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x$
65	55 60 64	3eqtr2rd	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in S \land z \in S)) \to (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x)$
66	37 65	syldan	$⊢ (((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \land (y \in {Base}_{H} \land z \in {Base}_{H})) \to (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x)$
67	66	ralrimivva	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to \forall y \in {Base}_{H} \forall z \in {Base}_{H} (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x)$
68	31 67	jca	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \land x \in Y) \to (0_{H} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = x \land \forall y \in {Base}_{H} \forall z \in {Base}_{H} (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x))$
69	68	ralrimiva	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to \forall x \in Y (0_{H} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = x \land \forall y \in {Base}_{H} \forall z \in {Base}_{H} (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x))$
70	18 69	jca	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to (({\underset{˙}{\oplus} ↾}_{(S \times Y)}) : {Base}_{H} \times Y ⟶ Y \land \forall x \in Y (0_{H} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = x \land \forall y \in {Base}_{H} \forall z \in {Base}_{H} (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x)))$
71		eqid	$⊢ {Base}_{H} = {Base}_{H}$
72		eqid	$⊢ +_{H} = +_{H}$
73		eqid	$⊢ 0_{H} = 0_{H}$
74	71 72 73	isga	$⊢ {\underset{˙}{\oplus} ↾}_{(S \times Y)} \in (H GrpAct Y) \leftrightarrow ((H \in Grp \land Y \in V) \land (({\underset{˙}{\oplus} ↾}_{(S \times Y)}) : {Base}_{H} \times Y ⟶ Y \land \forall x \in Y (0_{H} ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = x \land \forall y \in {Base}_{H} \forall z \in {Base}_{H} (y +_{H} z) ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x = y ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) (z ({\underset{˙}{\oplus} ↾}_{(S \times Y)}) x))))$
75	4 70 74	sylanbrc	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land S \in SubGrp (G)) \to {\underset{˙}{\oplus} ↾}_{(S \times Y)} \in (H GrpAct Y)$

Metamath Proof Explorer

Theorem gasubg

Proof