ogrpaddlt

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

	Ref	Expression
Hypotheses	ogrpaddlt.0	$⊢ B = {Base}_{G}$
	ogrpaddlt.1	$⊢ \underset{˙}{<} = <_{G}$
	ogrpaddlt.2	$⊢ \underset{˙}{+} = +_{G}$
Assertion	ogrpaddlt	$⊢ (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		ogrpaddlt.0	$⊢ B = {Base}_{G}$
2		ogrpaddlt.1	$⊢ \underset{˙}{<} = <_{G}$
3		ogrpaddlt.2	$⊢ \underset{˙}{+} = +_{G}$
4		isogrp	$⊢ G \in oGrp \leftrightarrow (G \in Grp \land G \in oMnd)$
5	4	simprbi	$⊢ G \in oGrp \to G \in oMnd$
6	5	3ad2ant1	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to G \in oMnd$
7		simp2	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to (X \in B \land Y \in B \land Z \in B)$
8		simp1	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to G \in oGrp$
9		simp21	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \in B$
10		simp22	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to Y \in B$
11		simp3	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \underset{˙}{<} Y$
12		eqid	$⊢ \leq_{G} = \leq_{G}$
13	12 2	pltle	$⊢ (G \in oGrp \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \leq_{G} Y)$
14	13	imp	$⊢ ((G \in oGrp \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \leq_{G} Y$
15	8 9 10 11 14	syl31anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \leq_{G} Y$
16	1 12 3	omndadd	$⊢ (G \in oMnd \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)$
17	6 7 15 16	syl3anc	$⊢ (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)$
18	2	pltne	$⊢ (G \in oGrp \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \neq Y)$
19	18	imp	$⊢ ((G \in oGrp \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to X \neq Y$
20	8 9 10 11 19	syl31anc	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{<} Y) \to X \neq Y$
21		ogrpgrp	$⊢ G \in oGrp \to G \in Grp$
22	1 3	grprcan	$⊢ (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)$
23	22	biimpd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z = Y \underset{˙}{+} Z \to X = Y)$
24	21 23	sylan	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z = Y \underset{˙}{+} Z \to X = Y)$
25	24	necon3d	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B)) \to (X \neq Y \to X \underset{˙}{+} Z \neq Y \underset{˙}{+} Z)$
26	25	3impia	$⊢ (G \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X \neq Y) \to X \underset{˙}{+} Z \neq Y \underset{˙}{+} Z$
27	8 7 20 26	syl3anc	$⊢ (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$
28		ovex	$⊢ X \underset{˙}{+} Z \in V$
29		ovex	$⊢ Y \underset{˙}{+} Z \in V$
30	12 2	pltval	$⊢ (G \in oGrp \land X \underset{˙}{+} Z \in V \land Y \underset{˙}{+} Z \in V) \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))$
31	28 29 30	mp3an23	$⊢ G \in oGrp \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))$
32	31	3ad2ant1	$⊢ (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))$
33	17 27 32	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 ogrpaddlt

Proof