Theorem orngmullt

Description: In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	orngmullt.b	$$⊢B={\mathrm{Base}}_R$$
	orngmullt.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	orngmullt.0	$$⊢\underset{\dot{}}{0}=0_R$$
	orngmullt.l	$$⊢\underset{\dot{}}{<}={<}_R$$
	orngmullt.1	$$⊢\phi \to R\in \mathrm{oRing}$$
	orngmullt.4	$$⊢\phi \to R\in \mathrm{DivRing}$$
	orngmullt.2	$$⊢\phi \to X\in B$$
	orngmullt.3	$$⊢\phi \to Y\in B$$
	orngmullt.x	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
	orngmullt.y	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}Y$$
Assertion	orngmullt	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}\left(X\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		orngmullt.b	$$⊢B={\mathrm{Base}}_R$$
2		orngmullt.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		orngmullt.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		orngmullt.l	$$⊢\underset{\dot{}}{<}={<}_R$$
5		orngmullt.1	$$⊢\phi \to R\in \mathrm{oRing}$$
6		orngmullt.4	$$⊢\phi \to R\in \mathrm{DivRing}$$
7		orngmullt.2	$$⊢\phi \to X\in B$$
8		orngmullt.3	$$⊢\phi \to Y\in B$$
9		orngmullt.x	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
10		orngmullt.y	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}Y$$
11		orngring	$$⊢R\in \mathrm{oRing}\to R\in \mathrm{Ring}$$
12		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
13	1 3	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
14	5 11 12 13	4syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
15		eqid	$$⊢{\le }_R={\le }_R$$
16	15 4	pltval	$$⊢\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{R}X\wedge \underset{\dot{}}{0}\ne X\right)\right)$$
17	5 14 7 16	syl3anc	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{R}X\wedge \underset{\dot{}}{0}\ne X\right)\right)$$
18	9 17	mpbid	$$⊢\phi \to \left(\underset{\dot{}}{0}{\le }_{R}X\wedge \underset{\dot{}}{0}\ne X\right)$$
19	18	simpld	$$⊢\phi \to \underset{\dot{}}{0}{\le }_{R}X$$
20	15 4	pltval	$$⊢\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge Y\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}Y\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{R}Y\wedge \underset{\dot{}}{0}\ne Y\right)\right)$$
21	5 14 8 20	syl3anc	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}Y\leftrightarrow \left(\underset{\dot{}}{0}{\le }_{R}Y\wedge \underset{\dot{}}{0}\ne Y\right)\right)$$
22	10 21	mpbid	$$⊢\phi \to \left(\underset{\dot{}}{0}{\le }_{R}Y\wedge \underset{\dot{}}{0}\ne Y\right)$$
23	22	simpld	$$⊢\phi \to \underset{\dot{}}{0}{\le }_{R}Y$$
24	1 15 3 2	orngmul	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}{\le }_{R}X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}{\le }_{R}Y\right)\right)\to \underset{\dot{}}{0}{\le }_R\left(X\underset{\dot{}}{·}Y\right)$$
25	5 7 19 8 23 24	syl122anc	$$⊢\phi \to \underset{\dot{}}{0}{\le }_R\left(X\underset{\dot{}}{·}Y\right)$$
26	18	simprd	$$⊢\phi \to \underset{\dot{}}{0}\ne X$$
27	26	necomd	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
28	22	simprd	$$⊢\phi \to \underset{\dot{}}{0}\ne Y$$
29	28	necomd	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
30	1 3 2 6 7 8	drngmulne0	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\leftrightarrow \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)$$
31	27 29 30	mpbir2and	$$⊢\phi \to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}$$
32	31	necomd	$$⊢\phi \to \underset{\dot{}}{0}\ne X\underset{\dot{}}{·}Y$$
33	5 11	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
34	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
35	33 7 8 34	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
36	15 4	pltval	$$⊢\left(R\in \mathrm{oRing}\wedge \underset{\dot{}}{0}\in B\wedge X\underset{\dot{}}{·}Y\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}\left(X\underset{\dot{}}{·}Y\right)\leftrightarrow \left(\underset{\dot{}}{0}{\le }_R\left(X\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{0}\ne X\underset{\dot{}}{·}Y\right)\right)$$
37	5 14 35 36	syl3anc	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}\left(X\underset{\dot{}}{·}Y\right)\leftrightarrow \left(\underset{\dot{}}{0}{\le }_R\left(X\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{0}\ne X\underset{\dot{}}{·}Y\right)\right)$$
38	25 32 37	mpbir2and	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}\left(X\underset{\dot{}}{·}Y\right)$$