Metamath Proof Explorer

Theorem orngrmulle

Description: In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018)

Ref Expression
Hypotheses ornglmullt.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ornglmullt.t ⊢ · = ( .r ‘ 𝑅 )
ornglmullt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
ornglmullt.1 ⊢ ( 𝜑 → 𝑅 ∈ oRing )
ornglmullt.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ornglmullt.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
ornglmullt.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
orngmulle.l ⊢ ≤ = ( le ‘ 𝑅 )
orngmulle.5 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
orngmulle.6 ⊢ ( 𝜑 → 0 ≤ 𝑍 )
Assertion orngrmulle ( 𝜑 → ( 𝑋 · 𝑍 ) ≤ ( 𝑌 · 𝑍 ) )

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 orngmulle.l ⊢ ≤ = ( le ‘ 𝑅 )
9 orngmulle.5 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
10 orngmulle.6 ⊢ ( 𝜑 → 0 ≤ 𝑍 )
11 orngogrp ⊢ ( 𝑅 ∈ oRing → 𝑅 ∈ oGrp )
12 4 11 syl ⊢ ( 𝜑 → 𝑅 ∈ oGrp )
13 isogrp ⊢ ( 𝑅 ∈ oGrp ↔ ( 𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd ) )
14 13 simprbi ⊢ ( 𝑅 ∈ oGrp → 𝑅 ∈ oMnd )
15 12 14 syl ⊢ ( 𝜑 → 𝑅 ∈ oMnd )
16 orngring ⊢ ( 𝑅 ∈ oRing → 𝑅 ∈ Ring )
17 4 16 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
18 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
19 17 18 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
20 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
21 19 20 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
22 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
23 17 6 7 22 syl3anc ⊢ ( 𝜑 → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
24 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
25 17 5 7 24 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
26 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
27 1 26 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑌 · 𝑍 ) ∈ 𝐵 ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) → ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ∈ 𝐵 )
28 19 23 25 27 syl3anc ⊢ ( 𝜑 → ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ∈ 𝐵 )
29 1 26 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 )
30 19 6 5 29 syl3anc ⊢ ( 𝜑 → ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 )
31 1 3 26 grpsubid ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝑅 ) 𝑋 ) = 0 )
32 19 5 31 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑅 ) 𝑋 ) = 0 )
33 1 8 26 ogrpsub ⊢ ( ( 𝑅 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( -g ‘ 𝑅 ) 𝑋 ) ≤ ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) )
34 12 5 6 5 9 33 syl131anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑅 ) 𝑋 ) ≤ ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) )
35 32 34 eqbrtrrd ⊢ ( 𝜑 → 0 ≤ ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) )
36 1 8 3 2 orngmul ⊢ ( ( 𝑅 ∈ oRing ∧ ( ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 ∧ 0 ≤ ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) ) ∧ ( 𝑍 ∈ 𝐵 ∧ 0 ≤ 𝑍 ) ) → 0 ≤ ( ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) · 𝑍 ) )
37 4 30 35 7 10 36 syl122anc ⊢ ( 𝜑 → 0 ≤ ( ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) · 𝑍 ) )
38 1 2 26 17 6 5 7 rngsubdir ⊢ ( 𝜑 → ( ( 𝑌 ( -g ‘ 𝑅 ) 𝑋 ) · 𝑍 ) = ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) )
39 37 38 breqtrd ⊢ ( 𝜑 → 0 ≤ ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) )
40 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
41 1 8 40 omndadd ⊢ ( ( 𝑅 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ∈ 𝐵 ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) ∧ 0 ≤ ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ≤ ( ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) )
42 15 21 28 25 39 41 syl131anc ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ≤ ( ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) )
43 1 40 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = ( 𝑋 · 𝑍 ) )
44 19 25 43 syl2anc ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = ( 𝑋 · 𝑍 ) )
45 1 40 26 grpnpcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑌 · 𝑍 ) ∈ 𝐵 ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) → ( ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = ( 𝑌 · 𝑍 ) )
46 19 23 25 45 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑌 · 𝑍 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = ( 𝑌 · 𝑍 ) )
47 42 44 46 3brtr3d ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) ≤ ( 𝑌 · 𝑍 ) )