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