Metamath Proof Explorer

Theorem orngmul

Description: In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Hypotheses orngmul.0 
|- B = ( Base ` R )
orngmul.1 
|- .<_ = ( le ` R )
orngmul.2 
|- .0. = ( 0g ` R )
orngmul.3 
|- .x. = ( .r ` R )
Assertion orngmul 
|- ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> .0. .<_ ( X .x. Y ) )

Proof

Step Hyp Ref Expression
1 orngmul.0 
 |-  B = ( Base ` R )
2 orngmul.1 
 |-  .<_ = ( le ` R )
3 orngmul.2 
 |-  .0. = ( 0g ` R )
4 orngmul.3 
 |-  .x. = ( .r ` R )
5 simp2r 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> .0. .<_ X )
6 simp3r 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> .0. .<_ Y )
7 simp2l 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> X e. B )
8 simp3l 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> Y e. B )
9 1 3 4 2 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 ) ) ) )
10 9 simp3bi 
 |-  ( R e. oRing -> A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) )
11 10 3ad2ant1 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) )
12 breq2 
 |-  ( a = X -> ( .0. .<_ a <-> .0. .<_ X ) )
13 12 anbi1d 
 |-  ( a = X -> ( ( .0. .<_ a /\ .0. .<_ b ) <-> ( .0. .<_ X /\ .0. .<_ b ) ) )
14 oveq1 
 |-  ( a = X -> ( a .x. b ) = ( X .x. b ) )
15 14 breq2d 
 |-  ( a = X -> ( .0. .<_ ( a .x. b ) <-> .0. .<_ ( X .x. b ) ) )
16 13 15 imbi12d 
 |-  ( a = X -> ( ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) <-> ( ( .0. .<_ X /\ .0. .<_ b ) -> .0. .<_ ( X .x. b ) ) ) )
17 breq2 
 |-  ( b = Y -> ( .0. .<_ b <-> .0. .<_ Y ) )
18 17 anbi2d 
 |-  ( b = Y -> ( ( .0. .<_ X /\ .0. .<_ b ) <-> ( .0. .<_ X /\ .0. .<_ Y ) ) )
19 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
20 19 breq2d 
 |-  ( b = Y -> ( .0. .<_ ( X .x. b ) <-> .0. .<_ ( X .x. Y ) ) )
21 18 20 imbi12d 
 |-  ( b = Y -> ( ( ( .0. .<_ X /\ .0. .<_ b ) -> .0. .<_ ( X .x. b ) ) <-> ( ( .0. .<_ X /\ .0. .<_ Y ) -> .0. .<_ ( X .x. Y ) ) ) )
22 16 21 rspc2va 
 |-  ( ( ( X e. B /\ Y e. B ) /\ A. a e. B A. b e. B ( ( .0. .<_ a /\ .0. .<_ b ) -> .0. .<_ ( a .x. b ) ) ) -> ( ( .0. .<_ X /\ .0. .<_ Y ) -> .0. .<_ ( X .x. Y ) ) )
23 7 8 11 22 syl21anc 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> ( ( .0. .<_ X /\ .0. .<_ Y ) -> .0. .<_ ( X .x. Y ) ) )
24 5 6 23 mp2and 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> .0. .<_ ( X .x. Y ) )