Metamath Proof Explorer

Theorem mulgnnp1

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

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

Proof

Step Hyp Ref Expression
1 mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulg1.m ⊢ · = ( .g ‘ 𝐺 )
3 mulgnnp1.p ⊢ + = ( +g ‘ 𝐺 )
4 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ℕ )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 4 5 eleqtrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
7 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) + ( ( ℕ × { 𝑋 } ) ‘ ( 𝑁 + 1 ) ) ) )
8 6 7 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) + ( ( ℕ × { 𝑋 } ) ‘ ( 𝑁 + 1 ) ) ) )
9 id ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐵 )
10 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
11 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑁 + 1 ) ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ ( 𝑁 + 1 ) ) = 𝑋 )
12 9 10 11 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( ℕ × { 𝑋 } ) ‘ ( 𝑁 + 1 ) ) = 𝑋 )
13 12 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) + ( ( ℕ × { 𝑋 } ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) + 𝑋 ) )
14 8 13 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) + 𝑋 ) )
15 eqid ⊢ seq 1 ( + , ( ℕ × { 𝑋 } ) ) = seq 1 ( + , ( ℕ × { 𝑋 } ) )
16 1 3 2 15 mulgnn ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 1 ) ) )
17 10 16 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 1 ) ) )
18 1 3 2 15 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
19 18 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) + 𝑋 ) )
20 14 17 19 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )