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	$⊢ 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	ornglmullt	$⊢ φ \to (Z \underset{˙}{\cdot} X) \underset{˙}{<} (Z \underset{˙}{\cdot} Y)$

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	ornglmulle	$⊢ φ \to (Z \underset{˙}{\cdot} X) \leq_{R} (Z \underset{˙}{\cdot} Y)$
25		simpr	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y$
26	25	oveq2d	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} X) = {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
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	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
36		eqid	$⊢ 1_{R} = 1_{R}$
37	31 35 2 36	unitlinv	$⊢ (R \in Ring \land Z \in Unit (R)) \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} Z = 1_{R}$
38	17 34 37	syl2anc	$⊢ φ \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} Z = 1_{R}$
39	38	oveq1d	$⊢ φ \to ({inv}_{r} (R) (Z) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} X$
40	31 35 1	ringinvcl	$⊢ (R \in Ring \land Z \in Unit (R)) \to {inv}_{r} (R) (Z) \in B$
41	17 34 40	syl2anc	$⊢ φ \to {inv}_{r} (R) (Z) \in B$
42	1 2	ringass	$⊢ (R \in Ring \land ({inv}_{r} (R) (Z) \in B \land Z \in B \land X \in B)) \to ({inv}_{r} (R) (Z) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} X = {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} X)$
43	17 41 7 5 42	syl13anc	$⊢ φ \to ({inv}_{r} (R) (Z) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} X = {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} X)$
44	1 2 36	ringlidm	$⊢ (R \in Ring \land X \in B) \to 1_{R} \underset{˙}{\cdot} X = X$
45	17 5 44	syl2anc	$⊢ φ \to 1_{R} \underset{˙}{\cdot} X = X$
46	39 43 45	3eqtr3d	$⊢ φ \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} X) = X$
47	46	adantr	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} X) = X$
48	38	oveq1d	$⊢ φ \to ({inv}_{r} (R) (Z) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y = 1_{R} \underset{˙}{\cdot} Y$
49	1 2	ringass	$⊢ (R \in Ring \land ({inv}_{r} (R) (Z) \in B \land Z \in B \land Y \in B)) \to ({inv}_{r} (R) (Z) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y = {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
50	17 41 7 6 49	syl13anc	$⊢ φ \to ({inv}_{r} (R) (Z) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y = {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
51	1 2 36	ringlidm	$⊢ (R \in Ring \land Y \in B) \to 1_{R} \underset{˙}{\cdot} Y = Y$
52	17 6 51	syl2anc	$⊢ φ \to 1_{R} \underset{˙}{\cdot} Y = Y$
53	48 50 52	3eqtr3d	$⊢ φ \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) = Y$
54	53	adantr	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to {inv}_{r} (R) (Z) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) = Y$
55	26 47 54	3eqtr3d	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to X = Y$
56	8	pltne	$⊢ (R \in oRing \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \neq Y)$
57	56	imp	$⊢ ((R \in oRing \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \neq Y$
58	4 5 6 10 57	syl31anc	$⊢ φ \to X \neq Y$
59	58	adantr	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to X \neq Y$
60	59	neneqd	$⊢ (φ \land Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y) \to \neg X = Y$
61	55 60	pm2.65da	$⊢ φ \to \neg Z \underset{˙}{\cdot} X = Z \underset{˙}{\cdot} Y$
62	61	neqned	$⊢ φ \to Z \underset{˙}{\cdot} X \neq Z \underset{˙}{\cdot} Y$
63	1 2	ringcl	$⊢ (R \in Ring \land Z \in B \land X \in B) \to Z \underset{˙}{\cdot} X \in B$
64	17 7 5 63	syl3anc	$⊢ φ \to Z \underset{˙}{\cdot} X \in B$
65	1 2	ringcl	$⊢ (R \in Ring \land Z \in B \land Y \in B) \to Z \underset{˙}{\cdot} Y \in B$
66	17 7 6 65	syl3anc	$⊢ φ \to Z \underset{˙}{\cdot} Y \in B$
67	12 8	pltval	$⊢ (R \in oRing \land Z \underset{˙}{\cdot} X \in B \land Z \underset{˙}{\cdot} Y \in B) \to ((Z \underset{˙}{\cdot} X) \underset{˙}{<} (Z \underset{˙}{\cdot} Y) \leftrightarrow ((Z \underset{˙}{\cdot} X) \leq_{R} (Z \underset{˙}{\cdot} Y) \land Z \underset{˙}{\cdot} X \neq Z \underset{˙}{\cdot} Y))$
68	4 64 66 67	syl3anc	$⊢ φ \to ((Z \underset{˙}{\cdot} X) \underset{˙}{<} (Z \underset{˙}{\cdot} Y) \leftrightarrow ((Z \underset{˙}{\cdot} X) \leq_{R} (Z \underset{˙}{\cdot} Y) \land Z \underset{˙}{\cdot} X \neq Z \underset{˙}{\cdot} Y))$
69	24 62 68	mpbir2and	$⊢ φ \to (Z \underset{˙}{\cdot} X) \underset{˙}{<} (Z \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem ornglmullt

Proof