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 
|- B = ( Base ` G )
ogrpsub.1 
|- .<_ = ( le ` G )
ogrpinv.2 
|- I = ( invg ` G )
ogrpinv.3 
|- .0. = ( 0g ` G )
Assertion ogrpinv0le 
|- ( ( G e. oGrp /\ X e. B ) -> ( .0. .<_ X <-> ( I ` X ) .<_ .0. ) )

Proof

Step Hyp Ref Expression
1 ogrpsub.0 
 |-  B = ( Base ` G )
2 ogrpsub.1 
 |-  .<_ = ( le ` G )
3 ogrpinv.2 
 |-  I = ( invg ` G )
4 ogrpinv.3 
 |-  .0. = ( 0g ` G )
5 isogrp 
 |-  ( G e. oGrp <-> ( G e. Grp /\ G e. oMnd ) )
6 5 simprbi 
 |-  ( G e. oGrp -> G e. oMnd )
7 6 ad2antrr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> G e. oMnd )
8 omndmnd 
 |-  ( G e. oMnd -> G e. Mnd )
9 1 4 mndidcl 
 |-  ( G e. Mnd -> .0. e. B )
10 7 8 9 3syl 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> .0. e. B )
11 simplr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> X e. B )
12 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
13 12 ad2antrr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> G e. Grp )
14 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` X ) e. B )
15 13 11 14 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> ( I ` X ) e. B )
16 simpr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> .0. .<_ X )
17 eqid 
 |-  ( +g ` G ) = ( +g ` G )
18 1 2 17 omndadd 
 |-  ( ( G e. oMnd /\ ( .0. e. B /\ X e. B /\ ( I ` X ) e. B ) /\ .0. .<_ X ) -> ( .0. ( +g ` G ) ( I ` X ) ) .<_ ( X ( +g ` G ) ( I ` X ) ) )
19 7 10 11 15 16 18 syl131anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> ( .0. ( +g ` G ) ( I ` X ) ) .<_ ( X ( +g ` G ) ( I ` X ) ) )
20 1 17 4 grplid 
 |-  ( ( G e. Grp /\ ( I ` X ) e. B ) -> ( .0. ( +g ` G ) ( I ` X ) ) = ( I ` X ) )
21 13 15 20 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> ( .0. ( +g ` G ) ( I ` X ) ) = ( I ` X ) )
22 1 17 4 3 grprinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X ( +g ` G ) ( I ` X ) ) = .0. )
23 13 11 22 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> ( X ( +g ` G ) ( I ` X ) ) = .0. )
24 19 21 23 3brtr3d 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .<_ X ) -> ( I ` X ) .<_ .0. )
25 6 ad2antrr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> G e. oMnd )
26 12 ad2antrr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> G e. Grp )
27 simplr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> X e. B )
28 26 27 14 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> ( I ` X ) e. B )
29 25 8 9 3syl 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> .0. e. B )
30 simpr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> ( I ` X ) .<_ .0. )
31 1 2 17 omndadd 
 |-  ( ( G e. oMnd /\ ( ( I ` X ) e. B /\ .0. e. B /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> ( ( I ` X ) ( +g ` G ) X ) .<_ ( .0. ( +g ` G ) X ) )
32 25 28 29 27 30 31 syl131anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> ( ( I ` X ) ( +g ` G ) X ) .<_ ( .0. ( +g ` G ) X ) )
33 1 17 4 3 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( I ` X ) ( +g ` G ) X ) = .0. )
34 26 27 33 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> ( ( I ` X ) ( +g ` G ) X ) = .0. )
35 1 17 4 grplid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( .0. ( +g ` G ) X ) = X )
36 26 27 35 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> ( .0. ( +g ` G ) X ) = X )
37 32 34 36 3brtr3d 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .<_ .0. ) -> .0. .<_ X )
38 24 37 impbida 
 |-  ( ( G e. oGrp /\ X e. B ) -> ( .0. .<_ X <-> ( I ` X ) .<_ .0. ) )