Metamath Proof Explorer

Theorem ogrpinvlt

Description: In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018)

Ref Expression
Hypotheses ogrpinvlt.0 ⊢ B = Base G
ogrpinvlt.1 ⊢ < ˙ = < G
ogrpinvlt.2 ⊢ I = inv g ⁡ G
Assertion ogrpinvlt ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X < ˙ Y ↔ I ⁡ Y < ˙ I ⁡ X

Proof

Step Hyp Ref Expression
1 ogrpinvlt.0 ⊢ B = Base G
2 ogrpinvlt.1 ⊢ < ˙ = < G
3 ogrpinvlt.2 ⊢ I = inv g ⁡ G
4 simp1l ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → G ∈ oGrp
5 simp2 ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X ∈ B
6 simp3 ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
7 ogrpgrp ⊢ G ∈ oGrp → G ∈ Grp
8 4 7 syl ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → G ∈ Grp
9 1 3 grpinvcl ⊢ G ∈ Grp ∧ Y ∈ B → I ⁡ Y ∈ B
10 8 6 9 syl2anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ Y ∈ B
11 eqid ⊢ + G = + G
12 1 2 11 ogrpaddltbi ⊢ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B ∧ I ⁡ Y ∈ B → X < ˙ Y ↔ X + G I ⁡ Y < ˙ Y + G I ⁡ Y
13 4 5 6 10 12 syl13anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X < ˙ Y ↔ X + G I ⁡ Y < ˙ Y + G I ⁡ Y
14 eqid ⊢ 0 G = 0 G
15 1 11 14 3 grprinv ⊢ G ∈ Grp ∧ Y ∈ B → Y + G I ⁡ Y = 0 G
16 8 6 15 syl2anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → Y + G I ⁡ Y = 0 G
17 16 breq2d ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X + G I ⁡ Y < ˙ Y + G I ⁡ Y ↔ X + G I ⁡ Y < ˙ 0 G
18 simp1r ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → opp 𝑔 ⁡ G ∈ oGrp
19 1 11 grpcl ⊢ G ∈ Grp ∧ X ∈ B ∧ I ⁡ Y ∈ B → X + G I ⁡ Y ∈ B
20 8 5 10 19 syl3anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X + G I ⁡ Y ∈ B
21 1 14 grpidcl ⊢ G ∈ Grp → 0 G ∈ B
22 4 7 21 3syl ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → 0 G ∈ B
23 1 3 grpinvcl ⊢ G ∈ Grp ∧ X ∈ B → I ⁡ X ∈ B
24 8 5 23 syl2anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∈ B
25 1 2 11 4 18 20 22 24 ogrpaddltrbid ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X + G I ⁡ Y < ˙ 0 G ↔ I ⁡ X + G X + G I ⁡ Y < ˙ I ⁡ X + G 0 G
26 13 17 25 3bitrd ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X < ˙ Y ↔ I ⁡ X + G X + G I ⁡ Y < ˙ I ⁡ X + G 0 G
27 1 11 14 3 grplinv ⊢ G ∈ Grp ∧ X ∈ B → I ⁡ X + G X = 0 G
28 8 5 27 syl2anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X + G X = 0 G
29 28 oveq1d ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X + G X + G I ⁡ Y = 0 G + G I ⁡ Y
30 1 11 grpass ⊢ G ∈ Grp ∧ I ⁡ X ∈ B ∧ X ∈ B ∧ I ⁡ Y ∈ B → I ⁡ X + G X + G I ⁡ Y = I ⁡ X + G X + G I ⁡ Y
31 8 24 5 10 30 syl13anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X + G X + G I ⁡ Y = I ⁡ X + G X + G I ⁡ Y
32 1 11 14 grplid ⊢ G ∈ Grp ∧ I ⁡ Y ∈ B → 0 G + G I ⁡ Y = I ⁡ Y
33 8 10 32 syl2anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → 0 G + G I ⁡ Y = I ⁡ Y
34 29 31 33 3eqtr3d ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X + G X + G I ⁡ Y = I ⁡ Y
35 1 11 14 grprid ⊢ G ∈ Grp ∧ I ⁡ X ∈ B → I ⁡ X + G 0 G = I ⁡ X
36 8 24 35 syl2anc ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X + G 0 G = I ⁡ X
37 34 36 breq12d ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → I ⁡ X + G X + G I ⁡ Y < ˙ I ⁡ X + G 0 G ↔ I ⁡ Y < ˙ I ⁡ X
38 26 37 bitrd ⊢ G ∈ oGrp ∧ opp 𝑔 ⁡ G ∈ oGrp ∧ X ∈ B ∧ Y ∈ B → X < ˙ Y ↔ I ⁡ Y < ˙ I ⁡ X