This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )