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={\mathrm{Base}}_G$$
	odm1inv.o	$$⊢O=\mathrm{od}\left(G\right)$$
	odm1inv.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odm1inv.i	$$⊢I={inv}_g\left(G\right)$$
	odm1inv.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	odm1inv.1	$$⊢\phi \to A\in X$$
Assertion	odm1inv	$$⊢\phi \to \left(O\left(A\right)-1\right)\underset{\dot{}}{·}A=I\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		odm1inv.x	$$⊢X={\mathrm{Base}}_G$$
2		odm1inv.o	$$⊢O=\mathrm{od}\left(G\right)$$
3		odm1inv.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		odm1inv.i	$$⊢I={inv}_g\left(G\right)$$
5		odm1inv.g	$$⊢\phi \to G\in \mathrm{Grp}$$
6		odm1inv.1	$$⊢\phi \to A\in X$$
7		eqid	$$⊢0_G=0_G$$
8	1 2 3 7	odid	$$⊢A\in X\to O\left(A\right)\underset{\dot{}}{·}A=0_G$$
9	6 8	syl	$$⊢\phi \to O\left(A\right)\underset{\dot{}}{·}A=0_G$$
10	1 3	mulg1	$$⊢A\in X\to 1\underset{\dot{}}{·}A=A$$
11	6 10	syl	$$⊢\phi \to 1\underset{\dot{}}{·}A=A$$
12	9 11	oveq12d	$$⊢\phi \to \left(O\left(A\right)\underset{\dot{}}{·}A\right){-}_G\left(1\underset{\dot{}}{·}A\right)=0_G{-}_{G}A$$
13	1 2 6	odcld	$$⊢\phi \to O\left(A\right)\in {\mathbb{N}}_0$$
14	13	nn0zd	$$⊢\phi \to O\left(A\right)\in \mathbb{Z}$$
15		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
16		eqid	$$⊢{-}_G={-}_G$$
17	1 3 16	mulgsubdir	$$⊢\left(G\in \mathrm{Grp}\wedge \left(O\left(A\right)\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge A\in X\right)\right)\to \left(O\left(A\right)-1\right)\underset{\dot{}}{·}A=\left(O\left(A\right)\underset{\dot{}}{·}A\right){-}_G\left(1\underset{\dot{}}{·}A\right)$$
18	5 14 15 6 17	syl13anc	$$⊢\phi \to \left(O\left(A\right)-1\right)\underset{\dot{}}{·}A=\left(O\left(A\right)\underset{\dot{}}{·}A\right){-}_G\left(1\underset{\dot{}}{·}A\right)$$
19	1 16 4 7	grpinvval2	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to I\left(A\right)=0_G{-}_{G}A$$
20	5 6 19	syl2anc	$$⊢\phi \to I\left(A\right)=0_G{-}_{G}A$$
21	12 18 20	3eqtr4d	$$⊢\phi \to \left(O\left(A\right)-1\right)\underset{\dot{}}{·}A=I\left(A\right)$$