mulg2

Description: Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	mulg1.b	$⊢ B = {Base}_{G}$
	mulg1.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnnp1.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulg2	$⊢ X \in B \to 2 \underset{˙}{\cdot} X = X \underset{˙}{+} X$

Step	Hyp	Ref	Expression
1		mulg1.b	$⊢ B = {Base}_{G}$
2		mulg1.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnnp1.p	$⊢ \underset{˙}{+} = +_{G}$
4		df-2	$⊢ 2 = 1 + 1$
5	4	oveq1i	$⊢ 2 \underset{˙}{\cdot} X = (1 + 1) \underset{˙}{\cdot} X$
6		1nn	$⊢ 1 \in ℕ$
7	1 2 3	mulgnnp1	$⊢ (1 \in ℕ \land X \in B) \to (1 + 1) \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) \underset{˙}{+} X$
8	6 7	mpan	$⊢ X \in B \to (1 + 1) \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) \underset{˙}{+} X$
9	5 8	eqtrid	$⊢ X \in B \to 2 \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) \underset{˙}{+} X$
10	1 2	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
11	10	oveq1d	$⊢ X \in B \to (1 \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} X$
12	9 11	eqtrd	$⊢ X \in B \to 2 \underset{˙}{\cdot} X = X \underset{˙}{+} X$

Metamath Proof Explorer