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 𝐵 = ( Base ‘ 𝑅 )
ornglmullt.t · = ( .r𝑅 )
ornglmullt.0 0 = ( 0g𝑅 )
ornglmullt.1 ( 𝜑𝑅 ∈ oRing )
ornglmullt.2 ( 𝜑𝑋𝐵 )
ornglmullt.3 ( 𝜑𝑌𝐵 )
ornglmullt.4 ( 𝜑𝑍𝐵 )
ornglmullt.l < = ( lt ‘ 𝑅 )
ornglmullt.d ( 𝜑𝑅 ∈ DivRing )
ornglmullt.5 ( 𝜑𝑋 < 𝑌 )
ornglmullt.6 ( 𝜑0 < 𝑍 )
Assertion orngrmullt ( 𝜑 → ( 𝑋 · 𝑍 ) < ( 𝑌 · 𝑍 ) )

Proof

Step Hyp Ref Expression
1 ornglmullt.b 𝐵 = ( Base ‘ 𝑅 )
2 ornglmullt.t · = ( .r𝑅 )
3 ornglmullt.0 0 = ( 0g𝑅 )
4 ornglmullt.1 ( 𝜑𝑅 ∈ oRing )
5 ornglmullt.2 ( 𝜑𝑋𝐵 )
6 ornglmullt.3 ( 𝜑𝑌𝐵 )
7 ornglmullt.4 ( 𝜑𝑍𝐵 )
8 ornglmullt.l < = ( lt ‘ 𝑅 )
9 ornglmullt.d ( 𝜑𝑅 ∈ DivRing )
10 ornglmullt.5 ( 𝜑𝑋 < 𝑌 )
11 ornglmullt.6 ( 𝜑0 < 𝑍 )
12 eqid ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
13 12 8 pltle ( ( 𝑅 ∈ oRing ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 < 𝑌𝑋 ( le ‘ 𝑅 ) 𝑌 ) )
14 13 imp ( ( ( 𝑅 ∈ oRing ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ( le ‘ 𝑅 ) 𝑌 )
15 4 5 6 10 14 syl31anc ( 𝜑𝑋 ( le ‘ 𝑅 ) 𝑌 )
16 orngring ( 𝑅 ∈ oRing → 𝑅 ∈ Ring )
17 4 16 syl ( 𝜑𝑅 ∈ Ring )
18 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
19 1 3 grpidcl ( 𝑅 ∈ Grp → 0𝐵 )
20 17 18 19 3syl ( 𝜑0𝐵 )
21 12 8 pltle ( ( 𝑅 ∈ oRing ∧ 0𝐵𝑍𝐵 ) → ( 0 < 𝑍0 ( le ‘ 𝑅 ) 𝑍 ) )
22 21 imp ( ( ( 𝑅 ∈ oRing ∧ 0𝐵𝑍𝐵 ) ∧ 0 < 𝑍 ) → 0 ( le ‘ 𝑅 ) 𝑍 )
23 4 20 7 11 22 syl31anc ( 𝜑0 ( le ‘ 𝑅 ) 𝑍 )
24 1 2 3 4 5 6 7 12 15 23 orngrmulle ( 𝜑 → ( 𝑋 · 𝑍 ) ( le ‘ 𝑅 ) ( 𝑌 · 𝑍 ) )
25 simpr ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
26 25 oveq1d ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → ( ( 𝑋 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = ( ( 𝑌 · 𝑍 ) ( /r𝑅 ) 𝑍 ) )
27 8 pltne ( ( 𝑅 ∈ oRing ∧ 0𝐵𝑍𝐵 ) → ( 0 < 𝑍0𝑍 ) )
28 27 imp ( ( ( 𝑅 ∈ oRing ∧ 0𝐵𝑍𝐵 ) ∧ 0 < 𝑍 ) → 0𝑍 )
29 4 20 7 11 28 syl31anc ( 𝜑0𝑍 )
30 29 necomd ( 𝜑𝑍0 )
31 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
32 1 31 3 drngunit ( 𝑅 ∈ DivRing → ( 𝑍 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑍𝐵𝑍0 ) ) )
33 32 biimpar ( ( 𝑅 ∈ DivRing ∧ ( 𝑍𝐵𝑍0 ) ) → 𝑍 ∈ ( Unit ‘ 𝑅 ) )
34 9 7 30 33 syl12anc ( 𝜑𝑍 ∈ ( Unit ‘ 𝑅 ) )
35 eqid ( /r𝑅 ) = ( /r𝑅 )
36 1 31 35 2 dvrcan3 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵𝑍 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑋 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = 𝑋 )
37 17 5 34 36 syl3anc ( 𝜑 → ( ( 𝑋 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = 𝑋 )
38 37 adantr ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → ( ( 𝑋 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = 𝑋 )
39 1 31 35 2 dvrcan3 ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑍 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑌 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = 𝑌 )
40 17 6 34 39 syl3anc ( 𝜑 → ( ( 𝑌 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = 𝑌 )
41 40 adantr ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → ( ( 𝑌 · 𝑍 ) ( /r𝑅 ) 𝑍 ) = 𝑌 )
42 26 38 41 3eqtr3d ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → 𝑋 = 𝑌 )
43 8 pltne ( ( 𝑅 ∈ oRing ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 < 𝑌𝑋𝑌 ) )
44 43 imp ( ( ( 𝑅 ∈ oRing ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋𝑌 )
45 4 5 6 10 44 syl31anc ( 𝜑𝑋𝑌 )
46 45 adantr ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → 𝑋𝑌 )
47 46 neneqd ( ( 𝜑 ∧ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) → ¬ 𝑋 = 𝑌 )
48 42 47 pm2.65da ( 𝜑 → ¬ ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
49 48 neqned ( 𝜑 → ( 𝑋 · 𝑍 ) ≠ ( 𝑌 · 𝑍 ) )
50 1 2 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵𝑍𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
51 17 5 7 50 syl3anc ( 𝜑 → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
52 1 2 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑍𝐵 ) → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
53 17 6 7 52 syl3anc ( 𝜑 → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
54 12 8 pltval ( ( 𝑅 ∈ oRing ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 · 𝑍 ) < ( 𝑌 · 𝑍 ) ↔ ( ( 𝑋 · 𝑍 ) ( le ‘ 𝑅 ) ( 𝑌 · 𝑍 ) ∧ ( 𝑋 · 𝑍 ) ≠ ( 𝑌 · 𝑍 ) ) ) )
55 4 51 53 54 syl3anc ( 𝜑 → ( ( 𝑋 · 𝑍 ) < ( 𝑌 · 𝑍 ) ↔ ( ( 𝑋 · 𝑍 ) ( le ‘ 𝑅 ) ( 𝑌 · 𝑍 ) ∧ ( 𝑋 · 𝑍 ) ≠ ( 𝑌 · 𝑍 ) ) ) )
56 24 49 55 mpbir2and ( 𝜑 → ( 𝑋 · 𝑍 ) < ( 𝑌 · 𝑍 ) )