Metamath Proof Explorer

Theorem ogrpinv0lt

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

Ref Expression
Hypotheses ogrpinvlt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ogrpinvlt.1 ⊢ < = ( lt ‘ 𝐺 )
ogrpinvlt.2 ⊢ 𝐼 = ( invg ‘ 𝐺 )
ogrpinv0lt.3 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion ogrpinv0lt ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ ( 𝐼 ‘ 𝑋 ) < 0 ) )

Proof

Step Hyp Ref Expression
1 ogrpinvlt.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ogrpinvlt.1 ⊢ < = ( lt ‘ 𝐺 )
3 ogrpinvlt.2 ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 ogrpinv0lt.3 ⊢ 0 = ( 0g ‘ 𝐺 )
5 simpll ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → 𝐺 ∈ oGrp )
6 ogrpgrp ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )
7 5 6 syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → 𝐺 ∈ Grp )
8 1 4 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
9 7 8 syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → 0 ∈ 𝐵 )
10 simplr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → 𝑋 ∈ 𝐵 )
11 1 3 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
12 7 10 11 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
13 simpr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → 0 < 𝑋 )
14 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
15 1 2 14 ogrpaddlt ⊢ ( ( 𝐺 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) < ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
16 5 9 10 12 13 15 syl131anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) < ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
17 1 14 4 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
18 7 12 17 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
19 1 14 4 3 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = 0 )
20 7 10 19 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = 0 )
21 16 18 20 3brtr3d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( 𝐼 ‘ 𝑋 ) < 0 )
22 simpll ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → 𝐺 ∈ oGrp )
23 22 6 syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → 𝐺 ∈ Grp )
24 simplr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → 𝑋 ∈ 𝐵 )
25 23 24 11 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
26 22 6 8 3syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → 0 ∈ 𝐵 )
27 simpr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → ( 𝐼 ‘ 𝑋 ) < 0 )
28 1 2 14 ogrpaddlt ⊢ ( ( 𝐺 ∈ oGrp ∧ ( ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) < ( 0 ( +g ‘ 𝐺 ) 𝑋 ) )
29 22 25 26 24 27 28 syl131anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) < ( 0 ( +g ‘ 𝐺 ) 𝑋 ) )
30 1 14 4 3 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) = 0 )
31 23 24 30 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) = 0 )
32 1 14 4 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) 𝑋 ) = 𝑋 )
33 23 24 32 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → ( 0 ( +g ‘ 𝐺 ) 𝑋 ) = 𝑋 )
34 29 31 33 3brtr3d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) < 0 ) → 0 < 𝑋 )
35 21 34 impbida ⊢ ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ ( 𝐼 ‘ 𝑋 ) < 0 ) )