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