Theorem ghomgrpilem2 13629

Description: Lemma for ghomgrpi 13630.

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 10195	. . . . . . 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 761	. . . . . 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 206	. . . . 5 |- (F:X-->W /\ A.x e. X A.y e. X ((F` x)H(F` y)) = (F` (xGy)))
12	11	simpli 347	. . . 4 |- F:X-->W
13		frn 4569	. . . 4 |- (F:X-->W -> ran F C_ W)
14	12, 13	ax-mp 7	. . 3 |- ran F C_ W
15	5, 14	eqsstri 2647	. 2 |- Z C_ W
16		ghomgrpilem1.11	. 2 |- S = (H |` (Z X. Z))
17	5	eleq2i 1961	. . . . . . 7 |- (x e. Z <-> x e. ran F)
18		ffn 4562	. . . . . . . . 9 |- (F:X-->W -> F Fn X)
19	12, 18	ax-mp 7	. . . . . . . 8 |- F Fn X
20		fvelrnb 4719	. . . . . . . 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	bitri 190	. . . . . 6 |- (x e. Z <-> E.z e. X (F` z) = x)
23	22	biimpi 168	. . . . 5 |- (x e. Z -> E.z e. X (F` z) = x)
24	5	eleq2i 1961	. . . . . . 7 |- (y e. Z <-> y e. ran F)
25		fvelrnb 4719	. . . . . . . 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	bitri 190	. . . . . 6 |- (y e. Z <-> E.w e. X (F` w) = y)
28	27	biimpi 168	. . . . 5 |- (y e. Z -> E.w e. X (F` w) = y)
29	23, 28	anim12i 360	. . . 4 |- ((x e. Z /\ y e. Z) -> (E.z e. X (F` z) = x /\ E.w e. X (F` w) = y))
30		reeanv 2249	. . . 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 217	. . 3 |- ((x e. Z /\ y e. Z) -> E.z e. X E.w e. X ((F` z) = x /\ (F` w) = y))
32		opreq12 4891	. . . . . 6 |- (((F` z) = x /\ (F` w) = y) -> ((F` z)H(F` w)) = (xHy))
33	32	eleq1d 1963	. . . . 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 13628	. . . . . 6 |- ((z e. X /\ w e. X) -> ((F` z)H(F` w)) = (F` (zGw)))
37	8	grpcl 9324	. . . . . . . 8 |- ((G e. Grp /\ z e. X /\ w e. X) -> (zGw) e. X)
38	7, 37	mp3an1 1178	. . . . . . 7 |- ((z e. X /\ w e. X) -> (zGw) e. X)
39		dffn3 4570	. . . . . . . . . 10 |- (F Fn X <-> F:X-->ran F)
40	19, 39	mpbi 206	. . . . . . . . 9 |- F:X-->ran F
41		feq3 4553	. . . . . . . . . 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 207	. . . . . . . 8 |- F:X-->Z
44	43	ffvelrni 4788	. . . . . . 7 |- ((zGw) e. X -> (F` (zGw)) e. Z)
45	38, 44	syl 12	. . . . . 6 |- ((z e. X /\ w e. X) -> (F` (zGw)) e. Z)
46	36, 45	eqeltrd 1971	. . . . 5 |- ((z e. X /\ w e. X) -> ((F` z)H(F` w)) e. Z)
47	33, 46	syl5cbi 226	. . . 4 |- ((z e. X /\ w e. X) -> (((F` z) = x /\ (F` w) = y) -> (xHy) e. Z))
48	47	r19.23aivv 2217	. . 3 |- (E.z e. X E.w e. X ((F` z) = x /\ (F` w) = y) -> (xHy) e. Z)
49	31, 48	syl 12	. 2 |- ((x e. Z /\ y e. Z) -> (xHy) e. Z)
50	8, 34	grpidcl 9343	. . . . . . . 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 13628	. . . . . . 7 |- ((U e. X /\ U e. X) -> ((F` U)H(F` U)) = (F` (UGU)))
53	51, 51, 52	mp2an 761	. . . . . 6 |- ((F` U)H(F` U)) = (F` (UGU))
54	8, 34	grplid 9345	. . . . . . . 8 |- ((G e. Grp /\ U e. X) -> (UGU) = U)
55	7, 51, 54	mp2an 761	. . . . . . 7 |- (UGU) = U
56	55	fveq2i 4684	. . . . . 6 |- (F` (UGU)) = (F` U)
57	53, 56	eqtri 1908	. . . . 5 |- ((F` U)H(F` U)) = (F` U)
58		ffvelrn 4787	. . . . . . 7 |- ((F:X-->W /\ U e. X) -> (F` U) e. W)
59	12, 51, 58	mp2an 761	. . . . . 6 |- (F` U) e. W
60		eqid 1884	. . . . . . 7 |- (Id` H) = (Id` H)
61	2, 60	grpid 9349	. . . . . 6 |- ((H e. Grp /\ (F` U) e. W) -> ((F` U) = (Id` H) <-> ((F` U)H(F` U)) = (F` U)))
62	1, 59, 61	mp2an 761	. . . . 5 |- ((F` U) = (Id` H) <-> ((F` U)H(F` U)) = (F` U))
63	57, 62	mpbir 207	. . . 4 |- (F` U) = (Id` H)
64	3, 63	eqtr4i 1911	. . 3 |- T = (F` U)
65		ffvelrn 4787	. . . 4 |- ((F:X-->Z /\ U e. X) -> (F` U) e. Z)
66	43, 51, 65	mp2an 761	. . 3 |- (F` U) e. Z
67	64, 66	eqeltri 1967	. 2 |- T e. Z
68		fveq2 4681	. . . . . 6 |- ((F` z) = x -> (M` (F` z)) = (M` x))
69	68	eleq1d 1963	. . . . 5 |- ((F` z) = x -> ((M` (F` z)) e. Z <-> (M` x) e. Z))
70	8, 35	grpinvcl 9352	. . . . . . . . . . 11 |- ((G e. Grp /\ z e. X) -> (N` z) e. X)
71	7, 70	mpan 759	. . . . . . . . . 10 |- (z e. X -> (N` z) e. X)
72	7, 1, 6, 8, 34, 35, 2, 3, 4, 5, 16	ghomgrpilem1 13628	. . . . . . . . . 10 |- ((z e. X /\ (N` z) e. X) -> ((F` z)H(F` (N` z))) = (F` (zG(N` z))))
73	71, 72	mpdan 768	. . . . . . . . 9 |- (z e. X -> ((F` z)H(F` (N` z))) = (F` (zG(N` z))))
74	8, 34, 35	grprinv 9355	. . . . . . . . . . 11 |- ((G e. Grp /\ z e. X) -> (zG(N` z)) = U)
75	7, 74	mpan 759	. . . . . . . . . 10 |- (z e. X -> (zG(N` z)) = U)
76	75	fveq2d 4685	. . . . . . . . 9 |- (z e. X -> (F` (zG(N` z))) = (F` U))
77	73, 76	eqtrd 1925	. . . . . . . 8 |- (z e. X -> ((F` z)H(F` (N` z))) = (F` U))
78	77, 64	syl6eqr 1946	. . . . . . 7 |- (z e. X -> ((F` z)H(F` (N` z))) = T)
79	12	ffvelrni 4788	. . . . . . . 8 |- (z e. X -> (F` z) e. W)
80	12	ffvelrni 4788	. . . . . . . . 9 |- ((N` z) e. X -> (F` (N` z)) e. W)
81	71, 80	syl 12	. . . . . . . 8 |- (z e. X -> (F` (N` z)) e. W)
82	2, 3, 4	grpinvid1 9356	. . . . . . . . 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))
83	1, 82	mp3an1 1178	. . . . . . . 8 |- (((F` z) e. W /\ (F` (N` z)) e. W) -> ((M` (F` z)) = (F` (N` z)) <-> ((F` z)H(F` (N` z))) = T))
84	79, 81, 83	syl11anc 524	. . . . . . 7 |- (z e. X -> ((M` (F` z)) = (F` (N` z)) <-> ((F` z)H(F` (N` z))) = T))
85	78, 84	mpbird 213	. . . . . 6 |- (z e. X -> (M` (F` z)) = (F` (N` z)))
86	43	ffvelrni 4788	. . . . . . 7 |- ((N` z) e. X -> (F` (N` z)) e. Z)
87	71, 86	syl 12	. . . . . 6 |- (z e. X -> (F` (N` z)) e. Z)
88	85, 87	eqeltrd 1971	. . . . 5 |- (z e. X -> (M` (F` z)) e. Z)
89	69, 88	syl5cbi 226	. . . 4 |- (z e. X -> ((F` z) = x -> (M` x) e. Z))
90	89	r19.23aiv 2211	. . 3 |- (E.z e. X (F` z) = x -> (M` x) e. Z)
91	22, 90	sylbi 216	. 2 |- (x e. Z -> (M` x) e. Z)
92	1, 2, 3, 4, 15, 16, 49, 67, 91	issubgi 9431	1 |- S e. (SubGrp` H)

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593   X. cxp 3984  ran crn 3987   |` cres 3988   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Grpcgr 9311  Idcgi 9312  invcgn 9313  SubGrpcsubg 9423   GrpHom cghom 10189

This theorem is referenced by:  ghomgrpi 13630

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-oprab 4887  df-grp 9316  df-gid 9317  df-ginv 9318  df-subg 9424  df-ghom 10190

Copyright terms: Public domain