Theorem mulgp1

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

	Ref	Expression
Hypotheses	mulgnndir.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgnndir.t	⊢ · = ( .g ‘ 𝐺 )
	mulgnndir.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	mulgp1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mulgnndir.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgnndir.t	⊢ · = ( .g ‘ 𝐺 )
3		mulgnndir.p	⊢ + = ( +g ‘ 𝐺 )
4		1z	⊢ 1 ∈ ℤ
5	1 2 3	mulgdir	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + ( 1 · 𝑋 ) ) )
6	4 5	mp3anr2	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + ( 1 · 𝑋 ) ) )
7	6	3impb	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + ( 1 · 𝑋 ) ) )
8	1 2	mulg1	⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )
9	8	3ad2ant3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )
10	9	oveq2d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 · 𝑋 ) + ( 1 · 𝑋 ) ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )
11	7 10	eqtrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )