Theorem ringi 8142

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.)

Hypotheses

Ref	Expression
ringi.1	|- G = (1st` R)
ringi.2	|- H = (2nd` R)
ringi.3	|- X = ran G

Assertion

Ref	Expression
ringi	|- (R 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,G,y,z   x,H,y,z   x,X,y,z

Proof of Theorem ringi

Step	Hyp	Ref	Expression
1		df-ring 8140	. . 3 |- 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)))}
2	1	eleq2i 1538	. 2 |- (R e. Ring <-> R e. {<.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		ringi.1	. . . . 5 |- G = (1st` R)
4	3	eqeq2i 1485	. . . 4 |- (g = G <-> g = (1st` R))
5		eleq1 1534	. . . . . 6 |- (g = G -> (g e. Abel <-> G e. Abel))
6		rneq 3339	. . . . . . . 8 |- (g = G -> ran g = ran G)
7		ringi.3	. . . . . . . 8 |- X = ran G
8	6, 7	syl6eqr 1525	. . . . . . 7 |- (g = G -> ran g = X)
9		xpeq1 3200	. . . . . . . . . 10 |- (ran g = X -> (ran g X. ran g) = (X X. ran g))
10		xpeq2 3201	. . . . . . . . . 10 |- (ran g = X -> (X X. ran g) = (X X. X))
11	9, 10	eqtrd 1507	. . . . . . . . 9 |- (ran g = X -> (ran g X. ran g) = (X X. X))
12		feq2 3621	. . . . . . . . 9 |- ((ran g X. ran g) = (X X. X) -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->ran g))
13	11, 12	syl 10	. . . . . . . 8 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->ran g))
14		feq3 3622	. . . . . . . 8 |- (ran g = X -> (h:(X X. X)-->ran g <-> h:(X X. X)-->X))
15	13, 14	bitrd 528	. . . . . . 7 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
16	8, 15	syl 10	. . . . . 6 |- (g = G -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
17	5, 16	anbi12d 628	. . . . 5 |- (g = G -> ((g e. Abel /\ h:(ran g X. ran g)-->ran g) <-> (G e. Abel /\ h:(X X. X)-->X)))
18		raleq1 1786	. . . . . . . . . 10 |- (ran g = X -> (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)))))
19	18	raleqd 1791	. . . . . . . . 9 |- (ran g = X -> (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)))))
20	19	raleqd 1791	. . . . . . . 8 |- (ran g = X -> (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) = ((xhz)g(yhz)))))
21	8, 20	syl 10	. . . . . . 7 |- (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) = ((xhz)g(yhz)))))
22		opreq 3967	. . . . . . . . . . . 12 |- (g = G -> (ygz) = (yGz))
23	22	opreq2d 3976	. . . . . . . . . . 11 |- (g = G -> (xh(ygz)) = (xh(yGz)))
24		opreq 3967	. . . . . . . . . . 11 |- (g = G -> ((xhy)g(xhz)) = ((xhy)G(xhz)))
25	23, 24	eqeq12d 1489	. . . . . . . . . 10 |- (g = G -> ((xh(ygz)) = ((xhy)g(xhz)) <-> (xh(yGz)) = ((xhy)G(xhz))))
26		opreq 3967	. . . . . . . . . . . 12 |- (g = G -> (xgy) = (xGy))
27	26	opreq1d 3975	. . . . . . . . . . 11 |- (g = G -> ((xgy)hz) = ((xGy)hz))
28		opreq 3967	. . . . . . . . . . 11 |- (g = G -> ((xhz)g(yhz)) = ((xhz)G(yhz)))
29	27, 28	eqeq12d 1489	. . . . . . . . . 10 |- (g = G -> (((xgy)hz) = ((xhz)g(yhz)) <-> ((xGy)hz) = ((xhz)G(yhz))))
30	25, 29	3anbi23d 896	. . . . . . . . 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)))))
31	30	ralbidv 1663	. . . . . . . 8 |- (g = G -> (A.z e. X (((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)))))
32	31	2ralbidv 1680	. . . . . . 7 |- (g = G -> (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))) <-> A.x e. X A.y e. X A.z e. X (((xhy)hz) = (xh(yhz)) /\ (xh