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

Metamath Proof Explorer

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 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑁 ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) )