# 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}}$

### Proof

Step Hyp Ref Expression
1 ogrpaddlt.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
4 1 2 3 ogrpaddlt
5 4 3expa
6 simpll
7 ogrpgrp ${⊢}{G}\in \mathrm{oGrp}\to {G}\in \mathrm{Grp}$
8 6 7 syl
9 simplr1
10 simplr3
11 1 3 grpcl
12 8 9 10 11 syl3anc
13 simplr2
14 1 3 grpcl
15 8 13 10 14 syl3anc
16 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
17 1 16 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {Z}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
18 8 10 17 syl2anc
19 simpr
20 1 2 3 ogrpaddlt
21 6 12 15 18 19 20 syl131anc
22 1 3 grpass
23 8 9 10 18 22 syl13anc
24 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
25 1 3 24 16 grprinv
26 8 10 25 syl2anc
27 26 oveq2d
28 1 3 24 grprid
29 8 9 28 syl2anc
30 23 27 29 3eqtrd
31 1 3 grpass
32 8 13 10 18 31 syl13anc
33 26 oveq2d
34 1 3 24 grprid
35 8 13 34 syl2anc
36 32 33 35 3eqtrd
37 21 30 36 3brtr3d
38 5 37 impbida