Theorem pserval2

Description: Value of the function G that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypothesis	pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
Assertion	pserval2	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑁 ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2	1	pserval	⊢ ( 𝑋 ∈ ℂ → ( 𝐺 ‘ 𝑋 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑦 ) · ( 𝑋 ↑ 𝑦 ) ) ) )
3	2	fveq1d	⊢ ( 𝑋 ∈ ℂ → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑁 ) = ( ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑦 ) · ( 𝑋 ↑ 𝑦 ) ) ) ‘ 𝑁 ) )
4		fveq2	⊢ ( 𝑦 = 𝑁 → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑁 ) )
5		oveq2	⊢ ( 𝑦 = 𝑁 → ( 𝑋 ↑ 𝑦 ) = ( 𝑋 ↑ 𝑁 ) )
6	4 5	oveq12d	⊢ ( 𝑦 = 𝑁 → ( ( 𝐴 ‘ 𝑦 ) · ( 𝑋 ↑ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) )
7		eqid	⊢ ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑦 ) · ( 𝑋 ↑ 𝑦 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑦 ) · ( 𝑋 ↑ 𝑦 ) ) )
8		ovex	⊢ ( ( 𝐴 ‘ 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑦 ) · ( 𝑋 ↑ 𝑦 ) ) ) ‘ 𝑁 ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) )
10	3 9	sylan9eq	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑁 ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) )