MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rngo Unicode version

Definition df-rngo 21043
Description: Define the class of all unital rings. (Contributed by Jeffrey 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
StepHypRef Expression
1 crngo 21042 . 2  class  RingOps
2 vg . . . . . . 7  set  g
32cv 1622 . . . . . 6  class  g
4 cablo 20948 . . . . . 6  class  AbelOp
53, 4wcel 1684 . . . . 5  wff  g  e. 
AbelOp
63crn 4690 . . . . . . 7  class  ran  g
76, 6cxp 4687 . . . . . 6  class  ( ran  g  X.  ran  g
)
8 vh . . . . . . 7  set  h
98cv 1622 . . . . . 6  class  h
107, 6, 9wf 5251 . . . . 5  wff  h : ( ran  g  X. 
ran  g ) --> ran  g
115, 10wa 358 . . . 4  wff  ( g  e.  AbelOp  /\  h :
( ran  g  X.  ran  g ) --> ran  g
)
12 vx . . . . . . . . . . . . 13  set  x
1312cv 1622 . . . . . . . . . . . 12  class  x
14 vy . . . . . . . . . . . . 13  set  y
1514cv 1622 . . . . . . . . . . . 12  class  y
1613, 15, 9co 5858 . . . . . . . . . . 11  class  ( x h y )
17 vz . . . . . . . . . . . 12  set  z
1817cv 1622 . . . . . . . . . . 11  class  z
1916, 18, 9co 5858 . . . . . . . . . 10  class  ( ( x h y ) h z )
2015, 18, 9co 5858 . . . . . . . . . . 11  class  ( y h z )
2113, 20, 9co 5858 . . . . . . . . . 10  class  ( x h ( y h z ) )
2219, 21wceq 1623 . . . . . . . . 9  wff  ( ( x h y ) h z )  =  ( x h ( y h z ) )
2315, 18, 3co 5858 . . . . . . . . . . 11  class  ( y g z )
2413, 23, 9co 5858 . . . . . . . . . 10  class  ( x h ( y g z ) )
2513, 18, 9co 5858 . . . . . . . . . . 11  class  ( x h z )
2616, 25, 3co 5858 . . . . . . . . . 10  class  ( ( x h y ) g ( x h z ) )
2724, 26wceq 1623 . . . . . . . . 9  wff  ( x h ( y g z ) )  =  ( ( x h y ) g ( x h z ) )
2813, 15, 3co 5858 . . . . . . . . . . 11  class  ( x g y )
2928, 18, 9co 5858 . . . . . . . . . 10  class  ( ( x g y ) h z )
3025, 20, 3co 5858 . . . . . . . . . 10  class  ( ( x h z ) g ( y h z ) )
3129, 30wceq 1623 . . . . . . . . 9  wff  ( ( x g y ) h z )  =  ( ( x h z ) g ( y h z ) )
3222, 27, 31w3a 934 . . . . . . . 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 ) ) )
3332, 17, 6wral 2543 . . . . . . 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 ) ) )
3433, 14, 6wral 2543 . . . . . 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 ) ) )
3534, 12, 6wral 2543 . . . . 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 ) ) )
3616, 15wceq 1623 . . . . . . . 8  wff  ( x h y )  =  y
3715, 13, 9co 5858 . . . . . . . . 9  class  ( y h x )
3837, 15wceq 1623 . . . . . . . 8  wff  ( y h x )  =  y
3936, 38wa 358 . . . . . . 7  wff  ( ( x h y )  =  y  /\  (
y h x )  =  y )
4039, 14, 6wral 2543 . . . . . 6  wff  A. y  e.  ran  g ( ( x h y )  =  y  /\  (
y h x )  =  y )
4140, 12, 6wrex 2544 . . . . 5  wff  E. x  e.  ran  g A. y  e.  ran  g ( ( x h y )  =  y  /\  (
y h x )  =  y )
4235, 41wa 358 . . . 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 ) )
4311, 42wa 358 . . 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 ) ) )
4443, 2, 8copab 4076 . 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 ) ) ) }
451, 44wceq 1623 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 ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  relrngo  21044  isrngo  21045
  Copyright terms: Public domain W3C validator