Theorem mulg2

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

	Ref	Expression
Hypotheses	mulg1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulg1.m	⊢ · = ( .g ‘ 𝐺 )
	mulgnnp1.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	mulg2	⊢ ( 𝑋 ∈ 𝐵 → ( 2 · 𝑋 ) = ( 𝑋 + 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mulg1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulg1.m	⊢ · = ( .g ‘ 𝐺 )
3		mulgnnp1.p	⊢ + = ( +g ‘ 𝐺 )
4		df-2	⊢ 2 = ( 1 + 1 )
5	4	oveq1i	⊢ ( 2 · 𝑋 ) = ( ( 1 + 1 ) · 𝑋 )
6		1nn	⊢ 1 ∈ ℕ
7	1 2 3	mulgnnp1	⊢ ( ( 1 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + 𝑋 ) )
8	6 7	mpan	⊢ ( 𝑋 ∈ 𝐵 → ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + 𝑋 ) )
9	5 8	eqtrid	⊢ ( 𝑋 ∈ 𝐵 → ( 2 · 𝑋 ) = ( ( 1 · 𝑋 ) + 𝑋 ) )
10	1 2	mulg1	⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )
11	10	oveq1d	⊢ ( 𝑋 ∈ 𝐵 → ( ( 1 · 𝑋 ) + 𝑋 ) = ( 𝑋 + 𝑋 ) )
12	9 11	eqtrd	⊢ ( 𝑋 ∈ 𝐵 → ( 2 · 𝑋 ) = ( 𝑋 + 𝑋 ) )