Theorem omndadd2d

Description: In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (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$$
	omndadd2d.m	$$⊢\phi \to M\in \mathrm{oMnd}$$
	omndadd2d.w	$$⊢\phi \to W\in B$$
	omndadd2d.x	$$⊢\phi \to X\in B$$
	omndadd2d.y	$$⊢\phi \to Y\in B$$
	omndadd2d.z	$$⊢\phi \to Z\in B$$
	omndadd2d.1	$$⊢\phi \to X\underset{\dot{}}{\le }Z$$
	omndadd2d.2	$$⊢\phi \to Y\underset{\dot{}}{\le }W$$
	omndadd2d.c	$$⊢\phi \to M\in \mathrm{CMnd}$$
Assertion	omndadd2d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\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		omndadd2d.m	$$⊢\phi \to M\in \mathrm{oMnd}$$
5		omndadd2d.w	$$⊢\phi \to W\in B$$
6		omndadd2d.x	$$⊢\phi \to X\in B$$
7		omndadd2d.y	$$⊢\phi \to Y\in B$$
8		omndadd2d.z	$$⊢\phi \to Z\in B$$
9		omndadd2d.1	$$⊢\phi \to X\underset{\dot{}}{\le }Z$$
10		omndadd2d.2	$$⊢\phi \to Y\underset{\dot{}}{\le }W$$
11		omndadd2d.c	$$⊢\phi \to M\in \mathrm{CMnd}$$
12		omndtos	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Toset}$$
13		tospos	$$⊢M\in \mathrm{Toset}\to M\in \mathrm{Poset}$$
14	4 12 13	3syl	$$⊢\phi \to M\in \mathrm{Poset}$$
15		omndmnd	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Mnd}$$
16	4 15	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
17	1 3	mndcl	$$⊢\left(M\in \mathrm{Mnd}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
18	16 6 7 17	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$
19	1 3	mndcl	$$⊢\left(M\in \mathrm{Mnd}\wedge Z\in B\wedge Y\in B\right)\to Z\underset{\dot{}}{+}Y\in B$$
20	16 8 7 19	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{+}Y\in B$$
21	1 3	mndcl	$$⊢\left(M\in \mathrm{Mnd}\wedge Z\in B\wedge W\in B\right)\to Z\underset{\dot{}}{+}W\in B$$
22	16 8 5 21	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{+}W\in B$$
23	18 20 22	3jca	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\in B\wedge Z\underset{\dot{}}{+}Y\in B\wedge Z\underset{\dot{}}{+}W\in B\right)$$
24	1 2 3	omndadd	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(X\in B\wedge Z\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{\le }Z\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}Y\right)$$
25	4 6 8 7 9 24	syl131anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}Y\right)$$
26	1 2 3	omndadd	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(Y\in B\wedge W\in B\wedge Z\in B\right)\wedge Y\underset{\dot{}}{\le }W\right)\to \left(Y\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(W\underset{\dot{}}{+}Z\right)$$
27	4 7 5 8 10 26	syl131anc	$$⊢\phi \to \left(Y\underset{\dot{}}{+}Z\right)\underset{\dot{}}{\le }\left(W\underset{\dot{}}{+}Z\right)$$
28	1 3	cmncom	$$⊢\left(M\in \mathrm{CMnd}\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
29	11 7 8 28	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
30	1 3	cmncom	$$⊢\left(M\in \mathrm{CMnd}\wedge W\in B\wedge Z\in B\right)\to W\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}W$$
31	11 5 8 30	syl3anc	$$⊢\phi \to W\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}W$$
32	27 29 31	3brtr3d	$$⊢\phi \to \left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)$$
33	1 2	postr	$$⊢\left(M\in \mathrm{Poset}\wedge \left(X\underset{\dot{}}{+}Y\in B\wedge Z\underset{\dot{}}{+}Y\in B\wedge Z\underset{\dot{}}{+}W\in B\right)\right)\to \left(\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}Y\right)\wedge \left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)\right)$$
34	33	imp	$$⊢\left(\left(M\in \mathrm{Poset}\wedge \left(X\underset{\dot{}}{+}Y\in B\wedge Z\underset{\dot{}}{+}Y\in B\wedge Z\underset{\dot{}}{+}W\in B\right)\right)\wedge \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}Y\right)\wedge \left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)$$
35	14 23 25 32 34	syl22anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)$$