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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
omndadd.1 ⊢ ≤ = ( le ‘ 𝑀 )
omndadd.2 ⊢ + = ( +g ‘ 𝑀 )
omndadd2d.m ⊢ ( 𝜑 → 𝑀 ∈ oMnd )
omndadd2d.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
omndadd2d.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
omndadd2d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
omndadd2d.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
omndadd2d.1 ⊢ ( 𝜑 → 𝑋 ≤ 𝑍 )
omndadd2d.2 ⊢ ( 𝜑 → 𝑌 ≤ 𝑊 )
omndadd2d.c ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
Assertion omndadd2d ( 𝜑 → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) )

Proof

Step Hyp Ref Expression
1 omndadd.0 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 omndadd.1 ⊢ ≤ = ( le ‘ 𝑀 )
3 omndadd.2 ⊢ + = ( +g ‘ 𝑀 )
4 omndadd2d.m ⊢ ( 𝜑 → 𝑀 ∈ oMnd )
5 omndadd2d.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
6 omndadd2d.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 omndadd2d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 omndadd2d.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 omndadd2d.1 ⊢ ( 𝜑 → 𝑋 ≤ 𝑍 )
10 omndadd2d.2 ⊢ ( 𝜑 → 𝑌 ≤ 𝑊 )
11 omndadd2d.c ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
12 omndtos ⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Toset )
13 tospos ⊢ ( 𝑀 ∈ Toset → 𝑀 ∈ Poset )
14 4 12 13 3syl ⊢ ( 𝜑 → 𝑀 ∈ Poset )
15 omndmnd ⊢ ( 𝑀 ∈ oMnd → 𝑀 ∈ Mnd )
16 4 15 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
17 1 3 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
18 16 6 7 17 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
19 1 3 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 + 𝑌 ) ∈ 𝐵 )
20 16 8 7 19 syl3anc ⊢ ( 𝜑 → ( 𝑍 + 𝑌 ) ∈ 𝐵 )
21 1 3 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
22 16 8 5 21 syl3anc ⊢ ( 𝜑 → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
23 18 20 22 3jca ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) )
24 1 2 3 omndadd ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑌 ) )
25 4 6 8 7 9 24 syl131anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑌 ) )
26 1 2 3 omndadd ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑊 ) → ( 𝑌 + 𝑍 ) ≤ ( 𝑊 + 𝑍 ) )
27 4 7 5 8 10 26 syl131anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ≤ ( 𝑊 + 𝑍 ) )
28 1 3 cmncom ⊢ ( ( 𝑀 ∈ CMnd ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
29 11 7 8 28 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
30 1 3 cmncom ⊢ ( ( 𝑀 ∈ CMnd ∧ 𝑊 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑊 + 𝑍 ) = ( 𝑍 + 𝑊 ) )
31 11 5 8 30 syl3anc ⊢ ( 𝜑 → ( 𝑊 + 𝑍 ) = ( 𝑍 + 𝑊 ) )
32 27 29 31 3brtr3d ⊢ ( 𝜑 → ( 𝑍 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) )
33 1 2 postr ⊢ ( ( 𝑀 ∈ Poset ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑌 ) ∧ ( 𝑍 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) ) → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) ) )
34 33 imp ⊢ ( ( ( 𝑀 ∈ Poset ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) ) ∧ ( ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑌 ) ∧ ( 𝑍 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) ) ) → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) )
35 14 23 25 32 34 syl22anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) )