Metamath Proof Explorer

Theorem orngrmulle

Description: In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018)

Ref Expression
Hypotheses ornglmullt.b 
|- B = ( Base ` R )
ornglmullt.t 
|- .x. = ( .r ` R )
ornglmullt.0 
|- .0. = ( 0g ` R )
ornglmullt.1 
|- ( ph -> R e. oRing )
ornglmullt.2 
|- ( ph -> X e. B )
ornglmullt.3 
|- ( ph -> Y e. B )
ornglmullt.4 
|- ( ph -> Z e. B )
orngmulle.l 
|- .<_ = ( le ` R )
orngmulle.5 
|- ( ph -> X .<_ Y )
orngmulle.6 
|- ( ph -> .0. .<_ Z )
Assertion orngrmulle 
|- ( ph -> ( X .x. Z ) .<_ ( Y .x. Z ) )

Proof

Step Hyp Ref Expression
1 ornglmullt.b 
 |-  B = ( Base ` R )
2 ornglmullt.t 
 |-  .x. = ( .r ` R )
3 ornglmullt.0 
 |-  .0. = ( 0g ` R )
4 ornglmullt.1 
 |-  ( ph -> R e. oRing )
5 ornglmullt.2 
 |-  ( ph -> X e. B )
6 ornglmullt.3 
 |-  ( ph -> Y e. B )
7 ornglmullt.4 
 |-  ( ph -> Z e. B )
8 orngmulle.l 
 |-  .<_ = ( le ` R )
9 orngmulle.5 
 |-  ( ph -> X .<_ Y )
10 orngmulle.6 
 |-  ( ph -> .0. .<_ Z )
11 orngogrp 
 |-  ( R e. oRing -> R e. oGrp )
12 4 11 syl 
 |-  ( ph -> R e. oGrp )
13 isogrp 
 |-  ( R e. oGrp <-> ( R e. Grp /\ R e. oMnd ) )
14 13 simprbi 
 |-  ( R e. oGrp -> R e. oMnd )
15 12 14 syl 
 |-  ( ph -> R e. oMnd )
16 orngring 
 |-  ( R e. oRing -> R e. Ring )
17 4 16 syl 
 |-  ( ph -> R e. Ring )
18 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
19 17 18 syl 
 |-  ( ph -> R e. Grp )
20 1 3 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
21 19 20 syl 
 |-  ( ph -> .0. e. B )
22 1 2 ringcl 
 |-  ( ( R e. Ring /\ Y e. B /\ Z e. B ) -> ( Y .x. Z ) e. B )
23 17 6 7 22 syl3anc 
 |-  ( ph -> ( Y .x. Z ) e. B )
24 1 2 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Z e. B ) -> ( X .x. Z ) e. B )
25 17 5 7 24 syl3anc 
 |-  ( ph -> ( X .x. Z ) e. B )
26 eqid 
 |-  ( -g ` R ) = ( -g ` R )
27 1 26 grpsubcl 
 |-  ( ( R e. Grp /\ ( Y .x. Z ) e. B /\ ( X .x. Z ) e. B ) -> ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) e. B )
28 19 23 25 27 syl3anc 
 |-  ( ph -> ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) e. B )
29 1 26 grpsubcl 
 |-  ( ( R e. Grp /\ Y e. B /\ X e. B ) -> ( Y ( -g ` R ) X ) e. B )
30 19 6 5 29 syl3anc 
 |-  ( ph -> ( Y ( -g ` R ) X ) e. B )
31 1 3 26 grpsubid 
 |-  ( ( R e. Grp /\ X e. B ) -> ( X ( -g ` R ) X ) = .0. )
32 19 5 31 syl2anc 
 |-  ( ph -> ( X ( -g ` R ) X ) = .0. )
33 1 8 26 ogrpsub 
 |-  ( ( R e. oGrp /\ ( X e. B /\ Y e. B /\ X e. B ) /\ X .<_ Y ) -> ( X ( -g ` R ) X ) .<_ ( Y ( -g ` R ) X ) )
34 12 5 6 5 9 33 syl131anc 
 |-  ( ph -> ( X ( -g ` R ) X ) .<_ ( Y ( -g ` R ) X ) )
35 32 34 eqbrtrrd 
 |-  ( ph -> .0. .<_ ( Y ( -g ` R ) X ) )
36 1 8 3 2 orngmul 
 |-  ( ( R e. oRing /\ ( ( Y ( -g ` R ) X ) e. B /\ .0. .<_ ( Y ( -g ` R ) X ) ) /\ ( Z e. B /\ .0. .<_ Z ) ) -> .0. .<_ ( ( Y ( -g ` R ) X ) .x. Z ) )
37 4 30 35 7 10 36 syl122anc 
 |-  ( ph -> .0. .<_ ( ( Y ( -g ` R ) X ) .x. Z ) )
38 1 2 26 17 6 5 7 rngsubdir 
 |-  ( ph -> ( ( Y ( -g ` R ) X ) .x. Z ) = ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) )
39 37 38 breqtrd 
 |-  ( ph -> .0. .<_ ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) )
40 eqid 
 |-  ( +g ` R ) = ( +g ` R )
41 1 8 40 omndadd 
 |-  ( ( R e. oMnd /\ ( .0. e. B /\ ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) e. B /\ ( X .x. Z ) e. B ) /\ .0. .<_ ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) ) -> ( .0. ( +g ` R ) ( X .x. Z ) ) .<_ ( ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) ( +g ` R ) ( X .x. Z ) ) )
42 15 21 28 25 39 41 syl131anc 
 |-  ( ph -> ( .0. ( +g ` R ) ( X .x. Z ) ) .<_ ( ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) ( +g ` R ) ( X .x. Z ) ) )
43 1 40 3 grplid 
 |-  ( ( R e. Grp /\ ( X .x. Z ) e. B ) -> ( .0. ( +g ` R ) ( X .x. Z ) ) = ( X .x. Z ) )
44 19 25 43 syl2anc 
 |-  ( ph -> ( .0. ( +g ` R ) ( X .x. Z ) ) = ( X .x. Z ) )
45 1 40 26 grpnpcan 
 |-  ( ( R e. Grp /\ ( Y .x. Z ) e. B /\ ( X .x. Z ) e. B ) -> ( ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) ( +g ` R ) ( X .x. Z ) ) = ( Y .x. Z ) )
46 19 23 25 45 syl3anc 
 |-  ( ph -> ( ( ( Y .x. Z ) ( -g ` R ) ( X .x. Z ) ) ( +g ` R ) ( X .x. Z ) ) = ( Y .x. Z ) )
47 42 44 46 3brtr3d 
 |-  ( ph -> ( X .x. Z ) .<_ ( Y .x. Z ) )