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 ) )