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

Metamath Proof Explorer

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 = {Base}_{G}$
		mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		mulgneg.i	$⊢ I = {inv}_{g} (G)$
	Assertion	mulgm1	$⊢ (G \in Grp \land X \in B) \to -1 \underset{˙}{\cdot} X = I (X)$

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	$⊢ B = {Base}_{G}$
2		mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgneg.i	$⊢ I = {inv}_{g} (G)$
4		1z	$⊢ 1 \in ℤ$
5	1 2 3	mulgneg	$⊢ (G \in Grp \land 1 \in ℤ \land X \in B) \to -1 \underset{˙}{\cdot} X = I (1 \underset{˙}{\cdot} X)$
6	4 5	mp3an2	$⊢ (G \in Grp \land X \in B) \to -1 \underset{˙}{\cdot} X = I (1 \underset{˙}{\cdot} X)$
7	1 2	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
8	7	adantl	$⊢ (G \in Grp \land X \in B) \to 1 \underset{˙}{\cdot} X = X$
9	8	fveq2d	$⊢ (G \in Grp \land X \in B) \to I (1 \underset{˙}{\cdot} X) = I (X)$
10	6 9	eqtrd	$⊢ (G \in Grp \land X \in B) \to -1 \underset{˙}{\cdot} X = I (X)$