ogrpaddltrd

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

	Ref	Expression
Hypotheses	ogrpaddlt.0	$⊢ B = {Base}_{G}$
	ogrpaddlt.1	$⊢ \underset{˙}{<} = <_{G}$
	ogrpaddlt.2	$⊢ \underset{˙}{+} = +_{G}$
	ogrpaddltrd.1	$⊢ φ \to G \in V$
	ogrpaddltrd.2	$⊢ φ \to {opp}_{𝑔} (G) \in oGrp$
	ogrpaddltrd.3	$⊢ φ \to X \in B$
	ogrpaddltrd.4	$⊢ φ \to Y \in B$
	ogrpaddltrd.5	$⊢ φ \to Z \in B$
	ogrpaddltrd.6	$⊢ φ \to X \underset{˙}{<} Y$
Assertion	ogrpaddltrd	$⊢ φ \to (Z \underset{˙}{+} X) \underset{˙}{<} (Z \underset{˙}{+} Y)$

Proof

Step	Hyp	Ref	Expression
1		ogrpaddlt.0	$⊢ B = {Base}_{G}$
2		ogrpaddlt.1	$⊢ \underset{˙}{<} = <_{G}$
3		ogrpaddlt.2	$⊢ \underset{˙}{+} = +_{G}$
4		ogrpaddltrd.1	$⊢ φ \to G \in V$
5		ogrpaddltrd.2	$⊢ φ \to {opp}_{𝑔} (G) \in oGrp$
6		ogrpaddltrd.3	$⊢ φ \to X \in B$
7		ogrpaddltrd.4	$⊢ φ \to Y \in B$
8		ogrpaddltrd.5	$⊢ φ \to Z \in B$
9		ogrpaddltrd.6	$⊢ φ \to X \underset{˙}{<} Y$
10		eqid	$⊢ {opp}_{𝑔} (G) = {opp}_{𝑔} (G)$
11	10 2	oppglt	$⊢ G \in V \to \underset{˙}{<} = <_{{opp}_{𝑔} (G)}$
12	4 11	syl	$⊢ φ \to \underset{˙}{<} = <_{{opp}_{𝑔} (G)}$
13	12	breqd	$⊢ φ \to (X \underset{˙}{<} Y \leftrightarrow X <_{{opp}_{𝑔} (G)} Y)$
14	9 13	mpbid	$⊢ φ \to X <_{{opp}_{𝑔} (G)} Y$
15	10 1	oppgbas	$⊢ B = {Base}_{{opp}_{𝑔} (G)}$
16		eqid	$⊢ <_{{opp}_{𝑔} (G)} = <_{{opp}_{𝑔} (G)}$
17		eqid	$⊢ +_{{opp}_{𝑔} (G)} = +_{{opp}_{𝑔} (G)}$
18	15 16 17	ogrpaddlt	$⊢ ({opp}_{𝑔} (G) \in oGrp \land (X \in B \land Y \in B \land Z \in B) \land X <_{{opp}_{𝑔} (G)} Y) \to (X +_{{opp}_{𝑔} (G)} Z) <_{{opp}_{𝑔} (G)} (Y +_{{opp}_{𝑔} (G)} Z)$
19	5 6 7 8 14 18	syl131anc	$⊢ φ \to (X +_{{opp}_{𝑔} (G)} Z) <_{{opp}_{𝑔} (G)} (Y +_{{opp}_{𝑔} (G)} Z)$
20	3 10 17	oppgplus	$⊢ X +_{{opp}_{𝑔} (G)} Z = Z \underset{˙}{+} X$
21	3 10 17	oppgplus	$⊢ Y +_{{opp}_{𝑔} (G)} Z = Z \underset{˙}{+} Y$
22	19 20 21	3brtr3g	$⊢ φ \to (Z \underset{˙}{+} X) <_{{opp}_{𝑔} (G)} (Z \underset{˙}{+} Y)$
23	12	breqd	$⊢ φ \to ((Z \underset{˙}{+} X) \underset{˙}{<} (Z \underset{˙}{+} Y) \leftrightarrow (Z \underset{˙}{+} X) <_{{opp}_{𝑔} (G)} (Z \underset{˙}{+} Y))$
24	22 23	mpbird	$⊢ φ \to (Z \underset{˙}{+} X) \underset{˙}{<} (Z \underset{˙}{+} Y)$

Metamath Proof Explorer

Theorem ogrpaddltrd

Proof