Definition df-rngo 33694

Description: Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-rngo	|- RingOps = { <. g , h >. | ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) ) }

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

Detailed syntax breakdown of Definition df-rngo

Step	Hyp	Ref	Expression
1		crngo 33693	. 2 class RingOps
2		vg	. . . . . . 7 setvar g
3	2	cv 1482	. . . . . 6 class g
4		cablo 27398	. . . . . 6 class AbelOp
5	3, 4	wcel 1990	. . . . 5 wff g e. AbelOp
6	3	crn 5115	. . . . . . 7 class ran g
7	6, 6	cxp 5112	. . . . . 6 class ( ran g X. ran g )
8		vh	. . . . . . 7 setvar h
9	8	cv 1482	. . . . . 6 class h
10	7, 6, 9	wf 5884	. . . . 5 wff h : ( ran g X. ran g ) --> ran g
11	5, 10	wa 384	. . . 4 wff ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g )
12		vx	. . . . . . . . . . . . 13 setvar x
13	12	cv 1482	. . . . . . . . . . . 12 class x
14		vy	. . . . . . . . . . . . 13 setvar y
15	14	cv 1482	. . . . . . . . . . . 12 class y
16	13, 15, 9	co 6650	. . . . . . . . . . 11 class ( x h y )
17		vz	. . . . . . . . . . . 12 setvar z
18	17	cv 1482	. . . . . . . . . . 11 class z
19	16, 18, 9	co 6650	. . . . . . . . . 10 class ( ( x h y ) h z )
20	15, 18, 9	co 6650	. . . . . . . . . . 11 class ( y h z )
21	13, 20, 9	co 6650	. . . . . . . . . 10 class ( x h ( y h z ) )
22	19, 21	wceq 1483	. . . . . . . . 9 wff ( ( x h y ) h z ) = ( x h ( y h z ) )
23	15, 18, 3	co 6650	. . . . . . . . . . 11 class ( y g z )
24	13, 23, 9	co 6650	. . . . . . . . . 10 class ( x h ( y g z ) )
25	13, 18, 9	co 6650	. . . . . . . . . . 11 class ( x h z )
26	16, 25, 3	co 6650	. . . . . . . . . 10 class ( ( x h y ) g ( x h z ) )
27	24, 26	wceq 1483	. . . . . . . . 9 wff ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) )
28	13, 15, 3	co 6650	. . . . . . . . . . 11 class ( x g y )
29	28, 18, 9	co 6650	. . . . . . . . . 10 class ( ( x g y ) h z )
30	25, 20, 3	co 6650	. . . . . . . . . 10 class ( ( x h z ) g ( y h z ) )
31	29, 30	wceq 1483	. . . . . . . . 9 wff ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) )
32	22, 27, 31	w3a 1037	. . . . . . . 8 wff ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) )
33	32, 17, 6	wral 2912	. . . . . . 7 wff A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) )
34	33, 14, 6	wral 2912	. . . . . 6 wff A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) )
35	34, 12, 6	wral 2912	. . . . 5 wff A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) )
36	16, 15	wceq 1483	. . . . . . . 8 wff ( x h y ) = y
37	15, 13, 9	co 6650	. . . . . . . . 9 class ( y h x )
38	37, 15	wceq 1483	. . . . . . . 8 wff ( y h x ) = y
39	36, 38	wa 384	. . . . . . 7 wff ( ( x h y ) = y /\ ( y h x ) = y )
40	39, 14, 6	wral 2912	. . . . . 6 wff A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y )
41	40, 12, 6	wrex 2913	. . . . 5 wff E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y )
42	35, 41	wa 384	. . . 4 wff ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) )
43	11, 42	wa 384	. . 3 wff ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) )
44	43, 2, 8	copab 4712	. 2 class { <. g , h >. | ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) ) }
45	1, 44	wceq 1483	1 wff RingOps = { <. g , h >. | ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) ) }

This definition is referenced by:  relrngo  33695  isrngo  33696