Theorem isgrp2i 8038

Description: An alternate way to show a group operation. Exercise 1 of [Herstein] p. 57.

Hypotheses

Ref	Expression
isgrp2i.1	|- X e. V
isgrp2i.2	|- X =/= (/)
isgrp2i.3	|- G:(X X. X)-->X
isgrp2i.4	|- ((x e. X /\ y e. X /\ z e. X) -> ((xGy)Gz) = (xG(yGz)))
isgrp2i.5	|- ((x e. X /\ y e. X) -> E.z e. X (zGx) = y)
isgrp2i.6	|- ((x e. X /\ y e. X) -> E.z e. X (xGz) = y)

Assertion

Ref	Expression
isgrp2i	|- G e. Grp

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

Proof of Theorem isgrp2i

Step	Hyp	Ref	Expression
1		isgrp2i.3	. . 3 |- G:(X X. X)-->X
2		isgrp2i.4	. . . 4 |- ((x e. X /\ y e. X /\ z e. X) -> ((xGy)Gz) = (xG(yGz)))
3	2	rgen3 1722	. . 3 |- A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz))
4		isgrp2i.2	. . . . 5 |- X =/= (/)
5		ne0 2285	. . . . 5 |- (X =/= (/) <-> E.w w e. X)
6	4, 5	mpbi 189	. . . 4 |- E.w w e. X
7		eleq1 1532	. . . . . . . . . . 11 |- (x = w -> (x e. X <-> w e. X))
8	7	anbi1d 616	. . . . . . . . . 10 |- (x = w -> ((x e. X /\ w e. X) <-> (w e. X /\ w e. X)))
9		opreq2 3964	. . . . . . . . . . . 12 |- (x = w -> (zGx) = (zGw))
10	9	eqeq1d 1481	. . . . . . . . . . 11 |- (x = w -> ((zGx) = w <-> (zGw) = w))
11	10	rexbidv 1662	. . . . . . . . . 10 |- (x = w -> (E.z e. X (zGx) = w <-> E.z e. X (zGw) = w))
12	8, 11	imbi12d 625	. . . . . . . . 9 |- (x = w -> (((x e. X /\ w e. X) -> E.z e. X (zGx) = w) <-> ((w e. X /\ w e. X) -> E.z e. X (zGw) = w)))
13		eleq1 1532	. . . . . . . . . . . 12 |- (y = w -> (y e. X <-> w e. X))
14	13	anbi2d 615	. . . . . . . . . . 11 |- (y = w -> ((x e. X /\ y e. X) <-> (x e. X /\ w e. X)))
15		eqeq2 1482	. . . . . . . . . . . 12 |- (y = w -> ((zGx) = y <-> (zGx) = w))
16	15	rexbidv 1662	. . . . . . . . . . 11 |- (y = w -> (E.z e. X (zGx) = y <-> E.z e. X (zGx) = w))
17	14, 16	imbi12d 625	. . . . . . . . . 10 |- (y = w -> (((x e. X /\ y e. X) -> E.z e. X (zGx) = y) <-> ((x e. X /\ w e. X) -> E.z e. X (zGx) = w)))
18		isgrp2i.5	. . . . . . . . . 10 |- ((x e. X /\ y e. X) -> E.z e. X (zGx) = y)
19	17, 18	chvarv 1326	. . . . . . . . 9 |- ((x e. X /\ w e. X) -> E.z e. X (zGx) = w)
20	12, 19	chvarv 1326	. . . . . . . 8 |- ((w e. X /\ w e. X) -> E.z e. X (zGw) = w)
21	20	anidms 434	. . . . . . 7 |- (w e. X -> E.z e. X (zGw) = w)
22		opreq1 3963	. . . . . . . . 9 |- (z = u -> (zGw) = (uGw))
23	22	eqeq1d 1481	. . . . . . . 8 |- (z = u -> ((zGw) = w <-> (uGw) = w))
24	23	cbvrexv 1798	. . . . . . 7 |- (E.z e. X (zGw) = w <-> E.u e. X (uGw) = w)
25	21, 24	sylib 198	. . . . . 6 |- (w e. X -> E.u e. X (uGw) = w)
26		opreq1 3963	. . . . . . . . . . . . . . . . . 18 |- (x = w -> (xGz) = (wGz))
27	26	eqeq1d 1481	. . . . . . . . . . . . . . . . 17 |- (x = w -> ((xGz) = y <-> (wGz) = y))
28	27	rexbidv 1662	. . . . . . . . . . . . . . . 16 |- (x = w -> (E.z e. X (xGz) = y <-> E.z e. X (wGz) = y))
29		eqeq2 1482	. . . . . . . . . . . . . . . . 17 |- (y = x -> ((wGz) = y <-> (wGz) = x))
30	29	rexbidv 1662	. . . . . . . . . . . . . . . 16 |- (y = x -> (E.z e. X (wGz) = y <-> E.z e. X (wGz) = x))
31		isgrp2i.6	. . . . . . . . . . . . . . . 16 |- ((x e. X /\ y e. X) -> E.z e. X (xGz) = y)
32	28, 30, 31	vtocl2ga 1850	. . . . . . . . . . . . . . 15 |- ((w e. X /\ x e. X) -> E.z e. X (wGz) = x)
33		opreq2 3964	. . . . . . . . . . . . . . . . 17 |- (z = v -> (wGz) = (wGv))
34	33	eqeq1d 1481	. . . . . . . . . . . . . . . 16 |- (z = v -> ((wGz) = x <-> (wGv) = x))
35	34	cbvrexv 1798	. . . . . . . . . . . . . . 15 |- (E.z e. X (wGz) = x <-> E.v e. X (wGv) = x)
36	32, 35	sylib 198	. . . . . . . . . . . . . 14 |- ((w e. X /\ x e. X) -> E.v e. X (wGv) = x)
37	36	adantlr 393	. . . . . . . . . . . . 13 |- (((w e. X /\ u e. X) /\ x e. X) -> E.v e. X (wGv) = x)
38	37	adantr 389	. . . . . . . . . . . 12 |- ((((w e. X /\ u e. X) /\ x e. X) /\ (uGw) = w) -> E.v e. X (wGv) = x)
39		eleq1 1532	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = u -> (x e. X <-> u e. X))
40	39	3anbi1d 896	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = u -> ((x e. X /\ w e. X /\ v e. X) <-> (u e. X /\ w e. X /\ v e. X)))
41		opreq1 3963	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = u -> (xGw) = (uGw))
42	41	opreq1d 3970	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = u -> ((xGw)Gv) = ((uGw)Gv))
43		opreq1 3963	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = u -> (xG(wGv)) = (uG(wGv)))
44	42, 43	eqeq12d 1487	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = u -> (((xGw)Gv) = (xG(wGv)) <-> ((uGw)Gv) = (uG(wGv))))
45	40, 44	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = u -> (((x e. X /\ w e. X /\ v e. X) -> ((xGw)Gv) = (xG(wGv))) <-> ((u e. X /\ w e. X /\ v e. X) -> ((uGw)Gv) = (uG(wGv)))))
46	13	3anbi2d 897	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = w -> ((x e. X /\ y e. X /\ v e. X) <-> (x e. X /\ w e. X /\ v e. X)))
47		opreq2 3964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = w -> (xGy) = (xGw))
48	47	opreq1d 3970	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = w -> ((xGy)Gv) = ((xGw)Gv))
49		opreq1 3963	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = w -> (yGv) = (wGv))
50	49	opreq2d 3971	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = w -> (xG(yGv)) = (xG(wGv)))
51	48, 50	eqeq12d 1487	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = w -> (((xGy)Gv) = (xG(yGv)) <-> ((xGw)Gv) = (xG(wGv))))
52	46, 51	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = w -> (((x e. X /\ y e. X /\ v e. X) -> ((xGy)Gv) = (xG(yGv))) <-> ((x e. X /\ w e. X /\ v e. X) -> ((xGw)Gv) = (xG(wGv)))))
53		eleq1 1532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = v -> (z e. X <-> v e. X))
54	53	3anbi3d 898	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = v -> ((x e. X /\ y e. X /\ z e. X) <-> (x e. X /\ y e. X /\ v e. X)))
55		opreq2 3964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = v -> ((xGy)Gz) = ((xGy)Gv))
56		opreq2 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z = v -> (yGz) = (yGv))
57	56	opreq2d 3971	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = v -> (xG(yGz)) = (xG(yGv)))
58	55, 57	eqeq12d 1487	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = v -> (((xGy)Gz) = (xG(yGz)) <-> ((xGy)Gv) = (xG(yGv))))
59	54, 58	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = v -> (((x e. X /\ y e. X /\ z e. X) -> ((xGy)Gz) = (xG(yGz))) <-> ((x e. X /\ y e. X /\ v e. X) -> ((xGy)Gv) = (xG(yGv)))))
60	59, 2	chvarv 1326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. X /\ y e. X /\ v e. X) -> ((xGy)Gv) = (xG(yGv)))
61	52, 60	chvarv 1326	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. X /\ w e. X /\ v e. X) -> ((xGw)Gv) = (xG(wGv)))
62	45, 61	chvarv 1326	. . . . . . . . . . . . . . . . . . . . 21 |- ((u e. X /\ w e. X /\ v e. X) -> ((uGw)Gv) = (uG(wGv)))
63	62	3com12 836	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. X /\ u e. X /\ v e. X) -> ((uGw)Gv) = (uG(wGv)))
64	63	3expa 832	. . . . . . . . . . . . . . . . . . 19 |- (((w e. X /\ u e. X) /\ v e. X) -> ((uGw)Gv) = (uG(wGv)