Metamath Proof Explorer

Theorem ornglmullt

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 ornglmullt 
|- ( ph -> ( Z .x. X ) .< ( Z .x. Y ) )

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 ornglmulle 
 |-  ( ph -> ( Z .x. X ) ( le ` R ) ( Z .x. Y ) )
25 simpr 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> ( Z .x. X ) = ( Z .x. Y ) )
26 25 oveq2d 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) )
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 
 |-  ( invr ` R ) = ( invr ` R )
36 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
37 31 35 2 36 unitlinv 
 |-  ( ( R e. Ring /\ Z e. ( Unit ` R ) ) -> ( ( ( invr ` R ) ` Z ) .x. Z ) = ( 1r ` R ) )
38 17 34 37 syl2anc 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. Z ) = ( 1r ` R ) )
39 38 oveq1d 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. X ) = ( ( 1r ` R ) .x. X ) )
40 31 35 1 ringinvcl 
 |-  ( ( R e. Ring /\ Z e. ( Unit ` R ) ) -> ( ( invr ` R ) ` Z ) e. B )
41 17 34 40 syl2anc 
 |-  ( ph -> ( ( invr ` R ) ` Z ) e. B )
42 1 2 ringass 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` Z ) e. B /\ Z e. B /\ X e. B ) ) -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. X ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) )
43 17 41 7 5 42 syl13anc 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. X ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) )
44 1 2 36 ringlidm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( 1r ` R ) .x. X ) = X )
45 17 5 44 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) .x. X ) = X )
46 39 43 45 3eqtr3d 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) = X )
47 46 adantr 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. X ) ) = X )
48 38 oveq1d 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. Y ) = ( ( 1r ` R ) .x. Y ) )
49 1 2 ringass 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` Z ) e. B /\ Z e. B /\ Y e. B ) ) -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. Y ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) )
50 17 41 7 6 49 syl13anc 
 |-  ( ph -> ( ( ( ( invr ` R ) ` Z ) .x. Z ) .x. Y ) = ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) )
51 1 2 36 ringlidm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( ( 1r ` R ) .x. Y ) = Y )
52 17 6 51 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) .x. Y ) = Y )
53 48 50 52 3eqtr3d 
 |-  ( ph -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) = Y )
54 53 adantr 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> ( ( ( invr ` R ) ` Z ) .x. ( Z .x. Y ) ) = Y )
55 26 47 54 3eqtr3d 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> X = Y )
56 8 pltne 
 |-  ( ( R e. oRing /\ X e. B /\ Y e. B ) -> ( X .< Y -> X =/= Y ) )
57 56 imp 
 |-  ( ( ( R e. oRing /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X =/= Y )
58 4 5 6 10 57 syl31anc 
 |-  ( ph -> X =/= Y )
59 58 adantr 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> X =/= Y )
60 59 neneqd 
 |-  ( ( ph /\ ( Z .x. X ) = ( Z .x. Y ) ) -> -. X = Y )
61 55 60 pm2.65da 
 |-  ( ph -> -. ( Z .x. X ) = ( Z .x. Y ) )
62 61 neqned 
 |-  ( ph -> ( Z .x. X ) =/= ( Z .x. Y ) )
63 1 2 ringcl 
 |-  ( ( R e. Ring /\ Z e. B /\ X e. B ) -> ( Z .x. X ) e. B )
64 17 7 5 63 syl3anc 
 |-  ( ph -> ( Z .x. X ) e. B )
65 1 2 ringcl 
 |-  ( ( R e. Ring /\ Z e. B /\ Y e. B ) -> ( Z .x. Y ) e. B )
66 17 7 6 65 syl3anc 
 |-  ( ph -> ( Z .x. Y ) e. B )
67 12 8 pltval 
 |-  ( ( R e. oRing /\ ( Z .x. X ) e. B /\ ( Z .x. Y ) e. B ) -> ( ( Z .x. X ) .< ( Z .x. Y ) <-> ( ( Z .x. X ) ( le ` R ) ( Z .x. Y ) /\ ( Z .x. X ) =/= ( Z .x. Y ) ) ) )
68 4 64 66 67 syl3anc 
 |-  ( ph -> ( ( Z .x. X ) .< ( Z .x. Y ) <-> ( ( Z .x. X ) ( le ` R ) ( Z .x. Y ) /\ ( Z .x. X ) =/= ( Z .x. Y ) ) ) )
69 24 62 68 mpbir2and 
 |-  ( ph -> ( Z .x. X ) .< ( Z .x. Y ) )