This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑍 + 𝑋 ) < ( 𝑍 + 𝑌 ) )