Metamath Proof Explorer

Theorem ogrpsub

Description: In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 ogrpsub.0 
 |-  B = ( Base ` G )
2 ogrpsub.1 
 |-  .<_ = ( le ` G )
3 ogrpsub.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 simp21 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> X e. B )
8 simp22 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> Y e. B )
9 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
10 9 3ad2ant1 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> G e. Grp )
11 simp23 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> Z e. B )
12 eqid 
 |-  ( invg ` G ) = ( invg ` G )
13 1 12 grpinvcl 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B )
14 10 11 13 syl2anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( ( invg ` G ) ` Z ) e. B )
15 simp3 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> X .<_ Y )
16 eqid 
 |-  ( +g ` G ) = ( +g ` G )
17 1 2 16 omndadd 
 |-  ( ( G e. oMnd /\ ( X e. B /\ Y e. B /\ ( ( invg ` G ) ` Z ) e. B ) /\ X .<_ Y ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Z ) ) .<_ ( Y ( +g ` G ) ( ( invg ` G ) ` Z ) ) )
18 6 7 8 14 15 17 syl131anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Z ) ) .<_ ( Y ( +g ` G ) ( ( invg ` G ) ` Z ) ) )
19 1 16 12 3 grpsubval 
 |-  ( ( X e. B /\ Z e. B ) -> ( X .- Z ) = ( X ( +g ` G ) ( ( invg ` G ) ` Z ) ) )
20 7 11 19 syl2anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( X .- Z ) = ( X ( +g ` G ) ( ( invg ` G ) ` Z ) ) )
21 1 16 12 3 grpsubval 
 |-  ( ( Y e. B /\ Z e. B ) -> ( Y .- Z ) = ( Y ( +g ` G ) ( ( invg ` G ) ` Z ) ) )
22 8 11 21 syl2anc 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( Y .- Z ) = ( Y ( +g ` G ) ( ( invg ` G ) ` Z ) ) )
23 18 20 22 3brtr4d 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Y ) -> ( X .- Z ) .<_ ( Y .- Z ) )