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	$⊢ B = {Base}_{R}$
	ornglmullt.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ornglmullt.0	$⊢ \underset{˙}{0} = 0_{R}$
	ornglmullt.1	$⊢ φ \to R \in oRing$
	ornglmullt.2	$⊢ φ \to X \in B$
	ornglmullt.3	$⊢ φ \to Y \in B$
	ornglmullt.4	$⊢ φ \to Z \in B$
	ornglmullt.l	$⊢ \underset{˙}{<} = <_{R}$
	ornglmullt.d	$⊢ φ \to R \in DivRing$
	ornglmullt.5	$⊢ φ \to X \underset{˙}{<} Y$
	ornglmullt.6	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} Z$
Assertion	orngrmullt	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{<} (Y \underset{˙}{\cdot} Z)$

Proof

Step	Hyp	Ref	Expression
1		ornglmullt.b	$⊢ B = {Base}_{R}$
2		ornglmullt.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ornglmullt.0	$⊢ \underset{˙}{0} = 0_{R}$
4		ornglmullt.1	$⊢ φ \to R \in oRing$
5		ornglmullt.2	$⊢ φ \to X \in B$
6		ornglmullt.3	$⊢ φ \to Y \in B$
7		ornglmullt.4	$⊢ φ \to Z \in B$
8		ornglmullt.l	$⊢ \underset{˙}{<} = <_{R}$
9		ornglmullt.d	$⊢ φ \to R \in DivRing$
10		ornglmullt.5	$⊢ φ \to X \underset{˙}{<} Y$
11		ornglmullt.6	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} Z$
12		eqid	$⊢ \leq_{R} = \leq_{R}$
13	12 8	pltle	$⊢ (R \in oRing \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \leq_{R} Y)$
14	13	imp	$⊢ ((R \in oRing \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \leq_{R} Y$
15	4 5 6 10 14	syl31anc	$⊢ φ \to X \leq_{R} Y$
16		orngring	$⊢ R \in oRing \to R \in Ring$
17	4 16	syl	$⊢ φ \to R \in Ring$
18		ringgrp	$⊢ R \in Ring \to R \in Grp$
19	1 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
20	17 18 19	3syl	$⊢ φ \to \underset{˙}{0} \in B$
21	12 8	pltle	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land Z \in B) \to (\underset{˙}{0} \underset{˙}{<} Z \to \underset{˙}{0} \leq_{R} Z)$
22	21	imp	$⊢ ((R \in oRing \land \underset{˙}{0} \in B \land Z \in B) \land \underset{˙}{0} \underset{˙}{<} Z) \to \underset{˙}{0} \leq_{R} Z$
23	4 20 7 11 22	syl31anc	$⊢ φ \to \underset{˙}{0} \leq_{R} Z$
24	1 2 3 4 5 6 7 12 15 23	orngrmulle	$⊢ φ \to (X \underset{˙}{\cdot} Z) \leq_{R} (Y \underset{˙}{\cdot} Z)$
25		simpr	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
26	25	oveq1d	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to (X \underset{˙}{\cdot} Z) /_{r} (R) Z = (Y \underset{˙}{\cdot} Z) /_{r} (R) Z$
27	8	pltne	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land Z \in B) \to (\underset{˙}{0} \underset{˙}{<} Z \to \underset{˙}{0} \neq Z)$
28	27	imp	$⊢ ((R \in oRing \land \underset{˙}{0} \in B \land Z \in B) \land \underset{˙}{0} \underset{˙}{<} Z) \to \underset{˙}{0} \neq Z$
29	4 20 7 11 28	syl31anc	$⊢ φ \to \underset{˙}{0} \neq Z$
30	29	necomd	$⊢ φ \to Z \neq \underset{˙}{0}$
31		eqid	$⊢ Unit (R) = Unit (R)$
32	1 31 3	drngunit	$⊢ R \in DivRing \to (Z \in Unit (R) \leftrightarrow (Z \in B \land Z \neq \underset{˙}{0}))$
33	32	biimpar	$⊢ (R \in DivRing \land (Z \in B \land Z \neq \underset{˙}{0})) \to Z \in Unit (R)$
34	9 7 30 33	syl12anc	$⊢ φ \to Z \in Unit (R)$
35		eqid	$⊢ /_{r} (R) = /_{r} (R)$
36	1 31 35 2	dvrcan3	$⊢ (R \in Ring \land X \in B \land Z \in Unit (R)) \to (X \underset{˙}{\cdot} Z) /_{r} (R) Z = X$
37	17 5 34 36	syl3anc	$⊢ φ \to (X \underset{˙}{\cdot} Z) /_{r} (R) Z = X$
38	37	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to (X \underset{˙}{\cdot} Z) /_{r} (R) Z = X$
39	1 31 35 2	dvrcan3	$⊢ (R \in Ring \land Y \in B \land Z \in Unit (R)) \to (Y \underset{˙}{\cdot} Z) /_{r} (R) Z = Y$
40	17 6 34 39	syl3anc	$⊢ φ \to (Y \underset{˙}{\cdot} Z) /_{r} (R) Z = Y$
41	40	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to (Y \underset{˙}{\cdot} Z) /_{r} (R) Z = Y$
42	26 38 41	3eqtr3d	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to X = Y$
43	8	pltne	$⊢ (R \in oRing \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \neq Y)$
44	43	imp	$⊢ ((R \in oRing \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \neq Y$
45	4 5 6 10 44	syl31anc	$⊢ φ \to X \neq Y$
46	45	adantr	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to X \neq Y$
47	46	neneqd	$⊢ (φ \land X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z) \to \neg X = Y$
48	42 47	pm2.65da	$⊢ φ \to \neg X \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
49	48	neqned	$⊢ φ \to X \underset{˙}{\cdot} Z \neq Y \underset{˙}{\cdot} Z$
50	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
51	17 5 7 50	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
52	1 2	ringcl	$⊢ (R \in Ring \land Y \in B \land Z \in B) \to Y \underset{˙}{\cdot} Z \in B$
53	17 6 7 52	syl3anc	$⊢ φ \to Y \underset{˙}{\cdot} Z \in B$
54	12 8	pltval	$⊢ (R \in oRing \land X \underset{˙}{\cdot} Z \in B \land Y \underset{˙}{\cdot} Z \in B) \to ((X \underset{˙}{\cdot} Z) \underset{˙}{<} (Y \underset{˙}{\cdot} Z) \leftrightarrow ((X \underset{˙}{\cdot} Z) \leq_{R} (Y \underset{˙}{\cdot} Z) \land X \underset{˙}{\cdot} Z \neq Y \underset{˙}{\cdot} Z))$
55	4 51 53 54	syl3anc	$⊢ φ \to ((X \underset{˙}{\cdot} Z) \underset{˙}{<} (Y \underset{˙}{\cdot} Z) \leftrightarrow ((X \underset{˙}{\cdot} Z) \leq_{R} (Y \underset{˙}{\cdot} Z) \land X \underset{˙}{\cdot} Z \neq Y \underset{˙}{\cdot} Z))$
56	24 49 55	mpbir2and	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{<} (Y \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem orngrmullt

Proof