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

Metamath Proof Explorer

Theorem ogrpaddltrd

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 )
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 )
ogrpaddltrd.6 
|- ( ph -> X .< Y )
Assertion ogrpaddltrd 
|- ( ph -> ( 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 ogrpaddltrd.6 
 |-  ( ph -> X .< Y )
10 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
11 10 2 oppglt 
 |-  ( G e. V -> .< = ( lt ` ( oppG ` G ) ) )
12 4 11 syl 
 |-  ( ph -> .< = ( lt ` ( oppG ` G ) ) )
13 12 breqd 
 |-  ( ph -> ( X .< Y <-> X ( lt ` ( oppG ` G ) ) Y ) )
14 9 13 mpbid 
 |-  ( ph -> X ( lt ` ( oppG ` G ) ) Y )
15 10 1 oppgbas 
 |-  B = ( Base ` ( oppG ` G ) )
16 eqid 
 |-  ( lt ` ( oppG ` G ) ) = ( lt ` ( oppG ` G ) )
17 eqid 
 |-  ( +g ` ( oppG ` G ) ) = ( +g ` ( oppG ` G ) )
18 15 16 17 ogrpaddlt 
 |-  ( ( ( oppG ` G ) e. oGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X ( lt ` ( oppG ` G ) ) Y ) -> ( X ( +g ` ( oppG ` G ) ) Z ) ( lt ` ( oppG ` G ) ) ( Y ( +g ` ( oppG ` G ) ) Z ) )
19 5 6 7 8 14 18 syl131anc 
 |-  ( ph -> ( X ( +g ` ( oppG ` G ) ) Z ) ( lt ` ( oppG ` G ) ) ( Y ( +g ` ( oppG ` G ) ) Z ) )
20 3 10 17 oppgplus 
 |-  ( X ( +g ` ( oppG ` G ) ) Z ) = ( Z .+ X )
21 3 10 17 oppgplus 
 |-  ( Y ( +g ` ( oppG ` G ) ) Z ) = ( Z .+ Y )
22 19 20 21 3brtr3g 
 |-  ( ph -> ( Z .+ X ) ( lt ` ( oppG ` G ) ) ( Z .+ Y ) )
23 12 breqd 
 |-  ( ph -> ( ( Z .+ X ) .< ( Z .+ Y ) <-> ( Z .+ X ) ( lt ` ( oppG ` G ) ) ( Z .+ Y ) ) )
24 22 23 mpbird 
 |-  ( ph -> ( Z .+ X ) .< ( Z .+ Y ) )