Theorem 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={\mathrm{Base}}_G$$
	ogrpaddlt.1	$$⊢\underset{\dot{}}{<}={<}_G$$
	ogrpaddlt.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	ogrpaddltrd.1	$$⊢\phi \to G\in V$$
	ogrpaddltrd.2	$$⊢\phi \to {opp}_{𝑔}\left(G\right)\in \mathrm{oGrp}$$
	ogrpaddltrd.3	$$⊢\phi \to X\in B$$
	ogrpaddltrd.4	$$⊢\phi \to Y\in B$$
	ogrpaddltrd.5	$$⊢\phi \to Z\in B$$
	ogrpaddltrd.6	$$⊢\phi \to X\underset{\dot{}}{<}Y$$
Assertion	ogrpaddltrd	$$⊢\phi \to \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)$$

Proof

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