Theorem ghomf1olem 10517

Description: Lemma for ghomf1o 10518.

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 8178	. . . . . . . 8 |- (G e. Grp -> U e. X)
4		fveq2 3800	. . . . . . . . . . . 12 |- (y = x -> (F` y) = (F` x))
5	4	eqeq1d 1520	. . . . . . . . . . 11 |- (y = x -> ((F` y) = (F` z) <-> (F` x) = (F` z)))
6		equequ1 1167	. . . . . . . . . . 11 |- (y = x -> (y = z <-> x = z))
7	5, 6	imbi12d 628	. . . . . . . . . 10 |- (y = x -> (((F` y) = (F` z) -> y = z) <-> ((F` x) = (F` z) -> x = z)))
8		fveq2 3800	. . . . . . . . . . . 12 |- (z = U -> (F` z) = (F` U))
9	8	eqeq2d 1523	. . . . . . . . . . 11 |- (z = U -> ((F` x) = (F` z) <-> (F` x) = (F` U)))
10		eqeq2 1521	. . . . . . . . . . 11 |- (z = U -> (x = z <-> x = U))
11	9, 10	imbi12d 628	. . . . . . . . . 10 |- (z = U -> (((F` x) = (F` z) -> x = z) <-> ((F` x) = (F` U) -> x = U)))
12	7, 11	rcla42v 1918	. . . . . . . . 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 372	. . . . . . . 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 10	. . . . . . 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 32	. . . . . 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 803	. . . . 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 3764	. . . . . . 7 |- (F:X-1-1-onto->Z -> F:X-1-1->Z)
18		dff13 3950	. . . . . . 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 196	. . . . . 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	pm3.27d 323	. . . . 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 21	. . . 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 10515	. . . . . . 7 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> (F` U) = T)
24	23	eqeq2d 1523	. . . . . 6 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((F` x) = (F` U) <-> (F` x) = T))
25	24	imbi1d 615	. . . . 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 614	. . . 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 200	. . 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 1756	. 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 3252	. . . . 5 |- (F:X-1-1-onto->Z <-> (F:X-1-1->Z /\ F:X-onto->Z))
30	29	biimpri 150	. . . 4 |- ((F:X-1-1->Z /\ F:X-onto->Z) -> F:X-1-1-onto->Z)
31	18	biimpri 150	. . . . 5 |- ((F:X-->Z /\ A.y e. X A.z e. X ((F` y) = (F` z) -> y = z)) -> F:X-1-1->Z)
32		ghomf1olem.2	. . . . . . . 8 |- Y = ran F
33		ghomf1olem.3	. . . . . . . 8 |- S = (H |` (Y X. Y))
34		ghomf1olem.4	. . . . . . . 8 |- Z = ran S
35	1, 32, 33, 34	ghomfo 10512	. . . . . . 7 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> F:X-onto->Z)
36	35	adantr 389	. . . . . 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)
37		fof 3747	. . . . . 6 |- (F:X-onto->Z -> F:X-->Z)
38	36, 37	syl 10	. . . . 5 |- (((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) /\ A.x e. X ((F` x) = T -> x = U)) -> F:X-->Z)
39	1	grpcl 8164	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ y e. X /\ (N` z) e. X) -> (yG(N` z)) e. X)
40		ghomf1olem.7	. . . . . . . . . . . . . . . . 17 |- N = (inv` G)
41	1, 40	grpinvcl 8187	. . . . . . . . . . . . . . . 16 |- ((G e. Grp /\ z e. X) -> (N` z) e. X)
42	41	3adant2 801	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ y e. X /\ z e. X) -> (N` z) e. X)
43	39, 42	syld3an3 873	. . . . . . . . . . . . . 14 |- ((G e. Grp /\ y e. X /\ z e. X) -> (yG(N` z)) e. X)
44	43	3expib 839	. . . . . . . . . . . . 13 |- (G e. Grp -> ((y e. X /\ z e. X) -> (yG(N` z)) e. X))
45	44	3ad2ant1 803	. . . . . . . . . . . 12 |- ((G e. Grp /\ H e. Grp /\ F e. (G GrpHom H)) -> ((y e. X /\ z e. X) -> (yG(N` z)) e. X))
46		fveq2 3800	. . . . . . . . . . . . . . 15 |- (x = (yG(N` z)) -> (F` x) = (F` (yG(N` z))))
47	46	eqeq1d 1520	. . . . . . . . . . . . . 14 |- (x = (yG(N` z)) -> ((F` x) = T <-> (F` (yG(N` z))) = T))
48		eqeq1 1518	. . . . . . . . . . . . . 14 |- (x = (yG(N` z)) -> (x = U <-> (yG(N` z)) = U))
49	47, 48	imbi12d 628	. . . . . . . . . . . . 13 |- (x = (yG(N` z)) -> (((F` x) = T -> x = U) <-> ((F` (yG(N` z))) = T -> (yG(N` z)) = U)))
50	49	rcla4v 1911	. . . . . . . . . . . 12 |- ((yG(N` z)) e. X -> (A.x e. X ((F` x) = T -> x = U) -> ((F` (yG(N` z))) = T -> (yG(N` z)) = U)))
51	45, 50	syl6 22	. . . . . . . . . . 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))))
52	51	imp 348	. . . . . . . . . 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)))
53		opreq1 4044	. . . . . . . . . . . . . 14 |- ((F` y) = (F` z) -> ((F` y)H(F` (N` z))) = ((F` z)H(F` (N` z))))
54	53	3ad2ant3 805	. . . . . . . . . . . . 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))))
55		simprl 414	. . . . . . . . . . . . . . . 16 |-