# Metamath Proof Explorer

## Theorem ogrpinvlt

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

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

### Proof

Step Hyp Ref Expression
1 ogrpinvlt.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ogrpinvlt.1
3 ogrpinvlt.2 ${⊢}{I}={inv}_{g}\left({G}\right)$
4 simp1l ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {G}\in \mathrm{oGrp}$
5 simp2 ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
6 simp3 ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
7 ogrpgrp ${⊢}{G}\in \mathrm{oGrp}\to {G}\in \mathrm{Grp}$
8 4 7 syl ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {G}\in \mathrm{Grp}$
9 1 3 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {Y}\in {B}\right)\to {I}\left({Y}\right)\in {B}$
10 8 6 9 syl2anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {I}\left({Y}\right)\in {B}$
11 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
13 4 5 6 10 12 syl13anc
14 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
15 1 11 14 3 grprinv ${⊢}\left({G}\in \mathrm{Grp}\wedge {Y}\in {B}\right)\to {Y}{+}_{{G}}{I}\left({Y}\right)={0}_{{G}}$
16 8 6 15 syl2anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}{+}_{{G}}{I}\left({Y}\right)={0}_{{G}}$
17 16 breq2d
18 simp1r ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}$
19 1 11 grpcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\wedge {I}\left({Y}\right)\in {B}\right)\to {X}{+}_{{G}}{I}\left({Y}\right)\in {B}$
20 8 5 10 19 syl3anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}{+}_{{G}}{I}\left({Y}\right)\in {B}$
21 1 14 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {B}$
22 4 7 21 3syl ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {0}_{{G}}\in {B}$
23 1 3 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {I}\left({X}\right)\in {B}$
24 8 5 23 syl2anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {I}\left({X}\right)\in {B}$
25 1 2 11 4 18 20 22 24 ogrpaddltrbid
26 13 17 25 3bitrd
27 1 11 14 3 grplinv ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {I}\left({X}\right){+}_{{G}}{X}={0}_{{G}}$
28 8 5 27 syl2anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {I}\left({X}\right){+}_{{G}}{X}={0}_{{G}}$
29 28 oveq1d ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({I}\left({X}\right){+}_{{G}}{X}\right){+}_{{G}}{I}\left({Y}\right)={0}_{{G}}{+}_{{G}}{I}\left({Y}\right)$
30 1 11 grpass ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({I}\left({X}\right)\in {B}\wedge {X}\in {B}\wedge {I}\left({Y}\right)\in {B}\right)\right)\to \left({I}\left({X}\right){+}_{{G}}{X}\right){+}_{{G}}{I}\left({Y}\right)={I}\left({X}\right){+}_{{G}}\left({X}{+}_{{G}}{I}\left({Y}\right)\right)$
31 8 24 5 10 30 syl13anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({I}\left({X}\right){+}_{{G}}{X}\right){+}_{{G}}{I}\left({Y}\right)={I}\left({X}\right){+}_{{G}}\left({X}{+}_{{G}}{I}\left({Y}\right)\right)$
32 1 11 14 grplid ${⊢}\left({G}\in \mathrm{Grp}\wedge {I}\left({Y}\right)\in {B}\right)\to {0}_{{G}}{+}_{{G}}{I}\left({Y}\right)={I}\left({Y}\right)$
33 8 10 32 syl2anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {0}_{{G}}{+}_{{G}}{I}\left({Y}\right)={I}\left({Y}\right)$
34 29 31 33 3eqtr3d ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {I}\left({X}\right){+}_{{G}}\left({X}{+}_{{G}}{I}\left({Y}\right)\right)={I}\left({Y}\right)$
35 1 11 14 grprid ${⊢}\left({G}\in \mathrm{Grp}\wedge {I}\left({X}\right)\in {B}\right)\to {I}\left({X}\right){+}_{{G}}{0}_{{G}}={I}\left({X}\right)$
36 8 24 35 syl2anc ${⊢}\left(\left({G}\in \mathrm{oGrp}\wedge {opp}_{𝑔}\left({G}\right)\in \mathrm{oGrp}\right)\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {I}\left({X}\right){+}_{{G}}{0}_{{G}}={I}\left({X}\right)$
37 34 36 breq12d
38 26 37 bitrd