Metamath Proof Explorer


Theorem ogrpsub

Description: In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses ogrpsub.0 B = Base G
ogrpsub.1 ˙ = G
ogrpsub.2 - ˙ = - G
Assertion ogrpsub G oGrp X B Y B Z B X ˙ Y X - ˙ Z ˙ Y - ˙ Z

Proof

Step Hyp Ref Expression
1 ogrpsub.0 B = Base G
2 ogrpsub.1 ˙ = G
3 ogrpsub.2 - ˙ = - G
4 isogrp G oGrp G Grp G oMnd
5 4 simprbi G oGrp G oMnd
6 5 3ad2ant1 G oGrp X B Y B Z B X ˙ Y G oMnd
7 simp21 G oGrp X B Y B Z B X ˙ Y X B
8 simp22 G oGrp X B Y B Z B X ˙ Y Y B
9 ogrpgrp G oGrp G Grp
10 9 3ad2ant1 G oGrp X B Y B Z B X ˙ Y G Grp
11 simp23 G oGrp X B Y B Z B X ˙ Y Z B
12 eqid inv g G = inv g G
13 1 12 grpinvcl G Grp Z B inv g G Z B
14 10 11 13 syl2anc G oGrp X B Y B Z B X ˙ Y inv g G Z B
15 simp3 G oGrp X B Y B Z B X ˙ Y X ˙ Y
16 eqid + G = + G
17 1 2 16 omndadd G oMnd X B Y B inv g G Z B X ˙ Y X + G inv g G Z ˙ Y + G inv g G Z
18 6 7 8 14 15 17 syl131anc G oGrp X B Y B Z B X ˙ Y X + G inv g G Z ˙ Y + G inv g G Z
19 1 16 12 3 grpsubval X B Z B X - ˙ Z = X + G inv g G Z
20 7 11 19 syl2anc G oGrp X B Y B Z B X ˙ Y X - ˙ Z = X + G inv g G Z
21 1 16 12 3 grpsubval Y B Z B Y - ˙ Z = Y + G inv g G Z
22 8 11 21 syl2anc G oGrp X B Y B Z B X ˙ Y Y - ˙ Z = Y + G inv g G Z
23 18 20 22 3brtr4d G oGrp X B Y B Z B X ˙ Y X - ˙ Z ˙ Y - ˙ Z