Metamath Proof Explorer

Definition df-rngo

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

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

Detailed syntax breakdown

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