Metamath Proof Explorer

Theorem ogrpaddltbi

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 ‘ 𝐺 )
Assertion ogrpaddltbi ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 ogrpaddlt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ogrpaddlt.1 ⊢ < = ( lt ‘ 𝐺 )
3 ogrpaddlt.2 ⊢ + = ( +g ‘ 𝐺 )
4 1 2 3 ogrpaddlt ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) )
5 4 3expa ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) )
6 simpll ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → 𝐺 ∈ oGrp )
7 ogrpgrp ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )
8 6 7 syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → 𝐺 ∈ Grp )
9 simplr1 ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → 𝑋 ∈ 𝐵 )
10 simplr3 ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → 𝑍 ∈ 𝐵 )
11 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 + 𝑍 ) ∈ 𝐵 )
12 8 9 10 11 syl3anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑋 + 𝑍 ) ∈ 𝐵 )
13 simplr2 ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → 𝑌 ∈ 𝐵 )
14 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 + 𝑍 ) ∈ 𝐵 )
15 8 13 10 14 syl3anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑌 + 𝑍 ) ∈ 𝐵 )
16 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
17 1 16 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
18 8 10 17 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
19 simpr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) )
20 1 2 3 ogrpaddlt ⊢ ( ( 𝐺 ∈ oGrp ∧ ( ( 𝑋 + 𝑍 ) ∈ 𝐵 ∧ ( 𝑌 + 𝑍 ) ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( 𝑋 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) < ( ( 𝑌 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
21 6 12 15 18 19 20 syl131anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( 𝑋 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) < ( ( 𝑌 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
22 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑋 + ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
23 8 9 10 18 22 syl13anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( 𝑋 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑋 + ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
24 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
25 1 3 24 16 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 0g ‘ 𝐺 ) )
26 8 10 25 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 0g ‘ 𝐺 ) )
27 26 oveq2d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑋 + ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) = ( 𝑋 + ( 0g ‘ 𝐺 ) ) )
28 1 3 24 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
29 8 9 28 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
30 23 27 29 3eqtrd ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( 𝑋 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = 𝑋 )
31 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑌 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑌 + ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
32 8 13 10 18 31 syl13anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( 𝑌 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑌 + ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
33 26 oveq2d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑌 + ( 𝑍 + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) = ( 𝑌 + ( 0g ‘ 𝐺 ) ) )
34 1 3 24 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 + ( 0g ‘ 𝐺 ) ) = 𝑌 )
35 8 13 34 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( 𝑌 + ( 0g ‘ 𝐺 ) ) = 𝑌 )
36 32 33 35 3eqtrd ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → ( ( 𝑌 + 𝑍 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = 𝑌 )
37 21 30 36 3brtr3d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) → 𝑋 < 𝑌 )
38 5 37 impbida ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 + 𝑍 ) < ( 𝑌 + 𝑍 ) ) )