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 = {Base}_{M}$
	omndadd.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
	omndadd.2	$⊢ \underset{˙}{+} = +_{M}$
Assertion	omndaddr	$⊢ ({opp}_{𝑔} (M) \in oMnd \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to (Z \underset{˙}{+} X) \underset{˙}{\leq} (Z \underset{˙}{+} Y)$

Step	Hyp	Ref	Expression
1		omndadd.0	$⊢ B = {Base}_{M}$
2		omndadd.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
3		omndadd.2	$⊢ \underset{˙}{+} = +_{M}$
4		eqid	$⊢ {opp}_{𝑔} (M) = {opp}_{𝑔} (M)$
5	4 1	oppgbas	$⊢ B = {Base}_{{opp}_{𝑔} (M)}$
6	4 2	oppgle	$⊢ \underset{˙}{\leq} = \leq_{{opp}_{𝑔} (M)}$
7		eqid	$⊢ +_{{opp}_{𝑔} (M)} = +_{{opp}_{𝑔} (M)}$
8	5 6 7	omndadd	$⊢ ({opp}_{𝑔} (M) \in oMnd \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to (X +_{{opp}_{𝑔} (M)} Z) \underset{˙}{\leq} (Y +_{{opp}_{𝑔} (M)} Z)$
9	3 4 7	oppgplus	$⊢ X +_{{opp}_{𝑔} (M)} Z = Z \underset{˙}{+} X$
10	3 4 7	oppgplus	$⊢ Y +_{{opp}_{𝑔} (M)} Z = Z \underset{˙}{+} Y$
11	8 9 10	3brtr3g	$⊢ ({opp}_{𝑔} (M) \in oMnd \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Y) \to (Z \underset{˙}{+} X) \underset{˙}{\leq} (Z \underset{˙}{+} Y)$

Metamath Proof Explorer