Theorem ghgrpilem3 8072

Description: Lemma for ghgrpi 8074.

Hypotheses

Ref	Expression
ghgrpi.1	⊢ G ∈ Grp
ghgrpi.2	⊢ X = ran G
ghgrpi.3	⊢ F:X–onto→Y
ghgrpi.4	⊢ Y ⊆ A
ghgrpi.5	⊢ O Fn (A × A)
ghgrpi.6	⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y)))
ghgrpi.7	⊢ H = (O ↾ (Y × Y))
ghgrpilem3.8	⊢ U = (Id ‘G)
ghgrpilem3.9	⊢ N = (inv ‘G)
ghgrpilem3.10	⊢ D = ( /g ‘G)

Assertion

Ref	Expression
ghgrpilem3	⊢ ((a ∈ Y ⋀ b ∈ Y) → (∃c ∈ Y (cHa) = b ⋀ ∃c ∈ 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 ∈ 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 × A)
6		ghgrpi.6	. . 3 ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y)))
7		ghgrpi.7	. . 3 ⊢ H = (O ↾ (Y × Y))
8		opreq1 3953	. . . . . . . 8 ⊢ (c = (F ‘(yDx)) → (cH(F ‘x)) = ((F ‘(yDx))H(F ‘x)))
9	8	eqeq1d 1475	. . . . . . 7 ⊢ (c = (F ‘(yDx)) → ((cH(F ‘x)) = (F ‘y) ↔ ((F ‘(yDx))H(F ‘x)) = (F ‘y)))
10	9	rcla4ev 1868	. . . . . 6 ⊢ (((F ‘(yDx)) ∈ Y ⋀ ((F ‘(yDx))H(F ‘x)) = (F ‘y)) → ∃c ∈ Y (cH(F ‘x)) = (F ‘y))
11		ghgrpilem3.10	. . . . . . . . . 10 ⊢ D = ( /g ‘G)
12	2, 11	grpdivcl 8021	. . . . . . . . 9 ⊢ ((G ∈ Grp ⋀ y ∈ X ⋀ x ∈ X) → (yDx) ∈ X)
13	1, 12	mp3an1 900	. . . . . . . 8 ⊢ ((y ∈ X ⋀ x ∈ X) → (yDx) ∈ X)
14		df-fo 3186	. . . . . . . . . . 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 3798	. . . . . . . . 9 ⊢ ((F Fn X ⋀ (yDx) ∈ X) → (F ‘(yDx)) ∈ ran F)
18	16, 17	mpan 693	. . . . . . . 8 ⊢ ((yDx) ∈ X → (F ‘(yDx)) ∈ ran F)
19	13, 18	syl 10	. . . . . . 7 ⊢ ((y ∈ X ⋀ x ∈ X) → (F ‘(yDx)) ∈ ran F)
20	15	pm3.27i 324	. . . . . . 7 ⊢ ran F = Y
21	19, 20	syl6eleq 1550	. . . . . 6 ⊢ ((y ∈ X ⋀ x ∈ X) → (F ‘(yDx)) ∈ Y)
22	1, 2, 3, 4, 5, 6, 7	ghgrpilem1 8070	. . . . . . . . 9 ⊢ (((yDx) ∈ X ⋀ x ∈ X) → (F ‘((yDx)Gx)) = ((F ‘(yDx))H(F ‘x)))
23	22, 13	sylan 448	. . . . . . . 8 ⊢ (((y ∈ X ⋀ x ∈ X) ⋀ x ∈ X) → (F ‘((yDx)Gx)) = ((F ‘(yDx))H(F ‘x)))
24	23	anabss3 499	. . . . . . 7 ⊢ ((y ∈ X ⋀ x ∈ X) → (F ‘((yDx)Gx)) = ((F ‘(yDx))H(F ‘x)))
25	2, 11	grpnpcan 8026	. . . . . . . . 9 ⊢ ((G ∈ Grp ⋀ y ∈ X ⋀ x ∈ X) → ((yDx)Gx) = y)
26	1, 25	mp3an1 900	. . . . . . . 8 ⊢ ((y ∈ X ⋀ x ∈ X) → ((yDx)Gx) = y)
27	26	fveq2d 3713	. . . . . . 7 ⊢ ((y ∈ X ⋀ x ∈ X) → (F ‘((yDx)Gx)) = (F ‘y))
28	24, 27	eqtr3d 1501	. . . . . 6 ⊢ ((y ∈ X ⋀ x ∈ X) → ((F ‘(yDx))H(F ‘x)) = (F ‘y))
29	10, 21, 28	sylanc 471	. . . . 5 ⊢ ((y ∈ X ⋀ x ∈ X) → ∃c ∈ Y (cH(F ‘x)) = (F ‘y))
30	29	ancoms 436	. . . 4 ⊢ ((x ∈ X ⋀ y ∈ X) → ∃c ∈ Y (cH(F ‘x)) = (F ‘y))
31		opreq2 3954	. . . . . 6 ⊢ ((F ‘x) = a → (cH(F ‘x)) = (cHa))
32	31	eqeq1d 1475	. . . . 5 ⊢ ((F ‘x) = a → ((cH(F ‘x)) = (F ‘y) ↔ (cHa) = (F ‘y)))
33	32	rexbidv 1656	. . . 4 ⊢ ((F ‘x) = a → (∃c ∈ Y (cH(F ‘x)) = (F ‘y) ↔ ∃c ∈ Y (cHa) = (F ‘y)))
34	1, 2, 3, 4, 5, 6, 7, 30, 33	ghgrpilem2 8071	. . 3 ⊢ ((y ∈ X ⋀ a ∈ Y) → ∃c ∈ Y (cHa) = (F ‘y))
35		eqeq2 1476	. . . 4 ⊢ ((F ‘y) = b → ((cHa) = (F ‘y) ↔ (cHa) = b))
36	35	rexbidv 1656	. . 3 ⊢ ((F ‘y) = b → (∃c ∈ Y (cHa) = (F ‘y) ↔ ∃c ∈ Y (cHa) = b))
37	1, 2, 3, 4, 5, 6, 7, 34, 36	ghgrpilem2 8071	. 2 ⊢ ((a ∈ Y ⋀ b ∈ Y) → ∃c ∈ Y (cHa) = b)
38		opreq2 3954	. . . . . . 7 ⊢ (c = (F ‘((N ‘x)Gy)) → ((F ‘x)Hc) = ((F ‘x)H(F ‘((N ‘x)Gy))))
39	38	eqeq1d 1475	. . . . . 6 ⊢ (c = (F ‘((N ‘x)Gy)) → (((F ‘x)Hc) = (F ‘y) ↔ ((F ‘x)H(F ‘((N ‘x)Gy))) = (F ‘y)))
40	39	rcla4ev 1868	. . . . 5 ⊢ (((F ‘((N ‘x)Gy)) ∈ Y ⋀ ((F ‘x)H(F ‘((N ‘x)Gy))) = (F ‘y)) → ∃c ∈ Y ((F ‘x)Hc) = (F ‘y))
41	2	grpcl 7978	. . . . . . . . 9 ⊢ ((G ∈ Grp ⋀ (N ‘x) ∈ X ⋀ y ∈ X) → ((N ‘x)Gy) ∈ X)
42	1, 41	mp3an1 900	. . . . . . . 8 ⊢ (((N ‘x) ∈ X ⋀ y ∈ X) → ((N ‘x)Gy) ∈ X)
43		ghgrpilem3.9	. . . . . . . . . 10 ⊢ N = (inv ‘G)
44	2, 43	grpinvcl 8002	. . . . . . . . 9 ⊢ ((G ∈ Grp ⋀ x ∈ X) → (N ‘x) ∈ X)
45	1, 44	mpan 693	. . . . . . . 8 ⊢ (x ∈ X → (N ‘x) ∈ X)
46	42, 45	sylan 448	. . . . . . 7 ⊢ ((x ∈ X ⋀ y ∈ X) → ((N ‘x)Gy) ∈ X)
47		fnfvelrn 3798	. . . . . . . 8 ⊢ ((F Fn X ⋀ ((N ‘x)Gy) ∈ X) → (F ‘((N ‘x)Gy)) ∈ ran F)
48	16, 47	mpan 693	. . . . . . 7 ⊢ (((N ‘x)Gy) ∈ X → (F ‘((N ‘x)Gy)) ∈ ran F)
49	46, 48	syl 10	. . . . . 6 ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘((N ‘x)Gy)) ∈ ran F)
50	49, 20	syl6eleq 1550	. . . . 5 ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘((N ‘x)Gy)) ∈ Y)
51	1, 2, 3, 4, 5, 6, 7	ghgrpilem1 8070	. . . . . . 7 ⊢ ((x ∈ X ⋀ ((N ‘x)Gy) ∈ X) → (F ‘(xG((N ‘x)Gy))) = ((F ‘x)H(F ‘((N ‘x)Gy))))
52	46, 51	syldan 467	. . . . . 6 ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xG((N ‘x)Gy))) = ((F ‘x)H(F ‘((N ‘x)Gy))))
53	2, 43	grpasscan1 8012	. . . . . . . 8 ⊢ ((G ∈ Grp ⋀ x ∈ X ⋀ y ∈ X) → (xG((N ‘x)Gy)) = y)
54	1, 53	mp3an1 900	. . . . . . 7 ⊢ ((x ∈ X ⋀ y ∈ X) → (xG((N ‘x)Gy)) = y)
55	54	fveq2d 3713	. . . . . 6 ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xG((N ‘x)Gy))) = (F ‘y))
56	52, 55	eqtr3d 1501	. . . . 5 ⊢ ((x ∈ X ⋀ y ∈ X) → ((F ‘x)H(F ‘((N ‘x)Gy))) = (F ‘y))
57	40, 50, 56	sylanc 471	. . . 4 ⊢ ((x ∈ X ⋀ y ∈ X) → ∃c ∈ Y ((F ‘x)Hc) = (F ‘y))
58		opreq1 3953	. . . . . 6 ⊢ ((F ‘x) = a → ((F ‘x)Hc) = (aHc))
59	58	eqeq1d 1475	. . . . 5 ⊢ ((F ‘x) = a → (((F ‘x)Hc) = (F ‘y) ↔ (aHc) = (F ‘y)))
60	59	rexbidv 1656	. . . 4 ⊢ ((F ‘x) = a → (∃c ∈ Y ((F ‘x)Hc) = (F ‘y) ↔ ∃c ∈ Y (aHc) = (F ‘y)))
61	1, 2, 3, 4, 5, 6, 7, 57, 60	ghgrpilem2 8071	. . 3 ⊢ ((y ∈ X ⋀ a ∈ Y) → ∃c ∈ Y (aHc) = (F ‘y))
62		eqeq2 1476	. . . 4 ⊢ ((F ‘y) = b → ((aHc) = (F ‘y) ↔ (aHc) = b))
63	62	rexbidv 1656	. . 3 ⊢ ((F ‘y) = b → (∃c ∈ Y (aHc) = (F ‘y) ↔ ∃c ∈ Y (aHc) = b))
64	1, 2, 3, 4, 5, 6, 7, 61, 63	ghgrpilem2 8071	. 2 ⊢ ((a ∈ Y ⋀ b ∈ Y) → ∃c ∈ Y (aHc) = b)
65	37, 64	jca 288	1 ⊢ ((a ∈ Y ⋀ b ∈ Y) → (∃c ∈ Y (cHa) = b ⋀ ∃c ∈ Y (aHc) = b))

Syntax hints:   → wi 3   ⋀ wa 223   = wceq 953   ∈ wcel 955  ∃wrex 1638   ⊆ wss 2037   × cxp 3158  ran crn 3161   ↾ cres 3162   Fn wfn 3167  –onto→wfo 3170   ‘cfv 3172  (class class class)co 3948  Grpcgr 7967  Idcgi 7968  invcgn 7969   /_g cgs 7970

This theorem is referenced by:  ghgrpilem4 8073

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fo 3186  df-fv 3188  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-grp 7971  df-gid 7972  df-ginv 7973  df-gdiv 7974

Copyright terms: Public domain