This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ogrpsub.1 ⊢ ≤ = ( le ‘ 𝐺 )
ogrpsub.2 ⊢ − = ( -g ‘ 𝐺 )
Assertion ogrpsub ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 − 𝑍 ) ≤ ( 𝑌 − 𝑍 ) )

Proof

Step Hyp Ref Expression
1 ogrpsub.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ogrpsub.1 ⊢ ≤ = ( le ‘ 𝐺 )
3 ogrpsub.2 ⊢ − = ( -g ‘ 𝐺 )
4 isogrp ⊢ ( 𝐺 ∈ oGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd ) )
5 4 simprbi ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ oMnd )
6 5 3ad2ant1 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐺 ∈ oMnd )
7 simp21 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝐵 )
8 simp22 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝐵 )
9 ogrpgrp ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )
10 9 3ad2ant1 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐺 ∈ Grp )
11 simp23 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑍 ∈ 𝐵 )
12 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
13 1 12 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
14 10 11 13 syl2anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
15 simp3 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
16 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
17 1 2 16 omndadd ⊢ ( ( 𝐺 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ≤ ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
18 6 7 8 14 15 17 syl131anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ≤ ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
19 1 16 12 3 grpsubval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
20 7 11 19 syl2anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
21 1 16 12 3 grpsubval ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
22 8 11 21 syl2anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
23 18 20 22 3brtr4d ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 − 𝑍 ) ≤ ( 𝑌 − 𝑍 ) )