Theorem mulgm1

Description: Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by Mario Carneiro, 20-Dec-2014)

	Ref	Expression
Hypotheses	mulgnncl.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnncl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgneg.i	$$⊢I={inv}_g\left(G\right)$$
Assertion	mulgm1	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to -1\underset{\dot{}}{·}X=I\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnncl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgneg.i	$$⊢I={inv}_g\left(G\right)$$
4		1z	$$⊢1\in \mathbb{Z}$$
5	1 2 3	mulgneg	$$⊢\left(G\in \mathrm{Grp}\wedge 1\in \mathbb{Z}\wedge X\in B\right)\to -1\underset{\dot{}}{·}X=I\left(1\underset{\dot{}}{·}X\right)$$
6	4 5	mp3an2	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to -1\underset{\dot{}}{·}X=I\left(1\underset{\dot{}}{·}X\right)$$
7	1 2	mulg1	$$⊢X\in B\to 1\underset{\dot{}}{·}X=X$$
8	7	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to 1\underset{\dot{}}{·}X=X$$
9	8	fveq2d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to I\left(1\underset{\dot{}}{·}X\right)=I\left(X\right)$$
10	6 9	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to -1\underset{\dot{}}{·}X=I\left(X\right)$$