Metamath Proof Explorer

Theorem ogrpaddltrbid

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

Ref Expression
Hypotheses ogrpaddlt.0 
|- B = ( Base ` G )
ogrpaddlt.1 
|- .< = ( lt ` G )
ogrpaddlt.2 
|- .+ = ( +g ` G )
ogrpaddltrd.1 
|- ( ph -> G e. V )
ogrpaddltrd.2 
|- ( ph -> ( oppG ` G ) e. oGrp )
ogrpaddltrd.3 
|- ( ph -> X e. B )
ogrpaddltrd.4 
|- ( ph -> Y e. B )
ogrpaddltrd.5 
|- ( ph -> Z e. B )
Assertion ogrpaddltrbid 
|- ( ph -> ( X .< Y <-> ( Z .+ X ) .< ( Z .+ Y ) ) )

Proof

Step Hyp Ref Expression
1 ogrpaddlt.0 
 |-  B = ( Base ` G )
2 ogrpaddlt.1 
 |-  .< = ( lt ` G )
3 ogrpaddlt.2 
 |-  .+ = ( +g ` G )
4 ogrpaddltrd.1 
 |-  ( ph -> G e. V )
5 ogrpaddltrd.2 
 |-  ( ph -> ( oppG ` G ) e. oGrp )
6 ogrpaddltrd.3 
 |-  ( ph -> X e. B )
7 ogrpaddltrd.4 
 |-  ( ph -> Y e. B )
8 ogrpaddltrd.5 
 |-  ( ph -> Z e. B )
9 4 adantr 
 |-  ( ( ph /\ X .< Y ) -> G e. V )
10 5 adantr 
 |-  ( ( ph /\ X .< Y ) -> ( oppG ` G ) e. oGrp )
11 6 adantr 
 |-  ( ( ph /\ X .< Y ) -> X e. B )
12 7 adantr 
 |-  ( ( ph /\ X .< Y ) -> Y e. B )
13 8 adantr 
 |-  ( ( ph /\ X .< Y ) -> Z e. B )
14 simpr 
 |-  ( ( ph /\ X .< Y ) -> X .< Y )
15 1 2 3 9 10 11 12 13 14 ogrpaddltrd 
 |-  ( ( ph /\ X .< Y ) -> ( Z .+ X ) .< ( Z .+ Y ) )
16 4 adantr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> G e. V )
17 5 adantr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( oppG ` G ) e. oGrp )
18 ogrpgrp 
 |-  ( ( oppG ` G ) e. oGrp -> ( oppG ` G ) e. Grp )
19 5 18 syl 
 |-  ( ph -> ( oppG ` G ) e. Grp )
20 19 adantr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( oppG ` G ) e. Grp )
21 6 adantr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> X e. B )
22 8 adantr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> Z e. B )
23 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
24 eqid 
 |-  ( +g ` ( oppG ` G ) ) = ( +g ` ( oppG ` G ) )
25 3 23 24 oppgplus 
 |-  ( X ( +g ` ( oppG ` G ) ) Z ) = ( Z .+ X )
26 23 1 oppgbas 
 |-  B = ( Base ` ( oppG ` G ) )
27 26 24 grpcl 
 |-  ( ( ( oppG ` G ) e. Grp /\ X e. B /\ Z e. B ) -> ( X ( +g ` ( oppG ` G ) ) Z ) e. B )
28 25 27 eqeltrrid 
 |-  ( ( ( oppG ` G ) e. Grp /\ X e. B /\ Z e. B ) -> ( Z .+ X ) e. B )
29 20 21 22 28 syl3anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( Z .+ X ) e. B )
30 7 adantr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> Y e. B )
31 3 23 24 oppgplus 
 |-  ( Y ( +g ` ( oppG ` G ) ) Z ) = ( Z .+ Y )
32 26 24 grpcl 
 |-  ( ( ( oppG ` G ) e. Grp /\ Y e. B /\ Z e. B ) -> ( Y ( +g ` ( oppG ` G ) ) Z ) e. B )
33 31 32 eqeltrrid 
 |-  ( ( ( oppG ` G ) e. Grp /\ Y e. B /\ Z e. B ) -> ( Z .+ Y ) e. B )
34 20 30 22 33 syl3anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( Z .+ Y ) e. B )
35 23 oppggrpb 
 |-  ( G e. Grp <-> ( oppG ` G ) e. Grp )
36 20 35 sylibr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> G e. Grp )
37 eqid 
 |-  ( invg ` G ) = ( invg ` G )
38 1 37 grpinvcl 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B )
39 36 22 38 syl2anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( invg ` G ) ` Z ) e. B )
40 simpr 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( Z .+ X ) .< ( Z .+ Y ) )
41 1 2 3 16 17 29 34 39 40 ogrpaddltrd 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) .< ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
42 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
43 1 3 42 37 grplinv 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( ( invg ` G ) ` Z ) .+ Z ) = ( 0g ` G ) )
44 36 22 43 syl2anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ Z ) = ( 0g ` G ) )
45 44 oveq1d 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( 0g ` G ) .+ X ) )
46 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` Z ) e. B /\ Z e. B /\ X e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) )
47 36 39 22 21 46 syl13anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) )
48 1 3 42 grplid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( 0g ` G ) .+ X ) = X )
49 36 21 48 syl2anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( 0g ` G ) .+ X ) = X )
50 45 47 49 3eqtr3d 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) = X )
51 44 oveq1d 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ Y ) = ( ( 0g ` G ) .+ Y ) )
52 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` Z ) e. B /\ Z e. B /\ Y e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ Y ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
53 36 39 22 30 52 syl13anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ Y ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
54 1 3 42 grplid 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( 0g ` G ) .+ Y ) = Y )
55 36 30 54 syl2anc 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( 0g ` G ) .+ Y ) = Y )
56 51 53 55 3eqtr3d 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) = Y )
57 41 50 56 3brtr3d 
 |-  ( ( ph /\ ( Z .+ X ) .< ( Z .+ Y ) ) -> X .< Y )
58 15 57 impbida 
 |-  ( ph -> ( X .< Y <-> ( Z .+ X ) .< ( Z .+ Y ) ) )