Definition df-ring 9464

Description: Define the class of all unital rings.

Assertion

Ref	Expression
df-ring	|- 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)))}

Distinct variable group:   g,h,x,y,z

Detailed syntax breakdown of Definition df-ring

Step	Hyp	Ref	Expression
1		cring 9463	. 2 class Ring
2		vg	. . . . . . 7 set g
3	2	cv 1297	. . . . . 6 class g
4		cabl 9407	. . . . . 6 class Abel
5	3, 4	wcel 1300	. . . . 5 wff g e. Abel
6	3	crn 3987	. . . . . . 7 class ran g
7	6, 6	cxp 3984	. . . . . 6 class (ran g X. ran g)
8		vh	. . . . . . 7 set h
9	8	cv 1297	. . . . . 6 class h
10	7, 6, 9	wf 3994	. . . . 5 wff h:(ran g X. ran g)-->ran g
11	5, 10	wa 240	. . . 4 wff (g e. Abel /\ h:(ran g X. ran g)-->ran g)
12		vx	. . . . . . . . . . . . 13 set x
13	12	cv 1297	. . . . . . . . . . . 12 class x
14		vy	. . . . . . . . . . . . 13 set y
15	14	cv 1297	. . . . . . . . . . . 12 class y
16	13, 15, 9	co 4884	. . . . . . . . . . 11 class (xhy)
17		vz	. . . . . . . . . . . 12 set z
18	17	cv 1297	. . . . . . . . . . 11 class z
19	16, 18, 9	co 4884	. . . . . . . . . 10 class ((xhy)hz)
20	15, 18, 9	co 4884	. . . . . . . . . . 11 class (yhz)
21	13, 20, 9	co 4884	. . . . . . . . . 10 class (xh(yhz))
22	19, 21	wceq 1298	. . . . . . . . 9 wff ((xhy)hz) = (xh(yhz))
23	15, 18, 3	co 4884	. . . . . . . . . . 11 class (ygz)
24	13, 23, 9	co 4884	. . . . . . . . . 10 class (xh(ygz))
25	13, 18, 9	co 4884	. . . . . . . . . . 11 class (xhz)
26	16, 25, 3	co 4884	. . . . . . . . . 10 class ((xhy)g(xhz))
27	24, 26	wceq 1298	. . . . . . . . 9 wff (xh(ygz)) = ((xhy)g(xhz))
28	13, 15, 3	co 4884	. . . . . . . . . . 11 class (xgy)
29	28, 18, 9	co 4884	. . . . . . . . . 10 class ((xgy)hz)
30	25, 20, 3	co 4884	. . . . . . . . . 10 class ((xhz)g(yhz))
31	29, 30	wceq 1298	. . . . . . . . 9 wff ((xgy)hz) = ((xhz)g(yhz))
32	22, 27, 31	w3a 858	. . . . . . . 8 wff (((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz)))
33	32, 17, 6	wral 2105	. . . . . . 7 wff A.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz)))
34	33, 14, 6	wral 2105	. . . . . 6 wff A.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz)))
35	34, 12, 6	wral 2105	. . . . 5 wff 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)))
36	15, 13, 9	co 4884	. . . . . . . . 9 class (yhx)
37	36, 15	wceq 1298	. . . . . . . 8 wff (yhx) = y
38	16, 15	wceq 1298	. . . . . . . 8 wff (xhy) = y
39	37, 38	wa 240	. . . . . . 7 wff ((yhx) = y /\ (xhy) = y)
40	39, 14, 6	wral 2105	. . . . . 6 wff A.y e. ran g((yhx) = y /\ (xhy) = y)
41	40, 12, 6	wrex 2106	. . . . 5 wff E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y)
42	35, 41	wa 240	. . . 4 wff (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))
43	11, 42	wa 240	. . 3 wff ((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)))
44	43, 2, 8	copab 3395	. 2 class {<.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)))}
45	1, 44	wceq 1298	1 wff 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)))}

This definition is referenced by:  isring 9465  ringi 9466  relrng 10399

Copyright terms: Public domain