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 ˙ = M
omndadd.2 + ˙ = + M
omndadd2d.m φ M oMnd
omndadd2d.w φ W B
omndadd2d.x φ X B
omndadd2d.y φ Y B
omndadd2d.z φ Z B
omndadd2d.1 φ X ˙ Z
omndadd2d.2 φ Y ˙ W
omndadd2d.c φ M CMnd
Assertion omndadd2d φ X + ˙ Y ˙ Z + ˙ W

Proof

Step Hyp Ref Expression
1 omndadd.0 B = Base M
2 omndadd.1 ˙ = M
3 omndadd.2 + ˙ = + M
4 omndadd2d.m φ M oMnd
5 omndadd2d.w φ W B
6 omndadd2d.x φ X B
7 omndadd2d.y φ Y B
8 omndadd2d.z φ Z B
9 omndadd2d.1 φ X ˙ Z
10 omndadd2d.2 φ Y ˙ W
11 omndadd2d.c φ M CMnd
12 omndtos M oMnd M Toset
13 tospos M Toset M Poset
14 4 12 13 3syl φ M Poset
15 omndmnd M oMnd M Mnd
16 4 15 syl φ M Mnd
17 1 3 mndcl M Mnd X B Y B X + ˙ Y B
18 16 6 7 17 syl3anc φ X + ˙ Y B
19 1 3 mndcl M Mnd Z B Y B Z + ˙ Y B
20 16 8 7 19 syl3anc φ Z + ˙ Y B
21 1 3 mndcl M Mnd Z B W B Z + ˙ W B
22 16 8 5 21 syl3anc φ Z + ˙ W B
23 18 20 22 3jca φ X + ˙ Y B Z + ˙ Y B Z + ˙ W B
24 1 2 3 omndadd M oMnd X B Z B Y B X ˙ Z X + ˙ Y ˙ Z + ˙ Y
25 4 6 8 7 9 24 syl131anc φ X + ˙ Y ˙ Z + ˙ Y
26 1 2 3 omndadd M oMnd Y B W B Z B Y ˙ W Y + ˙ Z ˙ W + ˙ Z
27 4 7 5 8 10 26 syl131anc φ Y + ˙ Z ˙ W + ˙ Z
28 1 3 cmncom M CMnd Y B Z B Y + ˙ Z = Z + ˙ Y
29 11 7 8 28 syl3anc φ Y + ˙ Z = Z + ˙ Y
30 1 3 cmncom M CMnd W B Z B W + ˙ Z = Z + ˙ W
31 11 5 8 30 syl3anc φ W + ˙ Z = Z + ˙ W
32 27 29 31 3brtr3d φ Z + ˙ Y ˙ Z + ˙ W
33 1 2 postr M Poset X + ˙ Y B Z + ˙ Y B Z + ˙ W B X + ˙ Y ˙ Z + ˙ Y Z + ˙ Y ˙ Z + ˙ W X + ˙ Y ˙ Z + ˙ W
34 33 imp M Poset X + ˙ Y B Z + ˙ Y B Z + ˙ W B X + ˙ Y ˙ Z + ˙ Y Z + ˙ Y ˙ Z + ˙ W X + ˙ Y ˙ Z + ˙ W
35 14 23 25 32 34 syl22anc φ X + ˙ Y ˙ Z + ˙ W