Metamath Proof Explorer

Definition df-orng

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 corng 
 |-  oRing
1 vr 
 |-  r
2 crg 
 |-  Ring
3 cogrp 
 |-  oGrp
4 2 3 cin 
 |-  ( Ring i^i oGrp )
5 cbs 
 |-  Base
6 1 cv 
 |-  r
7 6 5 cfv 
 |-  ( Base ` r )
8 vv 
 |-  v
9 c0g 
 |-  0g
10 6 9 cfv 
 |-  ( 0g ` r )
11 vz 
 |-  z
12 cmulr 
 |-  .r
13 6 12 cfv 
 |-  ( .r ` r )
14 vt 
 |-  t
15 cple 
 |-  le
16 6 15 cfv 
 |-  ( le ` r )
17 vl 
 |-  l
18 va 
 |-  a
19 8 cv 
 |-  v
20 vb 
 |-  b
21 11 cv 
 |-  z
22 17 cv 
 |-  l
23 18 cv 
 |-  a
24 21 23 22 wbr 
 |-  z l a
25 20 cv 
 |-  b
26 21 25 22 wbr 
 |-  z l b
27 24 26 wa 
 |-  ( z l a /\ z l b )
28 14 cv 
 |-  t
29 23 25 28 co 
 |-  ( a t b )
30 21 29 22 wbr 
 |-  z l ( a t b )
31 27 30 wi 
 |-  ( ( z l a /\ z l b ) -> z l ( a t b ) )
32 31 20 19 wral 
 |-  A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
33 32 18 19 wral 
 |-  A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
34 33 17 16 wsbc 
 |-  [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
35 34 14 13 wsbc 
 |-  [. ( .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 35 11 10 wsbc 
 |-  [. ( 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 ) )
37 36 8 7 wsbc 
 |-  [. ( 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 ) )
38 37 1 4 crab 
 |-  { 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 ) ) }
39 0 38 wceq 
 |-  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 ) ) }