Theorem omndadd2rd

Description: In a left- and right- ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 2-May-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$$
	omndadd2rd.c	$$⊢\phi \to {opp}_{𝑔}\left(M\right)\in \mathrm{oMnd}$$
Assertion	omndadd2rd	$$⊢\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		omndadd2rd.c	$$⊢\phi \to {opp}_{𝑔}\left(M\right)\in \mathrm{oMnd}$$
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 X\in B\wedge W\in B\right)\to X\underset{\dot{}}{+}W\in B$$
20	16 6 5 19	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}W\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 X\underset{\dot{}}{+}W\in B\wedge Z\underset{\dot{}}{+}W\in B\right)$$
24	1 2 3	omndaddr	$$⊢\left({opp}_{𝑔}\left(M\right)\in \mathrm{oMnd}\wedge \left(Y\in B\wedge W\in B\wedge X\in B\right)\wedge Y\underset{\dot{}}{\le }W\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{+}W\right)$$
25	11 7 5 6 10 24	syl131anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{+}W\right)$$
26	1 2 3	omndadd	$$⊢\left(M\in \mathrm{oMnd}\wedge \left(X\in B\wedge Z\in B\wedge W\in B\right)\wedge X\underset{\dot{}}{\le }Z\right)\to \left(X\underset{\dot{}}{+}W\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)$$
27	4 6 8 5 9 26	syl131anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}W\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)$$
28	1 2	postr	$$⊢\left(M\in \mathrm{Poset}\wedge \left(X\underset{\dot{}}{+}Y\in B\wedge X\underset{\dot{}}{+}W\in B\wedge Z\underset{\dot{}}{+}W\in B\right)\right)\to \left(\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{+}W\right)\wedge \left(X\underset{\dot{}}{+}W\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)$$
29	28	imp	$$⊢\left(\left(M\in \mathrm{Poset}\wedge \left(X\underset{\dot{}}{+}Y\in B\wedge X\underset{\dot{}}{+}W\in B\wedge Z\underset{\dot{}}{+}W\in B\right)\right)\wedge \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{+}W\right)\wedge \left(X\underset{\dot{}}{+}W\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)$$
30	14 23 25 27 29	syl22anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}W\right)$$