Theorem ghomgrpilem2 10320

Description: Lemma for ghomgrpi 10321.

Hypotheses

Ref	Expression
ghomgrpilem1.1	|- G e. Grp
ghomgrpilem1.2	|- H e. Grp
ghomgrpilem1.3	|- F e. (G GrpHom H)
ghomgrpilem1.4	|- X = ran G
ghomgrpilem1.5	|- U = (Id` G)
ghomgrpilem1.6	|- N = (inv` G)
ghomgrpilem1.7	|- W = ran H
ghomgrpilem1.8	|- T = (Id` H)
ghomgrpilem1.9	|- M = (inv` H)
ghomgrpilem1.10	|- Z = ran F
ghomgrpilem1.11	|- S = (H |` (Z X. Z))

Assertion

Ref	Expression
ghomgrpilem2	|- S e. (SubGrp` H)

Proof of Theorem ghomgrpilem2

Step	Hyp	Ref	Expression
1		ghomgrpilem1.2	. 2 |- H e. Grp
2		ghomgrpilem1.7	. 2 |- W = ran H
3		ghomgrpilem1.8	. 2 |- T = (Id` H)
4		ghomgrpilem1.9	. 2 |- M = (inv` H)
5		ghomgrpilem1.10	. . 3 |- Z = ran F
6		ghomgrpilem1.3	. . . . . 6 |- F e. (G GrpHom H)
7		ghomgrpilem1.1	. . . . . . 7 |- G e. Grp
8		ghomgrpilem1.4	. . . . . . . 8 |- X = ran G
9	8, 2	elghom 10318	. . . . . . 7 |- ((G e. Grp /\ H e. Grp) -> (F e. (G GrpHom H) <-> (F:X-->W /\ A.x e. X A.y e. X ((F` x)H(F` y)) = (F` (xGy)))))
10	7, 1, 9	mp2an 696	. . . . . 6 |- (F e. (G GrpHom H) <-> (F:X-->W /\ A.x e. X A.y e. X ((F` x)H(F` y)) = (F` (xGy))))
11	6, 10	mpbi 189	. . . . 5 |- (F:X-->W /\ A.x e. X A.y e. X ((F` x)H(F` y)) = (F` (xGy)))
12	11	pm3.26i 320	. . . 4 |- F:X-->W
13		frn 3624	. . . 4 |- (F:X-->W -> ran F (_ W)
14	12, 13	ax-mp 7	. . 3 |- ran F (_ W
15	5, 14	eqsstr 2087	. 2 |- Z (_ W
16		ghomgrpilem1.11	. 2 |- S = (H |` (Z X. Z))
17	5	eleq2i 1535	. . . . . . 7 |- (x e. Z <-> x e. ran F)
18		ffn 3619	. . . . . . . . 9 |- (F:X-->W -> F Fn X)
19	12, 18	ax-mp 7	. . . . . . . 8 |- F Fn X
20		fvelrnb 3751	. . . . . . . 8 |- (F Fn X -> (x e. ran F <-> E.z e. X (F` z) = x))
21	19, 20	ax-mp 7	. . . . . . 7 |- (x e. ran F <-> E.z e. X (F` z) = x)
22	17, 21	bitr 173	. . . . . 6 |- (x e. Z <-> E.z e. X (F` z) = x)
23	22	biimp 151	. . . . 5 |- (x e. Z -> E.z e. X (F` z) = x)
24	5	eleq2i 1535	. . . . . . 7 |- (y e. Z <-> y e. ran F)
25		fvelrnb 3751	. . . . . . . 8 |- (F Fn X -> (y e. ran F <-> E.w e. X (F` w) = y))
26	19, 25	ax-mp 7	. . . . . . 7 |- (y e. ran F <-> E.w e. X (F` w) = y)
27	24, 26	bitr 173	. . . . . 6 |- (y e. Z <-> E.w e. X (F` w) = y)
28	27	biimp 151	. . . . 5 |- (y e. Z -> E.w e. X (F` w) = y)
29	23, 28	anim12i 333	. . . 4 |- ((x e. Z /\ y e. Z) -> (E.z e. X (F` z) = x /\ E.w e. X (F` w) = y))
30		reeanv 1775	. . . 4 |- (E.z e. X E.w e. X ((F` z) = x /\ (F` w) = y) <-> (E.z e. X (F` z) = x /\ E.w e. X (F` w) = y))
31	29, 30	sylibr 200	. . 3 |- ((x e. Z /\ y e. Z) -> E.z e. X E.w e. X ((F` z) = x /\ (F` w) = y))
32		opreq12 3961	. . . . . 6 |- (((F` z) = x /\ (F` w) = y) -> ((F` z)H(F` w)) = (xHy))
33	32	eleq1d 1537	. . . . 5 |- (((F` z) = x /\ (F` w) = y) -> (((F` z)H(F` w)) e. Z <-> (xHy) e. Z))
34		ghomgrpilem1.5	. . . . . . 7 |- U = (Id` G)
35		ghomgrpilem1.6	. . . . . . 7 |- N = (inv` G)
36	7, 1, 6, 8, 34, 35, 2, 3, 4, 5, 16	ghomgrpilem1 10319	. . . . . 6 |- ((z e. X /\ w e. X) -> ((F` z)H(F` w)) = (F` (zGw)))
37	8	grpcl 7994	. . . . . . . 8 |- ((G e. Grp /\ z e. X /\ w e. X) -> (zGw) e. X)
38	7, 37	mp3an1 901	. . . . . . 7 |- ((z e. X /\ w e. X) -> (zGw) e. X)
39		fnfrn 3625	. . . . . . . . . 10 |- (F Fn X <-> F:X-->ran F)
40	19, 39	mpbi 189	. . . . . . . . 9 |- F:X-->ran F
41		feq3 3614	. . . . . . . . . 10 |- (Z = ran F -> (F:X-->Z <-> F:X-->ran F))
42	5, 41	ax-mp 7	. . . . . . . . 9 |- (F:X-->Z <-> F:X-->ran F)
43	40, 42	mpbir 190	. . . . . . . 8 |- F:X-->Z
44	43	ffvelrni 3806	. . . . . . 7 |- ((zGw) e. X -> (F` (zGw)) e. Z)
45	38, 44	syl 10	. . . . . 6 |- ((z e. X /\ w e. X) -> (F` (zGw)) e. Z)
46	36, 45	eqeltrd 1545	. . . . 5 |- ((z e. X /\ w e. X) -> ((F` z)H(F` w)) e. Z)
47	33, 46	syl5cbi 209	. . . 4 |- ((z e. X /\ w e. X) -> (((F` z) = x /\ (F` w) = y) -> (xHy) e. Z))
48	47	r19.23aivv 1745	. . 3 |- (E.z e. X E.w e. X ((F` z) = x /\ (F` w) = y) -> (xHy) e. Z)
49	31, 48	syl 10	. 2 |- ((x e. Z /\ y e. Z) -> (xHy) e. Z)
50	8, 34	grpidcl 8009	. . . . . . . 8 |- (G e. Grp -> U e. X)
51	7, 50	ax-mp 7	. . . . . . 7 |- U e. X
52	7, 1, 6, 8, 34, 35, 2, 3, 4, 5, 16	ghomgrpilem1 10319	. . . . . . 7 |- ((U e. X /\ U e. X) -> ((F` U)H(F` U)) = (F` (UGU)))
53	51, 51, 52	mp2an 696	. . . . . 6 |- ((F` U)H(F` U)) = (F` (UGU))
54	8, 34	grplid 8011	. . . . . . . 8 |- ((G e. Grp /\ U e. X) -> (UGU) = U)
55	7, 51, 54	mp2an 696	. . . . . . 7 |- (UGU) = U
56	55	fveq2i 3718	. . . . . 6 |- (F` (UGU)) = (F` U)
57	53, 56	eqtr 1492	. . . . 5 |- ((F` U)H(F` U)) = (F` U)
58		ffvelrn 3805	. . . . . . 7 |- ((F:X-->W /\ U e. X) -> (F` U) e. W)
59	12, 51, 58	mp2an 696	. . . . . 6 |- (F` U) e. W
60		eqid 1473	. . . . . . 7 |- (Id` H) = (Id` H)
61	2, 60	grpid 8015	. . . . . 6 |- ((H e. Grp /\ (F` U) e. W) -> ((F` U) = (Id` H) <-> ((F` U)H(F` U)) = (F` U)))
62	1, 59, 61	mp2an 696	. . . . 5 |- ((F` U) = (Id` H) <-> ((F` U)H(F` U)) = (F` U))
63	57, 62	mpbir 190	. . . 4 |- (F` U) = (Id` H)
64	3, 63	eqtr4 1495	. . 3 |- T = (F` U)
65		ffvelrn 3805	. . . 4 |- ((F:X-->Z /\ U e. X) -> (F` U) e. Z)
66	43, 51, 65	mp2an 696	. . 3 |- (F` U) e. Z
67	64, 66	eqeltr 1541	. 2 |- T e. Z
68		fveq2 3715	. . . . . 6 |- ((F` z) = x -> (M` (F` z)) = (M` x))
69	68	eleq1d 1537	. . . . 5 |- ((F` z) = x -> ((M` (F` z)) e. Z <-> (M` x) e. Z))
70	8, 35	grpinvcl 8018	. . . . . . . . . . 11 |- ((G e. Grp /\ z e. X) -> (N` z) e. X)
71	7, 70	mpan 694	. . . . . . . . . 10 |- (z e. X -> (N` z) e. X)
72	7, 1, 6, 8, 34, 35, 2, 3, 4, 5, 16	ghomgrpilem1 10319	. . . . . . . . . 10 |- ((z e. X /\ (N` z) e. X) -> ((F` z)H(F` (N` z))) = (F` (zG(N` z))))
73	71, 72	mpdan 703	. . . . . . . . 9 |- (z e. X -> ((F` z)H(F` (N` z))) = (F` (zG(N` z))))
74	8, 34, 35	grprinv 8021	. . . . . . . . . . 11 |- ((G e. Grp /\ z e. X) -> (zG(N` z)) = U)
75	7, 74	mpan 694	. . . . . . . . . 10 |- (z e. X -> (zG(N` z)) = U)
76	75	fveq2d 3719	. . . . . . . . 9 |- (z e. X -> (F` (zG(N` z))) = (F` U))
77	73, 76	eqtrd 1504	. . . . . . . 8 |- (z e. X -> ((F` z)H(F` (N` z))) = (F` U))
78	77, 64	syl6eqr 1522	. . . . . . 7 |- (z e. X -> ((F` z)H(F` (N` z))) = T)
79	2, 3, 4	grpinvid1 8022	. . . . . . . . 9 |- ((H e. Grp /\ (F` z) e. W /\ (F` (N` z)) e. W) -> ((M` (F` z)) = (F` (N` z)) <-> ((F` z)H(F` (N` z))) = T))
80	1, 79	mp3an1 901	. . . . . . . 8 |- (((F` z) e. W /\ (F` (N` z)) e. W) -> ((M` (F` z)) = (F` (N` z)) <-> ((F` z)H(F` (N` z))) = T))
81	12	ffvelrni 3806	. . . . . . . 8 |- (z e. X -> (F` z) e. W)
82	12	ffvelrni 3806	. . . . . . . . 9 |- ((N` z) e. X -> (F` (N` z)) e. W)
83	71, 82	syl 10	. . . . . . . 8 |- (z e. X -> (F` (N` z)) e. W)
84	80, 81, 83	sylanc 471	. . . . . . 7 |- (z e. X -> ((M` (F` z)) = (F` (N` z)) <-> ((F` z)H(F` (N` z))) = T))
85	78, 84	mpbird 196	. . . . . 6 |- (z e. X -> (M` (F` z)) = (F` (N