Theorem grplactf1o 8094

Description: The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.)

Hypotheses

Ref	Expression
grplact.1	|- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}
grplact.2	|- X = ran G

Assertion

Ref	Expression
grplactf1o	|- ((G e. Grp /\ A e. X) -> (F` A):X-1-1-onto->X)

Distinct variable groups:   A,a,b,g,h   G,a,b,g,h   X,a,b,g,h

Proof of Theorem grplactf1o

Step	Hyp	Ref	Expression
1		f1o5 3703	. . 3 |- ((F` A):X-1-1-onto->X <-> ((F` A):X-1-1->X /\ ran ( F` A) = X))
2	1	biimpr 152	. 2 |- (((F` A):X-1-1->X /\ ran ( F` A) = X) -> (F` A):X-1-1-onto->X)
3		f1fv 3880	. . . 4 |- ((F` A):X-1-1->X <-> ((F` A):X-->X /\ A.x e. X A.y e. X (((F` A)` x) = ((F` A)` y) -> x = y)))
4	3	biimpr 152	. . 3 |- (((F` A):X-->X /\ A.x e. X A.y e. X (((F` A)` x) = ((F` A)` y) -> x = y)) -> (F` A):X-1-1->X)
5		grplact.2	. . . . . . . 8 |- X = ran G
6	5	grpcl 8041	. . . . . . 7 |- ((G e. Grp /\ A e. X /\ a e. X) -> (AGa) e. X)
7	6	3expia 837	. . . . . 6 |- ((G e. Grp /\ A e. X) -> (a e. X -> (AGa) e. X))
8	7	r19.21aiv 1716	. . . . 5 |- ((G e. Grp /\ A e. X) -> A.a e. X (AGa) e. X)
9		eqid 1478	. . . . . 6 |- {<.a, b>. | (a e. X /\ b = (AGa))} = {<.a, b>. | (a e. X /\ b = (AGa))}
10	9	fopab2 3829	. . . . 5 |- (A.a e. X (AGa) e. X <-> {<.a, b>. | (a e. X /\ b = (AGa))}:X-->X)
11	8, 10	sylib 198	. . . 4 |- ((G e. Grp /\ A e. X) -> {<.a, b>. | (a e. X /\ b = (AGa))}:X-->X)
12		grplact.1	. . . . . 6 |- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}
13	12, 5	grplactfval 8092	. . . . 5 |- ((G e. Grp /\ A e. X) -> (F` A) = {<.a, b>. | (a e. X /\ b = (AGa))})
14	13	feq1d 3630	. . . 4 |- ((G e. Grp /\ A e. X) -> ((F` A):X-->X <-> {<.a, b>. | (a e. X /\ b = (AGa))}:X-->X))
15	11, 14	mpbird 196	. . 3 |- ((G e. Grp /\ A e. X) -> (F` A):X-->X)
16	12, 5	grplactval 8093	. . . . . . . . . . 11 |- ((G e. Grp /\ A e. X /\ x e. X) -> ((F` A)` x) = (AGx))
17	16	3expia 837	. . . . . . . . . 10 |- ((G e. Grp /\ A e. X) -> (x e. X -> ((F` A)` x) = (AGx)))
18	12, 5	grplactval 8093	. . . . . . . . . . 11 |- ((G e. Grp /\ A e. X /\ y e. X) -> ((F` A)` y) = (AGy))
19	18	3expia 837	. . . . . . . . . 10 |- ((G e. Grp /\ A e. X) -> (y e. X -> ((F` A)` y) = (AGy)))
20	17, 19	anim12d 560	. . . . . . . . 9 |- ((G e. Grp /\ A e. X) -> ((x e. X /\ y e. X) -> (((F` A)` x) = (AGx) /\ ((F` A)` y) = (AGy))))
21	20	imp 350	. . . . . . . 8 |- (((G e. Grp /\ A e. X) /\ (x e. X /\ y e. X)) -> (((F` A)` x) = (AGx) /\ ((F` A)` y) = (AGy)))
22		eqeq12 1490	. . . . . . . 8 |- ((((F` A)` x) = (AGx) /\ ((F` A)` y) = (AGy)) -> (((F` A)` x) = ((F` A)` y) <-> (AGx) = (AGy)))
23	21, 22	syl 10	. . . . . . 7 |- (((G e. Grp /\ A e. X) /\ (x e. X /\ y e. X)) -> (((F` A)` x) = ((F` A)` y) <-> (AGx) = (AGy)))
24	5	grplcan 8071	. . . . . . . . . . . 12 |- ((G e. Grp /\ (x e. X /\ y e. X /\ A e. X)) -> ((AGx) = (AGy) <-> x = y))
25	24	expcom 374	. . . . . . . . . . 11 |- ((x e. X /\ y e. X /\ A e. X) -> (G e. Grp -> ((AGx) = (AGy) <-> x = y)))
26	25	3expia 837	. . . . . . . . . 10 |- ((x e. X /\ y e. X) -> (A e. X -> (G e. Grp -> ((AGx) = (AGy) <-> x = y))))
27	26	com23 32	. . . . . . . . 9 |- ((x e. X /\ y e. X) -> (G e. Grp -> (A e. X -> ((AGx) = (AGy) <-> x = y))))
28	27	imp3a 361	. . . . . . . 8 |- ((x e. X /\ y e. X) -> ((G e. Grp /\ A e. X) -> ((AGx) = (AGy) <-> x = y)))
29	28	impcom 351	. . . . . . 7 |- (((G e. Grp /\ A e. X) /\ (x e. X /\ y e. X)) -> ((AGx) = (AGy) <-> x = y))
30	23, 29	bitrd 530	. . . . . 6 |- (((G e. Grp /\ A e. X) /\ (x e. X /\ y e. X)) -> (((F` A)` x) = ((F` A)` y) <-> x = y))
31	30	biimpd 153	. . . . 5 |- (((G e. Grp /\ A e. X) /\ (x e. X /\ y e. X)) -> (((F` A)` x) = ((F` A)` y) -> x = y))
32	31	ex 373	. . . 4 |- ((G e. Grp /\ A e. X) -> ((x e. X /\ y e. X) -> (((F` A)` x) = ((F` A)` y) -> x = y)))
33	32	r19.21aivv 1723	. . 3 |- ((G e. Grp /\ A e. X) -> A.x e. X A.y e. X (((F` A)` x) = ((F` A)` y) -> x = y))
34	4, 15, 33	sylanc 473	. 2 |- ((G e. Grp /\ A e. X) -> (F` A):X-1-1->X)
35		frn 3639	. . . 4 |- ((F` A):X-->X -> ran ( F` A) (_ X)
36	15, 35	syl 10	. . 3 |- ((G e. Grp /\ A e. X) -> ran ( F` A) (_ X)
37		opreq2 3975	. . . . . . . . 9 |- (a = (((inv` G)` A)Gy) -> (AGa) = (AG(((inv` G)` A)Gy)))
38	37	eqeq2d 1489	. . . . . . . 8 |- (a = (((inv` G)` A)Gy) -> (y = (AGa) <-> y = (AG(((inv` G)` A)Gy))))
39	38	rcla4ev 1880	. . . . . . 7 |- (((((inv` G)` A)Gy) e. X /\ y = (AG(((inv` G)` A)Gy))) -> E.a e. X y = (AGa))
40		eqid 1478	. . . . . . . . . 10 |- (inv` G) = (inv` G)
41	5, 40	grpinvcl 8064	. . . . . . . . 9 |- ((G e. Grp /\ A e. X) -> ((inv` G)` A) e. X)
42	5	grpcl 8041	. . . . . . . . . 10 |- ((G e. Grp /\ ((inv` G)` A) e. X /\ y e. X) -> (((inv` G)` A)Gy) e. X)
43	42	3expia 837	. . . . . . . . 9 |- ((G e. Grp /\ ((inv` G)` A) e. X) -> (y e. X -> (((inv` G)` A)Gy) e. X))
44	41, 43	syldan 469	. . . . . . . 8 |- ((G e. Grp /\ A e. X) -> (y e. X -> (((inv` G)` A)Gy) e. X))
45	44	3impia 832	. . . . . . 7 |- ((G e. Grp /\ A e. X /\ y e. X) -> (((inv` G)` A)Gy) e. X)
46	5, 40	grpasscan1 8073	. . . . . . . 8 |- ((G e. Grp /\ A e. X /\ y e. X) -> (AG(((inv` G)` A)Gy)) = y)
47	46	eqcomd 1483	. . . . . . 7 |- ((G e. Grp /\ A e. X /\ y e. X) -> y = (AG(((inv` G)` A)Gy)))
48	39, 45, 47	sylanc 473	. . . . . 6 |- ((G e. Grp /\ A e. X /\ y e. X) -> E.a e. X y = (AGa))
49	48	3expia 837	. . . . 5 |- ((G e. Grp /\ A e. X) -> (y e. X -> E.a e. X y = (AGa)))
50	13	rneqd 3347	. . . . . . 7 |- ((G e. Grp /\ A e. X) -> ran ( F` A) = ran {<.a, b>. | (a e. X /\ b = (AGa))})
51	50	eleq2d 1544	. . . . . 6 |- ((G e. Grp /\ A e. X) -> (y e. ran ( F` A) <-> y e. ran {<.a, b>. | (a e. X /\ b = (AGa))}))
52		oprex 3989	. . . . . . . 8 |- (AGa) e. V
53	52, 9	elrnopab 3807	. . . . . . 7 |- (y e. ran {<.a, b>. | (a e. X /\ b = (AGa))} <-> E.a e. X y =