Theorem omndaddr

Description: In a right ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	omndadd.0	⊢ 𝐵 = ( Base ‘ 𝑀 )
	omndadd.1	⊢ ≤ = ( le ‘ 𝑀 )
	omndadd.2	⊢ + = ( +g ‘ 𝑀 )
Assertion	omndaddr	⊢ ( ( ( oppg ‘ 𝑀 ) ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑍 + 𝑋 ) ≤ ( 𝑍 + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		omndadd.0	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		omndadd.1	⊢ ≤ = ( le ‘ 𝑀 )
3		omndadd.2	⊢ + = ( +g ‘ 𝑀 )
4		eqid	⊢ ( oppg ‘ 𝑀 ) = ( oppg ‘ 𝑀 )
5	4 1	oppgbas	⊢ 𝐵 = ( Base ‘ ( oppg ‘ 𝑀 ) )
6	4 2	oppgle	⊢ ≤ = ( le ‘ ( oppg ‘ 𝑀 ) )
7		eqid	⊢ ( +g ‘ ( oppg ‘ 𝑀 ) ) = ( +g ‘ ( oppg ‘ 𝑀 ) )
8	5 6 7	omndadd	⊢ ( ( ( oppg ‘ 𝑀 ) ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( +g ‘ ( oppg ‘ 𝑀 ) ) 𝑍 ) ≤ ( 𝑌 ( +g ‘ ( oppg ‘ 𝑀 ) ) 𝑍 ) )
9	3 4 7	oppgplus	⊢ ( 𝑋 ( +g ‘ ( oppg ‘ 𝑀 ) ) 𝑍 ) = ( 𝑍 + 𝑋 )
10	3 4 7	oppgplus	⊢ ( 𝑌 ( +g ‘ ( oppg ‘ 𝑀 ) ) 𝑍 ) = ( 𝑍 + 𝑌 )
11	8 9 10	3brtr3g	⊢ ( ( ( oppg ‘ 𝑀 ) ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑍 + 𝑋 ) ≤ ( 𝑍 + 𝑌 ) )