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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odm1inv.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	odm1inv.t	⊢ · = ( .g ‘ 𝐺 )
	odm1inv.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
	odm1inv.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	odm1inv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion	odm1inv	⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( 𝐼 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		odm1inv.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odm1inv.o	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odm1inv.t	⊢ · = ( .g ‘ 𝐺 )
4		odm1inv.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
5		odm1inv.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6		odm1inv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
7		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8	1 2 3 7	odid	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) )
9	6 8	syl	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) )
10	1 3	mulg1	⊢ ( 𝐴 ∈ 𝑋 → ( 1 · 𝐴 ) = 𝐴 )
11	6 10	syl	⊢ ( 𝜑 → ( 1 · 𝐴 ) = 𝐴 )
12	9 11	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ( -g ‘ 𝐺 ) ( 1 · 𝐴 ) ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
13	1 2 6	odcld	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
14	13	nn0zd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
15		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
16		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
17	1 3 16	mulgsubdir	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ( -g ‘ 𝐺 ) ( 1 · 𝐴 ) ) )
18	5 14 15 6 17	syl13anc	⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ( -g ‘ 𝐺 ) ( 1 · 𝐴 ) ) )
19	1 16 4 7	grpinvval2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
20	5 6 19	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
21	12 18 20	3eqtr4d	⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( 𝐼 ‘ 𝐴 ) )