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

Metamath Proof Explorer

Theorem ogrpsublt

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

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

Proof

Step Hyp Ref Expression
1 ogrpsublt.0 
 |-  B = ( Base ` G )
2 ogrpsublt.1 
 |-  .< = ( lt ` G )
3 ogrpsublt.2 
 |-  .- = ( -g ` G )
4 simp3 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X .< Y )
5 simp1 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> G e. oGrp )
6 simp21 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X e. B )
7 simp22 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> Y e. B )
8 eqid 
 |-  ( le ` G ) = ( le ` G )
9 8 2 pltval 
 |-  ( ( G e. oGrp /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X ( le ` G ) Y /\ X =/= Y ) ) )
10 5 6 7 9 syl3anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .< Y <-> ( X ( le ` G ) Y /\ X =/= Y ) ) )
11 4 10 mpbid 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X ( le ` G ) Y /\ X =/= Y ) )
12 11 simpld 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X ( le ` G ) Y )
13 1 8 3 ogrpsub 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X ( le ` G ) Y ) -> ( X .- Z ) ( le ` G ) ( Y .- Z ) )
14 12 13 syld3an3 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .- Z ) ( le ` G ) ( Y .- Z ) )
15 11 simprd 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> X =/= Y )
16 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
17 5 16 syl 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> G e. Grp )
18 simp23 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> Z e. B )
19 1 3 grpsubrcan 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Z ) = ( Y .- Z ) <-> X = Y ) )
20 17 6 7 18 19 syl13anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( ( X .- Z ) = ( Y .- Z ) <-> X = Y ) )
21 20 necon3bid 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( ( X .- Z ) =/= ( Y .- Z ) <-> X =/= Y ) )
22 15 21 mpbird 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .- Z ) =/= ( Y .- Z ) )
23 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( X .- Z ) e. B )
24 17 6 18 23 syl3anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .- Z ) e. B )
25 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ Y e. B /\ Z e. B ) -> ( Y .- Z ) e. B )
26 17 7 18 25 syl3anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( Y .- Z ) e. B )
27 8 2 pltval 
 |-  ( ( G e. oGrp /\ ( X .- Z ) e. B /\ ( Y .- Z ) e. B ) -> ( ( X .- Z ) .< ( Y .- Z ) <-> ( ( X .- Z ) ( le ` G ) ( Y .- Z ) /\ ( X .- Z ) =/= ( Y .- Z ) ) ) )
28 5 24 26 27 syl3anc 
 |-  ( ( 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 ) ) ) )
29 14 22 28 mpbir2and 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .- Z ) .< ( Y .- Z ) )