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

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 omndadd2rd.c ⊢ ( 𝜑 → ( oppg ‘ 𝑀 ) ∈ oMnd )
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 6 5 19 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑊 ) ∈ 𝐵 )
21 1 3 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
22 16 8 5 21 syl3anc ⊢ ( 𝜑 → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
23 18 20 22 3jca ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑊 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) )
24 1 2 3 omndaddr ⊢ ( ( ( oppg ‘ 𝑀 ) ∈ oMnd ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑊 ) → ( 𝑋 + 𝑌 ) ≤ ( 𝑋 + 𝑊 ) )
25 11 7 5 6 10 24 syl131anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≤ ( 𝑋 + 𝑊 ) )
26 1 2 3 omndadd ⊢ ( ( 𝑀 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑋 + 𝑊 ) ≤ ( 𝑍 + 𝑊 ) )
27 4 6 8 5 9 26 syl131anc ⊢ ( 𝜑 → ( 𝑋 + 𝑊 ) ≤ ( 𝑍 + 𝑊 ) )
28 1 2 postr ⊢ ( ( 𝑀 ∈ Poset ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑊 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑌 ) ≤ ( 𝑋 + 𝑊 ) ∧ ( 𝑋 + 𝑊 ) ≤ ( 𝑍 + 𝑊 ) ) → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) ) )
29 28 imp ⊢ ( ( ( 𝑀 ∈ Poset ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 + 𝑊 ) ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) ) ∧ ( ( 𝑋 + 𝑌 ) ≤ ( 𝑋 + 𝑊 ) ∧ ( 𝑋 + 𝑊 ) ≤ ( 𝑍 + 𝑊 ) ) ) → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) )
30 14 23 25 27 29 syl22anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≤ ( 𝑍 + 𝑊 ) )