Theorem orngrmulle

Description: In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-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$$
	orngmulle.l	$$⊢\underset{\dot{}}{\le }={\le }_R$$
	orngmulle.5	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
	orngmulle.6	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }Z$$
Assertion	orngrmulle	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{·}Z\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		orngmulle.l	$$⊢\underset{\dot{}}{\le }={\le }_R$$
9		orngmulle.5	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
10		orngmulle.6	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }Z$$
11		orngogrp	$$⊢R\in \mathrm{oRing}\to R\in \mathrm{oGrp}$$
12	4 11	syl	$$⊢\phi \to R\in \mathrm{oGrp}$$
13		isogrp	$$⊢R\in \mathrm{oGrp}\leftrightarrow \left(R\in \mathrm{Grp}\wedge R\in \mathrm{oMnd}\right)$$
14	13	simprbi	$$⊢R\in \mathrm{oGrp}\to R\in \mathrm{oMnd}$$
15	12 14	syl	$$⊢\phi \to R\in \mathrm{oMnd}$$
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	17 18	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
20	1 3	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
21	19 20	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
22	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{·}Z\in B$$
23	17 6 7 22	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{·}Z\in B$$
24	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Z\in B\right)\to X\underset{\dot{}}{·}Z\in B$$
25	17 5 7 24	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Z\in B$$
26		eqid	$$⊢{-}_R={-}_R$$
27	1 26	grpsubcl	$$⊢\left(R\in \mathrm{Grp}\wedge Y\underset{\dot{}}{·}Z\in B\wedge X\underset{\dot{}}{·}Z\in B\right)\to \left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\in B$$
28	19 23 25 27	syl3anc	$$⊢\phi \to \left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\in B$$
29	1 26	grpsubcl	$$⊢\left(R\in \mathrm{Grp}\wedge Y\in B\wedge X\in B\right)\to Y{-}_{R}X\in B$$
30	19 6 5 29	syl3anc	$$⊢\phi \to Y{-}_{R}X\in B$$
31	1 3 26	grpsubid	$$⊢\left(R\in \mathrm{Grp}\wedge X\in B\right)\to X{-}_{R}X=\underset{\dot{}}{0}$$
32	19 5 31	syl2anc	$$⊢\phi \to X{-}_{R}X=\underset{\dot{}}{0}$$
33	1 8 26	ogrpsub	$$⊢\left(R\in \mathrm{oGrp}\wedge \left(X\in B\wedge Y\in B\wedge X\in B\right)\wedge X\underset{\dot{}}{\le }Y\right)\to \left(X{-}_{R}X\right)\underset{\dot{}}{\le }\left(Y{-}_{R}X\right)$$
34	12 5 6 5 9 33	syl131anc	$$⊢\phi \to \left(X{-}_{R}X\right)\underset{\dot{}}{\le }\left(Y{-}_{R}X\right)$$
35	32 34	eqbrtrrd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(Y{-}_{R}X\right)$$
36	1 8 3 2	orngmul	$$⊢\left(R\in \mathrm{oRing}\wedge \left(Y{-}_{R}X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(Y{-}_{R}X\right)\right)\wedge \left(Z\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Z\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(Y{-}_{R}X\right)\underset{\dot{}}{·}Z\right)$$
37	4 30 35 7 10 36	syl122anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(Y{-}_{R}X\right)\underset{\dot{}}{·}Z\right)$$
38	1 2 26 17 6 5 7	rngsubdir	$$⊢\phi \to \left(Y{-}_{R}X\right)\underset{\dot{}}{·}Z=\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)$$
39	37 38	breqtrd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\right)$$
40		eqid	$$⊢{+}_R={+}_R$$
41	1 8 40	omndadd	$$⊢\left(R\in \mathrm{oMnd}\wedge \left(\underset{\dot{}}{0}\in B\wedge \left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\in B\wedge X\underset{\dot{}}{·}Z\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\right)\right)\to \left(\underset{\dot{}}{0}{+}_R\left(X\underset{\dot{}}{·}Z\right)\right)\underset{\dot{}}{\le }\left(\left(\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\right){+}_R\left(X\underset{\dot{}}{·}Z\right)\right)$$
42	15 21 28 25 39 41	syl131anc	$$⊢\phi \to \left(\underset{\dot{}}{0}{+}_R\left(X\underset{\dot{}}{·}Z\right)\right)\underset{\dot{}}{\le }\left(\left(\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\right){+}_R\left(X\underset{\dot{}}{·}Z\right)\right)$$
43	1 40 3	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge X\underset{\dot{}}{·}Z\in B\right)\to \underset{\dot{}}{0}{+}_R\left(X\underset{\dot{}}{·}Z\right)=X\underset{\dot{}}{·}Z$$
44	19 25 43	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{+}_R\left(X\underset{\dot{}}{·}Z\right)=X\underset{\dot{}}{·}Z$$
45	1 40 26	grpnpcan	$$⊢\left(R\in \mathrm{Grp}\wedge Y\underset{\dot{}}{·}Z\in B\wedge X\underset{\dot{}}{·}Z\in B\right)\to \left(\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\right){+}_R\left(X\underset{\dot{}}{·}Z\right)=Y\underset{\dot{}}{·}Z$$
46	19 23 25 45	syl3anc	$$⊢\phi \to \left(\left(Y\underset{\dot{}}{·}Z\right){-}_R\left(X\underset{\dot{}}{·}Z\right)\right){+}_R\left(X\underset{\dot{}}{·}Z\right)=Y\underset{\dot{}}{·}Z$$
47	42 44 46	3brtr3d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{·}Z\right)$$