Theorem knoppcnlem1

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Hypotheses	knoppcnlem1.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppcnlem1.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	knoppcnlem1.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
Assertion	knoppcnlem1	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem1.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
2		knoppcnlem1.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		knoppcnlem1.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4		oveq2	⊢ ( 𝑦 = 𝐴 → ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) = ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) )
5	4	fveq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) = ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) )
6	5	oveq2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) = ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) )
7	6	mpteq2dv	⊢ ( 𝑦 = 𝐴 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) ) )
8		nn0ex	⊢ ℕ0 ∈ V
9	8	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) ) ∈ V
10	9	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) ) ∈ V )
11	1 7 2 10	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) ) )
12		oveq2	⊢ ( 𝑛 = 𝑀 → ( 𝐶 ↑ 𝑛 ) = ( 𝐶 ↑ 𝑀 ) )
13		oveq2	⊢ ( 𝑛 = 𝑀 → ( ( 2 · 𝑁 ) ↑ 𝑛 ) = ( ( 2 · 𝑁 ) ↑ 𝑀 ) )
14	13	fvoveq1d	⊢ ( 𝑛 = 𝑀 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) = ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) )
15	12 14	oveq12d	⊢ ( 𝑛 = 𝑀 → ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝐴 ) ) ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
17		ovexd	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ V )
18	11 16 3 17	fvmptd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )