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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 − 𝑍 ) < ( 𝑌 − 𝑍 ) )