Theorem orngmul

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

	Ref	Expression
Hypotheses	orngmul.0	$$⊢B={\mathrm{Base}}_R$$
	orngmul.1	$$⊢\underset{\dot{}}{\le }={\le }_R$$
	orngmul.2	$$⊢\underset{\dot{}}{0}=0_R$$
	orngmul.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	orngmul	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		orngmul.0	$$⊢B={\mathrm{Base}}_R$$
2		orngmul.1	$$⊢\underset{\dot{}}{\le }={\le }_R$$
3		orngmul.2	$$⊢\underset{\dot{}}{0}=0_R$$
4		orngmul.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		simp2r	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$
6		simp3r	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }Y$$
7		simp2l	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to X\in B$$
8		simp3l	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to Y\in B$$
9	1 3 4 2	isorng	$$⊢R\in \mathrm{oRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge R\in \mathrm{oGrp}\wedge \forall a\in B\forall b\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\right)\right)$$
10	9	simp3bi	$$⊢R\in \mathrm{oRing}\to \forall a\in B\forall b\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\right)$$
11	10	3ad2ant1	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to \forall a\in B\forall b\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\right)$$
12		breq2	$$⊢a=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)$$
13	12	anbi1d	$$⊢a=X\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\right)$$
14		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}b=X\underset{\dot{}}{·}b$$
15	14	breq2d	$$⊢a=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}b\right)\right)$$
16	13 15	imbi12d	$$⊢a=X\to \left(\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}b\right)\right)\right)$$
17		breq2	$$⊢b=Y\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }b\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)$$
18	17	anbi2d	$$⊢b=Y\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)$$
19		oveq2	$$⊢b=Y\to X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}Y$$
20	19	breq2d	$$⊢b=Y\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}b\right)\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}Y\right)\right)$$
21	18 20	imbi12d	$$⊢b=Y\to \left(\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}b\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}Y\right)\right)\right)$$
22	16 21	rspc2va	$$⊢\left(\left(X\in B\wedge Y\in B\right)\wedge \forall a\in B\forall b\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }a\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }b\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(a\underset{\dot{}}{·}b\right)\right)\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}Y\right)\right)$$
23	7 8 11 22	syl21anc	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{\le }X\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}Y\right)\right)$$
24	5 6 23	mp2and	$$⊢\left(R\in \mathrm{oRing}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }X\right)\wedge \left(Y\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{\le }Y\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\le }\left(X\underset{\dot{}}{·}Y\right)$$