subgga

Description: A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	subgga.1	$⊢ X = {Base}_{G}$
	subgga.2	$⊢ \underset{˙}{+} = +_{G}$
	subgga.3	$⊢ H = G ↾_{𝑠} Y$
	subgga.4	$⊢ F = (x \in Y, y \in X ⟼ x \underset{˙}{+} y)$
Assertion	subgga	$⊢ Y \in SubGrp (G) \to F \in (H GrpAct X)$

Proof

Step	Hyp	Ref	Expression
1		subgga.1	$⊢ X = {Base}_{G}$
2		subgga.2	$⊢ \underset{˙}{+} = +_{G}$
3		subgga.3	$⊢ H = G ↾_{𝑠} Y$
4		subgga.4	$⊢ F = (x \in Y, y \in X ⟼ x \underset{˙}{+} y)$
5	3	subggrp	$⊢ Y \in SubGrp (G) \to H \in Grp$
6	1	fvexi	$⊢ X \in V$
7	5 6	jctir	$⊢ Y \in SubGrp (G) \to (H \in Grp \land X \in V)$
8		subgrcl	$⊢ Y \in SubGrp (G) \to G \in Grp$
9	8	adantr	$⊢ (Y \in SubGrp (G) \land (x \in Y \land y \in X)) \to G \in Grp$
10	1	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq X$
11	10	sselda	$⊢ (Y \in SubGrp (G) \land x \in Y) \to x \in X$
12	11	adantrr	$⊢ (Y \in SubGrp (G) \land (x \in Y \land y \in X)) \to x \in X$
13		simprr	$⊢ (Y \in SubGrp (G) \land (x \in Y \land y \in X)) \to y \in X$
14	1 2	grpcl	$⊢ (G \in Grp \land x \in X \land y \in X) \to x \underset{˙}{+} y \in X$
15	9 12 13 14	syl3anc	$⊢ (Y \in SubGrp (G) \land (x \in Y \land y \in X)) \to x \underset{˙}{+} y \in X$
16	15	ralrimivva	$⊢ Y \in SubGrp (G) \to \forall x \in Y \forall y \in X x \underset{˙}{+} y \in X$
17	4	fmpo	$⊢ \forall x \in Y \forall y \in X x \underset{˙}{+} y \in X \leftrightarrow F : Y \times X ⟶ X$
18	16 17	sylib	$⊢ Y \in SubGrp (G) \to F : Y \times X ⟶ X$
19	3	subgbas	$⊢ Y \in SubGrp (G) \to Y = {Base}_{H}$
20	19	xpeq1d	$⊢ Y \in SubGrp (G) \to Y \times X = {Base}_{H} \times X$
21	20	feq2d	$⊢ Y \in SubGrp (G) \to (F : Y \times X ⟶ X \leftrightarrow F : {Base}_{H} \times X ⟶ X)$
22	18 21	mpbid	$⊢ Y \in SubGrp (G) \to F : {Base}_{H} \times X ⟶ X$
23		eqid	$⊢ 0_{G} = 0_{G}$
24	23	subg0cl	$⊢ Y \in SubGrp (G) \to 0_{G} \in Y$
25		oveq12	$⊢ (x = 0_{G} \land y = u) \to x \underset{˙}{+} y = 0_{G} \underset{˙}{+} u$
26		ovex	$⊢ 0_{G} \underset{˙}{+} u \in V$
27	25 4 26	ovmpoa	$⊢ (0_{G} \in Y \land u \in X) \to 0_{G} F u = 0_{G} \underset{˙}{+} u$
28	24 27	sylan	$⊢ (Y \in SubGrp (G) \land u \in X) \to 0_{G} F u = 0_{G} \underset{˙}{+} u$
29	3 23	subg0	$⊢ Y \in SubGrp (G) \to 0_{G} = 0_{H}$
30	29	oveq1d	$⊢ Y \in SubGrp (G) \to 0_{G} F u = 0_{H} F u$
31	30	adantr	$⊢ (Y \in SubGrp (G) \land u \in X) \to 0_{G} F u = 0_{H} F u$
32	1 2 23	grplid	$⊢ (G \in Grp \land u \in X) \to 0_{G} \underset{˙}{+} u = u$
33	8 32	sylan	$⊢ (Y \in SubGrp (G) \land u \in X) \to 0_{G} \underset{˙}{+} u = u$
34	28 31 33	3eqtr3d	$⊢ (Y \in SubGrp (G) \land u \in X) \to 0_{H} F u = u$
35	8	ad2antrr	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to G \in Grp$
36	10	ad2antrr	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to Y \subseteq X$
37		simprl	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to v \in Y$
38	36 37	sseldd	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to v \in X$
39		simprr	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to w \in Y$
40	36 39	sseldd	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to w \in X$
41		simplr	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to u \in X$
42	1 2	grpass	$⊢ (G \in Grp \land (v \in X \land w \in X \land u \in X)) \to (v \underset{˙}{+} w) \underset{˙}{+} u = v \underset{˙}{+} (w \underset{˙}{+} u)$
43	35 38 40 41 42	syl13anc	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to (v \underset{˙}{+} w) \underset{˙}{+} u = v \underset{˙}{+} (w \underset{˙}{+} u)$
44	1 2	grpcl	$⊢ (G \in Grp \land w \in X \land u \in X) \to w \underset{˙}{+} u \in X$
45	35 40 41 44	syl3anc	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to w \underset{˙}{+} u \in X$
46		oveq12	$⊢ (x = v \land y = w \underset{˙}{+} u) \to x \underset{˙}{+} y = v \underset{˙}{+} (w \underset{˙}{+} u)$
47		ovex	$⊢ v \underset{˙}{+} (w \underset{˙}{+} u) \in V$
48	46 4 47	ovmpoa	$⊢ (v \in Y \land w \underset{˙}{+} u \in X) \to v F (w \underset{˙}{+} u) = v \underset{˙}{+} (w \underset{˙}{+} u)$
49	37 45 48	syl2anc	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to v F (w \underset{˙}{+} u) = v \underset{˙}{+} (w \underset{˙}{+} u)$
50	43 49	eqtr4d	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to (v \underset{˙}{+} w) \underset{˙}{+} u = v F (w \underset{˙}{+} u)$
51	2	subgcl	$⊢ (Y \in SubGrp (G) \land v \in Y \land w \in Y) \to v \underset{˙}{+} w \in Y$
52	51	3expb	$⊢ (Y \in SubGrp (G) \land (v \in Y \land w \in Y)) \to v \underset{˙}{+} w \in Y$
53	52	adantlr	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to v \underset{˙}{+} w \in Y$
54		oveq12	$⊢ (x = v \underset{˙}{+} w \land y = u) \to x \underset{˙}{+} y = (v \underset{˙}{+} w) \underset{˙}{+} u$
55		ovex	$⊢ (v \underset{˙}{+} w) \underset{˙}{+} u \in V$
56	54 4 55	ovmpoa	$⊢ (v \underset{˙}{+} w \in Y \land u \in X) \to (v \underset{˙}{+} w) F u = (v \underset{˙}{+} w) \underset{˙}{+} u$
57	53 41 56	syl2anc	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to (v \underset{˙}{+} w) F u = (v \underset{˙}{+} w) \underset{˙}{+} u$
58		oveq12	$⊢ (x = w \land y = u) \to x \underset{˙}{+} y = w \underset{˙}{+} u$
59		ovex	$⊢ w \underset{˙}{+} u \in V$
60	58 4 59	ovmpoa	$⊢ (w \in Y \land u \in X) \to w F u = w \underset{˙}{+} u$
61	39 41 60	syl2anc	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to w F u = w \underset{˙}{+} u$
62	61	oveq2d	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to v F (w F u) = v F (w \underset{˙}{+} u)$
63	50 57 62	3eqtr4d	$⊢ ((Y \in SubGrp (G) \land u \in X) \land (v \in Y \land w \in Y)) \to (v \underset{˙}{+} w) F u = v F (w F u)$
64	63	ralrimivva	$⊢ (Y \in SubGrp (G) \land u \in X) \to \forall v \in Y \forall w \in Y (v \underset{˙}{+} w) F u = v F (w F u)$
65	3 2	ressplusg	$⊢ Y \in SubGrp (G) \to \underset{˙}{+} = +_{H}$
66	65	oveqd	$⊢ Y \in SubGrp (G) \to v \underset{˙}{+} w = v +_{H} w$
67	66	oveq1d	$⊢ Y \in SubGrp (G) \to (v \underset{˙}{+} w) F u = (v +_{H} w) F u$
68	67	eqeq1d	$⊢ Y \in SubGrp (G) \to ((v \underset{˙}{+} w) F u = v F (w F u) \leftrightarrow (v +_{H} w) F u = v F (w F u))$
69	19 68	raleqbidv	$⊢ Y \in SubGrp (G) \to (\forall w \in Y (v \underset{˙}{+} w) F u = v F (w F u) \leftrightarrow \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u))$
70	19 69	raleqbidv	$⊢ Y \in SubGrp (G) \to (\forall v \in Y \forall w \in Y (v \underset{˙}{+} w) F u = v F (w F u) \leftrightarrow \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u))$
71	70	biimpa	$⊢ (Y \in SubGrp (G) \land \forall v \in Y \forall w \in Y (v \underset{˙}{+} w) F u = v F (w F u)) \to \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u)$
72	64 71	syldan	$⊢ (Y \in SubGrp (G) \land u \in X) \to \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u)$
73	34 72	jca	$⊢ (Y \in SubGrp (G) \land u \in X) \to (0_{H} F u = u \land \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u))$
74	73	ralrimiva	$⊢ Y \in SubGrp (G) \to \forall u \in X (0_{H} F u = u \land \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u))$
75	22 74	jca	$⊢ Y \in SubGrp (G) \to (F : {Base}_{H} \times X ⟶ X \land \forall u \in X (0_{H} F u = u \land \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u)))$
76		eqid	$⊢ {Base}_{H} = {Base}_{H}$
77		eqid	$⊢ +_{H} = +_{H}$
78		eqid	$⊢ 0_{H} = 0_{H}$
79	76 77 78	isga	$⊢ F \in (H GrpAct X) \leftrightarrow ((H \in Grp \land X \in V) \land (F : {Base}_{H} \times X ⟶ X \land \forall u \in X (0_{H} F u = u \land \forall v \in {Base}_{H} \forall w \in {Base}_{H} (v +_{H} w) F u = v F (w F u))))$
80	7 75 79	sylanbrc	$⊢ Y \in SubGrp (G) \to F \in (H GrpAct X)$

Metamath Proof Explorer

Theorem subgga

Proof