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