Metamath Proof Explorer

Theorem isorng

Description: An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018)

Ref Expression
Hypotheses isorng.0 
|- B = ( Base ` R )
isorng.1 
|- .0. = ( 0g ` R )
isorng.2 
|- .x. = ( .r ` R )
isorng.3 
|- .<_ = ( le ` R )
Assertion isorng 
|- ( R e. oRing <-> ( R e. Ring /\ R e. oGrp /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )

Proof

Step Hyp Ref Expression
1 isorng.0 
 |-  B = ( Base ` R )
2 isorng.1 
 |-  .0. = ( 0g ` R )
3 isorng.2 
 |-  .x. = ( .r ` R )
4 isorng.3 
 |-  .<_ = ( le ` R )
5 elin 
 |-  ( R e. ( Ring i^i oGrp ) <-> ( R e. Ring /\ R e. oGrp ) )
6 5 anbi1i 
 |-  ( ( R e. ( Ring i^i oGrp ) /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) <-> ( ( R e. Ring /\ R e. oGrp ) /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
7 fvexd 
 |-  ( r = R -> ( .r ` r ) e. _V )
8 simpr 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> t = ( .r ` r ) )
9 simpl 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> r = R )
10 9 fveq2d 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( .r ` r ) = ( .r ` R ) )
11 10 3 eqtr4di 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( .r ` r ) = .x. )
12 8 11 eqtrd 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> t = .x. )
13 12 oveqd 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( a t b ) = ( a .x. b ) )
14 13 breq2d 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( .0. l ( a t b ) <-> .0. l ( a .x. b ) ) )
15 14 imbi2d 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) <-> ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) ) )
16 15 2ralbidv 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) <-> A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) ) )
17 16 sbcbidv 
 |-  ( ( r = R /\ t = ( .r ` r ) ) -> ( [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) <-> [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) ) )
18 7 17 sbcied 
 |-  ( r = R -> ( [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) <-> [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) ) )
19 fvexd 
 |-  ( r = R -> ( Base ` r ) e. _V )
20 simpr 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> v = ( Base ` r ) )
21 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
22 21 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
23 22 adantr 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> ( Base ` r ) = B )
24 20 23 eqtrd 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> v = B )
25 raleq 
 |-  ( v = B -> ( A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
26 25 raleqbi1dv 
 |-  ( v = B -> ( A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
27 24 26 syl 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> ( A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
28 27 sbcbidv 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> ( [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
29 28 sbcbidv 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> ( [. ( .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 ) ) <-> [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
30 29 sbcbidv 
 |-  ( ( r = R /\ v = ( Base ` r ) ) -> ( [. ( 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 ) ) <-> [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
31 19 30 sbcied 
 |-  ( r = R -> ( [. ( 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 ) ) <-> [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) ) )
32 fvexd 
 |-  ( r = R -> ( 0g ` r ) e. _V )
33 simpr 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> z = ( 0g ` r ) )
34 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
35 34 2 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
36 35 adantr 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( 0g ` r ) = .0. )
37 33 36 eqtrd 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> z = .0. )
38 37 breq1d 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( z l a <-> .0. l a ) )
39 37 breq1d 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( z l b <-> .0. l b ) )
40 38 39 anbi12d 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( ( z l a /\ z l b ) <-> ( .0. l a /\ .0. l b ) ) )
41 37 breq1d 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( z l ( a t b ) <-> .0. l ( a t b ) ) )
42 40 41 imbi12d 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) ) )
43 42 2ralbidv 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) ) )
44 43 sbcbidv 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) ) )
45 44 sbcbidv 
 |-  ( ( r = R /\ z = ( 0g ` r ) ) -> ( [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) ) )
46 32 45 sbcied 
 |-  ( r = R -> ( [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( z l a /\ z l b ) -> z l ( a t b ) ) <-> [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) ) )
47 31 46 bitr2d 
 |-  ( r = R -> ( [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a t b ) ) <-> [. ( 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 ) ) ) )
48 fvexd 
 |-  ( r = R -> ( le ` r ) e. _V )
49 simpr 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> l = ( le ` r ) )
50 simpl 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> r = R )
51 50 fveq2d 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( le ` r ) = ( le ` R ) )
52 51 4 eqtr4di 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( le ` r ) = .<_ )
53 49 52 eqtrd 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> l = .<_ )
54 53 breqd 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( .0. l a <-> .0. .<_ a ) )
55 53 breqd 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( .0. l b <-> .0. .<_ b ) )
56 54 55 anbi12d 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( ( .0. l a /\ .0. l b ) <-> ( .0. .<_ a /\ .0. .<_ b ) ) )
57 53 breqd 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( .0. l ( a .x. b ) <-> .0. .<_ ( a .x. b ) ) )
58 56 57 imbi12d 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) <-> ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
59 58 2ralbidv 
 |-  ( ( r = R /\ l = ( le ` r ) ) -> ( A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) <-> A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
60 48 59 sbcied 
 |-  ( r = R -> ( [. ( le ` r ) / l ]. A. a e. B A. b e. B ( ( .0. l a /\ .0. l b ) -> .0. l ( a .x. b ) ) <-> A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
61 18 47 60 3bitr3d 
 |-  ( r = R -> ( [. ( 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 ) ) <-> A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
62 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 ) ) }
63 61 62 elrab2 
 |-  ( R e. oRing <-> ( R e. ( Ring i^i oGrp ) /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
64 df-3an 
 |-  ( ( R e. Ring /\ R e. oGrp /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) <-> ( ( R e. Ring /\ R e. oGrp ) /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )
65 6 63 64 3bitr4i 
 |-  ( R e. oRing <-> ( R e. Ring /\ R e. oGrp /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) )