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 ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) < ( 𝑌 · 𝑍 ) )