# Metamath Proof Explorer

## Theorem ogrpinv0le

Description: In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018)

Ref Expression
Hypotheses ogrpsub.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
ogrpsub.1
ogrpinv.2 ${⊢}{I}={inv}_{g}\left({G}\right)$
ogrpinv.3
Assertion ogrpinv0le

### Proof

Step Hyp Ref Expression
1 ogrpsub.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ogrpsub.1
3 ogrpinv.2 ${⊢}{I}={inv}_{g}\left({G}\right)$
4 ogrpinv.3
5 isogrp ${⊢}{G}\in \mathrm{oGrp}↔\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{oMnd}\right)$
6 5 simprbi ${⊢}{G}\in \mathrm{oGrp}\to {G}\in \mathrm{oMnd}$
8 omndmnd ${⊢}{G}\in \mathrm{oMnd}\to {G}\in \mathrm{Mnd}$
9 1 4 mndidcl
10 7 8 9 3syl
11 simplr
12 ogrpgrp ${⊢}{G}\in \mathrm{oGrp}\to {G}\in \mathrm{Grp}$
14 1 3 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {I}\left({X}\right)\in {B}$
15 13 11 14 syl2anc
16 simpr
17 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
18 1 2 17 omndadd
19 7 10 11 15 16 18 syl131anc
20 1 17 4 grplid
21 13 15 20 syl2anc
22 1 17 4 3 grprinv
23 13 11 22 syl2anc
24 19 21 23 3brtr3d