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