# Metamath Proof Explorer

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}={\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}$
14 simpr
15 1 2 3 9 10 11 12 13 14 ogrpaddltrd
18 ogrpgrp ${⊢}{opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\to {opp}_{𝑔}\left({G}\right)\in \mathrm{Grp}$
19 5 18 syl ${⊢}{\phi }\to {opp}_{𝑔}\left({G}\right)\in \mathrm{Grp}$
23 eqid ${⊢}{opp}_{𝑔}\left({G}\right)={opp}_{𝑔}\left({G}\right)$
24 eqid ${⊢}{+}_{{opp}_{𝑔}\left({G}\right)}={+}_{{opp}_{𝑔}\left({G}\right)}$
25 3 23 24 oppgplus
26 23 1 oppgbas ${⊢}{B}={\mathrm{Base}}_{{opp}_{𝑔}\left({G}\right)}$
27 26 24 grpcl ${⊢}\left({opp}_{𝑔}\left({G}\right)\in \mathrm{Grp}\wedge {X}\in {B}\wedge {Z}\in {B}\right)\to {X}{+}_{{opp}_{𝑔}\left({G}\right)}{Z}\in {B}$
28 25 27 eqeltrrid
29 20 21 22 28 syl3anc
31 3 23 24 oppgplus
32 26 24 grpcl ${⊢}\left({opp}_{𝑔}\left({G}\right)\in \mathrm{Grp}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to {Y}{+}_{{opp}_{𝑔}\left({G}\right)}{Z}\in {B}$
33 31 32 eqeltrrid
34 20 30 22 33 syl3anc
35 23 oppggrpb ${⊢}{G}\in \mathrm{Grp}↔{opp}_{𝑔}\left({G}\right)\in \mathrm{Grp}$
36 20 35 sylibr
37 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
38 1 37 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {Z}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
39 36 22 38 syl2anc
40 simpr
41 1 2 3 16 17 29 34 39 40 ogrpaddltrd
42 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
43 1 3 42 37 grplinv
44 36 22 43 syl2anc
45 44 oveq1d
46 1 3 grpass
47 36 39 22 21 46 syl13anc
48 1 3 42 grplid
49 36 21 48 syl2anc
50 45 47 49 3eqtr3d
51 44 oveq1d
52 1 3 grpass
53 36 39 22 30 52 syl13anc
54 1 3 42 grplid
55 36 30 54 syl2anc
56 51 53 55 3eqtr3d
57 41 50 56 3brtr3d
58 15 57 impbida