Theorem ghgrpilem4 8136

Description: Lemma for ghgrpi 8137.

Hypotheses

Ref	Expression
ghgrpi.1	|- G e. Grp
ghgrpi.2	|- X = ran G
ghgrpi.3	|- F:X-onto->Y
ghgrpi.4	|- Y (_ A
ghgrpi.5	|- O Fn (A X. A)
ghgrpi.6	|- ((x e. X /\ y e. X) -> (F` (xGy)) = ((F` x)O(F` y)))
ghgrpi.7	|- H = (O |` (Y X. Y))
ghgrpilem3.8	|- U = (Id` G)
ghgrpilem3.9	|- N = (inv` G)
ghgrpilem3.10	|- D = ( /g ` G)

Assertion

Ref	Expression
ghgrpilem4	|- H e. Grp

Distinct variable groups:   x,F,y   x,G,y   x,H,y   x,O,y   x,X,y   x,Y,y

Proof of Theorem ghgrpilem4

Step	Hyp	Ref	Expression
1		ghgrpi.2	. . . 4 |- X = ran G
2		ghgrpi.1	. . . . 5 |- G e. Grp
3		rnexg 3359	. . . . 5 |- (G e. Grp -> ran G e. V)
4	2, 3	ax-mp 7	. . . 4 |- ran G e. V
5	1, 4	eqeltr 1544	. . 3 |- X e. V
6		ghgrpi.3	. . 3 |- F:X-onto->Y
7		fornex 3679	. . 3 |- (X e. V -> (F:X-onto->Y -> Y e. V))
8	5, 6, 7	mp2 43	. 2 |- Y e. V
9		df-fo 3196	. . . . . . 7 |- (F:X-onto->Y <-> (F Fn X /\ ran F = Y))
10	6, 9	mpbi 189	. . . . . 6 |- (F Fn X /\ ran F = Y)
11	10	pm3.26i 320	. . . . 5 |- F Fn X
12		ghgrpilem3.8	. . . . . . 7 |- U = (Id` G)
13	1, 12	grpidcl 8059	. . . . . 6 |- (G e. Grp -> U e. X)
14	2, 13	ax-mp 7	. . . . 5 |- U e. X
15		fnfvelrn 3813	. . . . 5 |- ((F Fn X /\ U e. X) -> (F` U) e. ran F)
16	11, 14, 15	mp2an 697	. . . 4 |- (F` U) e. ran F
17	10	pm3.27i 324	. . . 4 |- ran F = Y
18	16, 17	eleqtr 1546	. . 3 |- (F` U) e. Y
19		ne0i 2286	. . 3 |- ((F` U) e. Y -> Y =/= (/))
20	18, 19	ax-mp 7	. 2 |- Y =/= (/)
21		ffnoprval 4014	. . 3 |- (H:(Y X. Y)-->Y <-> (H Fn (Y X. Y) /\ A.a e. Y A.b e. Y (aHb) e. Y))
22		ghgrpi.5	. . . . 5 |- O Fn (A X. A)
23		ghgrpi.4	. . . . . 6 |- Y (_ A
24		ssxp 3256	. . . . . 6 |- ((Y (_ A /\ Y (_ A) -> (Y X. Y) (_ (A X. A))
25	23, 23, 24	mp2an 697	. . . . 5 |- (Y X. Y) (_ (A X. A)
26		fnssres 3600	. . . . 5 |- ((O Fn (A X. A) /\ (Y X. Y) (_ (A X. A)) -> (O |` (Y X. Y)) Fn (Y X. Y))
27	22, 25, 26	mp2an 697	. . . 4 |- (O |` (Y X. Y)) Fn (Y X. Y)
28		ghgrpi.7	. . . . 5 |- H = (O |` (Y X. Y))
29		fneq1 3582	. . . . 5 |- (H = (O |` (Y X. Y)) -> (H Fn (Y X. Y) <-> (O |` (Y X. Y)) Fn (Y X. Y)))
30	28, 29	ax-mp 7	. . . 4 |- (H Fn (Y X. Y) <-> (O |` (Y X. Y)) Fn (Y X. Y))
31	27, 30	mpbir 190	. . 3 |- H Fn (Y X. Y)
32		ghgrpi.6	. . . . 5 |- ((x e. X /\ y e. X) -> (F` (xGy)) = ((F` x)O(F` y)))
33	2, 1, 6, 23, 22, 32, 28	ghgrpilem1 8133	. . . . . . . 8 |- ((x e. X /\ y e. X) -> (F` (xGy)) = ((F` x)H(F` y)))
34	1	grpcl 8044	. . . . . . . . . 10 |- ((G e. Grp /\ x e. X /\ y e. X) -> (xGy) e. X)
35	2, 34	mp3an1 903	. . . . . . . . 9 |- ((x e. X /\ y e. X) -> (xGy) e. X)
36		fnfvelrn 3813	. . . . . . . . . 10 |- ((F Fn X /\ (xGy) e. X) -> (F` (xGy)) e. ran F)
37	11, 36	mpan 695	. . . . . . . . 9 |- ((xGy) e. X -> (F` (xGy)) e. ran F)
38	35, 37	syl 10	. . . . . . . 8 |- ((x e. X /\ y e. X) -> (F` (xGy)) e. ran F)
39	33, 38	eqeltrrd 1549	. . . . . . 7 |- ((x e. X /\ y e. X) -> ((F` x)H(F` y)) e. ran F)
40	39, 17	syl6eleq 1558	. . . . . 6 |- ((x e. X /\ y e. X) -> ((F` x)H(F` y)) e. Y)
41		opreq1 3968	. . . . . . 7 |- ((F` x) = a -> ((F` x)H(F` y)) = (aH(F` y)))
42	41	eleq1d 1540	. . . . . 6 |- ((F` x) = a -> (((F` x)H(F` y)) e. Y <-> (aH(F` y)) e. Y))
43	2, 1, 6, 23, 22, 32, 28, 40, 42	ghgrpilem2 8134	. . . . 5 |- ((y e. X /\ a e. Y) -> (aH(F` y)) e. Y)
44		opreq2 3969	. . . . . 6 |- ((F` y) = b -> (aH(F` y)) = (aHb))
45	44	eleq1d 1540	. . . . 5 |- ((F` y) = b -> ((aH(F` y)) e. Y <-> (aHb) e. Y))
46	2, 1, 6, 23, 22, 32, 28, 43, 45	ghgrpilem2 8134	. . . 4 |- ((a e. Y /\ b e. Y) -> (aHb) e. Y)
47	46	rgen2a 1699	. . 3 |- A.a e. Y A.b e. Y (aHb) e. Y
48	21, 31, 47	mpbir2an 730	. 2 |- H:(Y X. Y)-->Y
49	1	grpass 8047	. . . . . . . . . . . . 13 |- ((G e. Grp /\ (x e. X /\ y e. X /\ z e. X)) -> ((xGy)Gz) = (xG(yGz)))
50	2, 49	mpan 695	. . . . . . . . . . . 12 |- ((x e. X /\ y e. X /\ z e. X) -> ((xGy)Gz) = (xG(yGz)))
51	50	fveq2d 3728	. . . . . . . . . . 11 |- ((x e. X /\ y e. X /\ z e. X) -> (F` ((xGy)Gz)) = (F` (xG(yGz))))
52	2, 1, 6, 23, 22, 32, 28	ghgrpilem1 8133	. . . . . . . . . . . . 13 |- (((xGy) e. X /\ z e. X) -> (F` ((xGy)Gz)) = ((F` (xGy))H(F` z)))
53	52, 35	sylan 448	. . . . . . . . . . . 12 |- (((x e. X /\ y e. X) /\ z e. X) -> (F` ((xGy)Gz)) = ((F` (xGy))H(F` z)))
54	53	3impa 828	. . . . . . . . . . 11 |- ((x e. X /\ y e. X /\ z e. X) -> (F` ((xGy)Gz)) = ((F` (xGy))H(F` z)))
55	2, 1, 6, 23, 22, 32, 28	ghgrpilem1 8133	. . . . . . . . . . . . 13 |- ((x e. X /\ (yGz) e. X) -> (F` (xG(yGz))) = ((F` x)H(F` (yGz))))
56	1	grpcl 8044	. . . . . . . . . . . . . 14 |- ((G e. Grp /\ y e. X /\ z e. X) -> (yGz) e. X)
57	2, 56	mp3an1 903	. . . . . . . . . . . . 13 |- ((y e. X /\ z e. X) -> (yGz) e. X)
58	55, 57	sylan2 451	. . . . . . . . . . . 12 |- ((x e. X /\ (y e. X /\ z e. X)) -> (F` (xG(yGz))) = ((F` x)H(F` (yGz))))
59	58	3impb 829	. . . . . . . . . . 11 |- ((x e. X /\ y e. X /\ z e. X) -> (F` (xG(yGz))) = ((F` x)H(F` (yGz))))
60	51, 54, 59	3eqtr3d 1515	. . . . . . . . . 10 |- ((x e. X /\ y e. X /\ z e. X) -> ((F` (xGy))H(F` z)) = ((F` x)H(F` (yGz))))
61	33	3adant3 799	. . . . . . . . . . 11 |- ((x e. X /\ y e. X /\ z e. X) -> (F` (xGy)) = ((F` x)H(F` y)))
62	61	opreq1d 3975	. . . . . . . . . 10 |- ((x e. X /\ y e. X /\ z e. X) -> ((F` (xGy))H(F` z)) = (((F` x)H(F` y))H(F` z)))
63	2, 1, 6, 23, 22, 32, 28	ghgrpilem1 8133	. . . . . . . . . . . 12 |- ((y e. X /\ z e. X) -> (F` (yGz)) = ((F` y)H(F` z)))
64	63	3adant1 797	. . . . . . . . . . 11 |- ((x e. X /\ y e. X /\ z e. X) -> (F` (yGz)) = ((F` y)H(F` z)))
65	64	opreq2d 3976	. . . . . . . . . 10 |- ((x e. X /\ y e. X /\ z e. X) -> ((F` x)H(F` (yGz))) = ((F` x)H((F` y)H(F` z))))
66	60, 62, 65	3eqtr3d 1515	. . . . . . . . 9 |- ((x e. X /\ y e. X /\ z e. X) -> (((F` x)H(F` y))H(F` z)) = ((F` x)H((F` y)H(F` z))))
67	66	3expb 834	. . . . . . . 8 |- ((x e. X /\ (y e. X /\ z e. X)) -> (((F` x)H(F` y))H(F` z)) = ((F` x)H((F` y)H(F` z))))
68	41	opreq1d 3975	. . . . . . . . 9 |- ((F` x) = a -> (((F` x)H(F` y))H(F` z)) = ((aH(F` y))H(F` z)))
69		opreq1 3968	. . . . . . . . 9 |- ((F` x) = a -> ((F` x)H((F` y)H(F` z))) = (aH((F` y)H(F` z))))
70	68, 69	eqeq12d 1489	. . . . . . . 8 |- ((F` x) = a -> ((((F` x)H(F` y))H(F` z)) = ((F` x)H((F` y)H(F` z))) <-> ((aH(F` y))<