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