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

Metamath Proof Explorer

Theorem pserval

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 pserval ( 𝑋 ∈ ℂ → ( 𝐺 ‘ 𝑋 ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )

Proof

Step Hyp Ref Expression
1 pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑚 ) )
3 2 oveq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) )
4 3 mpteq2dv ⊢ ( 𝑦 = 𝑋 → ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )
5 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑚 ) )
6 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑚 ) )
7 5 6 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) )
8 7 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) )
9 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝑚 ) = ( 𝑦 ↑ 𝑚 ) )
10 9 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) )
11 10 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) ) )
12 8 11 eqtrid ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) ) )
13 12 cbvmptv ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) ) )
14 1 13 eqtri ⊢ 𝐺 = ( 𝑦 ∈ ℂ ↦ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑦 ↑ 𝑚 ) ) ) )
15 nn0ex ⊢ ℕ0 ∈ V
16 15 mptex ⊢ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ∈ V
17 4 14 16 fvmpt ⊢ ( 𝑋 ∈ ℂ → ( 𝐺 ‘ 𝑋 ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )