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

Metamath Proof Explorer

Theorem odm1inv

Description: The (order-1)th multiple of an element is its inverse. (Contributed by SN, 31-Jan-2025)

Ref Expression
Hypotheses odm1inv.x 
|- X = ( Base ` G )
odm1inv.o 
|- O = ( od ` G )
odm1inv.t 
|- .x. = ( .g ` G )
odm1inv.i 
|- I = ( invg ` G )
odm1inv.g 
|- ( ph -> G e. Grp )
odm1inv.1 
|- ( ph -> A e. X )
Assertion odm1inv 
|- ( ph -> ( ( ( O ` A ) - 1 ) .x. A ) = ( I ` A ) )

Proof

Step Hyp Ref Expression
1 odm1inv.x 
 |-  X = ( Base ` G )
2 odm1inv.o 
 |-  O = ( od ` G )
3 odm1inv.t 
 |-  .x. = ( .g ` G )
4 odm1inv.i 
 |-  I = ( invg ` G )
5 odm1inv.g 
 |-  ( ph -> G e. Grp )
6 odm1inv.1 
 |-  ( ph -> A e. X )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 1 2 3 7 odid 
 |-  ( A e. X -> ( ( O ` A ) .x. A ) = ( 0g ` G ) )
9 6 8 syl 
 |-  ( ph -> ( ( O ` A ) .x. A ) = ( 0g ` G ) )
10 1 3 mulg1 
 |-  ( A e. X -> ( 1 .x. A ) = A )
11 6 10 syl 
 |-  ( ph -> ( 1 .x. A ) = A )
12 9 11 oveq12d 
 |-  ( ph -> ( ( ( O ` A ) .x. A ) ( -g ` G ) ( 1 .x. A ) ) = ( ( 0g ` G ) ( -g ` G ) A ) )
13 1 2 6 odcld 
 |-  ( ph -> ( O ` A ) e. NN0 )
14 13 nn0zd 
 |-  ( ph -> ( O ` A ) e. ZZ )
15 1zzd 
 |-  ( ph -> 1 e. ZZ )
16 eqid 
 |-  ( -g ` G ) = ( -g ` G )
17 1 3 16 mulgsubdir 
 |-  ( ( G e. Grp /\ ( ( O ` A ) e. ZZ /\ 1 e. ZZ /\ A e. X ) ) -> ( ( ( O ` A ) - 1 ) .x. A ) = ( ( ( O ` A ) .x. A ) ( -g ` G ) ( 1 .x. A ) ) )
18 5 14 15 6 17 syl13anc 
 |-  ( ph -> ( ( ( O ` A ) - 1 ) .x. A ) = ( ( ( O ` A ) .x. A ) ( -g ` G ) ( 1 .x. A ) ) )
19 1 16 4 7 grpinvval2 
 |-  ( ( G e. Grp /\ A e. X ) -> ( I ` A ) = ( ( 0g ` G ) ( -g ` G ) A ) )
20 5 6 19 syl2anc 
 |-  ( ph -> ( I ` A ) = ( ( 0g ` G ) ( -g ` G ) A ) )
21 12 18 20 3eqtr4d 
 |-  ( ph -> ( ( ( O ` A ) - 1 ) .x. A ) = ( I ` A ) )