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	$⊢ B = {Base}_{G}$
	ogrpsublt.1	$⊢ \underset{˙}{<} = <_{G}$
	ogrpsublt.2	$⊢ \underset{˙}{-} = -_{G}$
Assertion	ogrpsublt	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{-} Z) \underset{˙}{<} (Y \underset{˙}{-} Z)$

Proof

Step	Hyp	Ref	Expression
1		ogrpsublt.0	$⊢ B = {Base}_{G}$
2		ogrpsublt.1	$⊢ \underset{˙}{<} = <_{G}$
3		ogrpsublt.2	$⊢ \underset{˙}{-} = -_{G}$
4		simp3	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \underset{˙}{<} Y$
5		simp1	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to G \in oGrp$
6		simp21	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \in B$
7		simp22	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to Y \in B$
8		eqid	$⊢ \leq_{G} = \leq_{G}$
9	8 2	pltval	$⊢ (G \in oGrp \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{G} Y \land X \neq Y))$
10	5 6 7 9	syl3anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{G} Y \land X \neq Y))$
11	4 10	mpbid	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \leq_{G} Y \land X \neq Y)$
12	11	simpld	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \leq_{G} Y$
13	1 8 3	ogrpsub	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \leq_{G} Y) \to (X \underset{˙}{-} Z) \leq_{G} (Y \underset{˙}{-} Z)$
14	12 13	syld3an3	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{-} Z) \leq_{G} (Y \underset{˙}{-} Z)$
15	11	simprd	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \neq Y$
16		ogrpgrp	$⊢ G \in oGrp \to G \in Grp$
17	5 16	syl	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to G \in Grp$
18		simp23	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to Z \in B$
19	1 3	grpsubrcan	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Z = Y \underset{˙}{-} Z \leftrightarrow X = Y)$
20	17 6 7 18 19	syl13anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{-} Z = Y \underset{˙}{-} Z \leftrightarrow X = Y)$
21	20	necon3bid	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{-} Z \neq Y \underset{˙}{-} Z \leftrightarrow X \neq Y)$
22	15 21	mpbird	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \underset{˙}{-} Z \neq Y \underset{˙}{-} Z$
23	1 3	grpsubcl	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \underset{˙}{-} Z \in B$
24	17 6 18 23	syl3anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \underset{˙}{-} Z \in B$
25	1 3	grpsubcl	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to Y \underset{˙}{-} Z \in B$
26	17 7 18 25	syl3anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to Y \underset{˙}{-} Z \in B$
27	8 2	pltval	$⊢ (G \in oGrp \land X \underset{˙}{-} Z \in B \land Y \underset{˙}{-} Z \in B) \to ((X \underset{˙}{-} Z) \underset{˙}{<} (Y \underset{˙}{-} Z) \leftrightarrow ((X \underset{˙}{-} Z) \leq_{G} (Y \underset{˙}{-} Z) \land X \underset{˙}{-} Z \neq Y \underset{˙}{-} Z))$
28	5 24 26 27	syl3anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to ((X \underset{˙}{-} Z) \underset{˙}{<} (Y \underset{˙}{-} Z) \leftrightarrow ((X \underset{˙}{-} Z) \leq_{G} (Y \underset{˙}{-} Z) \land X \underset{˙}{-} Z \neq Y \underset{˙}{-} Z))$
29	14 22 28	mpbir2and	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \underset{˙}{-} Z) \underset{˙}{<} (Y \underset{˙}{-} Z)$

Metamath Proof Explorer

Theorem ogrpsublt

Proof