Metamath Proof Explorer

Theorem ogrpaddlt

Description: In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Hypotheses ogrpaddlt.0 
|- B = ( Base ` G )
ogrpaddlt.1 
|- .< = ( lt ` G )
ogrpaddlt.2 
|- .+ = ( +g ` G )
Assertion ogrpaddlt 
|- ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .+ Z ) .< ( Y .+ Z ) )

Proof

Step Hyp Ref Expression
1 ogrpaddlt.0 
 |-  B = ( Base ` G )
2 ogrpaddlt.1 
 |-  .< = ( lt ` G )
3 ogrpaddlt.2 
 |-  .+ = ( +g ` G )
4 isogrp 
 |-  ( G e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )
5 4 simprbi 
 |-  ( G e. oGrp -> G e. oMnd )
6 5 3ad2ant1 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> G e. oMnd )
7 simp2 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X e. B /\ Y e. B /\ Z e. B ) )
8 simp1 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> G e. oGrp )
9 simp21 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X e. B )
10 simp22 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> Y e. B )
11 simp3 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X .< Y )
12 eqid 
 |-  ( le ` G ) = ( le ` G )
13 12 2 pltle 
 |-  ( ( G e. oGrp /\ X e. B /\ Y e. B ) -> ( X .< Y -> X ( le ` G ) Y ) )
14 13 imp 
 |-  ( ( ( G e. oGrp /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X ( le ` G ) Y )
15 8 9 10 11 14 syl31anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X ( le ` G ) Y )
16 1 12 3 omndadd 
 |-  ( ( G e. oMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X ( le ` G ) Y ) -> ( X .+ Z ) ( le ` G ) ( Y .+ Z ) )
17 6 7 15 16 syl3anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .+ Z ) ( le ` G ) ( Y .+ Z ) )
18 2 pltne 
 |-  ( ( G e. oGrp /\ X e. B /\ Y e. B ) -> ( X .< Y -> X =/= Y ) )
19 18 imp 
 |-  ( ( ( G e. oGrp /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X =/= Y )
20 8 9 10 11 19 syl31anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X =/= Y )
21 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
22 1 3 grprcan 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) = ( Y .+ Z ) <-> X = Y ) )
23 22 biimpd 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) = ( Y .+ Z ) -> X = Y ) )
24 21 23 sylan 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) = ( Y .+ Z ) -> X = Y ) )
25 24 necon3d 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X =/= Y -> ( X .+ Z ) =/= ( Y .+ Z ) ) )
26 25 3impia 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X =/= Y ) -> ( X .+ Z ) =/= ( Y .+ Z ) )
27 8 7 20 26 syl3anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .+ Z ) =/= ( Y .+ Z ) )
28 ovex 
 |-  ( X .+ Z ) e. _V
29 ovex 
 |-  ( Y .+ Z ) e. _V
30 12 2 pltval 
 |-  ( ( G e. oGrp /\ ( X .+ Z ) e. _V /\ ( Y .+ Z ) e. _V ) -> ( ( X .+ Z ) .< ( Y .+ Z ) <-> ( ( X .+ Z ) ( le ` G ) ( Y .+ Z ) /\ ( X .+ Z ) =/= ( Y .+ Z ) ) ) )
31 28 29 30 mp3an23 
 |-  ( G e. oGrp -> ( ( X .+ Z ) .< ( Y .+ Z ) <-> ( ( X .+ Z ) ( le ` G ) ( Y .+ Z ) /\ ( X .+ Z ) =/= ( Y .+ Z ) ) ) )
32 31 3ad2ant1 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( ( X .+ Z ) .< ( Y .+ Z ) <-> ( ( X .+ Z ) ( le ` G ) ( Y .+ Z ) /\ ( X .+ Z ) =/= ( Y .+ Z ) ) ) )
33 17 27 32 mpbir2and 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .+ Z ) .< ( Y .+ Z ) )