Theorem omndaddr

Description: In a right 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	omndaddr	$$⊢\left({opp}_{𝑔}\left(M\right)\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(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}Y\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		eqid	$$⊢{opp}_{𝑔}\left(M\right)={opp}_{𝑔}\left(M\right)$$
5	4 1	oppgbas	$$⊢B={\mathrm{Base}}_{{opp}_{𝑔}\left(M\right)}$$
6	4 2	oppgle	$$⊢\underset{\dot{}}{\le }={\le }_{{opp}_{𝑔}\left(M\right)}$$
7		eqid	$$⊢{+}_{{opp}_{𝑔}\left(M\right)}={+}_{{opp}_{𝑔}\left(M\right)}$$
8	5 6 7	omndadd	$$⊢\left({opp}_{𝑔}\left(M\right)\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{+}_{{opp}_{𝑔}\left(M\right)}Z\right)\underset{\dot{}}{\le }\left(Y{+}_{{opp}_{𝑔}\left(M\right)}Z\right)$$
9	3 4 7	oppgplus	$$⊢X{+}_{{opp}_{𝑔}\left(M\right)}Z=Z\underset{\dot{}}{+}X$$
10	3 4 7	oppgplus	$$⊢Y{+}_{{opp}_{𝑔}\left(M\right)}Z=Z\underset{\dot{}}{+}Y$$
11	8 9 10	3brtr3g	$$⊢\left({opp}_{𝑔}\left(M\right)\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(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{\le }\left(Z\underset{\dot{}}{+}Y\right)$$