Metamath Proof Explorer

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}={\mathrm{Base}}_{{G}}$
ogrpaddltrd.1 ${⊢}{\phi }\to {G}\in {V}$
ogrpaddltrd.2 ${⊢}{\phi }\to {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}$
ogrpaddltrd.3 ${⊢}{\phi }\to {X}\in {B}$
ogrpaddltrd.4 ${⊢}{\phi }\to {Y}\in {B}$
ogrpaddltrd.5 ${⊢}{\phi }\to {Z}\in {B}$

Proof

Step Hyp Ref Expression
1 ogrpaddlt.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
4 ogrpaddltrd.1 ${⊢}{\phi }\to {G}\in {V}$
5 ogrpaddltrd.2 ${⊢}{\phi }\to {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}$
6 ogrpaddltrd.3 ${⊢}{\phi }\to {X}\in {B}$
7 ogrpaddltrd.4 ${⊢}{\phi }\to {Y}\in {B}$
8 ogrpaddltrd.5 ${⊢}{\phi }\to {Z}\in {B}$
10 eqid ${⊢}{opp}_{𝑔}\left({G}\right)={opp}_{𝑔}\left({G}\right)$
11 10 2 oppglt
12 4 11 syl
13 12 breqd
14 9 13 mpbid ${⊢}{\phi }\to {X}{<}_{{opp}_{𝑔}\left({G}\right)}{Y}$
15 10 1 oppgbas ${⊢}{B}={\mathrm{Base}}_{{opp}_{𝑔}\left({G}\right)}$
16 eqid ${⊢}{<}_{{opp}_{𝑔}\left({G}\right)}={<}_{{opp}_{𝑔}\left({G}\right)}$
17 eqid ${⊢}{+}_{{opp}_{𝑔}\left({G}\right)}={+}_{{opp}_{𝑔}\left({G}\right)}$
18 15 16 17 ogrpaddlt ${⊢}\left({opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\wedge {X}{<}_{{opp}_{𝑔}\left({G}\right)}{Y}\right)\to \left({X}{+}_{{opp}_{𝑔}\left({G}\right)}{Z}\right){<}_{{opp}_{𝑔}\left({G}\right)}\left({Y}{+}_{{opp}_{𝑔}\left({G}\right)}{Z}\right)$
19 5 6 7 8 14 18 syl131anc ${⊢}{\phi }\to \left({X}{+}_{{opp}_{𝑔}\left({G}\right)}{Z}\right){<}_{{opp}_{𝑔}\left({G}\right)}\left({Y}{+}_{{opp}_{𝑔}\left({G}\right)}{Z}\right)$
20 3 10 17 oppgplus
21 3 10 17 oppgplus
22 19 20 21 3brtr3g
23 12 breqd
24 22 23 mpbird