Theorem mulg2

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

	Ref	Expression
Hypotheses	mulg1.b	$$⊢B={\mathrm{Base}}_G$$
	mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnnp1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	mulg2	$$⊢X\in B\to 2\underset{\dot{}}{·}X=X\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		mulg1.b	$$⊢B={\mathrm{Base}}_G$$
2		mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnnp1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		df-2	$$⊢2=1+1$$
5	4	oveq1i	$$⊢2\underset{\dot{}}{·}X=\left(1+1\right)\underset{\dot{}}{·}X$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	1 2 3	mulgnnp1	$$⊢\left(1\in \mathbb{N}\wedge X\in B\right)\to \left(1+1\right)\underset{\dot{}}{·}X=\left(1\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X$$
8	6 7	mpan	$$⊢X\in B\to \left(1+1\right)\underset{\dot{}}{·}X=\left(1\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X$$
9	5 8	syl5eq	$$⊢X\in B\to 2\underset{\dot{}}{·}X=\left(1\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X$$
10	1 2	mulg1	$$⊢X\in B\to 1\underset{\dot{}}{·}X=X$$
11	10	oveq1d	$$⊢X\in B\to \left(1\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X=X\underset{\dot{}}{+}X$$
12	9 11	eqtrd	$$⊢X\in B\to 2\underset{\dot{}}{·}X=X\underset{\dot{}}{+}X$$