Theorem ringi 9466

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 9464	. . 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 1961	. 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 1894	. . . 4 |- (g = G <-> g = (1st` R))
5		eleq1 1957	. . . . . 6 |- (g = G -> (g e. Abel <-> G e. Abel))
6		rneq 4186	. . . . . . . 8 |- (g = G -> ran g = ran G)
7		ringi.3	. . . . . . . 8 |- X = ran G
8	6, 7	syl6eqr 1946	. . . . . . 7 |- (g = G -> ran g = X)
9		xpeq1 4016	. . . . . . . . . 10 |- (ran g = X -> (ran g X. ran g) = (X X. ran g))
10		xpeq2 4017	. . . . . . . . . 10 |- (ran g = X -> (X X. ran g) = (X X. X))
11	9, 10	eqtrd 1925	. . . . . . . . 9 |- (ran g = X -> (ran g X. ran g) = (X X. X))
12	11	feq2d 4557	. . . . . . . 8 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->ran g))
13		feq3 4553	. . . . . . . 8 |- (ran g = X -> (h:(X X. X)-->ran g <-> h:(X X. X)-->X))
14	12, 13	bitrd 587	. . . . . . 7 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
15	8, 14	syl 12	. . . . . 6 |- (g = G -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
16	5, 15	anbi12d 690	. . . . 5 |- (g = G -> ((g e. Abel /\ h:(ran g X. ran g)-->ran g) <-> (G e. Abel /\ h:(X X. X)-->X)))
17		raleq 2266	. . . . . . . . . 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)))))
18	17	raleqbi1dv 2271	. . . . . . . . 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)))))
19	18	raleqbi1dv 2271	. . . . . . . 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)))))
20	8, 19	syl 12	. . . . . . 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)))))
21		opreq 4888	. . . . . . . . . . . 12 |- (g = G -> (ygz) = (yGz))
22	21	opreq2d 4898	. . . . . . . . . . 11 |- (g = G -> (xh(ygz)) = (xh(yGz)))
23		opreq 4888	. . . . . . . . . . 11 |- (g = G -> ((xhy)g(xhz)) = ((xhy)G(xhz)))
24	22, 23	eqeq12d 1899	. . . . . . . . . 10 |- (g = G -> ((xh(ygz)) = ((xhy)g(xhz)) <-> (xh(yGz)) = ((xhy)G(xhz))))
25		opreq 4888	. . . . . . . . . . . 12 |- (g = G -> (xgy) = (xGy))
26	25	opreq1d 4897	. . . . . . . . . . 11 |- (g = G -> ((xgy)hz) = ((xGy)hz))
27		opreq 4888	. . . . . . . . . . 11 |- (g = G -> ((xhz)g(yhz)) = ((xhz)G(yhz)))
28	26, 27	eqeq12d 1899	. . . . . . . . . 10 |- (g = G -> (((xgy)hz) = ((xhz)g(yhz)) <-> ((xGy)hz) = ((xhz)G(yhz))))
29	24, 28	3anbi23d 1171	. . . . . . . . 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)))))
30	29	ralbidv 2123	. . . . . . . 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)))))
31	30	2ralbidv 2140	. . . . . . 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(yGz)) = ((xhy)G(xhz)) /\ ((xGy)hz) = ((xhz)G(yhz)))))
32	20, 31	bitrd 587	. . . . . 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) = ((xhz)G(yhz)))))
33	8	raleqdv 2269	. . . . . . 7 |- (g = G -> (A.y e. ran g((yhx) = y /\ (xhy) = y) <-> A.y e. X ((yhx) = y /\ (xhy) = y)))
34	8, 33	rexeqbidv 2275	. . . . . 6 |- (g = G -> (E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y) <-> E.x e. X A.y e. X ((yhx) = y /\ (xhy) = y)))
35	32, 34	anbi12d 690	. . . . 5 |- (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))) /\ E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y)) <-> (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))))
36	16, 35	anbi12d 690	. . . 4 |- (g = G -> (((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))) <-> ((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)))))
37	4, 36	sylbir 218	. . 3 |- (g = (1st` R) -> (((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))) <-> ((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)))))
38		ringi.2	. . . . 5 |- H = (2nd` R)
39	38	eqeq2i 1894	. . . 4 |- (h = H <-> h = (2nd` R))
40		feq1 4551	. . . . . 6 |- (h = H -> (h:(X X. X)-->X <-> H:(X X. X)-->X))
41	40	anbi2d 678	. . . . 5 |- (h = H -> ((G e. Abel /\ h:(X X. X)-->X) <-> (G e. Abel /\ H:(X X. X)-->X)))
42		opreq 4888	. . . . . . . . . . 11 |- (h = H -> ((xhy)hz) = ((xhy)Hz))
43		opreq 4888	. . . . . . . . . . . 12 |- (h = H -> (xhy) = (xHy))
44	43	opreq1d 4897	. . . . . . . . . . 11 |- (h = H -> ((xhy)Hz) = ((xHy)Hz))
45	42, 44	eqtrd 1925	. . . . . . . . . 10 |- (h = H -> ((xhy)hz) = ((xHy)Hz))
46		opreq 4888	. . . . . . . . . . 11 |- (h = H -> (xh(yhz)) = (xH(yhz)))
47		opreq 4888	. . . . . . . . . . . 12 |- (h = H -> (yhz) = (yHz))
48	47	opreq2d 4898	. . . . . . . . . . 11 |- (h = H -> (xH(yhz)) = (xH(yHz)))
49	46, 48	eqtrd 1925	. . . . . . . . . 10 |- (h = H -> (xh(yhz)) = (xH(yHz)))
50	45, 49	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> (((xhy)hz) = (xh(yhz)) <-> ((xHy)Hz) = (xH(yHz))))
51		opreq 4888	. . . . . . . . . 10 |- (h = H -> (xh(yGz)) = (xH(yGz)))
52		opreq 4888	. . . . . . . . . . 11 |- (h = H -> (xhz) = (xHz))
53	43, 52	opreq12d 4900	. . . . . . . . . 10 |- (h = H -> ((xhy)G(xhz)) = ((xHy)G(xHz)))
54	51, 53	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> ((xh(yGz)) = ((xhy)G(xhz)) <-> (xH(yGz)) = ((xHy)G(xHz))))
55		opreq 4888	. . . . . . . . . 10 |- (h = H -> ((xGy)hz) = ((xGy)Hz))
56	52, 47	opreq12d 4900	. . . . . . . . . 10 |- (h = H -> ((xhz)G(yhz)) = ((xHz)G(yHz)))
57	55, 56	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> (((xGy)hz) = ((xhz)G(yhz)) <-> ((xGy)Hz) = ((xHz)G(yHz))))
58	50, 54, 57	3anbi123d 1168	. . . . . . . 8 |- (h = H -> ((((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)))))
59	58	ralbidv 2123	. . . . . . 7 |- (h = H -> (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)))))
60	59	2ralbidv 2140	. . . . . 6 |- (h = H -> (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(yGz)) = ((xHy)G(xHz)) /\ ((xGy)Hz) = ((xHz)G(yHz)))))
61		opreq 4888	. . . . . . . . 9 |- (h = H -> (yhx) = (yHx))
62	61	eqeq1d 1892	. . . . . . . 8 |- (h = H -> ((yhx) = y <-> (yHx) = y))
63	43	eqeq1d 1892	. . . . . . . 8 |- (h = H -> ((xhy) = y <-> (xHy) = y))
64	62, 63	anbi12d 690	. . . . . . 7 |- (h = H -> (((yhx) = y /\ (xhy) = y) <-> ((yHx) = y /\ (xHy) = y)))
65	64	rexralbidv 2142	. . . . . 6 |- (h = H -> (E.x e. X A.y e. X ((yhx) = y /\ (xhy) = y) <-> E.x e. X A.y e. X ((yHx) = y /\ (xHy) = y)))
66	60, 65	anbi12d 690	. . . . 5 |- (h = H -> ((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)) <-> (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))))
67	41, 66	anbi12d 690	. . . 4 |- (h = H -> (((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. 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)))))
68	39, 67	sylbir 218	. . 3 |- (h = (2nd` R) -> (((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. 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)))))
69	37, 68	elopabi 5059	. 2 |- (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)))} -> ((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))))
70	2, 69	sylbi 216	1 |- (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))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {copab 3395   X. cxp 3984  ran crn 3987  -->wf 3994  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019  Abelcabl 9407  Ringcring 9463

This theorem is referenced by:  ringsm 9467  ringid 9469  ringideu 9470  ringdi 9471  ringdir 9472  ringass 9473  ringabl 9475  rnplrnml 10404  unmnd 10405  ununr 14769  fldi 14776

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-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-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-f 4010  df-fv 4014  df-opr 4886  df-1st 5020  df-2nd 5021  df-ring 9464

Copyright terms: Public domain