Theorem isring 8137

Description: The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeffrey Hankins, 21-Nov-2006.)

Hypothesis

Ref	Expression
isring.1	|- X = ran G

Assertion

Ref	Expression
isring	|- (H e. A -> (<.G, H>. e. Ring <-> ((G e. Abel /\ H:(X X. X)-->X) /\ (A.x e. X A.y e. X A.z e. X (((xHy)Hz) = (xH(yHz)) /\ (xH(yGz)) = ((xHy)G(xHz)) /\ ((xGy)Hz) = ((xHz)G(yHz))) /\ E.x e. X A.y e. X ((yHx) = y /\ (xHy) = y)))))

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

Proof of Theorem isring

Step	Hyp	Ref	Expression
1		df-br 2625	. . . . 5 |- (GRingH <-> <.G, H>. e. Ring)
2		relopab 3272	. . . . . . 7 |- Rel {<.g, h>. | ((g e. Abel /\ h:(ran g X. ran g)-->ran g) /\ (A.x e. ran gA.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) /\ E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y)))}
3		df-ring 8136	. . . . . . . 8 |- Ring = {<.g, h>. | ((g e. Abel /\ h:(ran g X. ran g)-->ran g) /\ (A.x e. ran gA.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) /\ E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y)))}
4	3	releqi 3250	. . . . . . 7 |- (Rel Ring <-> Rel {<.g, h>. | ((g e. Abel /\ h:(ran g X. ran g)-->ran g) /\ (A.x e. ran gA.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) /\ E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y)))})
5	2, 4	mpbir 190	. . . . . 6 |- Rel Ring
6	5	brrelexi 3214	. . . . 5 |- (GRingH -> G e. V)
7	1, 6	sylbir 201	. . . 4 |- (<.G, H>. e. Ring -> G e. V)
8	7	anim1i 334	. . 3 |- ((<.G, H>. e. Ring /\ H e. A) -> (G e. V /\ H e. A))
9	8	ancoms 438	. 2 |- ((H e. A /\ <.G, H>. e. Ring) -> (G e. V /\ H e. A))
10		elisset 1820	. . . . . 6 |- (G e. Abel -> G e. V)
11	10	anim1i 334	. . . . 5 |- ((G e. Abel /\ H e. A) -> (G e. V /\ H e. A))
12	11	ancoms 438	. . . 4 |- ((H e. A /\ G e. Abel) -> (G e. V /\ H e. A))
13	12	adantrr 397	. . 3 |- ((H e. A /\ (G e. Abel /\ H:(X X. X)-->X)) -> (G e. V /\ H e. A))
14	13	adantrr 397	. 2 |- ((H e. A /\ ((G e. Abel /\ H:(X X. X)-->X) /\ (A.x e. X A.y e. X A.z e. X (((xHy)Hz) = (xH(yHz)) /\ (xH(yGz)) = ((xHy)G(xHz)) /\ ((xGy)Hz) = ((xHz)G(yHz))) /\ E.x e. X A.y e. X ((yHx) = y /\ (xHy) = y)))) -> (G e. V /\ H e. A))
15		eleq1 1537	. . . . . 6 |- (g = G -> (g e. Abel <-> G e. Abel))
16		rneq 3345	. . . . . . . 8 |- (g = G -> ran g = ran G)
17		isring.1	. . . . . . . 8 |- X = ran G
18	16, 17	syl6eqr 1528	. . . . . . 7 |- (g = G -> ran g = X)
19		xpeq1 3206	. . . . . . . . . 10 |- (ran g = X -> (ran g X. ran g) = (X X. ran g))
20		xpeq2 3207	. . . . . . . . . 10 |- (ran g = X -> (X X. ran g) = (X X. X))
21	19, 20	eqtrd 1510	. . . . . . . . 9 |- (ran g = X -> (ran g X. ran g) = (X X. X))
22		feq2 3627	. . . . . . . . 9 |- ((ran g X. ran g) = (X X. X) -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->ran g))
23	21, 22	syl 10	. . . . . . . 8 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->ran g))
24		feq3 3628	. . . . . . . 8 |- (ran g = X -> (h:(X X. X)-->ran g <-> h:(X X. X)-->X))
25	23, 24	bitrd 530	. . . . . . 7 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
26	18, 25	syl 10	. . . . . 6 |- (g = G -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
27	15, 26	anbi12d 630	. . . . 5 |- (g = G -> ((g e. Abel /\ h:(ran g X. ran g)-->ran g) <-> (G e. Abel /\ h:(X X. X)-->X)))
28		opreq 3973	. . . . . . . . . . . 12 |- (g = G -> (ygz) = (yGz))
29	28	opreq2d 3982	. . . . . . . . . . 11 |- (g = G -> (xh(ygz)) = (xh(yGz)))
30		opreq 3973	. . . . . . . . . . 11 |- (g = G -> ((xhy)g(xhz)) = ((xhy)G(xhz)))
31	29, 30	eqeq12d 1492	. . . . . . . . . 10 |- (g = G -> ((xh(ygz)) = ((xhy)g(xhz)) <-> (xh(yGz)) = ((xhy)G(xhz))))
32		opreq 3973	. . . . . . . . . . . 12 |- (g = G -> (xgy) = (xGy))
33	32	opreq1d 3981	. . . . . . . . . . 11 |- (g = G -> ((xgy)hz) = ((xGy)hz))
34		opreq 3973	. . . . . . . . . . 11 |- (g = G -> ((xhz)g(yhz)) = ((xhz)G(yhz)))
35	33, 34	eqeq12d 1492	. . . . . . . . . 10 |- (g = G -> (((xgy)hz) = ((xhz)g(yhz)) <-> ((xGy)hz) = ((xhz)G(yhz))))
36	31, 35	3anbi23d 898	. . . . . . . . 9 |- (g = G -> ((((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) <-> (((xhy)hz) = (xh(yhz)) /\ (xh(yGz)) = ((xhy)G(xhz)) /\ ((xGy)hz) = ((xhz)G(yhz)))))
37	18, 36	raleq12d 1797	. . . . . . . 8 |- (g = G -> (A.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) <-> A.z e. X (((xhy)hz) = (xh(yhz)) /\ (xh(yGz)) = ((xhy)G(xhz)) /\ ((xGy)hz) = ((xhz)G(yhz)))))
38	18, 37	raleq12d 1797	. . . . . . 7 |- (g = G -> (A.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) <-> A.y e. X A.z e. X (((xhy)hz) = (xh(yhz)) /\ (xh(yGz)) = ((xhy)G(xhz)) /\ ((xGy)hz) = ((xhz)G(yhz)))))
39	18, 38	raleq12d 1797	. . . . . 6 |- (g = G -> (A.x e. ran gA.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) <-> A.x e. X A.y e. X A.z e. X (((xhy)hz) = (xh(yhz)) /\ (xh(yGz)) = ((xhy)G(xhz)) /\ ((xGy)hz) = (