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

Metamath Proof Explorer

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