Theorem isring 9465

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 3339	. . . . 5 |- (GRingH <-> <.G, H>. e. Ring)
2		relopab 4104	. . . . . . 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 9464	. . . . . . . 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 4072	. . . . . . 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 207	. . . . . 6 |- Rel Ring
6	5	brrelexi 4029	. . . . 5 |- (GRingH -> G e. _V)
7	1, 6	sylbir 218	. . . 4 |- (<.G, H>. e. Ring -> G e. _V)
8	7	anim1i 361	. . 3 |- ((<.G, H>. e. Ring /\ H e. A) -> (G e. _V /\ H e. A))
9	8	ancoms 484	. 2 |- ((H e. A /\ <.G, H>. e. Ring) -> (G e. _V /\ H e. A))
10		elisset 2299	. . . . . 6 |- (G e. Abel -> G e. _V)
11	10	anim1i 361	. . . . 5 |- ((G e. Abel /\ H e. A) -> (G e. _V /\ H e. A))
12	11	ancoms 484	. . . 4 |- ((H e. A /\ G e. Abel) -> (G e. _V /\ H e. A))
13	12	adantrr 431	. . 3 |- ((H e. A /\ (G e. Abel /\ H:(X X. X)-->X)) -> (G e. _V /\ H e. A))
14	13	adantrr 431	. 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 1957	. . . . . 6 |- (g = G -> (g e. Abel <-> G e. Abel))
16		rneq 4186	. . . . . . . 8 |- (g = G -> ran g = ran G)
17		isring.1	. . . . . . . 8 |- X = ran G
18	16, 17	syl6eqr 1946	. . . . . . 7 |- (g = G -> ran g = X)
19		xpeq1 4016	. . . . . . . . . 10 |- (ran g = X -> (ran g X. ran g) = (X X. ran g))
20		xpeq2 4017	. . . . . . . . . 10 |- (ran g = X -> (X X. ran g) = (X X. X))
21	19, 20	eqtrd 1925	. . . . . . . . 9 |- (ran g = X -> (ran g X. ran g) = (X X. X))
22	21	feq2d 4557	. . . . . . . 8 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->ran g))
23		feq3 4553	. . . . . . . 8 |- (ran g = X -> (h:(X X. X)-->ran g <-> h:(X X. X)-->X))
24	22, 23	bitrd 587	. . . . . . 7 |- (ran g = X -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
25	18, 24	syl 12	. . . . . 6 |- (g = G -> (h:(ran g X. ran g)-->ran g <-> h:(X X. X)-->X))
26	15, 25	anbi12d 690	. . . . 5 |- (g = G -> ((g e. Abel /\ h:(ran g X. ran g)-->ran g) <-> (G e. Abel /\ h:(X X. X)-->X)))
27		opreq 4888	. . . . . . . . . . . 12 |- (g = G -> (ygz) = (yGz))
28	27	opreq2d 4898	. . . . . . . . . . 11 |- (g = G -> (xh(ygz)) = (xh(yGz)))
29		opreq 4888	. . . . . . . . . . 11 |- (g = G -> ((xhy)g(xhz)) = ((xhy)G(xhz)))
30	28, 29	eqeq12d 1899	. . . . . . . . . 10 |- (g = G -> ((xh(ygz)) = ((xhy)g(xhz)) <-> (xh(yGz)) = ((xhy)G(xhz))))
31		opreq 4888	. . . . . . . . . . . 12 |- (g = G -> (xgy) = (xGy))
32	31	opreq1d 4897	. . . . . . . . . . 11 |- (g = G -> ((xgy)hz) = ((xGy)hz))
33		opreq 4888	. . . . . . . . . . 11 |- (g = G -> ((xhz)g(yhz)) = ((xhz)G(yhz)))
34	32, 33	eqeq12d 1899	. . . . . . . . . 10 |- (g = G -> (((xgy)hz) = ((xhz)g(yhz)) <-> ((xGy)hz) = ((xhz)G(yhz))))
35	30, 34	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)))))
36	18, 35	raleqbidv 2274	. . . . . . . 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)))))
37	18, 36	raleqbidv 2274	. . . . . . 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)))))
38	18, 37	raleqbidv 2274	. . . . . 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)))))
39	18	raleqdv 2269	. . . . . . 7 |- (g = G -> (A.y e. ran g((yhx) = y /\ (xhy) = y) <-> A.y e. X ((yhx) = y /\ (xhy) = y)))
40	18, 39	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)))
41	38, 40	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))))
42	26, 41	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)))))
43		feq1 4551	. . . . . 6 |- (h = H -> (h:(X X. X)-->X <-> H:(X X. X)-->X))
44	43	anbi2d 678	. . . . 5 |- (h = H -> ((G e. Abel /\ h:(X X. X)-->X) <-> (G e. Abel /\ H:(X X. X)-->X)))
45		opreq 4888	. . . . . . . . . . 11 |- (h = H -> ((xhy)hz) = ((xhy)Hz))
46		opreq 4888	. . . . . . . . . . . 12 |- (h = H -> (xhy) = (xHy))
47	46	opreq1d 4897	. . . . . . . . . . 11 |- (h = H -> ((xhy)Hz) = ((xHy)Hz))
48	45, 47	eqtrd 1925	. . . . . . . . . 10 |- (h = H -> ((xhy)hz) = ((xHy)Hz))
49		opreq 4888	. . . . . . . . . . 11 |- (h = H -> (xh(yhz)) = (xH(yhz)))
50		opreq 4888	. . . . . . . . . . . 12 |- (h = H -> (yhz) = (yHz))
51	50	opreq2d 4898	. . . . . . . . . . 11 |- (h = H -> (xH(yhz)) = (xH(yHz)))
52	49, 51	eqtrd 1925	. . . . . . . . . 10 |- (h = H -> (xh(yhz)) = (xH(yHz)))
53	48, 52	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> (((xhy)hz) = (xh(yhz)) <-> ((xHy)Hz) = (xH(yHz))))
54		opreq 4888	. . . . . . . . . 10 |- (h = H -> (xh(yGz)) = (xH(yGz)))
55		opreq 4888	. . . . . . . . . . 11 |- (h = H -> (xhz) = (xHz))
56	46, 55	opreq12d 4900	. . . . . . . . . 10 |- (h = H -> ((xhy)G(xhz)) = ((xHy)G(xHz)))
57	54, 56	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> ((xh(yGz)) = ((xhy)G(xhz)) <-> (xH(yGz)) = ((xHy)G(xHz))))
58		opreq 4888	. . . . . . . . . 10 |- (h = H -> ((xGy)hz) = ((xGy)Hz))
59	55, 50	opreq12d 4900	. . . . . . . . . 10 |- (h = H -> ((xhz)G(yhz)) = ((xHz)G(yHz)))
60	58, 59	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> (((xGy)hz) = ((xhz)G(yhz)) <-> ((xGy)Hz) = ((xHz)G(yHz))))
61	53, 57, 60	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)))))
62	61	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)))))
63	62	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)))))
64		opreq 4888	. . . . . . . . 9 |- (h = H -> (yhx) = (yHx))
65	64	eqeq1d 1892	. . . . . . . 8 |- (h = H -> ((yhx) = y <-> (yHx) = y))
66	46	eqeq1d 1892	. . . . . . . 8 |- (h = H -> ((xhy) = y <-> (xHy) = y))
67	65, 66	anbi12d 690	. . . . . . 7 |- (h = H -> (((yhx) = y /\ (xhy) = y) <-> ((yHx) = y /\ (xHy) = y)))
68	67	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)))
69	63, 68	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))))
70	44, 69	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)))))
71	42, 70	opelopabg 3567	. . 3 |- ((G e. _V /\ H e. A) -> (<.G, H>. 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)))))
72	3	eleq2i 1961	. . 3 |- (<.G, H>. e. Ring <-> <.G, H>. 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)))})
73	71, 72	syl5bb 591	. 2 |- ((G e. _V /\ 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)))))
74	9, 14, 73	pm5.21nd 744	1 |- (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)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292  <.cop 3046   class class class wbr 3338  {copab 3395   X. cxp 3984  ran crn 3987  Rel wrel 3991  -->wf 3994  (class class class)co 4884  Abelcabl 9407  Ringcring 9463

This theorem is referenced by:  cnring 9489  ringsn 9490  isringd 16097

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

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-ring 9464

Copyright terms: Public domain