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 = Base G
ogrpinvlt.1 < ˙ = < G
ogrpinvlt.2 I = inv g G
Assertion ogrpinvlt G oGrp opp 𝑔 G oGrp X B Y B X < ˙ Y I Y < ˙ I X

Proof

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