Metamath Proof Explorer

Theorem omndadd2d

Description: In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 30-Jan-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 )
omndadd2d.c 
|- ( ph -> M e. CMnd )
Assertion omndadd2d 
|- ( 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 omndadd2d.c 
 |-  ( ph -> M e. CMnd )
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 /\ Z e. B /\ Y e. B ) -> ( Z .+ Y ) e. B )
20 16 8 7 19 syl3anc 
 |-  ( ph -> ( Z .+ Y ) 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 /\ ( Z .+ Y ) e. B /\ ( Z .+ W ) e. B ) )
24 1 2 3 omndadd 
 |-  ( ( M e. oMnd /\ ( X e. B /\ Z e. B /\ Y e. B ) /\ X .<_ Z ) -> ( X .+ Y ) .<_ ( Z .+ Y ) )
25 4 6 8 7 9 24 syl131anc 
 |-  ( ph -> ( X .+ Y ) .<_ ( Z .+ Y ) )
26 1 2 3 omndadd 
 |-  ( ( M e. oMnd /\ ( Y e. B /\ W e. B /\ Z e. B ) /\ Y .<_ W ) -> ( Y .+ Z ) .<_ ( W .+ Z ) )
27 4 7 5 8 10 26 syl131anc 
 |-  ( ph -> ( Y .+ Z ) .<_ ( W .+ Z ) )
28 1 3 cmncom 
 |-  ( ( M e. CMnd /\ Y e. B /\ Z e. B ) -> ( Y .+ Z ) = ( Z .+ Y ) )
29 11 7 8 28 syl3anc 
 |-  ( ph -> ( Y .+ Z ) = ( Z .+ Y ) )
30 1 3 cmncom 
 |-  ( ( M e. CMnd /\ W e. B /\ Z e. B ) -> ( W .+ Z ) = ( Z .+ W ) )
31 11 5 8 30 syl3anc 
 |-  ( ph -> ( W .+ Z ) = ( Z .+ W ) )
32 27 29 31 3brtr3d 
 |-  ( ph -> ( Z .+ Y ) .<_ ( Z .+ W ) )
33 1 2 postr 
 |-  ( ( M e. Poset /\ ( ( X .+ Y ) e. B /\ ( Z .+ Y ) e. B /\ ( Z .+ W ) e. B ) ) -> ( ( ( X .+ Y ) .<_ ( Z .+ Y ) /\ ( Z .+ Y ) .<_ ( Z .+ W ) ) -> ( X .+ Y ) .<_ ( Z .+ W ) ) )
34 33 imp 
 |-  ( ( ( M e. Poset /\ ( ( X .+ Y ) e. B /\ ( Z .+ Y ) e. B /\ ( Z .+ W ) e. B ) ) /\ ( ( X .+ Y ) .<_ ( Z .+ Y ) /\ ( Z .+ Y ) .<_ ( Z .+ W ) ) ) -> ( X .+ Y ) .<_ ( Z .+ W ) )
35 14 23 25 32 34 syl22anc 
 |-  ( ph -> ( X .+ Y ) .<_ ( Z .+ W ) )