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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ogrpaddlt.1	⊢ < = ( lt ‘ 𝐺 )
	ogrpaddlt.2	⊢ + = ( +g ‘ 𝐺 )
	ogrpaddltrd.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	ogrpaddltrd.2	⊢ ( 𝜑 → ( oppg ‘ 𝐺 ) ∈ oGrp )
	ogrpaddltrd.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ogrpaddltrd.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ogrpaddltrd.5	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	ogrpaddltrbid	⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ogrpaddlt.0	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ogrpaddlt.1	⊢ < = ( lt ‘ 𝐺 )
3		ogrpaddlt.2	⊢ + = ( +g ‘ 𝐺 )
4		ogrpaddltrd.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		ogrpaddltrd.2	⊢ ( 𝜑 → ( oppg ‘ 𝐺 ) ∈ oGrp )
6		ogrpaddltrd.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		ogrpaddltrd.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		ogrpaddltrd.5	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝐺 ∈ 𝑉 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( oppg ‘ 𝐺 ) ∈ oGrp )
11	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ 𝐵 )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ 𝐵 )
13	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑍 ∈ 𝐵 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
15	1 2 3 9 10 11 12 13 14	ogrpaddltrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) )
16	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → 𝐺 ∈ 𝑉 )
17	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( oppg ‘ 𝐺 ) ∈ oGrp )
18		ogrpgrp	⊢ ( ( oppg ‘ 𝐺 ) ∈ oGrp → ( oppg ‘ 𝐺 ) ∈ Grp )
19	5 18	syl	⊢ ( 𝜑 → ( oppg ‘ 𝐺 ) ∈ Grp )
20	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( oppg ‘ 𝐺 ) ∈ Grp )
21	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → 𝑋 ∈ 𝐵 )
22	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → 𝑍 ∈ 𝐵 )
23		eqid	⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
24		eqid	⊢ ( +g ‘ ( oppg ‘ 𝐺 ) ) = ( +g ‘ ( oppg ‘ 𝐺 ) )
25	3 23 24	oppgplus	⊢ ( 𝑋 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) = ( 𝑍 + 𝑋 )
26	23 1	oppgbas	⊢ 𝐵 = ( Base ‘ ( oppg ‘ 𝐺 ) )
27	26 24	grpcl	⊢ ( ( ( oppg ‘ 𝐺 ) ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) ∈ 𝐵 )
28	25 27	eqeltrrid	⊢ ( ( ( oppg ‘ 𝐺 ) ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 + 𝑋 ) ∈ 𝐵 )
29	20 21 22 28	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( 𝑍 + 𝑋 ) ∈ 𝐵 )
30	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → 𝑌 ∈ 𝐵 )
31	3 23 24	oppgplus	⊢ ( 𝑌 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) = ( 𝑍 + 𝑌 )
32	26 24	grpcl	⊢ ( ( ( oppg ‘ 𝐺 ) ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) ∈ 𝐵 )
33	31 32	eqeltrrid	⊢ ( ( ( oppg ‘ 𝐺 ) ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 + 𝑌 ) ∈ 𝐵 )
34	20 30 22 33	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( 𝑍 + 𝑌 ) ∈ 𝐵 )
35	23	oppggrpb	⊢ ( 𝐺 ∈ Grp ↔ ( oppg ‘ 𝐺 ) ∈ Grp )
36	20 35	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → 𝐺 ∈ Grp )
37		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
38	1 37	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
39	36 22 38	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
40		simpr	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) )
41	1 2 3 16 17 29 34 39 40	ogrpaddltrd	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) < ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
42		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
43	1 3 42 37	grplinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) = ( 0g ‘ 𝐺 ) )
44	36 22 43	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) = ( 0g ‘ 𝐺 ) )
45	44	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( 0g ‘ 𝐺 ) + 𝑋 ) )
46	1 3	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) )
47	36 39 22 21 46	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) )
48	1 3 42	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑋 ) = 𝑋 )
49	36 21 48	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑋 ) = 𝑋 )
50	45 47 49	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) = 𝑋 )
51	44	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑌 ) = ( ( 0g ‘ 𝐺 ) + 𝑌 ) )
52	1 3	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑌 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
53	36 39 22 30 52	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑌 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
54	1 3 42	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑌 ) = 𝑌 )
55	36 30 54	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑌 ) = 𝑌 )
56	51 53 55	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) = 𝑌 )
57	41 50 56	3brtr3d	⊢ ( ( 𝜑 ∧ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) → 𝑋 < 𝑌 )
58	15 57	impbida	⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ) )