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

Metamath Proof Explorer

Theorem mulgnegneg

Description: The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

		Ref	Expression
	Hypotheses	mulgnncl.b	$⊢ B = {Base}_{G}$
		mulgnncl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		mulgneg.i	$⊢ I = {inv}_{g} (G)$
	Assertion	mulgnegneg	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (-N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} 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	1 2 3	mulgneg	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = I (N \underset{˙}{\cdot} X)$
5	4	fveq2d	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (-N \underset{˙}{\cdot} X) = I (I (N \underset{˙}{\cdot} X))$
6		simp1	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to G \in Grp$
7	1 2	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
8	1 3	grpinvinv	$⊢ (G \in Grp \land N \underset{˙}{\cdot} X \in B) \to I (I (N \underset{˙}{\cdot} X)) = N \underset{˙}{\cdot} X$
9	6 7 8	syl2anc	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (I (N \underset{˙}{\cdot} X)) = N \underset{˙}{\cdot} X$
10	5 9	eqtrd	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (-N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$