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

Metamath Proof Explorer

Theorem ogrpsublt

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

Ref Expression
Hypotheses ogrpsublt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ogrpsublt.1 ⊢ < = ( lt ‘ 𝐺 )
ogrpsublt.2 ⊢ − = ( -g ‘ 𝐺 )
Assertion ogrpsublt ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 − 𝑍 ) < ( 𝑌 − 𝑍 ) )

Proof

Step Hyp Ref Expression
1 ogrpsublt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ogrpsublt.1 ⊢ < = ( lt ‘ 𝐺 )
3 ogrpsublt.2 ⊢ − = ( -g ‘ 𝐺 )
4 simp3 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
5 simp1 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝐺 ∈ oGrp )
6 simp21 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ 𝐵 )
7 simp22 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ 𝐵 )
8 eqid ⊢ ( le ‘ 𝐺 ) = ( le ‘ 𝐺 )
9 8 2 pltval ⊢ ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐺 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
10 5 6 7 9 syl3anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐺 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
11 4 10 mpbid ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 ( le ‘ 𝐺 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) )
12 11 simpld ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ( le ‘ 𝐺 ) 𝑌 )
13 1 8 3 ogrpsub ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐺 ) 𝑌 ) → ( 𝑋 − 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 − 𝑍 ) )
14 12 13 syld3an3 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 − 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 − 𝑍 ) )
15 11 simprd ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ≠ 𝑌 )
16 ogrpgrp ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )
17 5 16 syl ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝐺 ∈ Grp )
18 simp23 ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑍 ∈ 𝐵 )
19 1 3 grpsubrcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 − 𝑍 ) = ( 𝑌 − 𝑍 ) ↔ 𝑋 = 𝑌 ) )
20 17 6 7 18 19 syl13anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑋 − 𝑍 ) = ( 𝑌 − 𝑍 ) ↔ 𝑋 = 𝑌 ) )
21 20 necon3bid ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑋 − 𝑍 ) ≠ ( 𝑌 − 𝑍 ) ↔ 𝑋 ≠ 𝑌 ) )
22 15 21 mpbird ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 − 𝑍 ) ≠ ( 𝑌 − 𝑍 ) )
23 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 − 𝑍 ) ∈ 𝐵 )
24 17 6 18 23 syl3anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 − 𝑍 ) ∈ 𝐵 )
25 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 − 𝑍 ) ∈ 𝐵 )
26 17 7 18 25 syl3anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑍 ) ∈ 𝐵 )
27 8 2 pltval ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 − 𝑍 ) ∈ 𝐵 ∧ ( 𝑌 − 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 − 𝑍 ) < ( 𝑌 − 𝑍 ) ↔ ( ( 𝑋 − 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 − 𝑍 ) ∧ ( 𝑋 − 𝑍 ) ≠ ( 𝑌 − 𝑍 ) ) ) )
28 5 24 26 27 syl3anc ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑋 − 𝑍 ) < ( 𝑌 − 𝑍 ) ↔ ( ( 𝑋 − 𝑍 ) ( le ‘ 𝐺 ) ( 𝑌 − 𝑍 ) ∧ ( 𝑋 − 𝑍 ) ≠ ( 𝑌 − 𝑍 ) ) ) )
29 14 22 28 mpbir2and ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 − 𝑍 ) < ( 𝑌 − 𝑍 ) )