Theorem cayleylem2 10410

Description: Lemma for cayleyi 10412.

Hypotheses

Ref	Expression
cayleylem1.1	|- G e. Grp
cayleylem1.2	|- P = {f | f:X-1-1-onto->X}
cayleylem1.3	|- X = ran G
cayleylem1.4	|- U = (Id` G)
cayleylem1.5	|- H = (SymGrp` X)
cayleylem1.6	|- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}
cayleylem1.7	|- Y = ran F
cayleylem1.8	|- S = (H |` (Y X. Y))

Assertion

Ref	Expression
cayleylem2	|- F e. (G GrpHom H)

Distinct variable groups:   a,b,f,g,h   f,F   G,a,b,f,g,h   P,g,h   U,a,b   X,a,b,f,g,h

Proof of Theorem cayleylem2

Step	Hyp	Ref	Expression
1		cayleylem1.1	. . 3 |- G e. Grp
2		cayleylem1.5	. . . 4 |- H = (SymGrp` X)
3		cayleylem1.3	. . . . . 6 |- X = ran G
4		rnexg 3359	. . . . . . 7 |- (G e. Grp -> ran G e. V)
5	1, 4	ax-mp 7	. . . . . 6 |- ran G e. V
6	3, 5	eqeltr 1544	. . . . 5 |- X e. V
7	6	symggrpi 10406	. . . 4 |- (SymGrp` X) e. Grp
8	2, 7	eqeltr 1544	. . 3 |- H e. Grp
9		cayleylem1.2	. . . . . . . 8 |- P = {f | f:X-1-1-onto->X}
10	6, 9	symgf 10405	. . . . . . 7 |- (SymGrp` X):(P X. P)-->P
11	10	fdmi 3632	. . . . . 6 |- dom (SymGrp` X) = (P X. P)
12	7, 11	grprn 8056	. . . . 5 |- P = ran (SymGrp` X)
13	2	rneqi 3340	. . . . 5 |- ran H = ran (SymGrp` X)
14	12, 13	eqtr4 1498	. . . 4 |- P = ran H
15	3, 14	elghom 10384	. . 3 |- ((G e. Grp /\ H e. Grp) -> (F e. (G GrpHom H) <-> (F:X-->P /\ A.x e. X A.y e. X ((F` x)H(F` y)) = (F` (xGy)))))
16	1, 8, 15	mp2an 697	. 2 |- (F e. (G GrpHom H) <-> (F:X-->P /\ A.x e. X A.y e. X ((F` x)H(F` y)) = (F` (xGy))))
17		cayleylem1.6	. . . . . . 7 |- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}
18	17, 3	grplactfval 8096	. . . . . 6 |- ((G e. Grp /\ c e. X) -> (F` c) = {<.a, b>. | (a e. X /\ b = (cGa))})
19	1, 18	mpan 695	. . . . 5 |- (c e. X -> (F` c) = {<.a, b>. | (a e. X /\ b = (cGa))})
20		cayleylem1.4	. . . . . 6 |- U = (Id` G)
21		cayleylem1.7	. . . . . 6 |- Y = ran F
22		cayleylem1.8	. . . . . 6 |- S = (H |` (Y X. Y))
23	1, 9, 3, 20, 2, 17, 21, 22	cayleylem1 10409	. . . . 5 |- (c e. X -> (F` c) e. P)
24	19, 23	eqeltrrd 1549	. . . 4 |- (c e. X -> {<.a, b>. | (a e. X /\ b = (cGa))} e. P)
25	24	rgen 1698	. . 3 |- A.c e. X {<.a, b>. | (a e. X /\ b = (cGa))} e. P
26		opreq1 3968	. . . . . . . . 9 |- (c = g -> (cGa) = (gGa))
27	26	eqeq2d 1486	. . . . . . . 8 |- (c = g -> (b = (cGa) <-> b = (gGa)))
28	27	anbi2d 616	. . . . . . 7 |- (c = g -> ((a e. X /\ b = (cGa)) <-> (a e. X /\ b = (gGa))))
29	28	opabbidv 2670	. . . . . 6 |- (c = g -> {<.a, b>. | (a e. X /\ b = (cGa))} = {<.a, b>. | (a e. X /\ b = (gGa))})
30	29	eleq1d 1540	. . . . 5 |- (c = g -> ({<.a, b>. | (a e. X /\ b = (cGa))} e. P <-> {<.a, b>. | (a e. X /\ b = (gGa))} e. P))
31	30	cbvralv 1800	. . . 4 |- (A.c e. X {<.a, b>. | (a e. X /\ b = (cGa))} e. P <-> A.g e. X {<.a, b>. | (a e. X /\ b = (gGa))} e. P)
32	17	fopab2 3823	. . . 4 |- (A.g e. X {<.a, b>. | (a e. X /\ b = (gGa))} e. P <-> F:X-->P)
33	31, 32	bitr 173	. . 3 |- (A.c e. X {<.a, b>. | (a e. X /\ b = (cGa))} e. P <-> F:X-->P)
34	25, 33	mpbi 189	. 2 |- F:X-->P
35	6, 9	symgoprval 10404	. . . . . . 7 |- (((F` z) e. P /\ (F` w) e. P) -> ((F` z)(SymGrp` X)(F` w)) = ((F` z) o. (F` w)))
36	1, 9, 3, 20, 2, 17, 21, 22	cayleylem1 10409	. . . . . . 7 |- (z e. X -> (F` z) e. P)
37	1, 9, 3, 20, 2, 17, 21, 22	cayleylem1 10409	. . . . . . 7 |- (w e. X -> (F` w) e. P)
38	35, 36, 37	syl2an 454	. . . . . 6 |- ((z e. X /\ w e. X) -> ((F` z)(SymGrp` X)(F` w)) = ((F` z) o. (F` w)))
39	2	opreqi 3974	. . . . . 6 |- ((F` z)H(F` w)) = ((F` z)(SymGrp` X)(F` w))
40	38, 39	syl5eq 1519	. . . . 5 |- ((z e. X /\ w e. X) -> ((F` z)H(F` w)) = ((F` z) o. (F` w)))
41	3	grpass 8047	. . . . . . . . . 10 |- ((G e. Grp /\ (z e. X /\ w e. X /\ x e. X)) -> ((zGw)Gx) = (zG(wGx)))
42	1, 41	mpan 695	. . . . . . . . 9 |- ((z e. X /\ w e. X /\ x e. X) -> ((zGw)Gx) = (zG(wGx)))
43	17, 3	grplactval 8097	. . . . . . . . . . . 12 |- ((G e. Grp /\ (zGw) e. X /\ x e. X) -> ((F` (zGw))` x) = ((zGw)Gx))
44	1, 43	mp3an1 903	. . . . . . . . . . 11 |- (((zGw) e. X /\ x e. X) -> ((F` (zGw))` x) = ((zGw)Gx))
45	3	grpcl 8044	. . . . . . . . . . . 12 |- ((G e. Grp /\ z e. X /\ w e. X) -> (zGw) e. X)
46	1, 45	mp3an1 903	. . . . . . . . . . 11 |- ((z e. X /\ w e. X) -> (zGw) e. X)
47	44, 46	sylan 448	. . . . . . . . . 10 |- (((z e. X /\ w e. X) /\ x e. X) -> ((F` (zGw))` x) = ((zGw)Gx))
48	47	3impa 828	. . . . . . . . 9 |- ((z e. X /\ w e. X /\ x e. X) -> ((F` (zGw))` x) = ((zGw)Gx))
49		fvco2 3775	. . . . . . . . . . . . 13 |- ((Fun (F` z) /\ (F` w) Fn X /\ x e. X) -> (((F` z) o. (F` w))` x) = ((F` z)` ((F` w)` x)))
50	49	3expia 835	. . . . . . . . . . . 12 |- ((Fun (F` z) /\ (F` w) Fn X) -> (x e. X -> (((F` z) o. (F` w))` x) = ((F` z)` ((F` w)` x))))
51	6, 9	elsymgrn 10401	. . . . . . . . . . . . . . 15 |- ((F` z) e. P <-> (F` z):X-1-1-onto->X)
52	36, 51	sylib 198	. . . . . . . . . . . . . 14 |- (z e. X -> (F` z):X-1-1-onto->X)
53		f1of 3689	. . . . . . . . . . . . . 14 |- ((F` z):X-1-1-onto->X -> (F` z):X-->X)
54		ffn 3627	. . . . . . . . . . . . . 14 |- ((F` z):X-->X -> (F` z) Fn X)
55	52, 53, 54	3syl 20	. . . . . . . . . . . . 13 |- (z e. X -> (F` z) Fn X)
56		fnfun 3585	. . . . . . . . . . . . 13 |- ((F` z) Fn X -> Fun (F` z))
57	55, 56	syl 10	. . . . . . . . . . . 12 |- (z e. X -> Fun (F` z))
58	6, 9	elsymgrn 10401	. . . . . . . . . . . . . 14 |- ((F` w) e. P <-> (F` w):X-1-1-onto->X)
59	37, 58	sylib 198	. . . . . . . . . . . . 13 |- (w e. X -> (F` w):X-1-1-onto->X)
60		f1of 3689	. . . . . . . . . . . . 13 |- ((F` w):X-1-1-onto->X -> (F` w):X-->X)
61		ffn 3627	. . . . . . . . . . . . 13 |- ((F` w):X-->X -> (F` w) Fn X)
62	59, 60, 61	3syl 20	. . . . . . . . . . . 12 |- (w e. X -> (F` w) Fn X)
63	50, 57, 62	syl2an 454	. . . . . . . . . . 11 |- ((z e. X /\ w e. X) -> (x e. X -> (((F` z) o. (F` w))` x) = ((F` z)` ((F` w)` x))))
64	63	3impia 830	. . . . . . . . . 10 |- ((z e. X /\ w e. X /\ x e. X) -> (((F` z) o. (F` w))` x) = ((F` z)` ((F` w)` x)))
65	17, 3	grplactval 8097	. . . . . . . . . . . . 13 |- ((G e. Grp /\ w e. X /\ x e. X) -> ((F` w)` x) = (wGx))
66	1, 65	mp3an1 903	. . . . . . . . . . . 12 |- ((w e. X /\ x e. X) -> ((F` w)` x) = (wGx))
67	66	fveq2d 3728	. . . . . . . . . . 11 |- ((w e. X /\ x e. X) -> ((F` z)` ((F` w)` x)) = ((F` z)` (wGx)))
68	67	3adant1 797	. . . . . . . . . 10 |- ((z e. X /\ w e. X /\ x e. X) -> ((F` z)` ((F` w)` x)) = ((F` z)` (wGx)))
69	17, 3	grplactval 8097	. . . . . . . . . . . . 13 |- ((G e. Grp /\ z e. X /\ (wGx) e. X) -> ((F` z)` (wGx)) = (zG(wGx))