Theorem isringNEW 17142

Description: The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187.

Hypotheses

Ref	Expression
isring.0NEW	|- S = Struct(3, r, T. )
isring.1NEW	|- B = (base` R)
isring.2NEW	|- P = (+g` R)
isring.3NEW	|- T = (.r` R)

Assertion

Ref	Expression
isringNEW	|- (R e. RingNEW <-> (R e. S /\ (R e. AbelNEW /\ A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x))))

Distinct variable groups:   u,r,x,y,z,B   P,r,u,x,y,z   R,r   T,r,u,x,y,z

Proof of Theorem isringNEW

Step	Hyp	Ref	Expression
1		df-ringNEW 17094	. . 3 |- RingNEW = Struct(3, r, (r e. AbelNEW /\ E.bE.pE.t((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))))
2	1	eleq2i 1961	. 2 |- (R e. RingNEW <-> R e. Struct(3, r, (r e. AbelNEW /\ E.bE.pE.t((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)))))
3		isring.0NEW	. . 3 |- S = Struct(3, r, T. )
4		eleq1 1957	. . . 4 |- (r = R -> (r e. AbelNEW <-> R e. AbelNEW))
5		fveq2 4681	. . . . . . . . . 10 |- (r = R -> (base` r) = (base` R))
6		isring.1NEW	. . . . . . . . . 10 |- B = (base` R)
7	5, 6	syl6eqr 1946	. . . . . . . . 9 |- (r = R -> (base` r) = B)
8	7	eqeq2d 1895	. . . . . . . 8 |- (r = R -> (b = (base` r) <-> b = B))
9		fveq2 4681	. . . . . . . . . 10 |- (r = R -> (+g` r) = (+g` R))
10		isring.2NEW	. . . . . . . . . 10 |- P = (+g` R)
11	9, 10	syl6eqr 1946	. . . . . . . . 9 |- (r = R -> (+g` r) = P)
12	11	eqeq2d 1895	. . . . . . . 8 |- (r = R -> (p = (+g` r) <-> p = P))
13		fveq2 4681	. . . . . . . . . 10 |- (r = R -> (.r` r) = (.r` R))
14		isring.3NEW	. . . . . . . . . 10 |- T = (.r` R)
15	13, 14	syl6eqr 1946	. . . . . . . . 9 |- (r = R -> (.r` r) = T)
16	15	eqeq2d 1895	. . . . . . . 8 |- (r = R -> (t = (.r` r) <-> t = T))
17	8, 12, 16	3anbi123d 1168	. . . . . . 7 |- (r = R -> ((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) <-> (b = B /\ p = P /\ t = T)))
18	17	3anbi1d 1172	. . . . . 6 |- (r = R -> (((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)) <-> ((b = B /\ p = P /\ t = T) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))))
19		3anass 862	. . . . . 6 |- (((b = B /\ p = P /\ t = T) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)) <-> ((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))))
20	18, 19	syl6bb 595	. . . . 5 |- (r = R -> (((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)) <-> ((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)))))
21	20	3exbidv 1660	. . . 4 |- (r = R -> (E.bE.pE.t((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)) <-> E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)))))
22	4, 21	anbi12d 690	. . 3 |- (r = R -> ((r e. AbelNEW /\ E.bE.pE.t((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))) <-> (R e. AbelNEW /\ E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))))))
23	3, 22	elstr2 16718	. 2 |- (R e. Struct(3, r, (r e. AbelNEW /\ E.bE.pE.t((b = (base` r) /\ p = (+g` r) /\ t = (.r` r)) /\ A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)))) <-> (R e. S /\ (R e. AbelNEW /\ E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))))))
24		fvex 4689	. . . . . . 7 |- (base` R) e. _V
25	6, 24	eqeltri 1967	. . . . . 6 |- B e. _V
26		fvex 4689	. . . . . . 7 |- (+g` R) e. _V
27	10, 26	eqeltri 1967	. . . . . 6 |- P e. _V
28		fvex 4689	. . . . . . 7 |- (.r` R) e. _V
29	14, 28	eqeltri 1967	. . . . . 6 |- T e. _V
30		eleq2 1958	. . . . . . . . . . 11 |- (b = B -> ((xty) e. b <-> (xty) e. B))
31	30	anbi1d 679	. . . . . . . . . 10 |- (b = B -> (((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz))))))
32	31	raleqbi1dv 2271	. . . . . . . . 9 |- (b = B -> (A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz))))))
33	32	raleqbi1dv 2271	. . . . . . . 8 |- (b = B -> (A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz))))))
34	33	raleqbi1dv 2271	. . . . . . 7 |- (b = B -> (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz))))))
35		raleq 2266	. . . . . . . 8 |- (b = B -> (A.x e. b ((utx) = x /\ (xtu) = x) <-> A.x e. B ((utx) = x /\ (xtu) = x)))
36	35	rexeqbi1dv 2272	. . . . . . 7 |- (b = B -> (E.u e. b A.x e. b ((utx) = x /\ (xtu) = x) <-> E.u e. B A.x e. B ((utx) = x /\ (xtu) = x)))
37	34, 36	anbi12d 690	. . . . . 6 |- (b = B -> ((A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)) <-> (A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. B A.x e. B ((utx) = x /\ (xtu) = x))))
38		opreq 4888	. . . . . . . . . . . . 13 |- (p = P -> (ypz) = (yPz))
39	38	opreq2d 4898	. . . . . . . . . . . 12 |- (p = P -> (xt(ypz)) = (xt(yPz)))
40		opreq 4888	. . . . . . . . . . . 12 |- (p = P -> ((xty)p(xtz)) = ((xty)P(xtz)))
41	39, 40	eqeq12d 1899	. . . . . . . . . . 11 |- (p = P -> ((xt(ypz)) = ((xty)p(xtz)) <-> (xt(yPz)) = ((xty)P(xtz))))
42		opreq 4888	. . . . . . . . . . . . 13 |- (p = P -> (xpy) = (xPy))
43	42	opreq1d 4897	. . . . . . . . . . . 12 |- (p = P -> ((xpy)tz) = ((xPy)tz))
44		opreq 4888	. . . . . . . . . . . 12 |- (p = P -> ((xtz)p(ytz)) = ((xtz)P(ytz)))
45	43, 44	eqeq12d 1899	. . . . . . . . . . 11 |- (p = P -> (((xpy)tz) = ((xtz)p(ytz)) <-> ((xPy)tz) = ((xtz)P(ytz))))
46	41, 45	3anbi23d 1171	. . . . . . . . . 10 |- (p = P -> ((((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz))) <-> (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz)))))
47	46	anbi2d 678	. . . . . . . . 9 |- (p = P -> (((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz))))))
48	47	ralbidv 2123	. . . . . . . 8 |- (p = P -> (A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz))))))
49	48	2ralbidv 2140	. . . . . . 7 |- (p = P -> (A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) <-> A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz))))))
50	49	anbi1d 679	. . . . . 6 |- (p = P -> ((A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. B A.x e. B ((utx) = x /\ (xtu) = x)) <-> (A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz)))) /\ E.u e. B A.x e. B ((utx) = x /\ (xtu) = x))))
51		opreq 4888	. . . . . . . . . . 11 |- (t = T -> (xty) = (xTy))
52	51	eleq1d 1963	. . . . . . . . . 10 |- (t = T -> ((xty) e. B <-> (xTy) e. B))
53		opreq 4888	. . . . . . . . . . . . 13 |- (t = T -> ((xty)tz) = ((xty)Tz))
54	51	opreq1d 4897	. . . . . . . . . . . . 13 |- (t = T -> ((xty)Tz) = ((xTy)Tz))
55	53, 54	eqtrd 1925	. . . . . . . . . . . 12 |- (t = T -> ((xty)tz) = ((xTy)Tz))
56		opreq 4888	. . . . . . . . . . . . 13 |- (t = T -> (xt(ytz)) = (xT(ytz)))
57		opreq 4888	. . . . . . . . . . . . . 14 |- (t = T -> (ytz) = (yTz))
58	57	opreq2d 4898	. . . . . . . . . . . . 13 |- (t = T -> (xT(ytz)) = (xT(yTz)))
59	56, 58	eqtrd 1925	. . . . . . . . . . . 12 |- (t = T -> (xt(ytz)) = (xT(yTz)))
60	55, 59	eqeq12d 1899	. . . . . . . . . . 11 |- (t = T -> (((xty)tz) = (xt(ytz)) <-> ((xTy)Tz) = (xT(yTz))))
61		opreq 4888	. . . . . . . . . . . 12 |- (t = T -> (xt(yPz)) = (xT(yPz)))
62		opreq 4888	. . . . . . . . . . . . 13 |- (t = T -> (xtz) = (xTz))
63	51, 62	opreq12d 4900	. . . . . . . . . . . 12 |- (t = T -> ((xty)P(xtz)) = ((xTy)P(xTz)))
64	61, 63	eqeq12d 1899	. . . . . . . . . . 11 |- (t = T -> ((xt(yPz)) = ((xty)P(xtz)) <-> (xT(yPz)) = ((xTy)P(xTz))))
65		opreq 4888	. . . . . . . . . . . 12 |- (t = T -> ((xPy)tz) = ((xPy)Tz))
66	62, 57	opreq12d 4900	. . . . . . . . . . . 12 |- (t = T -> ((xtz)P(ytz)) = ((xTz)P(yTz)))
67	65, 66	eqeq12d 1899	. . . . . . . . . . 11 |- (t = T -> (((xPy)tz) = ((xtz)P(ytz)) <-> ((xPy)Tz) = ((xTz)P(yTz))))
68	60, 64, 67	3anbi123d 1168	. . . . . . . . . 10 |- (t = T -> ((((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz))) <-> (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))))
69	52, 68	anbi12d 690	. . . . . . . . 9 |- (t = T -> (((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz)))) <-> ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz))))))
70	69	ralbidv 2123	. . . . . . . 8 |- (t = T -> (A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz)))) <-> A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz))))))
71	70	2ralbidv 2140	. . . . . . 7 |- (t = T -> (A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz)))) <-> A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz))))))
72		opreq 4888	. . . . . . . . . 10 |- (t = T -> (utx) = (uTx))
73	72	eqeq1d 1892	. . . . . . . . 9 |- (t = T -> ((utx) = x <-> (uTx) = x))
74		opreq 4888	. . . . . . . . . 10 |- (t = T -> (xtu) = (xTu))
75	74	eqeq1d 1892	. . . . . . . . 9 |- (t = T -> ((xtu) = x <-> (xTu) = x))
76	73, 75	anbi12d 690	. . . . . . . 8 |- (t = T -> (((utx) = x /\ (xtu) = x) <-> ((uTx) = x /\ (xTu) = x)))
77	76	rexralbidv 2142	. . . . . . 7 |- (t = T -> (E.u e. B A.x e. B ((utx) = x /\ (xtu) = x) <-> E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x)))
78	71, 77	anbi12d 690	. . . . . 6 |- (t = T -> ((A.x e. B A.y e. B A.z e. B ((xty) e. B /\ (((xty)tz) = (xt(ytz)) /\ (xt(yPz)) = ((xty)P(xtz)) /\ ((xPy)tz) = ((xtz)P(ytz)))) /\ E.u e. B A.x e. B ((utx) = x /\ (xtu) = x)) <-> (A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x))))
79	25, 27, 29, 37, 50, 78	ceqsex3v 2330	. . . . 5 |- (E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))) <-> (A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x)))
80	79	anbi2i 538	. . . 4 |- ((R e. AbelNEW /\ E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)))) <-> (R e. AbelNEW /\ (A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x))))
81		3anass 862	. . . 4 |- ((R e. AbelNEW /\ A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x)) <-> (R e. AbelNEW /\ (A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x))))
82	80, 81	bitr4i 193	. . 3 |- ((R e. AbelNEW /\ E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x)))) <-> (R e. AbelNEW /\ A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x)))
83	82	anbi2i 538	. 2 |- ((R e. S /\ (R e. AbelNEW /\ E.bE.pE.t((b = B /\ p = P /\ t = T) /\ (A.x e. b A.y e. b A.z e. b ((xty) e. b /\ (((xty)tz) = (xt(ytz)) /\ (xt(ypz)) = ((xty)p(xtz)) /\ ((xpy)tz) = ((xtz)p(ytz)))) /\ E.u e. b A.x e. b ((utx) = x /\ (xtu) = x))))) <-> (R e. S /\ (R e. AbelNEW /\ A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x))))
84	2, 23, 83	3bitri 194	1 |- (R e. RingNEW <-> (R e. S /\ (R e. AbelNEW /\ A.x e. B A.y e. B A.z e. B ((xTy) e. B /\ (((xTy)Tz) = (xT(yTz)) /\ (xT(yPz)) = ((xTy)P(xTz)) /\ ((xPy)Tz) = ((xTz)P(yTz)))) /\ E.u e. B A.x e. B ((uTx) = x /\ (xTu) = x))))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858   T. wtru 1260   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  _Vcvv 2292  ` cfv 3998  (class class class)co 4884  3c3 7146  Structcstru 16707  basecbs 16758  +_gcplusg 17080  AbelNEWcabel 17084  ._rcmulr 17085  RingNEWcrg 17086

This theorem is referenced by:  ringiNEW 17143  ringideuNEW 17146  ringablNEW 17151

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-tru 1262  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-opr 4886  df-struct 16708  df-ringNEW 17094

Copyright terms: Public domain