Theorem omndadd

Description: In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	omndadd.0	$$⊢B={\mathrm{Base}}_M$$
	omndadd.1	$$⊢\underset{\dot{}}{\le }={\le }_M$$
	omndadd.2	$$⊢\underset{\dot{}}{+}={+}_M$$
Assertion	omndadd	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\wedge X\underset{\dot{}}{\le }Y\right)\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		omndadd.0	$$⊢B={\mathrm{Base}}_M$$
2		omndadd.1	$$⊢\underset{\dot{}}{\le }={\le }_M$$
3		omndadd.2	$$⊢\underset{\dot{}}{+}={+}_M$$
4	1 3 2	isomnd	$$⊢M\in \mathrm{oMnd}\leftrightarrow \left(M\in \mathrm{Mnd}\wedge M\in \mathrm{Toset}\wedge \forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{\le }b\to \left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)\right)$$
5	4	simp3bi	$$⊢M\in \mathrm{oMnd}\to \forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{\le }b\to \left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)$$
6		breq1	$$⊢a=X\to \left(a\underset{\dot{}}{\le }b\leftrightarrow X\underset{\dot{}}{\le }b\right)$$
7		oveq1	$$⊢a=X\to a\underset{\dot{}}{+}c=X\underset{\dot{}}{+}c$$
8	7	breq1d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\leftrightarrow \left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)$$
9	6 8	imbi12d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{\le }b\to \left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }b\to \left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)\right)$$
10		breq2	$$⊢b=Y\to \left(X\underset{\dot{}}{\le }b\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
11		oveq1	$$⊢b=Y\to b\underset{\dot{}}{+}c=Y\underset{\dot{}}{+}c$$
12	11	breq2d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\leftrightarrow \left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}c\right)\right)$$
13	10 12	imbi12d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{\le }b\to \left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\to \left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}c\right)\right)\right)$$
14		oveq2	$$⊢c=Z\to X\underset{\dot{}}{+}c=X\underset{\dot{}}{+}Z$$
15		oveq2	$$⊢c=Z\to Y\underset{\dot{}}{+}c=Y\underset{\dot{}}{+}Z$$
16	14 15	breq12d	$$⊢c=Z\to \left(\left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}c\right)\leftrightarrow \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}Z\right)\right)$$
17	16	imbi2d	$$⊢c=Z\to \left(\left(X\underset{\dot{}}{\le }Y\to \left(X\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}c\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}Z\right)\right)\right)$$
18	9 13 17	rspc3v	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(\forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{\le }b\to \left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }\left(b\underset{\dot{}}{+}c\right)\right)\to \left(X\underset{\dot{}}{\le }Y\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}Z\right)\right)\right)$$
19	5 18	mpan9	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{\le }Y\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}Z\right)\right)$$
20	19	3impia	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\wedge X\underset{\dot{}}{\le }Y\right)\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{+}Z\right)$$