Theorem ghomf1olem 13637

Description: Lemma for ghomf1o 13638.

Hypotheses

Ref	Expression
ghomf1olem.1	|- X = ran G
ghomf1olem.2	|- Y = ran F
ghomf1olem.3	|- S = (H |` (Y X. Y))
ghomf1olem.4	|- Z = ran S
ghomf1olem.5	|- U = (Id` G)
ghomf1olem.6	|- T = (Id` H)
ghomf1olem.7	|- N = (inv` G)

Assertion

Ref	Expression
ghomf1olem	|- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F:X-1-1-onto->Z <-> A.x e. X ((F` x) = T -> x = U)))

Distinct variable groups:   x,F   x,G   x,H   x,T   x,U   x,X   x,Z   x,N

Proof of Theorem ghomf1olem

Step	Hyp	Ref	Expression
1		ghomf1olem.1	. . . . . . . . 9 |- X = ran G
2		ghomf1olem.5	. . . . . . . . 9 |- U = (Id` G)
3	1, 2	grpidcl 9343	. . . . . . . 8 |- (G e. Grp -> U e. X)
4		fveq2 4681	. . . . . . . . . . . 12 |- (y = x -> (F` y) = (F` x))
5	4	eqeq1d 1892	. . . . . . . . . . 11 |- (y = x -> ((F` y) = (F` z) <-> (F` x) = (F` z)))
6		equequ1 1494	. . . . . . . . . . 11 |- (y = x -> (y = z <-> x = z))
7	5, 6	imbi12d 688	. . . . . . . . . 10 |- (y = x -> (((F` y) = (F` z) -> y = z) <-> ((F` x) = (F` z) -> x = z)))
8		fveq2 4681	. . . . . . . . . . . 12 |- (z = U -> (F` z) = (F` U))
9	8	eqeq2d 1895	. . . . . . . . . . 11 |- (z = U -> ((F` x) = (F` z) <-> (F` x) = (F` U)))
10		eqeq2 1893	. . . . . . . . . . 11 |- (z = U -> (x = z <-> x = U))
11	9, 10	imbi12d 688	. . . . . . . . . 10 |- (z = U -> (((F` x) = (F` z) -> x = z) <-> ((F` x) = (F` U) -> x = U)))
12	7, 11	rcla42v 2384	. . . . . . . . 9 |- ((x e. X /\ U e. X) -> (A.y e. X A.z e. X ((F` y) = (F` z) -> y = z) -> ((F` x) = (F` U) -> x = U)))
13	12	expcom 403	. . . . . . . 8 |- (U e. X -> (x e. X -> (A.y e. X A.z e. X ((F` y) = (F` z) -> y = z) -> ((F` x) = (F` U) -> x = U))))
14	3, 13	syl 12	. . . . . . 7 |- (G e. Grp -> (x e. X -> (A.y e. X A.z e. X ((F` y) = (F` z) -> y = z) -> ((F` x) = (F` U) -> x = U))))
15	14	com23 36	. . . . . 6 |- (G e. Grp -> (A.y e. X A.z e. X ((F` y) = (F` z) -> y = z) -> (x e. X -> ((F` x) = (F` U) -> x = U))))
16	15	3ad2ant1 897	. . . . 5 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (A.y e. X A.z e. X ((F` y) = (F` z) -> y = z) -> (x e. X -> ((F` x) = (F` U) -> x = U))))
17		f1of1 4634	. . . . . . 7 |- (F:X-1-1-onto->Z -> F:X-1-1->Z)
18		dff13 4850	. . . . . . 7 |- (F:X-1-1->Z <-> (F:X-->Z /\ A.y e. X A.z e. X ((F` y) = (F` z) -> y = z)))
19	17, 18	sylib 215	. . . . . 6 |- (F:X-1-1-onto->Z -> (F:X-->Z /\ A.y e. X A.z e. X ((F` y) = (F` z) -> y = z)))
20	19	simprd 352	. . . . 5 |- (F:X-1-1-onto->Z -> A.y e. X A.z e. X ((F` y) = (F` z) -> y = z))
21	16, 20	syl5 20	. . . 4 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F:X-1-1-onto->Z -> (x e. X -> ((F` x) = (F` U) -> x = U))))
22		ghomf1olem.6	. . . . . . . 8 |- T = (Id` H)
23	2, 22	ghomid 10197	. . . . . . 7 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F` U) = T)
24	23	eqeq2d 1895	. . . . . 6 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((F` x) = (F` U) <-> (F` x) = T))
25	24	imbi1d 675	. . . . 5 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (((F` x) = (F` U) -> x = U) <-> ((F` x) = T -> x = U)))
26	25	imbi2d 674	. . . 4 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((x e. X -> ((F` x) = (F` U) -> x = U)) <-> (x e. X -> ((F` x) = T -> x = U))))
27	21, 26	sylibd 219	. . 3 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F:X-1-1-onto->Z -> (x e. X -> ((F` x) = T -> x = U))))
28	27	r19.21adv 2181	. 2 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F:X-1-1-onto->Z -> A.x e. X ((F` x) = T -> x = U)))
29		df-f1o 4013	. . . 4 |- (F:X-1-1-onto->Z <-> (F:X-1-1->Z /\ F:X-onto->Z))
30		ghomf1olem.2	. . . . . . . 8 |- Y = ran F
31		ghomf1olem.3	. . . . . . . 8 |- S = (H |` (Y X. Y))
32		ghomf1olem.4	. . . . . . . 8 |- Z = ran S
33	1, 30, 31, 32	ghomfo 13634	. . . . . . 7 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> F:X-onto->Z)
34	33	adantr 425	. . . . . 6 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> F:X-onto->Z)
35		fof 4617	. . . . . 6 |- (F:X-onto->Z -> F:X-->Z)
36	34, 35	syl 12	. . . . 5 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> F:X-->Z)
37	1	grpcl 9324	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ y e. X /\ (N` z) e. X) -> (yG(N` z)) e. X)
38		ghomf1olem.7	. . . . . . . . . . . . . . . . 17 |- N = (inv` G)
39	1, 38	grpinvcl 9352	. . . . . . . . . . . . . . . 16 |- ((G e. Grp /\ z e. X) -> (N` z) e. X)
40	39	3adant2 895	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ y e. X /\ z e. X) -> (N` z) e. X)
41	37, 40	syld3an3 1142	. . . . . . . . . . . . . 14 |- ((G e. Grp /\ y e. X /\ z e. X) -> (yG(N` z)) e. X)
42	41	3expib 1070	. . . . . . . . . . . . 13 |- (G e. Grp -> ((y e. X /\ z e. X) -> (yG(N` z)) e. X))
43	42	3ad2ant1 897	. . . . . . . . . . . 12 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((y e. X /\ z e. X) -> (yG(N` z)) e. X))
44		fveq2 4681	. . . . . . . . . . . . . . 15 |- (x = (yG(N` z)) -> (F` x) = (F` (yG(N` z))))
45	44	eqeq1d 1892	. . . . . . . . . . . . . 14 |- (x = (yG(N` z)) -> ((F` x) = T <-> (F` (yG(N` z))) = T))
46		eqeq1 1890	. . . . . . . . . . . . . 14 |- (x = (yG(N` z)) -> (x = U <-> (yG(N` z)) = U))
47	45, 46	imbi12d 688	. . . . . . . . . . . . 13 |- (x = (yG(N` z)) -> (((F` x) = T -> x = U) <-> ((F` (yG(N` z))) = T -> (yG(N` z)) = U)))
48	47	rcla4v 2376	. . . . . . . . . . . 12 |- ((yG(N` z)) e. X -> (A.x e. X ((F` x) = T -> x = U) -> ((F` (yG(N` z))) = T -> (yG(N` z)) = U)))
49	43, 48	syl6 25	. . . . . . . . . . 11 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((y e. X /\ z e. X) -> (A.x e. X ((F` x) = T -> x = U) -> ((F` (yG(N` z))) = T -> (yG(N` z)) = U))))
50	49	imp 377	. . . . . . . . . 10 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (A.x e. X ((F` x) = T -> x = U) -> ((F` (yG(N` z))) = T -> (yG(N` z)) = U)))
51		opreq1 4889	. . . . . . . . . . . . . 14 |- ((F` y) = (F` z) -> ((F` y)H(F` (N` z))) = ((F` z)H(F` (N` z))))
52	51	3ad2ant3 899	. . . . . . . . . . . . 13 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X) /\ (F` y) = (F` z)) -> ((F` y)H(F` (N` z))) = ((F` z)H(F` (N` z))))
53		simprl 450	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> y e. X)
54	39	3ad2antl1 1038	. . . . . . . . . . . . . . . . 17 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ z e. X) -> (N` z) e. X)
55	54	adantrl 430	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (N` z) e. X)
56	53, 55	jca 310	. . . . . . . . . . . . . . 15 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (y e. X /\ (N` z) e. X))
57	1	ghomlin 10196	. . . . . . . . . . . . . . 15 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ (N` z) e. X)) -> ((F` y)H(F` (N` z))) = (F` (yG(N` z))))
58	56, 57	syldan 516	. . . . . . . . . . . . . 14 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> ((F` y)H(F` (N` z))) = (F` (yG(N` z))))
59	58	3adant3 896	. . . . . . . . . . . . 13 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X) /\ (F` y) = (F` z)) -> ((F` y)H(F` (N` z))) = (F` (yG(N` z))))
60		simprr 451	. . . . . . . . . . . . . . . . 17 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> z e. X)
61	60, 55	jca 310	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (z e. X /\ (N` z) e. X))
62	1	ghomlin 10196	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (z e. X /\ (N` z) e. X)) -> ((F` z)H(F` (N` z))) = (F` (zG(N` z))))
63	61, 62	syldan 516	. . . . . . . . . . . . . . 15 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> ((F` z)H(F` (N` z))) = (F` (zG(N` z))))
64	1, 2, 38	grprinv 9355	. . . . . . . . . . . . . . . . . 18 |- ((G e. Grp /\ z e. X) -> (zG(N` z)) = U)
65	64	3ad2antl1 1038	. . . . . . . . . . . . . . . . 17 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ z e. X) -> (zG(N` z)) = U)
66	65	adantrl 430	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (zG(N` z)) = U)
67	66	fveq2d 4685	. . . . . . . . . . . . . . 15 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (F` (zG(N` z))) = (F` U))
68	23	adantr 425	. . . . . . . . . . . . . . 15 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (F` U) = T)
69	63, 67, 68	3eqtrd 1929	. . . . . . . . . . . . . 14 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> ((F` z)H(F` (N` z))) = T)
70	69	3adant3 896	. . . . . . . . . . . . 13 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X) /\ (F` y) = (F` z)) -> ((F` z)H(F` (N` z))) = T)
71	52, 59, 70	3eqtr3d 1934	. . . . . . . . . . . 12 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X) /\ (F` y) = (F` z)) -> (F` (yG(N` z))) = T)
72	71	3expia 1069	. . . . . . . . . . 11 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> ((F` y) = (F` z) -> (F` (yG(N` z))) = T))
73	1, 38	grp2inv 9363	. . . . . . . . . . . . . . . . . 18 |- ((G e. Grp /\ z e. X) -> (N` (N` z)) = z)
74	73	3adant2 895	. . . . . . . . . . . . . . . . 17 |- ((G e. Grp /\ y e. X /\ z e. X) -> (N` (N` z)) = z)
75	74	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- ((G e. Grp /\ y e. X /\ z e. X) -> ((N` (N` z)) = y <-> z = y))
76	1, 2, 38	grpinvid2 9357	. . . . . . . . . . . . . . . . . 18 |- ((G e. Grp /\ (N` z) e. X /\ y e. X) -> ((N` (N` z)) = y <-> (yG(N` z)) = U))
77	76	3com23 1074	. . . . . . . . . . . . . . . . 17 |- ((G e. Grp /\ y e. X /\ (N` z) e. X) -> ((N` (N` z)) = y <-> (yG(N` z)) = U))
78	77, 40	syld3an3 1142	. . . . . . . . . . . . . . . 16 |- ((G e. Grp /\ y e. X /\ z e. X) -> ((N` (N` z)) = y <-> (yG(N` z)) = U))
79	75, 78	bitr3d 589	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ y e. X /\ z e. X) -> (z = y <-> (yG(N` z)) = U))
80		equcom 1488	. . . . . . . . . . . . . . 15 |- (z = y <-> y = z)
81	79, 80	syl5bbr 593	. . . . . . . . . . . . . 14 |- ((G e. Grp /\ y e. X /\ z e. X) -> (y = z <-> (yG(N` z)) = U))
82	81	3expb 1068	. . . . . . . . . . . . 13 |- ((G e. Grp /\ (y e. X /\ z e. X)) -> (y = z <-> (yG(N` z)) = U))
83	82	3ad2antl1 1038	. . . . . . . . . . . 12 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (y = z <-> (yG(N` z)) = U))
84	83	biimprd 171	. . . . . . . . . . 11 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> ((yG(N` z)) = U -> y = z))
85	72, 84	imim12d 69	. . . . . . . . . 10 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (((F` (yG(N` z))) = T -> (yG(N` z)) = U) -> ((F` y) = (F` z) -> y = z)))
86	50, 85	syld 30	. . . . . . . . 9 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ (y e. X /\ z e. X)) -> (A.x e. X ((F` x) = T -> x = U) -> ((F` y) = (F` z) -> y = z)))
87	86	ex 402	. . . . . . . 8 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((y e. X /\ z e. X) -> (A.x e. X ((F` x) = T -> x = U) -> ((F` y) = (F` z) -> y = z))))
88	87	com23 36	. . . . . . 7 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (A.x e. X ((F` x) = T -> x = U) -> ((y e. X /\ z e. X) -> ((F` y) = (F` z) -> y = z))))
89	88	imp 377	. . . . . 6 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> ((y e. X /\ z e. X) -> ((F` y) = (F` z) -> y = z)))
90	89	r19.21aivv 2183	. . . . 5 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> A.y e. X A.z e. X ((F` y) = (F` z) -> y = z))
91	18, 36, 90	sylanbrc 527	. . . 4 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> F:X-1-1->Z)
92	29, 91, 34	sylanbrc 527	. . 3 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> F:X-1-1-onto->Z)
93	92	ex 402	. 2 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (A.x e. X ((F` x) = T -> x = U) -> F:X-1-1-onto->Z))
94	28, 93	impbid 574	1 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F:X-1-1-onto->Z <-> A.x e. X ((F` x) = T -> x = U)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   X. cxp 3984  ran crn 3987   |` cres 3988  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  Grpcgr 9311  Idcgi 9312  invcgn 9313   GrpHom cghom 10189

This theorem is referenced by:  ghomf1o 13638

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