Metamath Proof Explorer

Theorem ogrpaddltbi

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

Ref Expression
Hypotheses ogrpaddlt.0 
|- B = ( Base ` G )
ogrpaddlt.1 
|- .< = ( lt ` G )
ogrpaddlt.2 
|- .+ = ( +g ` G )
Assertion ogrpaddltbi 
|- ( ( 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 1 2 3 ogrpaddlt 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .< Y ) -> ( X .+ Z ) .< ( Y .+ Z ) )
5 4 3expa 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( X .+ Z ) .< ( Y .+ Z ) )
6 simpll 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> G e. oGrp )
7 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
8 6 7 syl 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> G e. Grp )
9 simplr1 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> X e. B )
10 simplr3 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> Z e. B )
11 1 3 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( X .+ Z ) e. B )
12 8 9 10 11 syl3anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( X .+ Z ) e. B )
13 simplr2 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> Y e. B )
14 1 3 grpcl 
 |-  ( ( G e. Grp /\ Y e. B /\ Z e. B ) -> ( Y .+ Z ) e. B )
15 8 13 10 14 syl3anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( Y .+ Z ) e. B )
16 eqid 
 |-  ( invg ` G ) = ( invg ` G )
17 1 16 grpinvcl 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B )
18 8 10 17 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( invg ` G ) ` Z ) e. B )
19 simpr 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( X .+ Z ) .< ( Y .+ Z ) )
20 1 2 3 ogrpaddlt 
 |-  ( ( G e. oGrp /\ ( ( X .+ Z ) e. B /\ ( Y .+ Z ) e. B /\ ( ( invg ` G ) ` Z ) e. B ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( X .+ Z ) .+ ( ( invg ` G ) ` Z ) ) .< ( ( Y .+ Z ) .+ ( ( invg ` G ) ` Z ) ) )
21 6 12 15 18 19 20 syl131anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( X .+ Z ) .+ ( ( invg ` G ) ` Z ) ) .< ( ( Y .+ Z ) .+ ( ( invg ` G ) ` Z ) ) )
22 1 3 grpass 
 |-  ( ( G e. Grp /\ ( X e. B /\ Z e. B /\ ( ( invg ` G ) ` Z ) e. B ) ) -> ( ( X .+ Z ) .+ ( ( invg ` G ) ` Z ) ) = ( X .+ ( Z .+ ( ( invg ` G ) ` Z ) ) ) )
23 8 9 10 18 22 syl13anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( X .+ Z ) .+ ( ( invg ` G ) ` Z ) ) = ( X .+ ( Z .+ ( ( invg ` G ) ` Z ) ) ) )
24 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
25 1 3 24 16 grprinv 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( Z .+ ( ( invg ` G ) ` Z ) ) = ( 0g ` G ) )
26 8 10 25 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( Z .+ ( ( invg ` G ) ` Z ) ) = ( 0g ` G ) )
27 26 oveq2d 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( X .+ ( Z .+ ( ( invg ` G ) ` Z ) ) ) = ( X .+ ( 0g ` G ) ) )
28 1 3 24 grprid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( 0g ` G ) ) = X )
29 8 9 28 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( X .+ ( 0g ` G ) ) = X )
30 23 27 29 3eqtrd 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( X .+ Z ) .+ ( ( invg ` G ) ` Z ) ) = X )
31 1 3 grpass 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B /\ ( ( invg ` G ) ` Z ) e. B ) ) -> ( ( Y .+ Z ) .+ ( ( invg ` G ) ` Z ) ) = ( Y .+ ( Z .+ ( ( invg ` G ) ` Z ) ) ) )
32 8 13 10 18 31 syl13anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( Y .+ Z ) .+ ( ( invg ` G ) ` Z ) ) = ( Y .+ ( Z .+ ( ( invg ` G ) ` Z ) ) ) )
33 26 oveq2d 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( Y .+ ( Z .+ ( ( invg ` G ) ` Z ) ) ) = ( Y .+ ( 0g ` G ) ) )
34 1 3 24 grprid 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( Y .+ ( 0g ` G ) ) = Y )
35 8 13 34 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( Y .+ ( 0g ` G ) ) = Y )
36 32 33 35 3eqtrd 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> ( ( Y .+ Z ) .+ ( ( invg ` G ) ` Z ) ) = Y )
37 21 30 36 3brtr3d 
 |-  ( ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .+ Z ) .< ( Y .+ Z ) ) -> X .< Y )
38 5 37 impbida 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Y <-> ( X .+ Z ) .< ( Y .+ Z ) ) )