Theorem ssga 9455

Description: A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009.)

Hypotheses

Ref	Expression
ssga.1	|- X = ran G
ssga.2	|- Y = ran H

Assertion

Ref	Expression
ssga	|- (H e. (SubGrp` G) -> <.H, (G |` (Y X. X))>. e. GrpAct)

Proof of Theorem ssga

Step	Hyp	Ref	Expression
1		issubg 9425	. . . . 5 |- (H e. (SubGrp` G) <-> (G e. Grp /\ H e. Grp /\ H C_ G))
2	1	simp2bi 892	. . . 4 |- (H e. (SubGrp` G) -> H e. Grp)
3		df-fn 4009	. . . . . . 7 |- ((G |` (Y X. X)) Fn (Y X. X) <-> (Fun (G |` (Y X. X)) /\ dom ( G |` (Y X. X)) = (Y X. X)))
4	1	simp1bi 891	. . . . . . . 8 |- (H e. (SubGrp` G) -> G e. Grp)
5		ssga.1	. . . . . . . . 9 |- X = ran G
6	5	grpfo 9323	. . . . . . . 8 |- (G e. Grp -> G:(X X. X)-onto->X)
7		fofun 4618	. . . . . . . . 9 |- (G:(X X. X)-onto->X -> Fun G)
8		funres 4459	. . . . . . . . 9 |- (Fun G -> Fun (G |` (Y X. X)))
9	7, 8	syl 12	. . . . . . . 8 |- (G:(X X. X)-onto->X -> Fun (G |` (Y X. X)))
10	4, 6, 9	3syl 24	. . . . . . 7 |- (H e. (SubGrp` G) -> Fun (G |` (Y X. X)))
11		ssga.2	. . . . . . . . . . 11 |- Y = ran H
12	5, 11	subgrnss 9428	. . . . . . . . . 10 |- (H e. (SubGrp` G) -> Y C_ X)
13		ssel 2615	. . . . . . . . . . . . . . . . . . . 20 |- (Y C_ X -> (y e. Y -> y e. X))
14	13	impcom 378	. . . . . . . . . . . . . . . . . . 19 |- ((y e. Y /\ Y C_ X) -> y e. X)
15	14	adantlr 429	. . . . . . . . . . . . . . . . . 18 |- (((y e. Y /\ z e. X) /\ Y C_ X) -> y e. X)
16		simplr 449	. . . . . . . . . . . . . . . . . 18 |- (((y e. Y /\ z e. X) /\ Y C_ X) -> z e. X)
17		opelxpi 4040	. . . . . . . . . . . . . . . . . 18 |- ((y e. X /\ z e. X) -> <.y, z>. e. (X X. X))
18	15, 16, 17	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- (((y e. Y /\ z e. X) /\ Y C_ X) -> <.y, z>. e. (X X. X))
19	18	ex 402	. . . . . . . . . . . . . . . 16 |- ((y e. Y /\ z e. X) -> (Y C_ X -> <.y, z>. e. (X X. X)))
20	19	adantl 424	. . . . . . . . . . . . . . 15 |- ((x = <.y, z>. /\ (y e. Y /\ z e. X)) -> (Y C_ X -> <.y, z>. e. (X X. X)))
21		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (x = <.y, z>. -> (x e. (X X. X) <-> <.y, z>. e. (X X. X)))
22	21	adantr 425	. . . . . . . . . . . . . . 15 |- ((x = <.y, z>. /\ (y e. Y /\ z e. X)) -> (x e. (X X. X) <-> <.y, z>. e. (X X. X)))
23	20, 22	sylibrd 221	. . . . . . . . . . . . . 14 |- ((x = <.y, z>. /\ (y e. Y /\ z e. X)) -> (Y C_ X -> x e. (X X. X)))
24	23	19.23aivv 1675	. . . . . . . . . . . . 13 |- (E.yE.z(x = <.y, z>. /\ (y e. Y /\ z e. X)) -> (Y C_ X -> x e. (X X. X)))
25	24	com12 14	. . . . . . . . . . . 12 |- (Y C_ X -> (E.yE.z(x = <.y, z>. /\ (y e. Y /\ z e. X)) -> x e. (X X. X)))
26		elxp 4018	. . . . . . . . . . . 12 |- (x e. (Y X. X) <-> E.yE.z(x = <.y, z>. /\ (y e. Y /\ z e. X)))
27	25, 26	syl5ib 223	. . . . . . . . . . 11 |- (Y C_ X -> (x e. (Y X. X) -> x e. (X X. X)))
28	27	ssrdv 2622	. . . . . . . . . 10 |- (Y C_ X -> (Y X. X) C_ (X X. X))
29	12, 28	syl 12	. . . . . . . . 9 |- (H e. (SubGrp` G) -> (Y X. X) C_ (X X. X))
30		fof 4617	. . . . . . . . . . 11 |- (G:(X X. X)-onto->X -> G:(X X. X)-->X)
31		fdm 4567	. . . . . . . . . . 11 |- (G:(X X. X)-->X -> dom G = (X X. X))
32	30, 31	syl 12	. . . . . . . . . 10 |- (G:(X X. X)-onto->X -> dom G = (X X. X))
33	4, 6, 32	3syl 24	. . . . . . . . 9 |- (H e. (SubGrp` G) -> dom G = (X X. X))
34	29, 33	sseqtr4d 2654	. . . . . . . 8 |- (H e. (SubGrp` G) -> (Y X. X) C_ dom G)
35		ssdmres 4235	. . . . . . . 8 |- ((Y X. X) C_ dom G <-> dom ( G |` (Y X. X)) = (Y X. X))
36	34, 35	sylib 215	. . . . . . 7 |- (H e. (SubGrp` G) -> dom ( G |` (Y X. X)) = (Y X. X))
37	3, 10, 36	sylanbrc 527	. . . . . 6 |- (H e. (SubGrp` G) -> (G |` (Y X. X)) Fn (Y X. X))
38		resss 4237	. . . . . . . 8 |- (G |` (Y X. X)) C_ G
39		rnss 4189	. . . . . . . 8 |- ((G |` (Y X. X)) C_ G -> ran ( G |` (Y X. X)) C_ ran G)
40	38, 39	ax-mp 7	. . . . . . 7 |- ran ( G |` (Y X. X)) C_ ran G
41	40, 5	sseqtr4i 2650	. . . . . 6 |- ran ( G |` (Y X. X)) C_ X
42	37, 41	jctir 317	. . . . 5 |- (H e. (SubGrp` G) -> ((G |` (Y X. X)) Fn (Y X. X) /\ ran ( G |` (Y X. X)) C_ X))
43		df-f 4010	. . . . 5 |- ((G |` (Y X. X)):(Y X. X)-->X <-> ((G |` (Y X. X)) Fn (Y X. X) /\ ran ( G |` (Y X. X)) C_ X))
44	42, 43	sylibr 217	. . . 4 |- (H e. (SubGrp` G) -> (G |` (Y X. X)):(Y X. X)-->X)
45		opelxpi 4040	. . . . . . . . . 10 |- (((Id` H) e. Y /\ x e. X) -> <.(Id` H), x>. e. (Y X. X))
46		eqid 1884	. . . . . . . . . . . . 13 |- (Id` H) = (Id` H)
47	11, 46	grpidcl 9343	. . . . . . . . . . . 12 |- (H e. Grp -> (Id` H) e. Y)
48	47	3ad2ant2 898	. . . . . . . . . . 11 |- ((G e. Grp /\ H e. Grp /\ H C_ G) -> (Id` H) e. Y)
49	1, 48	sylbi 216	. . . . . . . . . 10 |- (H e. (SubGrp` G) -> (Id` H) e. Y)
50	45, 49	sylan 497	. . . . . . . . 9 |- ((H e. (SubGrp` G) /\ x e. X) -> <.(Id` H), x>. e. (Y X. X))
51		fvres 4691	. . . . . . . . 9 |- (<.(Id` H), x>. e. (Y X. X) -> ((G |` (Y X. X))` <.(Id` H), x>.) = (G` <.(Id` H), x>.))
52	50, 51	syl 12	. . . . . . . 8 |- ((H e. (SubGrp` G) /\ x e. X) -> ((G |` (Y X. X))` <.(Id` H), x>.) = (G` <.(Id` H), x>.))
53		eqid 1884	. . . . . . . . . . . . 13 |- (Id` G) = (Id` G)
54	53, 46	subgid 9429	. . . . . . . . . . . 12 |- (H e. (SubGrp` G) -> (Id` H) = (Id` G))
55	54	adantr 425	. . . . . . . . . . 11 |- ((H e. (SubGrp` G) /\ x e. X) -> (Id` H) = (Id` G))
56	55	opreq1d 4897	. . . . . . . . . 10 |- ((H e. (SubGrp` G) /\ x e. X) -> ((Id` H)Gx) = ((Id` G)Gx))
57	5, 53	grplid 9345	. . . . . . . . . . 11 |- ((G e. Grp /\ x e. X) -> ((Id` G)Gx) = x)
58	57, 4	sylan 497	. . . . . . . . . 10 |- ((H e. (SubGrp` G) /\ x e. X) -> ((Id` G)Gx) = x)
59	56, 58	eqtrd 1925	. . . . . . . . 9 |- ((H e. (SubGrp` G) /\ x e. X) -> ((Id` H)Gx) = x)
60		df-opr 4886	. . . . . . . . 9 |- ((Id` H)Gx) = (G` <.(Id` H), x>.)
61	59, 60	syl5eqr 1942	. . . . . . . 8 |- ((H e. (SubGrp` G) /\ x e. X) -> (G` <.(Id` H), x>.) = x)
62	52, 61	eqtrd 1925	. . . . . . 7 |- ((H e. (SubGrp` G) /\ x e. X) -> ((G |` (Y X. X))` <.(Id` H), x>.) = x)
63		df-opr 4886	. . . . . . 7 |- ((Id` H)(G |` (Y X. X))x) = ((G |` (Y X. X))` <.(Id` H), x>.)
64	62, 63	syl5eq 1940	. . . . . 6 |- ((H e. (SubGrp` G) /\ x e. X) -> ((Id` H)(G |` (Y X. X))x) = x)
65	11	grpfo 9323	. . . . . . . . . . . . . . . . 17 |- (H e. Grp -> H:(Y X. Y)-onto->Y)
66		fof 4617	. . . . . . . . . . . . . . . . 17 |- (H:(Y X. Y)-onto->Y -> H:(Y X. Y)-->Y)
67	65, 66	syl 12	. . . . . . . . . . . . . . . 16 |- (H e. Grp -> H:(Y X. Y)-->Y)
68	67	3ad2ant2 898	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ H e. Grp /\ H C_ G) -> H:(Y X. Y)-->Y)
69	1, 68	sylbi 216	. . . . . . . . . . . . . 14 |- (H e. (SubGrp` G) -> H:(Y X. Y)-->Y)
70	69	ad2antrr 440	. . . . . . . . . . . . 13 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> H:(Y X. Y)-->Y)
71		simprl 450	. . . . . . . . . . . . 13 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> y e. Y)
72		simprr 451	. . . . . . . . . . . . 13 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> z e. Y)
73		foprrn 4965	. . . . . . . . . . . . 13 |- ((H:(Y X. Y)-->Y /\ y e. Y /\ z e. Y) -> (yHz) e. Y)
74	70, 71, 72, 73	syl111anc 1100	. . . . . . . . . . . 12 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (yHz) e. Y)
75		simplr 449	. . . . . . . . . . . 12 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> x e. X)
76		opelxpi 4040	. . . . . . . . . . . 12 |- (((yHz) e. Y /\ x e. X) -> <.(yHz), x>. e. (Y X. X))
77	74, 75, 76	syl11anc 524	. . . . . . . . . . 11 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> <.(yHz), x>. e. (Y X. X))
78		fvres 4691	. . . . . . . . . . 11 |- (<.(yHz), x>. e. (Y X. X) -> ((G |` (Y X. X))` <.(yHz), x>.) = (G` <.(yHz), x>.))
79	77, 78	syl 12	. . . . . . . . . 10 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((G |` (Y X. X))` <.(yHz), x>.) = (G` <.(yHz), x>.))
80		df-opr 4886	. . . . . . . . . 10 |- ((yHz)(G |` (Y X. X))x) = ((G |` (Y X. X))` <.(yHz), x>.)
81	79, 80	syl5eq 1940	. . . . . . . . 9 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((yHz)(G |` (Y X. X))x) = (G` <.(yHz), x>.))
82		simpll 448	. . . . . . . . . . . 12 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> H e. (SubGrp` G))
83		simpr 350	. . . . . . . . . . . 12 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (y e. Y /\ z e. Y))
84	11	subgopr 9427	. . . . . . . . . . . 12 |- (H e. (SubGrp` G) -> ((y e. Y /\ z e. Y) -> (yHz) = (yGz)))
85	82, 83, 84	sylc 83	. . . . . . . . . . 11 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (yHz) = (yGz))
86	85	opreq1d 4897	. . . . . . . . . 10 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((yHz)Gx) = ((yGz)Gx))
87		df-opr 4886	. . . . . . . . . 10 |- ((yHz)Gx) = (G` <.(yHz), x>.)
88	86, 87	syl5eqr 1942	. . . . . . . . 9 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (G` <.(yHz), x>.) = ((yGz)Gx))
89		opelxpi 4040	. . . . . . . . . . . . . . . 16 |- ((z e. Y /\ x e. X) -> <.z, x>. e. (Y X. X))
90	89	ancoms 484	. . . . . . . . . . . . . . 15 |- ((x e. X /\ z e. Y) -> <.z, x>. e. (Y X. X))
91	90	adantll 428	. . . . . . . . . . . . . 14 |- (((H e. (SubGrp` G) /\ x e. X) /\ z e. Y) -> <.z, x>. e. (Y X. X))
92		fvres 4691	. . . . . . . . . . . . . 14 |- (<.z, x>. e. (Y X. X) -> ((G |` (Y X. X))` <.z, x>.) = (G` <.z, x>.))
93	91, 92	syl 12	. . . . . . . . . . . . 13 |- (((H e. (SubGrp` G) /\ x e. X) /\ z e. Y) -> ((G |` (Y X. X))` <.z, x>.) = (G` <.z, x>.))
94		df-opr 4886	. . . . . . . . . . . . 13 |- (z(G |` (Y X. X))x) = ((G |` (Y X. X))` <.z, x>.)
95		df-opr 4886	. . . . . . . . . . . . 13 |- (zGx) = (G` <.z, x>.)
96	93, 94, 95	3eqtr4g 1953	. . . . . . . . . . . 12 |- (((H e. (SubGrp` G) /\ x e. X) /\ z e. Y) -> (z(G |` (Y X. X))x) = (zGx))
97	96	adantrl 430	. . . . . . . . . . 11 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (z(G |` (Y X. X))x) = (zGx))
98	97	opreq2d 4898	. . . . . . . . . 10 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (yG(z(G |` (Y X. X))x)) = (yG(zGx)))
99	90	ad2ant2l 444	. . . . . . . . . . . . . . . 16 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> <.z, x>. e. (Y X. X))
100	99, 92	syl 12	. . . . . . . . . . . . . . 15 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((G |` (Y X. X))` <.z, x>.) = (G` <.z, x>.))
101	100, 94	syl5eq 1940	. . . . . . . . . . . . . 14 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (z(G |` (Y X. X))x) = (G` <.z, x>.))
102	4, 6, 30	3syl 24	. . . . . . . . . . . . . . . . 17 |- (H e. (SubGrp` G) -> G:(X X. X)-->X)
103	102	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> G:(X X. X)-->X)
104		ssel2 2616	. . . . . . . . . . . . . . . . . 18 |- ((Y C_ X /\ z e. Y) -> z e. X)
105	104	ad2ant2rl 447	. . . . . . . . . . . . . . . . 17 |- (((Y C_ X /\ x e. X) /\ (y e. Y /\ z e. Y)) -> z e. X)
106	105, 12	sylanl1 509	. . . . . . . . . . . . . . . 16 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> z e. X)
107		foprrn 4965	. . . . . . . . . . . . . . . 16 |- ((G:(X X. X)-->X /\ z e. X /\ x e. X) -> (zGx) e. X)
108	103, 106, 75, 107	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (zGx) e. X)
109	108, 95	syl5eqelr 1976	. . . . . . . . . . . . . 14 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (G` <.z, x>.) e. X)
110	101, 109	eqeltrd 1971	. . . . . . . . . . . . 13 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (z(G |` (Y X. X))x) e. X)
111		opelxpi 4040	. . . . . . . . . . . . 13 |- ((y e. Y /\ (z(G |` (Y X. X))x) e. X) -> <.y, (z(G |` (Y X. X))x)>. e. (Y X. X))
112	71, 110, 111	syl11anc 524	. . . . . . . . . . . 12 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> <.y, (z(G |` (Y X. X))x)>. e. (Y X. X))
113		fvres 4691	. . . . . . . . . . . 12 |- (<.y, (z(G |` (Y X. X))x)>. e. (Y X. X) -> ((G |` (Y X. X))` <.y, (z(G |` (Y X. X))x)>.) = (G` <.y, (z(G |` (Y X. X))x)>.))
114	112, 113	syl 12	. . . . . . . . . . 11 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((G |` (Y X. X))` <.y, (z(G |` (Y X. X))x)>.) = (G` <.y, (z(G |` (Y X. X))x)>.))
115		df-opr 4886	. . . . . . . . . . 11 |- (y(G |` (Y X. X))(z(G |` (Y X. X))x)) = ((G |` (Y X. X))` <.y, (z(G |` (Y X. X))x)>.)
116		df-opr 4886	. . . . . . . . . . 11 |- (yG(z(G |` (Y X. X))x)) = (G` <.y, (z(G |` (Y X. X))x)>.)
117	114, 115, 116	3eqtr4g 1953	. . . . . . . . . 10 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (y(G |` (Y X. X))(z(G |` (Y X. X))x)) = (yG(z(G |` (Y X. X))x)))
118	4	ad2antrr 440	. . . . . . . . . . 11 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> G e. Grp)
119		ssel2 2616	. . . . . . . . . . . . . 14 |- ((Y C_ X /\ y e. Y) -> y e. X)
120	119	ad2ant2r 445	. . . . . . . . . . . . 13 |- (((Y C_ X /\ x e. X) /\ (y e. Y /\ z e. Y)) -> y e. X)
121		simplr 449	. . . . . . . . . . . . 13 |- (((Y C_ X /\ x e. X) /\ (y e. Y /\ z e. Y)) -> x e. X)
122	120, 105, 121	3jca 1050	. . . . . . . . . . . 12 |- (((Y C_ X /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (y e. X /\ z e. X /\ x e. X))
123	122, 12	sylanl1 509	. . . . . . . . . . 11 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> (y e. X /\ z e. X /\ x e. X))
124	5	grpass 9327	. . . . . . . . . . 11 |- ((G e. Grp /\ (y e. X /\ z e. X /\ x e. X)) -> ((yGz)Gx) = (yG(zGx)))
125	118, 123, 124	syl11anc 524	. . . . . . . . . 10 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((yGz)Gx) = (yG(zGx)))
126	98, 117, 125	3eqtr4rd 1939	. . . . . . . . 9 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((yGz)Gx) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))
127	81, 88, 126	3eqtrd 1929	. . . . . . . 8 |- (((H e. (SubGrp` G) /\ x e. X) /\ (y e. Y /\ z e. Y)) -> ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))
128	127	ex 402	. . . . . . 7 |- ((H e. (SubGrp` G) /\ x e. X) -> ((y e. Y /\ z e. Y) -> ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))
129	128	r19.21aivv 2183	. . . . . 6 |- ((H e. (SubGrp` G) /\ x e. X) -> A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))
130	64, 129	jca 310	. . . . 5 |- ((H e. (SubGrp` G) /\ x e. X) -> (((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))
131	130	r19.21aiva 2176	. . . 4 |- (H e. (SubGrp` G) -> A.x e. X (((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))
132	2, 44, 131	3jca 1050	. . 3 |- (H e. (SubGrp` G) -> (H e. Grp /\ (G |` (Y X. X)):(Y X. X)-->X /\ A.x e. X (((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))))
133		imassrn 4278	. . . . . . . 8 |- (G"(Y X. X)) C_ ran G
134	133, 5	sseqtr4i 2650	. . . . . . 7 |- (G"(Y X. X)) C_ X
135	134	a1i 8	. . . . . 6 |- (H e. (SubGrp` G) -> (G"(Y X. X)) C_ X)
136	2, 47	syl 12	. . . . . . . . . . . . 13 |- (H e. (SubGrp` G) -> (Id` H) e. Y)
137	136	adantr 425	. . . . . . . . . . . 12 |- ((H e. (SubGrp` G) /\ x e. X) -> (Id` H) e. Y)
138		simpr 350	. . . . . . . . . . . 12 |- ((H e. (SubGrp` G) /\ x e. X) -> x e. X)
139		df-opr 4886	. . . . . . . . . . . . . . 15 |- ((Id` G)Gx) = (G` <.(Id` G), x>.)
140	57, 139	syl5eqr 1942	. . . . . . . . . . . . . 14 |- ((G e. Grp /\ x e. X) -> (G` <.(Id` G), x>.) = x)
141	140, 4	sylan 497	. . . . . . . . . . . . 13 |- ((H e. (SubGrp` G) /\ x e. X) -> (G` <.(Id` G), x>.) = x)
142		opeq1 3158	. . . . . . . . . . . . . . . . 17 |- ((Id` H) = (Id` G) -> <.(Id` H), x>. = <.(Id` G), x>.)
143	142	fveq2d 4685	. . . . . . . . . . . . . . . 16 |- ((Id` H) = (Id` G) -> (G` <.(Id` H), x>.) = (G` <.(Id` G), x>.))
144	143	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- ((Id` H) = (Id` G) -> ((G` <.(Id` H), x>.) = x <-> (G` <.(Id` G), x>.) = x))
145	54, 144	syl 12	. . . . . . . . . . . . . 14 |- (H e. (SubGrp` G) -> ((G` <.(Id` H), x>.) = x <-> (G` <.(Id` G), x>.) = x))
146	145	adantr 425	. . . . . . . . . . . . 13 |- ((H e. (SubGrp` G) /\ x e. X) -> ((G` <.(Id` H), x>.) = x <-> (G` <.(Id` G), x>.) = x))
147	141, 146	mpbird 213	. . . . . . . . . . . 12 |- ((H e. (SubGrp` G) /\ x e. X) -> (G` <.(Id` H), x>.) = x)
148	137, 138, 147	jca31 311	. . . . . . . . . . 11 |- ((H e. (SubGrp` G) /\ x e. X) -> (((Id` H) e. Y /\ x e. X) /\ (G` <.(Id` H), x>.) = x))
149		visset 2295	. . . . . . . . . . . . . . 15 |- x e. _V
150	149	opelxp 4036	. . . . . . . . . . . . . 14 |- (<.(Id` H), x>. e. (Y X. X) <-> ((Id` H) e. Y /\ x e. X))
151	150	bicomi 189	. . . . . . . . . . . . 13 |- (((Id` H) e. Y /\ x e. X) <-> <.(Id` H), x>. e. (Y X. X))
152	151	a1i 8	. . . . . . . . . . . 12 |- ((H e. (SubGrp` G) /\ x e. X) -> (((Id` H) e. Y /\ x e. X) <-> <.(Id` H), x>. e. (Y X. X)))
153	4, 6, 7	3syl 24	. . . . . . . . . . . . . 14 |- (H e. (SubGrp` G) -> Fun G)
154	153	adantr 425	. . . . . . . . . . . . 13 |- ((H e. (SubGrp` G) /\ x e. X) -> Fun G)
155		opelxpi 4040	. . . . . . . . . . . . . . 15 |- (((Id` H) e. X /\ x e. X) -> <.(Id` H), x>. e. (X X. X))
156	12, 136	sseldd 2620	. . . . . . . . . . . . . . 15 |- (H e. (SubGrp` G) -> (Id` H) e. X)
157	155, 156	sylan 497	. . . . . . . . . . . . . 14 |- ((H e. (SubGrp` G) /\ x e. X) -> <.(Id` H), x>. e. (X X. X))
158	4, 6	syl 12	. . . . . . . . . . . . . . . 16 |- (H e. (SubGrp` G) -> G:(X X. X)-onto->X)
159	158, 30, 31	3syl 24	. . . . . . . . . . . . . . 15 |- (H e. (SubGrp` G) -> dom G = (X X. X))
160	159	adantr 425	. . . . . . . . . . . . . 14 |- ((H e. (SubGrp` G) /\ x e. X) -> dom G = (X X. X))
161	157, 160	eleqtrrd 1974	. . . . . . . . . . . . 13 |- ((H e. (SubGrp` G) /\ x e. X) -> <.(Id` H), x>. e. dom G)
162	149	funopfvb 4715	. . . . . . . . . . . . 13 |- ((Fun G /\ <.(Id` H), x>. e. dom G) -> ((G` <.(Id` H), x>.) = x <-> <.<.(Id` H), x>., x>. e. G))
163	154, 161, 162	syl11anc 524	. . . . . . . . . . . 12 |- ((H e. (SubGrp` G) /\ x e. X) -> ((G` <.(Id` H), x>.) = x <-> <.<.(Id` H), x>., x>. e. G))
164	152, 163	anbi12d 690	. . . . . . . . . . 11 |- ((H e. (SubGrp` G) /\ x e. X) -> ((((Id` H) e. Y /\ x e. X) /\ (G` <.(Id` H), x>.) = x) <-> (<.(Id` H), x>. e. (Y X. X) /\ <.<.(Id` H), x>., x>. e. G)))
165	148, 164	mpbid 212	. . . . . . . . . 10 |- ((H e. (SubGrp` G) /\ x e. X) -> (<.(Id` H), x>. e. (Y X. X) /\ <.<.(Id` H), x>., x>. e. G))
166	165	ex 402	. . . . . . . . 9 |- (H e. (SubGrp` G) -> (x e. X -> (<.(Id` H), x>. e. (Y X. X) /\ <.<.(Id` H), x>., x>. e. G)))
167		opex 3527	. . . . . . . . . 10 |- <.(Id` H), x>. e. _V
168		eleq1 1957	. . . . . . . . . . 11 |- (y = <.(Id` H), x>. -> (y e. (Y X. X) <-> <.(Id` H), x>. e. (Y X. X)))
169		opeq1 3158	. . . . . . . . . . . 12 |- (y = <.(Id` H), x>. -> <.y, x>. = <.<.(Id` H), x>., x>.)
170	169	eleq1d 1963	. . . . . . . . . . 11 |- (y = <.(Id` H), x>. -> (<.y, x>. e. G <-> <.<.(Id` H), x>., x>. e. G))
171	168, 170	anbi12d 690	. . . . . . . . . 10 |- (y = <.(Id` H), x>. -> ((y e. (Y X. X) /\ <.y, x>. e. G) <-> (<.(Id` H), x>. e. (Y X. X) /\ <.<.(Id` H), x>., x>. e. G)))
172	167, 171	cla4ev 2371	. . . . . . . . 9 |- ((<.(Id` H), x>. e. (Y X. X) /\ <.<.(Id` H), x>., x>. e. G) -> E.y(y e. (Y X. X) /\ <.y, x>. e. G))
173	166, 172	syl6 25	. . . . . . . 8 |- (H e. (SubGrp` G) -> (x e. X -> E.y(y e. (Y X. X) /\ <.y, x>. e. G)))
174	149	elima3 4272	. . . . . . . 8 |- (x e. (G"(Y X. X)) <-> E.y(y e. (Y X. X) /\ <.y, x>. e. G))
175	173, 174	syl6ibr 230	. . . . . . 7 |- (H e. (SubGrp` G) -> (x e. X -> x e. (G"(Y X. X))))
176	175	ssrdv 2622	. . . . . 6 |- (H e. (SubGrp` G) -> X C_ (G"(Y X. X)))
177	135, 176	eqssd 2633	. . . . 5 |- (H e. (SubGrp` G) -> (G"(Y X. X)) = X)
178		df-ima 4007	. . . . 5 |- (G"(Y X. X)) = ran ( G |` (Y X. X))
179	177, 178	syl5eqr 1942	. . . 4 |- (H e. (SubGrp` G) -> ran ( G |` (Y X. X)) = X)
180		xpeq2 4017	. . . . . 6 |- (ran ( G |` (Y X. X)) = X -> (Y X. ran ( G |` (Y X. X))) = (Y X. X))
181		feq23 4554	. . . . . 6 |- (((Y X. ran ( G |` (Y X. X))) = (Y X. X) /\ ran ( G |` (Y X. X)) = X) -> ((G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) <-> (G |` (Y X. X)):(Y X. X)-->X))
182	180, 181	mpancom 769	. . . . 5 |- (ran ( G |` (Y X. X)) = X -> ((G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) <-> (G |` (Y X. X)):(Y X. X)-->X))
183		raleq 2266	. . . . 5 |- (ran ( G |` (Y X. X)) = X -> (A.x e. ran ( G |` (Y X. X))(((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))) <-> A.x e. X (((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))))
184	182, 183	3anbi23d 1171	. . . 4 |- (ran ( G |` (Y X. X)) = X -> ((H e. Grp /\ (G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) /\ A.x e. ran ( G |` (Y X. X))(((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))) <-> (H e. Grp /\ (G |` (Y X. X)):(Y X. X)-->X /\ A.x e. X (((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))))
185	179, 184	syl 12	. . 3 |- (H e. (SubGrp` G) -> ((H e. Grp /\ (G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) /\ A.x e. ran ( G |` (Y X. X))(((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))) <-> (H e. Grp /\ (G |` (Y X. X)):(Y X. X)-->X /\ A.x e. X (((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))))
186	132, 185	mpbird 213	. 2 |- (H e. (SubGrp` G) -> (H e. Grp /\ (G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) /\ A.x e. ran ( G |` (Y X. X))(((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x)))))
187		resexg 4250	. . 3 |- (G e. Grp -> (G |` (Y X. X)) e. _V)
188		eqid 1884	. . . 4 |- ran ( G |` (Y X. X)) = ran ( G |` (Y X. X))
189	11, 188, 46	isga2 9452	. . 3 |- ((G |` (Y X. X)) e. _V -> (<.H, (G |` (Y X. X))>. e. GrpAct <-> (H e. Grp /\ (G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) /\ A.x e. ran ( G |` (Y X. X))(((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))))
190	4, 187, 189	3syl 24	. 2 |- (H e. (SubGrp` G) -> (<.H, (G |` (Y X. X))>. e. GrpAct <-> (H e. Grp /\ (G |` (Y X. X)):(Y X. ran ( G |` (Y X. X)))-->ran ( G |` (Y X. X)) /\ A.x e. ran ( G |` (Y X. X))(((Id` H)(G |` (Y X. X))x) = x /\ A.y e. Y A.z e. Y ((yHz)(G |` (Y X. X))x) = (y(G |` (Y X. X))(z(G |` (Y X. X))x))))))
191	186, 190	mpbird 213	1 |- (H e. (SubGrp` G) -> <.H, (G |` (Y X. X))>. e. GrpAct)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292   C_ wss 2593  <.cop 3046   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884  Grpcgr 9311  Idcgi 9312  SubGrpcsubg 9423  GrpActcga 9447

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-grp 9316  df-gid 9317  df-subg 9424  df-ga 9448

Copyright terms: Public domain