Theorem isgrp 8038

Description: The predicate "is a group operation." Note that X is the base set of the group.

Hypothesis

Ref	Expression
isgrp.1	|- X = ran G

Assertion

Ref	Expression
isgrp	|- (G e. A -> (G e. Grp <-> (G:(X X. X)-->X /\ A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz)) /\ E.u e. X A.x e. X ((uGx) = x /\ E.y e. X (yGx) = u))))

Distinct variable groups:   x,u,y,z,G   u,X,x,y,z

Proof of Theorem isgrp

Step	Hyp	Ref	Expression
1		feq1 3626	. . . . . 6 |- (g = G -> (g:(t X. t)-->t <-> G:(t X. t)-->t))
2		opreq 3973	. . . . . . . . . 10 |- (g = G -> ((xgy)gz) = ((xgy)Gz))
3		opreq 3973	. . . . . . . . . . 11 |- (g = G -> (xgy) = (xGy))
4	3	opreq1d 3981	. . . . . . . . . 10 |- (g = G -> ((xgy)Gz) = ((xGy)Gz))
5	2, 4	eqtrd 1510	. . . . . . . . 9 |- (g = G -> ((xgy)gz) = ((xGy)Gz))
6		opreq 3973	. . . . . . . . . 10 |- (g = G -> (xg(ygz)) = (xG(ygz)))
7		opreq 3973	. . . . . . . . . . 11 |- (g = G -> (ygz) = (yGz))
8	7	opreq2d 3982	. . . . . . . . . 10 |- (g = G -> (xG(ygz)) = (xG(yGz)))
9	6, 8	eqtrd 1510	. . . . . . . . 9 |- (g = G -> (xg(ygz)) = (xG(yGz)))
10	5, 9	eqeq12d 1492	. . . . . . . 8 |- (g = G -> (((xgy)gz) = (xg(ygz)) <-> ((xGy)Gz) = (xG(yGz))))
11	10	ralbidv 1666	. . . . . . 7 |- (g = G -> (A.z e. t ((xgy)gz) = (xg(ygz)) <-> A.z e. t ((xGy)Gz) = (xG(yGz))))
12	11	2ralbidv 1683	. . . . . 6 |- (g = G -> (A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) <-> A.x e. t A.y e. t A.z e. t ((xGy)Gz) = (xG(yGz))))
13		opreq 3973	. . . . . . . . 9 |- (g = G -> (ugx) = (uGx))
14	13	eqeq1d 1486	. . . . . . . 8 |- (g = G -> ((ugx) = x <-> (uGx) = x))
15		opreq 3973	. . . . . . . . . 10 |- (g = G -> (ygx) = (yGx))
16	15	eqeq1d 1486	. . . . . . . . 9 |- (g = G -> ((ygx) = u <-> (yGx) = u))
17	16	rexbidv 1667	. . . . . . . 8 |- (g = G -> (E.y e. t (ygx) = u <-> E.y e. t (yGx) = u))
18	14, 17	anbi12d 630	. . . . . . 7 |- (g = G -> (((ugx) = x /\ E.y e. t (ygx) = u) <-> ((uGx) = x /\ E.y e. t (yGx) = u)))
19	18	rexralbidv 1685	. . . . . 6 |- (g = G -> (E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u) <-> E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u)))
20	1, 12, 19	3anbi123d 895	. . . . 5 |- (g = G -> ((g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u)) <-> (G:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xGy)Gz) = (xG(yGz)) /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u))))
21	20	exbidv 1281	. . . 4 |- (g = G -> (E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u)) <-> E.t(G:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xGy)Gz) = (xG(yGz)) /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u))))
22		df-grp 8034	. . . 4 |- Grp = {g | E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))}
23	21, 22	elab2g 1903	. . 3 |- (G e. A -> (G e. Grp <-> E.t(G:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xGy)Gz) = (xG(yGz)) /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u))))
24		opreq2 3975	. . . . . . . . . . . . . . . . 17 |- (x = z -> (uGx) = (uGz))
25		id 59	. . . . . . . . . . . . . . . . 17 |- (x = z -> x = z)
26	24, 25	eqeq12d 1492	. . . . . . . . . . . . . . . 16 |- (x = z -> ((uGx) = x <-> (uGz) = z))
27		eqcom 1480	. . . . . . . . . . . . . . . 16 |- ((uGz) = z <-> z = (uGz))
28	26, 27	syl6bb 538	. . . . . . . . . . . . . . 15 |- (x = z -> ((uGx) = x <-> z = (uGz)))
29	28	rcla4v 1876	. . . . . . . . . . . . . 14 |- (z e. t -> (A.x e. t (uGx) = x -> z = (uGz)))
30		opreq2 3975	. . . . . . . . . . . . . . . . 17 |- (y = z -> (uGy) = (uGz))
31	30	eqeq2d 1489	. . . . . . . . . . . . . . . 16 |- (y = z -> (z = (uGy) <-> z = (uGz)))
32	31	rcla4ev 1880	. . . . . . . . . . . . . . 15 |- ((z e. t /\ z = (uGz)) -> E.y e. t z = (uGy))
33	32	ex 373	. . . . . . . . . . . . . 14 |- (z e. t -> (z = (uGz) -> E.y e. t z = (uGy)))
34	29, 33	syld 27	. . . . . . . . . . . . 13 |- (z e. t -> (A.x e. t (uGx) = x -> E.y e. t z = (uGy)))
35		pm3.26 319	. . . . . . . . . . . . . 14 |- (((uGx) = x /\ E.y e. t (yGx) = u) -> (uGx) = x)
36	35	r19.20si 1709	. . . . . . . . . . . . 13 |- (A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u) -> A.x e. t (uGx) = x)
37	34, 36	syl5 21	. . . . . . . . . . . 12 |- (z e. t -> (A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u) -> E.y e. t z = (uGy)))
38	37	r19.22sdv 1741	. . . . . . . . . . 11 |- (z e. t -> (E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u) -> E.u e. t E.y e. t z = (uGy)))
39	38	impcom 351	. . . . . . . . . 10 |- ((E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u) /\ z e. t) -> E.u e. t E.y e. t z = (uGy))
40	39	r19.21aiva 1717	. . . . . . . . 9 |- (E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u) -> A.z e. t E.u e. t E.y e. t z = (uGy))
41	40	anim2i 335	. . . . . . . 8 |- ((G:(t X. t)-->t /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u)) -> (G:(t X. t)-->t /\ A.z e. t E.u e. t E.y e. t z = (uGy)))
42		fooprval 4043	. . . . . . . 8 |- (G:(t X. t)-onto->t <-> (G:(t X. t)-->t /\ A.z e. t E.u e. t E.y e. t z = (uGy)))
43	41, 42	sylibr 200	. . . . . . 7 |- ((G:(t X. t)-->t /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u)) -> G:(t X. t)-onto->t)
44		forn 3680	. . . . . . . 8 |- (G:(t X. t)-onto->t -> ran G = t)
45	44	eqcomd 1483	. . . . . . 7 |- (G:(t X. t)-onto->t -> t = ran G)
46	43, 45	syl 10	. . . . . 6 |- ((G:(t X. t)-->t /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx) = u)) -> t = ran G)
47	46	3adant2 800	. . . . 5 |- ((G:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xGy)Gz) = (xG(yGz)) /\ E.u e. t A.x e. t ((uGx) = x /\ E.y e. t (yGx)