This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )