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 
|- .< = ( lt ` G )
ogrpinvlt.2 
|- I = ( invg ` G )
Assertion ogrpinvlt 
|- ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( I ` Y ) .< ( I ` X ) ) )

Proof

Step Hyp Ref Expression
1 ogrpinvlt.0 
 |-  B = ( Base ` G )
2 ogrpinvlt.1 
 |-  .< = ( lt ` G )
3 ogrpinvlt.2 
 |-  I = ( invg ` G )
4 simp1l 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> G e. oGrp )
5 simp2 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> X e. B )
6 simp3 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> Y e. B )
7 ogrpgrp 
 |-  ( G e. oGrp -> G e. Grp )
8 4 7 syl 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> G e. Grp )
9 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( I ` Y ) e. B )
10 8 6 9 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( I ` Y ) e. B )
11 eqid 
 |-  ( +g ` G ) = ( +g ` G )
12 1 2 11 ogrpaddltbi 
 |-  ( ( G e. oGrp /\ ( X e. B /\ Y e. B /\ ( I ` Y ) e. B ) ) -> ( X .< Y <-> ( X ( +g ` G ) ( I ` Y ) ) .< ( Y ( +g ` G ) ( I ` Y ) ) ) )
13 4 5 6 10 12 syl13anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X ( +g ` G ) ( I ` Y ) ) .< ( Y ( +g ` G ) ( I ` Y ) ) ) )
14 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
15 1 11 14 3 grprinv 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( Y ( +g ` G ) ( I ` Y ) ) = ( 0g ` G ) )
16 8 6 15 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( Y ( +g ` G ) ( I ` Y ) ) = ( 0g ` G ) )
17 16 breq2d 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( X ( +g ` G ) ( I ` Y ) ) .< ( Y ( +g ` G ) ( I ` Y ) ) <-> ( X ( +g ` G ) ( I ` Y ) ) .< ( 0g ` G ) ) )
18 simp1r 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( oppG ` G ) e. oGrp )
19 1 11 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ ( I ` Y ) e. B ) -> ( X ( +g ` G ) ( I ` Y ) ) e. B )
20 8 5 10 19 syl3anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( X ( +g ` G ) ( I ` Y ) ) e. B )
21 1 14 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
22 4 7 21 3syl 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( 0g ` G ) e. B )
23 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` X ) e. B )
24 8 5 23 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( I ` X ) e. B )
25 1 2 11 4 18 20 22 24 ogrpaddltrbid 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( X ( +g ` G ) ( I ` Y ) ) .< ( 0g ` G ) <-> ( ( I ` X ) ( +g ` G ) ( X ( +g ` G ) ( I ` Y ) ) ) .< ( ( I ` X ) ( +g ` G ) ( 0g ` G ) ) ) )
26 13 17 25 3bitrd 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( ( I ` X ) ( +g ` G ) ( X ( +g ` G ) ( I ` Y ) ) ) .< ( ( I ` X ) ( +g ` G ) ( 0g ` G ) ) ) )
27 1 11 14 3 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( I ` X ) ( +g ` G ) X ) = ( 0g ` G ) )
28 8 5 27 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( I ` X ) ( +g ` G ) X ) = ( 0g ` G ) )
29 28 oveq1d 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( ( I ` X ) ( +g ` G ) X ) ( +g ` G ) ( I ` Y ) ) = ( ( 0g ` G ) ( +g ` G ) ( I ` Y ) ) )
30 1 11 grpass 
 |-  ( ( G e. Grp /\ ( ( I ` X ) e. B /\ X e. B /\ ( I ` Y ) e. B ) ) -> ( ( ( I ` X ) ( +g ` G ) X ) ( +g ` G ) ( I ` Y ) ) = ( ( I ` X ) ( +g ` G ) ( X ( +g ` G ) ( I ` Y ) ) ) )
31 8 24 5 10 30 syl13anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( ( I ` X ) ( +g ` G ) X ) ( +g ` G ) ( I ` Y ) ) = ( ( I ` X ) ( +g ` G ) ( X ( +g ` G ) ( I ` Y ) ) ) )
32 1 11 14 grplid 
 |-  ( ( G e. Grp /\ ( I ` Y ) e. B ) -> ( ( 0g ` G ) ( +g ` G ) ( I ` Y ) ) = ( I ` Y ) )
33 8 10 32 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( 0g ` G ) ( +g ` G ) ( I ` Y ) ) = ( I ` Y ) )
34 29 31 33 3eqtr3d 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( I ` X ) ( +g ` G ) ( X ( +g ` G ) ( I ` Y ) ) ) = ( I ` Y ) )
35 1 11 14 grprid 
 |-  ( ( G e. Grp /\ ( I ` X ) e. B ) -> ( ( I ` X ) ( +g ` G ) ( 0g ` G ) ) = ( I ` X ) )
36 8 24 35 syl2anc 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( I ` X ) ( +g ` G ) ( 0g ` G ) ) = ( I ` X ) )
37 34 36 breq12d 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( ( ( I ` X ) ( +g ` G ) ( X ( +g ` G ) ( I ` Y ) ) ) .< ( ( I ` X ) ( +g ` G ) ( 0g ` G ) ) <-> ( I ` Y ) .< ( I ` X ) ) )
38 26 37 bitrd 
 |-  ( ( ( G e. oGrp /\ ( oppG ` G ) e. oGrp ) /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( I ` Y ) .< ( I ` X ) ) )