Metamath Proof Explorer

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 = ( Base ` M )
omndadd.1 
|- .<_ = ( le ` M )
omndadd.2 
|- .+ = ( +g ` M )
omndadd2d.m 
|- ( ph -> M e. oMnd )
omndadd2d.w 
|- ( ph -> W e. B )
omndadd2d.x 
|- ( ph -> X e. B )
omndadd2d.y 
|- ( ph -> Y e. B )
omndadd2d.z 
|- ( ph -> Z e. B )
omndadd2d.1 
|- ( ph -> X .<_ Z )
omndadd2d.2 
|- ( ph -> Y .<_ W )
omndadd2rd.c 
|- ( ph -> ( oppG ` M ) e. oMnd )
Assertion omndadd2rd 
|- ( ph -> ( X .+ Y ) .<_ ( Z .+ W ) )

Proof

Step Hyp Ref Expression
1 omndadd.0 
 |-  B = ( Base ` M )
2 omndadd.1 
 |-  .<_ = ( le ` M )
3 omndadd.2 
 |-  .+ = ( +g ` M )
4 omndadd2d.m 
 |-  ( ph -> M e. oMnd )
5 omndadd2d.w 
 |-  ( ph -> W e. B )
6 omndadd2d.x 
 |-  ( ph -> X e. B )
7 omndadd2d.y 
 |-  ( ph -> Y e. B )
8 omndadd2d.z 
 |-  ( ph -> Z e. B )
9 omndadd2d.1 
 |-  ( ph -> X .<_ Z )
10 omndadd2d.2 
 |-  ( ph -> Y .<_ W )
11 omndadd2rd.c 
 |-  ( ph -> ( oppG ` M ) e. oMnd )
12 omndtos 
 |-  ( M e. oMnd -> M e. Toset )
13 tospos 
 |-  ( M e. Toset -> M e. Poset )
14 4 12 13 3syl 
 |-  ( ph -> M e. Poset )
15 omndmnd 
 |-  ( M e. oMnd -> M e. Mnd )
16 4 15 syl 
 |-  ( ph -> M e. Mnd )
17 1 3 mndcl 
 |-  ( ( M e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
18 16 6 7 17 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. B )
19 1 3 mndcl 
 |-  ( ( M e. Mnd /\ X e. B /\ W e. B ) -> ( X .+ W ) e. B )
20 16 6 5 19 syl3anc 
 |-  ( ph -> ( X .+ W ) e. B )
21 1 3 mndcl 
 |-  ( ( M e. Mnd /\ Z e. B /\ W e. B ) -> ( Z .+ W ) e. B )
22 16 8 5 21 syl3anc 
 |-  ( ph -> ( Z .+ W ) e. B )
23 18 20 22 3jca 
 |-  ( ph -> ( ( X .+ Y ) e. B /\ ( X .+ W ) e. B /\ ( Z .+ W ) e. B ) )
24 1 2 3 omndaddr 
 |-  ( ( ( oppG ` M ) e. oMnd /\ ( Y e. B /\ W e. B /\ X e. B ) /\ Y .<_ W ) -> ( X .+ Y ) .<_ ( X .+ W ) )
25 11 7 5 6 10 24 syl131anc 
 |-  ( ph -> ( X .+ Y ) .<_ ( X .+ W ) )
26 1 2 3 omndadd 
 |-  ( ( M e. oMnd /\ ( X e. B /\ Z e. B /\ W e. B ) /\ X .<_ Z ) -> ( X .+ W ) .<_ ( Z .+ W ) )
27 4 6 8 5 9 26 syl131anc 
 |-  ( ph -> ( X .+ W ) .<_ ( Z .+ W ) )
28 1 2 postr 
 |-  ( ( M e. Poset /\ ( ( X .+ Y ) e. B /\ ( X .+ W ) e. B /\ ( Z .+ W ) e. B ) ) -> ( ( ( X .+ Y ) .<_ ( X .+ W ) /\ ( X .+ W ) .<_ ( Z .+ W ) ) -> ( X .+ Y ) .<_ ( Z .+ W ) ) )
29 28 imp 
 |-  ( ( ( M e. Poset /\ ( ( X .+ Y ) e. B /\ ( X .+ W ) e. B /\ ( Z .+ W ) e. B ) ) /\ ( ( X .+ Y ) .<_ ( X .+ W ) /\ ( X .+ W ) .<_ ( Z .+ W ) ) ) -> ( X .+ Y ) .<_ ( Z .+ W ) )
30 14 23 25 27 29 syl22anc 
 |-  ( ph -> ( X .+ Y ) .<_ ( Z .+ W ) )