This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orngrmullt

Description: In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-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 )
ornglmullt.l 
|- .< = ( lt ` R )
ornglmullt.d 
|- ( ph -> R e. DivRing )
ornglmullt.5 
|- ( ph -> X .< Y )
ornglmullt.6 
|- ( ph -> .0. .< Z )
Assertion orngrmullt 
|- ( 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 ornglmullt.l 
 |-  .< = ( lt ` R )
9 ornglmullt.d 
 |-  ( ph -> R e. DivRing )
10 ornglmullt.5 
 |-  ( ph -> X .< Y )
11 ornglmullt.6 
 |-  ( ph -> .0. .< Z )
12 eqid 
 |-  ( le ` R ) = ( le ` R )
13 12 8 pltle 
 |-  ( ( R e. oRing /\ X e. B /\ Y e. B ) -> ( X .< Y -> X ( le ` R ) Y ) )
14 13 imp 
 |-  ( ( ( R e. oRing /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X ( le ` R ) Y )
15 4 5 6 10 14 syl31anc 
 |-  ( ph -> X ( le ` R ) Y )
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 1 3 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
20 17 18 19 3syl 
 |-  ( ph -> .0. e. B )
21 12 8 pltle 
 |-  ( ( R e. oRing /\ .0. e. B /\ Z e. B ) -> ( .0. .< Z -> .0. ( le ` R ) Z ) )
22 21 imp 
 |-  ( ( ( R e. oRing /\ .0. e. B /\ Z e. B ) /\ .0. .< Z ) -> .0. ( le ` R ) Z )
23 4 20 7 11 22 syl31anc 
 |-  ( ph -> .0. ( le ` R ) Z )
24 1 2 3 4 5 6 7 12 15 23 orngrmulle 
 |-  ( ph -> ( X .x. Z ) ( le ` R ) ( Y .x. Z ) )
25 simpr 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> ( X .x. Z ) = ( Y .x. Z ) )
26 25 oveq1d 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> ( ( X .x. Z ) ( /r ` R ) Z ) = ( ( Y .x. Z ) ( /r ` R ) Z ) )
27 8 pltne 
 |-  ( ( R e. oRing /\ .0. e. B /\ Z e. B ) -> ( .0. .< Z -> .0. =/= Z ) )
28 27 imp 
 |-  ( ( ( R e. oRing /\ .0. e. B /\ Z e. B ) /\ .0. .< Z ) -> .0. =/= Z )
29 4 20 7 11 28 syl31anc 
 |-  ( ph -> .0. =/= Z )
30 29 necomd 
 |-  ( ph -> Z =/= .0. )
31 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
32 1 31 3 drngunit 
 |-  ( R e. DivRing -> ( Z e. ( Unit ` R ) <-> ( Z e. B /\ Z =/= .0. ) ) )
33 32 biimpar 
 |-  ( ( R e. DivRing /\ ( Z e. B /\ Z =/= .0. ) ) -> Z e. ( Unit ` R ) )
34 9 7 30 33 syl12anc 
 |-  ( ph -> Z e. ( Unit ` R ) )
35 eqid 
 |-  ( /r ` R ) = ( /r ` R )
36 1 31 35 2 dvrcan3 
 |-  ( ( R e. Ring /\ X e. B /\ Z e. ( Unit ` R ) ) -> ( ( X .x. Z ) ( /r ` R ) Z ) = X )
37 17 5 34 36 syl3anc 
 |-  ( ph -> ( ( X .x. Z ) ( /r ` R ) Z ) = X )
38 37 adantr 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> ( ( X .x. Z ) ( /r ` R ) Z ) = X )
39 1 31 35 2 dvrcan3 
 |-  ( ( R e. Ring /\ Y e. B /\ Z e. ( Unit ` R ) ) -> ( ( Y .x. Z ) ( /r ` R ) Z ) = Y )
40 17 6 34 39 syl3anc 
 |-  ( ph -> ( ( Y .x. Z ) ( /r ` R ) Z ) = Y )
41 40 adantr 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> ( ( Y .x. Z ) ( /r ` R ) Z ) = Y )
42 26 38 41 3eqtr3d 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> X = Y )
43 8 pltne 
 |-  ( ( R e. oRing /\ X e. B /\ Y e. B ) -> ( X .< Y -> X =/= Y ) )
44 43 imp 
 |-  ( ( ( R e. oRing /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X =/= Y )
45 4 5 6 10 44 syl31anc 
 |-  ( ph -> X =/= Y )
46 45 adantr 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> X =/= Y )
47 46 neneqd 
 |-  ( ( ph /\ ( X .x. Z ) = ( Y .x. Z ) ) -> -. X = Y )
48 42 47 pm2.65da 
 |-  ( ph -> -. ( X .x. Z ) = ( Y .x. Z ) )
49 48 neqned 
 |-  ( ph -> ( X .x. Z ) =/= ( Y .x. Z ) )
50 1 2 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Z e. B ) -> ( X .x. Z ) e. B )
51 17 5 7 50 syl3anc 
 |-  ( ph -> ( X .x. Z ) e. B )
52 1 2 ringcl 
 |-  ( ( R e. Ring /\ Y e. B /\ Z e. B ) -> ( Y .x. Z ) e. B )
53 17 6 7 52 syl3anc 
 |-  ( ph -> ( Y .x. Z ) e. B )
54 12 8 pltval 
 |-  ( ( R e. oRing /\ ( X .x. Z ) e. B /\ ( Y .x. Z ) e. B ) -> ( ( X .x. Z ) .< ( Y .x. Z ) <-> ( ( X .x. Z ) ( le ` R ) ( Y .x. Z ) /\ ( X .x. Z ) =/= ( Y .x. Z ) ) ) )
55 4 51 53 54 syl3anc 
 |-  ( ph -> ( ( X .x. Z ) .< ( Y .x. Z ) <-> ( ( X .x. Z ) ( le ` R ) ( Y .x. Z ) /\ ( X .x. Z ) =/= ( Y .x. Z ) ) ) )
56 24 49 55 mpbir2and 
 |-  ( ph -> ( X .x. Z ) .< ( Y .x. Z ) )