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

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		ogrpaddltrd.6	⊢ ( 𝜑 → 𝑋 < 𝑌 )
10		eqid	⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
11	10 2	oppglt	⊢ ( 𝐺 ∈ 𝑉 → < = ( lt ‘ ( oppg ‘ 𝐺 ) ) )
12	4 11	syl	⊢ ( 𝜑 → < = ( lt ‘ ( oppg ‘ 𝐺 ) ) )
13	12	breqd	⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ 𝑋 ( lt ‘ ( oppg ‘ 𝐺 ) ) 𝑌 ) )
14	9 13	mpbid	⊢ ( 𝜑 → 𝑋 ( lt ‘ ( oppg ‘ 𝐺 ) ) 𝑌 )
15	10 1	oppgbas	⊢ 𝐵 = ( Base ‘ ( oppg ‘ 𝐺 ) )
16		eqid	⊢ ( lt ‘ ( oppg ‘ 𝐺 ) ) = ( lt ‘ ( oppg ‘ 𝐺 ) )
17		eqid	⊢ ( +g ‘ ( oppg ‘ 𝐺 ) ) = ( +g ‘ ( oppg ‘ 𝐺 ) )
18	15 16 17	ogrpaddlt	⊢ ( ( ( oppg ‘ 𝐺 ) ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ( lt ‘ ( oppg ‘ 𝐺 ) ) 𝑌 ) → ( 𝑋 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) ( lt ‘ ( oppg ‘ 𝐺 ) ) ( 𝑌 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) )
19	5 6 7 8 14 18	syl131anc	⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) ( lt ‘ ( oppg ‘ 𝐺 ) ) ( 𝑌 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) )
20	3 10 17	oppgplus	⊢ ( 𝑋 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) = ( 𝑍 + 𝑋 )
21	3 10 17	oppgplus	⊢ ( 𝑌 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑍 ) = ( 𝑍 + 𝑌 )
22	19 20 21	3brtr3g	⊢ ( 𝜑 → ( 𝑍 + 𝑋 ) ( lt ‘ ( oppg ‘ 𝐺 ) ) ( 𝑍 + 𝑌 ) )
23	12	breqd	⊢ ( 𝜑 → ( ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) ↔ ( 𝑍 + 𝑋 ) ( lt ‘ ( oppg ‘ 𝐺 ) ) ( 𝑍 + 𝑌 ) ) )
24	22 23	mpbird	⊢ ( 𝜑 → ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) )