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	$$⊢B={\mathrm{Base}}_R$$
	ornglmullt.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ornglmullt.0	$$⊢\underset{\dot{}}{0}=0_R$$
	ornglmullt.1	$$⊢\phi \to R\in \mathrm{oRing}$$
	ornglmullt.2	$$⊢\phi \to X\in B$$
	ornglmullt.3	$$⊢\phi \to Y\in B$$
	ornglmullt.4	$$⊢\phi \to Z\in B$$
	ornglmullt.l	$$⊢\underset{\dot{}}{<}={<}_R$$
	ornglmullt.d	$$⊢\phi \to R\in \mathrm{DivRing}$$
	ornglmullt.5	$$⊢\phi \to X\underset{\dot{}}{<}Y$$
	ornglmullt.6	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}Z$$
Assertion	ornglmullt	$$⊢\phi \to \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ornglmullt.b	$$⊢B={\mathrm{Base}}_R$$
2		ornglmullt.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		ornglmullt.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		ornglmullt.1	$$⊢\phi \to R\in \mathrm{oRing}$$
5		ornglmullt.2	$$⊢\phi \to X\in B$$
6		ornglmullt.3	$$⊢\phi \to Y\in B$$
7		ornglmullt.4	$$⊢\phi \to Z\in B$$
8		ornglmullt.l	$$⊢\underset{\dot{}}{<}={<}_R$$
9		ornglmullt.d	$$⊢\phi \to R\in \mathrm{DivRing}$$
10		ornglmullt.5	$$⊢\phi \to X\underset{\dot{}}{<}Y$$
11		ornglmullt.6	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}Z$$
12		eqid	$$⊢{\le }_R={\le }_R$$
13	12 8	pltle	$$⊢\left(R\in \mathrm{oRing}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to X{\le }_{R}Y\right)$$
14	13	imp	$$⊢\left(\left(R\in \mathrm{oRing}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to X{\le }_{R}Y$$
15	4 5 6 10 14	syl31anc	$$⊢\phi \to X{\le }_{R}Y$$
16		orngring	$$⊢R\in \mathrm{oRing}\to R\in \mathrm{Ring}$$
17	4 16	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
18		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
19	1 3	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
20	17 18 19	3syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
21	12 8	pltle	$$⊢\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge Z\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}Z\to \underset{\dot{}}{0}{\le }_{R}Z\right)$$
22	21	imp	$$⊢\left(\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge Z\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}Z\right)\to \underset{\dot{}}{0}{\le }_{R}Z$$
23	4 20 7 11 22	syl31anc	$$⊢\phi \to \underset{\dot{}}{0}{\le }_{R}Z$$
24	1 2 3 4 5 6 7 12 15 23	ornglmulle	$$⊢\phi \to \left(Z\underset{\dot{}}{·}X\right){\le }_R\left(Z\underset{\dot{}}{·}Y\right)$$
25		simpr	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y$$
26	25	oveq2d	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
27	8	pltne	$$⊢\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge Z\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}Z\to \underset{\dot{}}{0}\ne Z\right)$$
28	27	imp	$$⊢\left(\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge Z\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}Z\right)\to \underset{\dot{}}{0}\ne Z$$
29	4 20 7 11 28	syl31anc	$$⊢\phi \to \underset{\dot{}}{0}\ne Z$$
30	29	necomd	$$⊢\phi \to Z\ne \underset{\dot{}}{0}$$
31		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
32	1 31 3	drngunit	$$⊢R\in \mathrm{DivRing}\to \left(Z\in \mathrm{Unit}\left(R\right)\leftrightarrow \left(Z\in B\wedge Z\ne \underset{\dot{}}{0}\right)\right)$$
33	32	biimpar	$$⊢\left(R\in \mathrm{DivRing}\wedge \left(Z\in B\wedge Z\ne \underset{\dot{}}{0}\right)\right)\to Z\in \mathrm{Unit}\left(R\right)$$
34	9 7 30 33	syl12anc	$$⊢\phi \to Z\in \mathrm{Unit}\left(R\right)$$
35		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
36		eqid	$$⊢1_R=1_R$$
37	31 35 2 36	unitlinv	$$⊢\left(R\in \mathrm{Ring}\wedge Z\in \mathrm{Unit}\left(R\right)\right)\to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z=1_R$$
38	17 34 37	syl2anc	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z=1_R$$
39	38	oveq1d	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}X=1_R\underset{\dot{}}{·}X$$
40	31 35 1	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge Z\in \mathrm{Unit}\left(R\right)\right)\to {inv}_r\left(R\right)\left(Z\right)\in B$$
41	17 34 40	syl2anc	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\in B$$
42	1 2	ringass	$$⊢\left(R\in \mathrm{Ring}\wedge \left({inv}_r\left(R\right)\left(Z\right)\in B\wedge Z\in B\wedge X\in B\right)\right)\to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}X={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)$$
43	17 41 7 5 42	syl13anc	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}X={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)$$
44	1 2 36	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to 1_R\underset{\dot{}}{·}X=X$$
45	17 5 44	syl2anc	$$⊢\phi \to 1_R\underset{\dot{}}{·}X=X$$
46	39 43 45	3eqtr3d	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)=X$$
47	46	adantr	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)=X$$
48	38	oveq1d	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y=1_R\underset{\dot{}}{·}Y$$
49	1 2	ringass	$$⊢\left(R\in \mathrm{Ring}\wedge \left({inv}_r\left(R\right)\left(Z\right)\in B\wedge Z\in B\wedge Y\in B\right)\right)\to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
50	17 41 7 6 49	syl13anc	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
51	1 2 36	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to 1_R\underset{\dot{}}{·}Y=Y$$
52	17 6 51	syl2anc	$$⊢\phi \to 1_R\underset{\dot{}}{·}Y=Y$$
53	48 50 52	3eqtr3d	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)=Y$$
54	53	adantr	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)=Y$$
55	26 47 54	3eqtr3d	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to X=Y$$
56	8	pltne	$$⊢\left(R\in \mathrm{oRing}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to X\ne Y\right)$$
57	56	imp	$$⊢\left(\left(R\in \mathrm{oRing}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to X\ne Y$$
58	4 5 6 10 57	syl31anc	$$⊢\phi \to X\ne Y$$
59	58	adantr	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to X\ne Y$$
60	59	neneqd	$$⊢\left(\phi \wedge Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y\right)\to \neg X=Y$$
61	55 60	pm2.65da	$$⊢\phi \to \neg Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y$$
62	61	neqned	$$⊢\phi \to Z\underset{\dot{}}{·}X\ne Z\underset{\dot{}}{·}Y$$
63	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge Z\in B\wedge X\in B\right)\to Z\underset{\dot{}}{·}X\in B$$
64	17 7 5 63	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{·}X\in B$$
65	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge Z\in B\wedge Y\in B\right)\to Z\underset{\dot{}}{·}Y\in B$$
66	17 7 6 65	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{·}Y\in B$$
67	12 8	pltval	$$⊢\left(R\in \mathrm{oRing}\wedge Z\underset{\dot{}}{·}X\in B\wedge Z\underset{\dot{}}{·}Y\in B\right)\to \left(\left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{·}Y\right)\leftrightarrow \left(\left(Z\underset{\dot{}}{·}X\right){\le }_R\left(Z\underset{\dot{}}{·}Y\right)\wedge Z\underset{\dot{}}{·}X\ne Z\underset{\dot{}}{·}Y\right)\right)$$
68	4 64 66 67	syl3anc	$$⊢\phi \to \left(\left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{·}Y\right)\leftrightarrow \left(\left(Z\underset{\dot{}}{·}X\right){\le }_R\left(Z\underset{\dot{}}{·}Y\right)\wedge Z\underset{\dot{}}{·}X\ne Z\underset{\dot{}}{·}Y\right)\right)$$
69	24 62 68	mpbir2and	$$⊢\phi \to \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{·}Y\right)$$