Metamath Proof Explorer


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 = Base M
omndadd.1 ˙ = M
omndadd.2 + ˙ = + M
Assertion omndaddr opp 𝑔 M oMnd X B Y B Z B X ˙ Y Z + ˙ X ˙ Z + ˙ Y

Proof

Step Hyp Ref Expression
1 omndadd.0 B = Base M
2 omndadd.1 ˙ = M
3 omndadd.2 + ˙ = + M
4 eqid opp 𝑔 M = opp 𝑔 M
5 4 1 oppgbas B = Base opp 𝑔 M
6 4 2 oppgle ˙ = opp 𝑔 M
7 eqid + opp 𝑔 M = + opp 𝑔 M
8 5 6 7 omndadd opp 𝑔 M oMnd X B Y B Z B X ˙ Y X + opp 𝑔 M Z ˙ Y + opp 𝑔 M Z
9 3 4 7 oppgplus X + opp 𝑔 M Z = Z + ˙ X
10 3 4 7 oppgplus Y + opp 𝑔 M Z = Z + ˙ Y
11 8 9 10 3brtr3g opp 𝑔 M oMnd X B Y B Z B X ˙ Y Z + ˙ X ˙ Z + ˙ Y