Metamath Proof Explorer

Theorem omndadd

Description: In an 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 omndadd 
|- ( ( M e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( X .+ Z ) .<_ ( Y .+ Z ) )

Proof

Step Hyp Ref Expression
1 omndadd.0 
 |-  B = ( Base ` M )
2 omndadd.1 
 |-  .<_ = ( le ` M )
3 omndadd.2 
 |-  .+ = ( +g ` M )
4 1 3 2 isomnd 
 |-  ( M e. oMnd <-> ( M e. Mnd /\ M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) )
5 4 simp3bi 
 |-  ( M e. oMnd -> A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) )
6 breq1 
 |-  ( a = X -> ( a .<_ b <-> X .<_ b ) )
7 oveq1 
 |-  ( a = X -> ( a .+ c ) = ( X .+ c ) )
8 7 breq1d 
 |-  ( a = X -> ( ( a .+ c ) .<_ ( b .+ c ) <-> ( X .+ c ) .<_ ( b .+ c ) ) )
9 6 8 imbi12d 
 |-  ( a = X -> ( ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) <-> ( X .<_ b -> ( X .+ c ) .<_ ( b .+ c ) ) ) )
10 breq2 
 |-  ( b = Y -> ( X .<_ b <-> X .<_ Y ) )
11 oveq1 
 |-  ( b = Y -> ( b .+ c ) = ( Y .+ c ) )
12 11 breq2d 
 |-  ( b = Y -> ( ( X .+ c ) .<_ ( b .+ c ) <-> ( X .+ c ) .<_ ( Y .+ c ) ) )
13 10 12 imbi12d 
 |-  ( b = Y -> ( ( X .<_ b -> ( X .+ c ) .<_ ( b .+ c ) ) <-> ( X .<_ Y -> ( X .+ c ) .<_ ( Y .+ c ) ) ) )
14 oveq2 
 |-  ( c = Z -> ( X .+ c ) = ( X .+ Z ) )
15 oveq2 
 |-  ( c = Z -> ( Y .+ c ) = ( Y .+ Z ) )
16 14 15 breq12d 
 |-  ( c = Z -> ( ( X .+ c ) .<_ ( Y .+ c ) <-> ( X .+ Z ) .<_ ( Y .+ Z ) ) )
17 16 imbi2d 
 |-  ( c = Z -> ( ( X .<_ Y -> ( X .+ c ) .<_ ( Y .+ c ) ) <-> ( X .<_ Y -> ( X .+ Z ) .<_ ( Y .+ Z ) ) ) )
18 9 13 17 rspc3v 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) -> ( X .<_ Y -> ( X .+ Z ) .<_ ( Y .+ Z ) ) ) )
19 5 18 mpan9 
 |-  ( ( M e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( X .+ Z ) .<_ ( Y .+ Z ) ) )
20 19 3impia 
 |-  ( ( M e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( X .+ Z ) .<_ ( Y .+ Z ) )