Theorem knoppcnlem1

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

	Ref	Expression
Hypotheses	knoppcnlem1.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
	knoppcnlem1.2	$$⊢\phi \to A\in ℝ$$
	knoppcnlem1.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
Assertion	knoppcnlem1	$$⊢\phi \to F\left(A\right)\left(M\right)=C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem1.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
2		knoppcnlem1.2	$$⊢\phi \to A\in ℝ$$
3		knoppcnlem1.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
4		oveq2	$$⊢y=A\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A$$
5	4	fveq2d	$$⊢y=A\to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)=T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)$$
6	5	oveq2d	$$⊢y=A\to C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)=C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)$$
7	6	mpteq2dv	$$⊢y=A\to \left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)=\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)\right)$$
8		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
9	8	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)\right)\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)\right)\in \mathrm{V}$$
11	1 7 2 10	fvmptd3	$$⊢\phi \to F\left(A\right)=\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)\right)$$
12		oveq2	$$⊢n=M\to C^n=C^M$$
13		oveq2	$$⊢n=M\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^n={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^M$$
14	13	fvoveq1d	$$⊢n=M\to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)=T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$
15	12 14	oveq12d	$$⊢n=M\to C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)=C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$
16	15	adantl	$$⊢\left(\phi \wedge n=M\right)\to C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}A\right)=C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$
17		ovexd	$$⊢\phi \to C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in \mathrm{V}$$
18	11 16 3 17	fvmptd	$$⊢\phi \to F\left(A\right)\left(M\right)=C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$