Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-orng Structured version   Unicode version

Definition df-orng 26411
Description: Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
Assertion
Ref Expression
df-orng  |- oRing  =  {
r  e.  ( Ring 
i^i oGrp )  |  [. ( Base `  r )  / 
v ]. [. ( 0g
`  r )  / 
z ]. [. ( .r
`  r )  / 
t ]. [. ( le
`  r )  / 
l ]. A. a  e.  v  A. b  e.  v  ( ( z l a  /\  z
l b )  -> 
z l ( a t b ) ) }
Distinct variable group:    a, b, l, r, t, v, z

Detailed syntax breakdown of Definition df-orng
StepHypRef Expression
1 corng 26409 . 2  class oRing
2 vz . . . . . . . . . . . . 13  setvar  z
32cv 1369 . . . . . . . . . . . 12  class  z
4 va . . . . . . . . . . . . 13  setvar  a
54cv 1369 . . . . . . . . . . . 12  class  a
6 vl . . . . . . . . . . . . 13  setvar  l
76cv 1369 . . . . . . . . . . . 12  class  l
83, 5, 7wbr 4401 . . . . . . . . . . 11  wff  z l a
9 vb . . . . . . . . . . . . 13  setvar  b
109cv 1369 . . . . . . . . . . . 12  class  b
113, 10, 7wbr 4401 . . . . . . . . . . 11  wff  z l b
128, 11wa 369 . . . . . . . . . 10  wff  ( z l a  /\  z
l b )
13 vt . . . . . . . . . . . . 13  setvar  t
1413cv 1369 . . . . . . . . . . . 12  class  t
155, 10, 14co 6201 . . . . . . . . . . 11  class  ( a t b )
163, 15, 7wbr 4401 . . . . . . . . . 10  wff  z l ( a t b )
1712, 16wi 4 . . . . . . . . 9  wff  ( ( z l a  /\  z l b )  ->  z l ( a t b ) )
18 vv . . . . . . . . . 10  setvar  v
1918cv 1369 . . . . . . . . 9  class  v
2017, 9, 19wral 2799 . . . . . . . 8  wff  A. b  e.  v  ( (
z l a  /\  z l b )  ->  z l ( a t b ) )
2120, 4, 19wral 2799 . . . . . . 7  wff  A. a  e.  v  A. b  e.  v  ( (
z l a  /\  z l b )  ->  z l ( a t b ) )
22 vr . . . . . . . . 9  setvar  r
2322cv 1369 . . . . . . . 8  class  r
24 cple 14365 . . . . . . . 8  class  le
2523, 24cfv 5527 . . . . . . 7  class  ( le
`  r )
2621, 6, 25wsbc 3294 . . . . . 6  wff  [. ( le `  r )  / 
l ]. A. a  e.  v  A. b  e.  v  ( ( z l a  /\  z
l b )  -> 
z l ( a t b ) )
27 cmulr 14359 . . . . . . 7  class  .r
2823, 27cfv 5527 . . . . . 6  class  ( .r
`  r )
2926, 13, 28wsbc 3294 . . . . 5  wff  [. ( .r `  r )  / 
t ]. [. ( le
`  r )  / 
l ]. A. a  e.  v  A. b  e.  v  ( ( z l a  /\  z
l b )  -> 
z l ( a t b ) )
30 c0g 14498 . . . . . 6  class  0g
3123, 30cfv 5527 . . . . 5  class  ( 0g
`  r )
3229, 2, 31wsbc 3294 . . . 4  wff  [. ( 0g `  r )  / 
z ]. [. ( .r
`  r )  / 
t ]. [. ( le
`  r )  / 
l ]. A. a  e.  v  A. b  e.  v  ( ( z l a  /\  z
l b )  -> 
z l ( a t b ) )
33 cbs 14293 . . . . 5  class  Base
3423, 33cfv 5527 . . . 4  class  ( Base `  r )
3532, 18, 34wsbc 3294 . . 3  wff  [. ( Base `  r )  / 
v ]. [. ( 0g
`  r )  / 
z ]. [. ( .r
`  r )  / 
t ]. [. ( le
`  r )  / 
l ]. A. a  e.  v  A. b  e.  v  ( ( z l a  /\  z
l b )  -> 
z l ( a t b ) )
36 crg 16769 . . . 4  class  Ring
37 cogrp 26307 . . . 4  class oGrp
3836, 37cin 3436 . . 3  class  ( Ring 
i^i oGrp )
3935, 22, 38crab 2803 . 2  class  { r  e.  ( Ring  i^i oGrp )  |  [. ( Base `  r )  /  v ]. [. ( 0g `  r )  /  z ]. [. ( .r `  r )  /  t ]. [. ( le `  r )  /  l ]. A. a  e.  v 
A. b  e.  v  ( ( z l a  /\  z l b )  ->  z
l ( a t b ) ) }
401, 39wceq 1370 1  wff oRing  =  {
r  e.  ( Ring 
i^i oGrp )  |  [. ( Base `  r )  / 
v ]. [. ( 0g
`  r )  / 
z ]. [. ( .r
`  r )  / 
t ]. [. ( le
`  r )  / 
l ]. A. a  e.  v  A. b  e.  v  ( ( z l a  /\  z
l b )  -> 
z l ( a t b ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  isorng  26413
  Copyright terms: Public domain W3C validator