Theorem ogrpaddltrbid

Description: In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 4-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$$
Assertion	ogrpaddltrbid	$$⊢\phi \to \left(X\underset{\dot{}}{<}Y\leftrightarrow \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\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	4	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to G\in V$$
10	5	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to {opp}_{𝑔}\left(G\right)\in \mathrm{oGrp}$$
11	6	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to X\in B$$
12	7	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to Y\in B$$
13	8	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to Z\in B$$
14		simpr	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to X\underset{\dot{}}{<}Y$$
15	1 2 3 9 10 11 12 13 14	ogrpaddltrd	$$⊢\left(\phi \wedge X\underset{\dot{}}{<}Y\right)\to \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)$$
16	4	adantr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to G\in V$$
17	5	adantr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to {opp}_{𝑔}\left(G\right)\in \mathrm{oGrp}$$
18		ogrpgrp	$$⊢{opp}_{𝑔}\left(G\right)\in \mathrm{oGrp}\to {opp}_{𝑔}\left(G\right)\in \mathrm{Grp}$$
19	5 18	syl	$$⊢\phi \to {opp}_{𝑔}\left(G\right)\in \mathrm{Grp}$$
20	19	adantr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to {opp}_{𝑔}\left(G\right)\in \mathrm{Grp}$$
21	6	adantr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to X\in B$$
22	8	adantr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to Z\in B$$
23		eqid	$$⊢{opp}_{𝑔}\left(G\right)={opp}_{𝑔}\left(G\right)$$
24		eqid	$$⊢{+}_{{opp}_{𝑔}\left(G\right)}={+}_{{opp}_{𝑔}\left(G\right)}$$
25	3 23 24	oppgplus	$$⊢X{+}_{{opp}_{𝑔}\left(G\right)}Z=Z\underset{\dot{}}{+}X$$
26	23 1	oppgbas	$$⊢B={\mathrm{Base}}_{{opp}_{𝑔}\left(G\right)}$$
27	26 24	grpcl	$$⊢\left({opp}_{𝑔}\left(G\right)\in \mathrm{Grp}\wedge X\in B\wedge Z\in B\right)\to X{+}_{{opp}_{𝑔}\left(G\right)}Z\in B$$
28	25 27	eqeltrrid	$$⊢\left({opp}_{𝑔}\left(G\right)\in \mathrm{Grp}\wedge X\in B\wedge Z\in B\right)\to Z\underset{\dot{}}{+}X\in B$$
29	20 21 22 28	syl3anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to Z\underset{\dot{}}{+}X\in B$$
30	7	adantr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to Y\in B$$
31	3 23 24	oppgplus	$$⊢Y{+}_{{opp}_{𝑔}\left(G\right)}Z=Z\underset{\dot{}}{+}Y$$
32	26 24	grpcl	$$⊢\left({opp}_{𝑔}\left(G\right)\in \mathrm{Grp}\wedge Y\in B\wedge Z\in B\right)\to Y{+}_{{opp}_{𝑔}\left(G\right)}Z\in B$$
33	31 32	eqeltrrid	$$⊢\left({opp}_{𝑔}\left(G\right)\in \mathrm{Grp}\wedge Y\in B\wedge Z\in B\right)\to Z\underset{\dot{}}{+}Y\in B$$
34	20 30 22 33	syl3anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to Z\underset{\dot{}}{+}Y\in B$$
35	23	oppggrpb	$$⊢G\in \mathrm{Grp}\leftrightarrow {opp}_{𝑔}\left(G\right)\in \mathrm{Grp}$$
36	20 35	sylibr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to G\in \mathrm{Grp}$$
37		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
38	1 37	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge Z\in B\right)\to {inv}_g\left(G\right)\left(Z\right)\in B$$
39	36 22 38	syl2anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to {inv}_g\left(G\right)\left(Z\right)\in B$$
40		simpr	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)$$
41	1 2 3 16 17 29 34 39 40	ogrpaddltrd	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}X\right)\right)\underset{\dot{}}{<}\left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)\right)$$
42		eqid	$$⊢0_G=0_G$$
43	1 3 42 37	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge Z\in B\right)\to {inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z=0_G$$
44	36 22 43	syl2anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to {inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z=0_G$$
45	44	oveq1d	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}X=0_G\underset{\dot{}}{+}X$$
46	1 3	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left({inv}_g\left(G\right)\left(Z\right)\in B\wedge Z\in B\wedge X\in B\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}X={inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}X\right)$$
47	36 39 22 21 46	syl13anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}X={inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}X\right)$$
48	1 3 42	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to 0_G\underset{\dot{}}{+}X=X$$
49	36 21 48	syl2anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to 0_G\underset{\dot{}}{+}X=X$$
50	45 47 49	3eqtr3d	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to {inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}X\right)=X$$
51	44	oveq1d	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y=0_G\underset{\dot{}}{+}Y$$
52	1 3	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left({inv}_g\left(G\right)\left(Z\right)\in B\wedge Z\in B\wedge Y\in B\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y={inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)$$
53	36 39 22 30 52	syl13anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to \left({inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y={inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)$$
54	1 3 42	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to 0_G\underset{\dot{}}{+}Y=Y$$
55	36 30 54	syl2anc	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to 0_G\underset{\dot{}}{+}Y=Y$$
56	51 53 55	3eqtr3d	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to {inv}_g\left(G\right)\left(Z\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)=Y$$
57	41 50 56	3brtr3d	$$⊢\left(\phi \wedge \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)\to X\underset{\dot{}}{<}Y$$
58	15 57	impbida	$$⊢\phi \to \left(X\underset{\dot{}}{<}Y\leftrightarrow \left(Z\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(Z\underset{\dot{}}{+}Y\right)\right)$$