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	syl5eq	⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ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 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) )