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