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 ) )