Theorem ghgrpilem3 8131

Description: Lemma for ghgrpi 8133.

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
ghgrpilem3	|- ((a e. Y /\ b e. Y) -> (E.c e. Y (cHa) = b /\ E.c e. Y (aHc) = b))

Distinct variable groups:   x,F,y   G,a,b,x,y   H,a,b,x,y   x,O,y   x,X,y   Y,a,b,x,y   D,c   F,c   G,c   H,c,a,b,x,y   N,c   Y,c

Proof of Theorem ghgrpilem3

Step	Hyp	Ref	Expression
1		ghgrpi.1	. . 3 |- G e. Grp
2		ghgrpi.2	. . 3 |- X = ran G
3		ghgrpi.3	. . 3 |- F:X-onto->Y
4		ghgrpi.4	. . 3 |- Y (_ A
5		ghgrpi.5	. . 3 |- O Fn (A X. A)
6		ghgrpi.6	. . 3 |- ((x e. X /\ y e. X) -> (F` (xGy)) = ((F` x)O(F` y)))
7		ghgrpi.7	. . 3 |- H = (O |` (Y X. Y))
8		opreq1 3974	. . . . . . . 8 |- (c = (F` (yDx)) -> (cH(F` x)) = ((F` (yDx))H(F` x)))
9	8	eqeq1d 1486	. . . . . . 7 |- (c = (F` (yDx)) -> ((cH(F` x)) = (F` y) <-> ((F` (yDx))H(F` x)) = (F` y)))
10	9	rcla4ev 1880	. . . . . 6 |- (((F` (yDx)) e. Y /\ ((F` (yDx))H(F` x)) = (F` y)) -> E.c e. Y (cH(F` x)) = (F` y))
11		ghgrpilem3.10	. . . . . . . . . 10 |- D = ( /g ` G)
12	2, 11	grpdivcl 8082	. . . . . . . . 9 |- ((G e. Grp /\ y e. X /\ x e. X) -> (yDx) e. X)
13	1, 12	mp3an1 905	. . . . . . . 8 |- ((y e. X /\ x e. X) -> (yDx) e. X)
14		df-fo 3202	. . . . . . . . . . 11 |- (F:X-onto->Y <-> (F Fn X /\ ran F = Y))
15	3, 14	mpbi 189	. . . . . . . . . 10 |- (F Fn X /\ ran F = Y)
16	15	pm3.26i 320	. . . . . . . . 9 |- F Fn X
17		fnfvelrn 3819	. . . . . . . . 9 |- ((F Fn X /\ (yDx) e. X) -> (F` (yDx)) e. ran F)
18	16, 17	mpan 697	. . . . . . . 8 |- ((yDx) e. X -> (F` (yDx)) e. ran F)
19	13, 18	syl 10	. . . . . . 7 |- ((y e. X /\ x e. X) -> (F` (yDx)) e. ran F)
20	15	pm3.27i 324	. . . . . . 7 |- ran F = Y
21	19, 20	syl6eleq 1561	. . . . . 6 |- ((y e. X /\ x e. X) -> (F` (yDx)) e. Y)
22	1, 2, 3, 4, 5, 6, 7	ghgrpilem1 8129	. . . . . . . 8 |- (((yDx) e. X /\ x e. X) -> (F` ((yDx)Gx)) = ((F` (yDx))H(F` x)))
23	13, 22	sylancom 477	. . . . . . 7 |- ((y e. X /\ x e. X) -> (F` ((yDx)Gx)) = ((F` (yDx))H(F` x)))
24	2, 11	grpnpcan 8087	. . . . . . . . 9 |- ((G e. Grp /\ y e. X /\ x e. X) -> ((yDx)Gx) = y)
25	1, 24	mp3an1 905	. . . . . . . 8 |- ((y e. X /\ x e. X) -> ((yDx)Gx) = y)
26	25	fveq2d 3734	. . . . . . 7 |- ((y e. X /\ x e. X) -> (F` ((yDx)Gx)) = (F` y))
27	23, 26	eqtr3d 1512	. . . . . 6 |- ((y e. X /\ x e. X) -> ((F` (yDx))H(F` x)) = (F` y))
28	10, 21, 27	sylanc 473	. . . . 5 |- ((y e. X /\ x e. X) -> E.c e. Y (cH(F` x)) = (F` y))
29	28	ancoms 438	. . . 4 |- ((x e. X /\ y e. X) -> E.c e. Y (cH(F` x)) = (F` y))
30		opreq2 3975	. . . . . 6 |- ((F` x) = a -> (cH(F` x)) = (cHa))
31	30	eqeq1d 1486	. . . . 5 |- ((F` x) = a -> ((cH(F` x)) = (F` y) <-> (cHa) = (F` y)))
32	31	rexbidv 1667	. . . 4 |- ((F` x) = a -> (E.c e. Y (cH(F` x)) = (F` y) <-> E.c e. Y (cHa) = (F` y)))
33	1, 2, 3, 4, 5, 6, 7, 29, 32	ghgrpilem2 8130	. . 3 |- ((y e. X /\ a e. Y) -> E.c e. Y (cHa) = (F` y))
34		eqeq2 1487	. . . 4 |- ((F` y) = b -> ((cHa) = (F` y) <-> (cHa) = b))
35	34	rexbidv 1667	. . 3 |- ((F` y) = b -> (E.c e. Y (cHa) = (F` y) <-> E.c e. Y (cHa) = b))
36	1, 2, 3, 4, 5, 6, 7, 33, 35	ghgrpilem2 8130	. 2 |- ((a e. Y /\ b e. Y) -> E.c e. Y (cHa) = b)
37		opreq2 3975	. . . . . . 7 |- (c = (F` ((N` x)Gy)) -> ((F` x)Hc) = ((F` x)H(F` ((N` x)Gy))))
38	37	eqeq1d 1486	. . . . . 6 |- (c = (F` ((N` x)Gy)) -> (((F` x)Hc) = (F` y) <-> ((F` x)H(F` ((N` x)Gy))) = (F` y)))
39	38	rcla4ev 1880	. . . . 5 |- (((F` ((N` x)Gy)) e. Y /\ ((F` x)H(F` ((N` x)Gy))) = (F` y)) -> E.c e. Y ((F` x)Hc) = (F` y))
40	2	grpcl 8041	. . . . . . . . 9 |- ((G e. Grp /\ (N` x) e. X /\ y e. X) -> ((N` x)Gy) e. X)
41	1, 40	mp3an1 905	. . . . . . . 8 |- (((N` x) e. X /\ y e. X) -> ((N` x)Gy) e. X)
42		ghgrpilem3.9	. . . . . . . . . 10 |- N = (inv` G)
43	2, 42	grpinvcl 8064	. . . . . . . . 9 |- ((G e. Grp /\ x e. X) -> (N` x) e. X)
44	1, 43	mpan 697	. . . . . . . 8 |- (x e. X -> (N` x) e. X)
45	41, 44	sylan 450	. . . . . . 7 |- ((x e. X /\ y e. X) -> ((N` x)Gy) e. X)
46		fnfvelrn 3819	. . . . . . . 8 |- ((F Fn X /\ ((N` x)Gy) e. X) -> (F` ((N` x)Gy)) e. ran F)
47	16, 46	mpan 697	. . . . . . 7 |- (((N` x)Gy) e. X -> (F` ((N` x)Gy)) e. ran F)
48	45, 47	syl 10	. . . . . 6 |- ((x e. X /\ y e. X) -> (F` ((N` x)Gy)) e. ran F)
49	48, 20	syl6eleq 1561	. . . . 5 |- ((x e. X /\ y e. X) -> (F` ((N` x)Gy)) e. Y)
50	1, 2, 3, 4, 5, 6, 7	ghgrpilem1 8129	. . . . . . 7 |- ((x e. X /\ ((N` x)Gy) e. X) -> (F` (xG((N` x)Gy))) = ((F` x)H(F` ((N` x)Gy))))
51	45, 50	syldan 469	. . . . . 6 |- ((x e. X /\ y e. X) -> (F` (xG((N` x)Gy))) = ((F` x)H(F` ((N` x)Gy))))
52	2, 42	grpasscan1 8073	. . . . . . . 8 |- ((G e. Grp /\ x e. X /\ y e. X) -> (xG((N` x)Gy)) = y)
53	1, 52	mp3an1 905	. . . . . . 7 |- ((x e. X /\ y e. X) -> (xG((N` x)Gy)) = y)
54	53	fveq2d 3734	. . . . . 6 |- ((x e. X /\ y e. X) -> (F` (xG((N` x)Gy))) = (F` y))
55	51, 54	eqtr3d 1512	. . . . 5 |- ((x e. X /\ y e. X) -> ((F` x)H(F` ((N` x)Gy))) = (F` y))
56	39, 49, 55	sylanc 473	. . . 4 |- ((x e. X /\ y e. X) -> E.c e. Y ((F` x)Hc) = (F` y))
57		opreq1 3974	. . . . . 6 |- ((F` x) = a -> ((F` x)Hc) = (aHc))
58	57	eqeq1d 1486	. . . . 5 |- ((F` x) = a -> (((F` x)Hc) = (F` y) <-> (aHc) = (F` y)))
59	58	rexbidv 1667	. . . 4 |- ((F` x) = a -> (E.c e. Y ((F` x)Hc) = (F` y) <-> E.c e. Y (aHc) = (F` y)))
60	1, 2, 3, 4, 5, 6, 7, 56, 59	ghgrpilem2 8130	. . 3 |- ((y e. X /\ a e. Y) -> E.c e. Y (aHc) = (F` y))
61		eqeq2 1487	. . . 4 |- ((F` y) = b -> ((aHc) = (F` y) <-> (aHc) = b))
62	61	rexbidv 1667	. . 3 |- ((F` y) = b -> (E.c e. Y (aHc) = (F` y) <-> E.c e. Y (aHc) =