mulgp1

Description: Group multiple (exponentiation) operation at a successor, extended to ZZ . (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgnndir.b	$⊢ B = {Base}_{G}$
	mulgnndir.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnndir.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulgp1	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$

Step	Hyp	Ref	Expression
1		mulgnndir.b	$⊢ B = {Base}_{G}$
2		mulgnndir.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnndir.p	$⊢ \underset{˙}{+} = +_{G}$
4		1z	$⊢ 1 \in ℤ$
5	1 2 3	mulgdir	$⊢ (G \in Grp \land (N \in ℤ \land 1 \in ℤ \land X \in B)) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} (1 \underset{˙}{\cdot} X)$
6	4 5	mp3anr2	$⊢ (G \in Grp \land (N \in ℤ \land X \in B)) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} (1 \underset{˙}{\cdot} X)$
7	6	3impb	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} (1 \underset{˙}{\cdot} X)$
8	1 2	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
9	8	3ad2ant3	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to 1 \underset{˙}{\cdot} X = X$
10	9	oveq2d	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to (N \underset{˙}{\cdot} X) \underset{˙}{+} (1 \underset{˙}{\cdot} X) = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$
11	7 10	eqtrd	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$

Metamath Proof Explorer