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

Metamath Proof Explorer

Theorem ogrpinv0le

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

Ref Expression
Hypotheses ogrpsub.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ogrpsub.1 ⊢ ≤ = ( le ‘ 𝐺 )
ogrpinv.2 ⊢ 𝐼 = ( invg ‘ 𝐺 )
ogrpinv.3 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion ogrpinv0le ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) → ( 0 ≤ 𝑋 ↔ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) )

Proof

Step Hyp Ref Expression
1 ogrpsub.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ogrpsub.1 ⊢ ≤ = ( le ‘ 𝐺 )
3 ogrpinv.2 ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 ogrpinv.3 ⊢ 0 = ( 0g ‘ 𝐺 )
5 isogrp ⊢ ( 𝐺 ∈ oGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd ) )
6 5 simprbi ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ oMnd )
7 6 ad2antrr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → 𝐺 ∈ oMnd )
8 omndmnd ⊢ ( 𝐺 ∈ oMnd → 𝐺 ∈ Mnd )
9 1 4 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
10 7 8 9 3syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → 0 ∈ 𝐵 )
11 simplr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
12 ogrpgrp ⊢ ( 𝐺 ∈ oGrp → 𝐺 ∈ Grp )
13 12 ad2antrr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → 𝐺 ∈ Grp )
14 1 3 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
15 13 11 14 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
16 simpr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → 0 ≤ 𝑋 )
17 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
18 1 2 17 omndadd ⊢ ( ( 𝐺 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) ≤ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
19 7 10 11 15 16 18 syl131anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) ≤ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
20 1 17 4 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
21 13 15 20 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
22 1 17 4 3 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = 0 )
23 13 11 22 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = 0 )
24 19 21 23 3brtr3d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ≤ 𝑋 ) → ( 𝐼 ‘ 𝑋 ) ≤ 0 )
25 6 ad2antrr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → 𝐺 ∈ oMnd )
26 12 ad2antrr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → 𝐺 ∈ Grp )
27 simplr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → 𝑋 ∈ 𝐵 )
28 26 27 14 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
29 25 8 9 3syl ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → 0 ∈ 𝐵 )
30 simpr ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → ( 𝐼 ‘ 𝑋 ) ≤ 0 )
31 1 2 17 omndadd ⊢ ( ( 𝐺 ∈ oMnd ∧ ( ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ≤ ( 0 ( +g ‘ 𝐺 ) 𝑋 ) )
32 25 28 29 27 30 31 syl131anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ≤ ( 0 ( +g ‘ 𝐺 ) 𝑋 ) )
33 1 17 4 3 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) = 0 )
34 26 27 33 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → ( ( 𝐼 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) = 0 )
35 1 17 4 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) 𝑋 ) = 𝑋 )
36 26 27 35 syl2anc ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → ( 0 ( +g ‘ 𝐺 ) 𝑋 ) = 𝑋 )
37 32 34 36 3brtr3d ⊢ ( ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) → 0 ≤ 𝑋 )
38 24 37 impbida ⊢ ( ( 𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ) → ( 0 ≤ 𝑋 ↔ ( 𝐼 ‘ 𝑋 ) ≤ 0 ) )