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

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

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 ornglmulle ⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) ( le ‘ 𝑅 ) ( 𝑍 · 𝑌 ) )
25 simpr ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) )
26 25 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) )
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 ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
36 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
37 31 35 2 36 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) = ( 1r ‘ 𝑅 ) )
38 17 34 37 syl2anc ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) = ( 1r ‘ 𝑅 ) )
39 38 oveq1d ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
40 31 35 1 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
41 17 34 40 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
42 1 2 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) )
43 17 41 7 5 42 syl13anc ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) )
44 1 2 36 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
45 17 5 44 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
46 39 43 45 3eqtr3d ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) = 𝑋 )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) = 𝑋 )
48 38 oveq1d ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑌 ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
49 1 2 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) )
50 17 41 7 6 49 syl13anc ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) )
51 1 2 36 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
52 17 6 51 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
53 48 50 52 3eqtr3d ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) = 𝑌 )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) = 𝑌 )
55 26 47 54 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → 𝑋 = 𝑌 )
56 8 pltne ⊢ ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → 𝑋 ≠ 𝑌 ) )
57 56 imp ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ≠ 𝑌 )
58 4 5 6 10 57 syl31anc ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
59 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → 𝑋 ≠ 𝑌 )
60 59 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) → ¬ 𝑋 = 𝑌 )
61 55 60 pm2.65da ⊢ ( 𝜑 → ¬ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) )
62 61 neqned ⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) ≠ ( 𝑍 · 𝑌 ) )
63 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑍 · 𝑋 ) ∈ 𝐵 )
64 17 7 5 63 syl3anc ⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) ∈ 𝐵 )
65 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 · 𝑌 ) ∈ 𝐵 )
66 17 7 6 65 syl3anc ⊢ ( 𝜑 → ( 𝑍 · 𝑌 ) ∈ 𝐵 )
67 12 8 pltval ⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑍 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑍 · 𝑌 ) ∈ 𝐵 ) → ( ( 𝑍 · 𝑋 ) < ( 𝑍 · 𝑌 ) ↔ ( ( 𝑍 · 𝑋 ) ( le ‘ 𝑅 ) ( 𝑍 · 𝑌 ) ∧ ( 𝑍 · 𝑋 ) ≠ ( 𝑍 · 𝑌 ) ) ) )
68 4 64 66 67 syl3anc ⊢ ( 𝜑 → ( ( 𝑍 · 𝑋 ) < ( 𝑍 · 𝑌 ) ↔ ( ( 𝑍 · 𝑋 ) ( le ‘ 𝑅 ) ( 𝑍 · 𝑌 ) ∧ ( 𝑍 · 𝑋 ) ≠ ( 𝑍 · 𝑌 ) ) ) )
69 24 62 68 mpbir2and ⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) < ( 𝑍 · 𝑌 ) )