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	|- B = ( Base ` M )
	omndadd.1	|- .<_ = ( le ` M )
	omndadd.2	|- .+ = ( +g ` M )
Assertion	omndaddr	|- ( ( ( oppG ` M ) e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( Z .+ X ) .<_ ( Z .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		omndadd.0	|- B = ( Base ` M )
2		omndadd.1	|- .<_ = ( le ` M )
3		omndadd.2	|- .+ = ( +g ` M )
4		eqid	|- ( oppG ` M ) = ( oppG ` M )
5	4 1	oppgbas	|- B = ( Base ` ( oppG ` M ) )
6	4 2	oppgle	|- .<_ = ( le ` ( oppG ` M ) )
7		eqid	|- ( +g ` ( oppG ` M ) ) = ( +g ` ( oppG ` M ) )
8	5 6 7	omndadd	|- ( ( ( oppG ` M ) e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( X ( +g ` ( oppG ` M ) ) Z ) .<_ ( Y ( +g ` ( oppG ` M ) ) Z ) )
9	3 4 7	oppgplus	|- ( X ( +g ` ( oppG ` M ) ) Z ) = ( Z .+ X )
10	3 4 7	oppgplus	|- ( Y ( +g ` ( oppG ` M ) ) Z ) = ( Z .+ Y )
11	8 9 10	3brtr3g	|- ( ( ( oppG ` M ) e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( Z .+ X ) .<_ ( Z .+ Y ) )