Theorem issrng 17176

Description: The predicate "is a star ring."

Hypotheses

Ref	Expression
issrng.1	|- S = Struct(4, f, T. )
issrng.k	|- K = (base` R)
issrng.p	|- P = (+g` R)
issrng.t	|- T = (.r` R)
issrng.i	|- I = (*v` R)

Assertion

Ref	Expression
issrng	|- (R e. Ring* <-> (R e. S /\ R e. RingNEW /\ A.q e. K A.r e. K ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q))))

Distinct variable groups:   f,q,r,I   f,K,q,r   P,f,q,r   R,f,q,r   T,f,q,r

Proof of Theorem issrng

Step	Hyp	Ref	Expression
1		df-starrng 17175	. . 3 |- Ring* = Struct(4, f, (f e. RingNEW /\ E.kE.pE.tE.i((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f)) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))))
2	1	eleq2i 1961	. 2 |- (R e. Ring* <-> R e. Struct(4, f, (f e. RingNEW /\ E.kE.pE.tE.i((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f)) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))))
3		issrng.1	. . 3 |- S = Struct(4, f, T. )
4		eleq1 1957	. . . 4 |- (f = R -> (f e. RingNEW <-> R e. RingNEW))
5		fveq2 4681	. . . . . . . . 9 |- (f = R -> (base` f) = (base` R))
6		issrng.k	. . . . . . . . 9 |- K = (base` R)
7	5, 6	syl6eqr 1946	. . . . . . . 8 |- (f = R -> (base` f) = K)
8	7	eqeq2d 1895	. . . . . . 7 |- (f = R -> (k = (base` f) <-> k = K))
9		fveq2 4681	. . . . . . . . 9 |- (f = R -> (+g` f) = (+g` R))
10		issrng.p	. . . . . . . . 9 |- P = (+g` R)
11	9, 10	syl6eqr 1946	. . . . . . . 8 |- (f = R -> (+g` f) = P)
12	11	eqeq2d 1895	. . . . . . 7 |- (f = R -> (p = (+g` f) <-> p = P))
13	8, 12	anbi12d 690	. . . . . 6 |- (f = R -> ((k = (base` f) /\ p = (+g` f)) <-> (k = K /\ p = P)))
14		fveq2 4681	. . . . . . . . 9 |- (f = R -> (.r` f) = (.r` R))
15		issrng.t	. . . . . . . . 9 |- T = (.r` R)
16	14, 15	syl6eqr 1946	. . . . . . . 8 |- (f = R -> (.r` f) = T)
17	16	eqeq2d 1895	. . . . . . 7 |- (f = R -> (t = (.r` f) <-> t = T))
18		fveq2 4681	. . . . . . . . 9 |- (f = R -> (*v` f) = (*v` R))
19		issrng.i	. . . . . . . . 9 |- I = (*v` R)
20	18, 19	syl6eqr 1946	. . . . . . . 8 |- (f = R -> (*v` f) = I)
21	20	eqeq2d 1895	. . . . . . 7 |- (f = R -> (i = (*v` f) <-> i = I))
22	17, 21	anbi12d 690	. . . . . 6 |- (f = R -> ((t = (.r` f) /\ i = (*v` f)) <-> (t = T /\ i = I)))
23	13, 22	3anbi12d 1169	. . . . 5 |- (f = R -> (((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f)) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))) <-> ((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))))
24	23	4exbidv 1661	. . . 4 |- (f = R -> (E.kE.pE.tE.i((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f)) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))) <-> E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))))
25	4, 24	anbi12d 690	. . 3 |- (f = R -> ((f e. RingNEW /\ E.kE.pE.tE.i((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f)) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))) <-> (R e. RingNEW /\ E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))))
26	3, 25	elstr2 16718	. 2 |- (R e. Struct(4, f, (f e. RingNEW /\ E.kE.pE.tE.i((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f)) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))) <-> (R e. S /\ (R e. RingNEW /\ E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))))
27		3anass 862	. . 3 |- ((R e. S /\ R e. RingNEW /\ E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))) <-> (R e. S /\ (R e. RingNEW /\ E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))))
28		fvex 4689	. . . . . 6 |- (base` R) e. _V
29	6, 28	eqeltri 1967	. . . . 5 |- K e. _V
30		fvex 4689	. . . . . 6 |- (+g` R) e. _V
31	10, 30	eqeltri 1967	. . . . 5 |- P e. _V
32		fvex 4689	. . . . . 6 |- (.r` R) e. _V
33	15, 32	eqeltri 1967	. . . . 5 |- T e. _V
34		fvex 4689	. . . . . 6 |- (*v` R) e. _V
35	19, 34	eqeltri 1967	. . . . 5 |- I e. _V
36		eleq2 1958	. . . . . . . 8 |- (k = K -> ((i` q) e. k <-> (i` q) e. K))
37	36	anbi1d 679	. . . . . . 7 |- (k = K -> (((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> ((i` q) e. K /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))
38	37	raleqbi1dv 2271	. . . . . 6 |- (k = K -> (A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> A.r e. K ((i` q) e. K /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))
39	38	raleqbi1dv 2271	. . . . 5 |- (k = K -> (A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> A.q e. K A.r e. K ((i` q) e. K /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))
40		opreq 4888	. . . . . . . . . 10 |- (p = P -> (qpr) = (qPr))
41	40	fveq2d 4685	. . . . . . . . 9 |- (p = P -> (i` (qpr)) = (i` (qPr)))
42		opreq 4888	. . . . . . . . 9 |- (p = P -> ((i` q)p(i` r)) = ((i` q)P(i` r)))
43	41, 42	eqeq12d 1899	. . . . . . . 8 |- (p = P -> ((i` (qpr)) = ((i` q)p(i` r)) <-> (i` (qPr)) = ((i` q)P(i` r))))
44	43	3anbi1d 1172	. . . . . . 7 |- (p = P -> (((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q) <-> ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))
45	44	anbi2d 678	. . . . . 6 |- (p = P -> (((i` q) e. K /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> ((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))
46	45	2ralbidv 2140	. . . . 5 |- (p = P -> (A.q e. K A.r e. K ((i` q) e. K /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> A.q e. K A.r e. K ((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))
47		opreq 4888	. . . . . . . . . 10 |- (t = T -> (qtr) = (qTr))
48	47	fveq2d 4685	. . . . . . . . 9 |- (t = T -> (i` (qtr)) = (i` (qTr)))
49		opreq 4888	. . . . . . . . 9 |- (t = T -> ((i` r)t(i` q)) = ((i` r)T(i` q)))
50	48, 49	eqeq12d 1899	. . . . . . . 8 |- (t = T -> ((i` (qtr)) = ((i` r)t(i` q)) <-> (i` (qTr)) = ((i` r)T(i` q))))
51	50	3anbi2d 1173	. . . . . . 7 |- (t = T -> (((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q) <-> ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qTr)) = ((i` r)T(i` q)) /\ (i` (i` q)) = q)))
52	51	anbi2d 678	. . . . . 6 |- (t = T -> (((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> ((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qTr)) = ((i` r)T(i` q)) /\ (i` (i` q)) = q))))
53	52	2ralbidv 2140	. . . . 5 |- (t = T -> (A.q e. K A.r e. K ((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)) <-> A.q e. K A.r e. K ((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qTr)) = ((i` r)T(i` q)) /\ (i` (i` q)) = q))))
54		fveq1 4680	. . . . . . . 8 |- (i = I -> (i` q) = (I` q))
55	54	eleq1d 1963	. . . . . . 7 |- (i = I -> ((i` q) e. K <-> (I` q) e. K))
56		fveq1 4680	. . . . . . . . 9 |- (i = I -> (i` (qPr)) = (I` (qPr)))
57		fveq1 4680	. . . . . . . . . 10 |- (i = I -> (i` r) = (I` r))
58	54, 57	opreq12d 4900	. . . . . . . . 9 |- (i = I -> ((i` q)P(i` r)) = ((I` q)P(I` r)))
59	56, 58	eqeq12d 1899	. . . . . . . 8 |- (i = I -> ((i` (qPr)) = ((i` q)P(i` r)) <-> (I` (qPr)) = ((I` q)P(I` r))))
60		fveq1 4680	. . . . . . . . 9 |- (i = I -> (i` (qTr)) = (I` (qTr)))
61	57, 54	opreq12d 4900	. . . . . . . . 9 |- (i = I -> ((i` r)T(i` q)) = ((I` r)T(I` q)))
62	60, 61	eqeq12d 1899	. . . . . . . 8 |- (i = I -> ((i` (qTr)) = ((i` r)T(i` q)) <-> (I` (qTr)) = ((I` r)T(I` q))))
63		id 73	. . . . . . . . . 10 |- (i = I -> i = I)
64	63, 54	fveq12d 10152	. . . . . . . . 9 |- (i = I -> (i` (i` q)) = (I` (I` q)))
65	64	eqeq1d 1892	. . . . . . . 8 |- (i = I -> ((i` (i` q)) = q <-> (I` (I` q)) = q))
66	59, 62, 65	3anbi123d 1168	. . . . . . 7 |- (i = I -> (((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qTr)) = ((i` r)T(i` q)) /\ (i` (i` q)) = q) <-> ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q)))
67	55, 66	anbi12d 690	. . . . . 6 |- (i = I -> (((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qTr)) = ((i` r)T(i` q)) /\ (i` (i` q)) = q)) <-> ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q))))
68	67	2ralbidv 2140	. . . . 5 |- (i = I -> (A.q e. K A.r e. K ((i` q) e. K /\ ((i` (qPr)) = ((i` q)P(i` r)) /\ (i` (qTr)) = ((i` r)T(i` q)) /\ (i` (i` q)) = q)) <-> A.q e. K A.r e. K ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q))))
69	29, 31, 33, 35, 39, 46, 53, 68	ceqsex4v 2331	. . . 4 |- (E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))) <-> A.q e. K A.r e. K ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q)))
70	69	3anbi3i 1060	. . 3 |- ((R e. S /\ R e. RingNEW /\ E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q)))) <-> (R e. S /\ R e. RingNEW /\ A.q e. K A.r e. K ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q))))
71	27, 70	bitr3i 192	. 2 |- ((R e. S /\ (R e. RingNEW /\ E.kE.pE.tE.i((k = K /\ p = P) /\ (t = T /\ i = I) /\ A.q e. k A.r e. k ((i` q) e. k /\ ((i` (qpr)) = ((i` q)p(i` r)) /\ (i` (qtr)) = ((i` r)t(i` q)) /\ (i` (i` q)) = q))))) <-> (R e. S /\ R e. RingNEW /\ A.q e. K A.r e. K ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q))))
72	2, 26, 71	3bitri 194	1 |- (R e. Ring* <-> (R e. S /\ R e. RingNEW /\ A.q e. K A.r e. K ((I` q) e. K /\ ((I` (qPr)) = ((I` q)P(I` r)) /\ (I` (qTr)) = ((I` r)T(I` q)) /\ (I` (I` q)) = q))))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858   T. wtru 1260   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292  ` cfv 3998  (class class class)co 4884  4c4 7147  Structcstru 16707  basecbs 16758  +_gcplusg 17080  ._rcmulr 17085  RingNEWcrg 17086  *_vcstv 17172  Ring*csr 17173

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-starrng 17175

Copyright terms: Public domain