# Metamath Proof Explorer

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}}$
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}$
omndadd2rd.c ${⊢}{\phi }\to {opp}_{𝑔}\left({M}\right)\in \mathrm{oMnd}$

### Proof

Step Hyp Ref Expression
1 omndadd.0 ${⊢}{B}={\mathrm{Base}}_{{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}$
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
18 16 6 7 17 syl3anc
19 1 3 mndcl
20 16 6 5 19 syl3anc
21 1 3 mndcl
22 16 8 5 21 syl3anc
23 18 20 22 3jca