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 
|- B = ( Base ` G )
ogrpinvlt.1 
|- .< = ( lt ` G )
ogrpinvlt.2 
|- I = ( invg ` G )
ogrpinv0lt.3 
|- .0. = ( 0g ` G )
Assertion ogrpinv0lt 
|- ( ( G e. oGrp /\ X e. B ) -> ( .0. .< X <-> ( I ` X ) .< .0. ) )

Proof

Step Hyp Ref Expression
1 ogrpinvlt.0 
 |-  B = ( Base ` G )
2 ogrpinvlt.1 
 |-  .< = ( lt ` G )
3 ogrpinvlt.2 
 |-  I = ( invg ` G )
4 ogrpinv0lt.3 
 |-  .0. = ( 0g ` G )
5 simpll 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> G e. oGrp )
6 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
7 5 6 syl 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> G e. Grp )
8 1 4 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
9 7 8 syl 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> .0. e. B )
10 simplr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> X e. B )
11 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` X ) e. B )
12 7 10 11 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> ( I ` X ) e. B )
13 simpr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> .0. .< X )
14 eqid 
 |-  ( +g ` G ) = ( +g ` G )
15 1 2 14 ogrpaddlt 
 |-  ( ( G e. oGrp /\ ( .0. e. B /\ X e. B /\ ( I ` X ) e. B ) /\ .0. .< X ) -> ( .0. ( +g ` G ) ( I ` X ) ) .< ( X ( +g ` G ) ( I ` X ) ) )
16 5 9 10 12 13 15 syl131anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> ( .0. ( +g ` G ) ( I ` X ) ) .< ( X ( +g ` G ) ( I ` X ) ) )
17 1 14 4 grplid 
 |-  ( ( G e. Grp /\ ( I ` X ) e. B ) -> ( .0. ( +g ` G ) ( I ` X ) ) = ( I ` X ) )
18 7 12 17 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> ( .0. ( +g ` G ) ( I ` X ) ) = ( I ` X ) )
19 1 14 4 3 grprinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X ( +g ` G ) ( I ` X ) ) = .0. )
20 7 10 19 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> ( X ( +g ` G ) ( I ` X ) ) = .0. )
21 16 18 20 3brtr3d 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ .0. .< X ) -> ( I ` X ) .< .0. )
22 simpll 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> G e. oGrp )
23 22 6 syl 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> G e. Grp )
24 simplr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> X e. B )
25 23 24 11 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> ( I ` X ) e. B )
26 22 6 8 3syl 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> .0. e. B )
27 simpr 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> ( I ` X ) .< .0. )
28 1 2 14 ogrpaddlt 
 |-  ( ( G e. oGrp /\ ( ( I ` X ) e. B /\ .0. e. B /\ X e. B ) /\ ( I ` X ) .< .0. ) -> ( ( I ` X ) ( +g ` G ) X ) .< ( .0. ( +g ` G ) X ) )
29 22 25 26 24 27 28 syl131anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> ( ( I ` X ) ( +g ` G ) X ) .< ( .0. ( +g ` G ) X ) )
30 1 14 4 3 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( I ` X ) ( +g ` G ) X ) = .0. )
31 23 24 30 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> ( ( I ` X ) ( +g ` G ) X ) = .0. )
32 1 14 4 grplid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( .0. ( +g ` G ) X ) = X )
33 23 24 32 syl2anc 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> ( .0. ( +g ` G ) X ) = X )
34 29 31 33 3brtr3d 
 |-  ( ( ( G e. oGrp /\ X e. B ) /\ ( I ` X ) .< .0. ) -> .0. .< X )
35 21 34 impbida 
 |-  ( ( G e. oGrp /\ X e. B ) -> ( .0. .< X <-> ( I ` X ) .< .0. ) )