Theorem etransclem1

Description: H is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem1.x	$$⊢\phi \to X\subseteq ℂ$$
	etransclem1.p	$$⊢\phi \to P\in \mathbb{N}$$
	etransclem1.h	$$⊢H=\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)$$
	etransclem1.j	$$⊢\phi \to J\in \left(0\dots M\right)$$
Assertion	etransclem1	$$⊢\phi \to H\left(J\right):X⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		etransclem1.x	$$⊢\phi \to X\subseteq ℂ$$
2		etransclem1.p	$$⊢\phi \to P\in \mathbb{N}$$
3		etransclem1.h	$$⊢H=\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)$$
4		etransclem1.j	$$⊢\phi \to J\in \left(0\dots M\right)$$
5	1	sselda	$$⊢\left(\phi \wedge x\in X\right)\to x\in ℂ$$
6	4	elfzelzd	$$⊢\phi \to J\in \mathbb{Z}$$
7	6	zcnd	$$⊢\phi \to J\in ℂ$$
8	7	adantr	$$⊢\left(\phi \wedge x\in X\right)\to J\in ℂ$$
9	5 8	subcld	$$⊢\left(\phi \wedge x\in X\right)\to x-J\in ℂ$$
10		nnm1nn0	$$⊢P\in \mathbb{N}\to P-1\in {\mathbb{N}}_0$$
11	2 10	syl	$$⊢\phi \to P-1\in {\mathbb{N}}_0$$
12	2	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
13	11 12	ifcld	$$⊢\phi \to if\left(J=0,P-1,P\right)\in {\mathbb{N}}_0$$
14	13	adantr	$$⊢\left(\phi \wedge x\in X\right)\to if\left(J=0,P-1,P\right)\in {\mathbb{N}}_0$$
15	9 14	expcld	$$⊢\left(\phi \wedge x\in X\right)\to {\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\in ℂ$$
16		eqid	$$⊢\left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right)$$
17	15 16	fmptd	$$⊢\phi \to \left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right):X⟶ℂ$$
18		oveq2	$$⊢j=n\to x-j=x-n$$
19		eqeq1	$$⊢j=n\to \left(j=0\leftrightarrow n=0\right)$$
20	19	ifbid	$$⊢j=n\to if\left(j=0,P-1,P\right)=if\left(n=0,P-1,P\right)$$
21	18 20	oveq12d	$$⊢j=n\to {\left(x-j\right)}^{if\left(j=0,P-1,P\right)}={\left(x-n\right)}^{if\left(n=0,P-1,P\right)}$$
22	21	mpteq2dv	$$⊢j=n\to \left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x-n\right)}^{if\left(n=0,P-1,P\right)}\right)$$
23	22	cbvmptv	$$⊢\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)=\left(n\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-n\right)}^{if\left(n=0,P-1,P\right)}\right)\right)$$
24	3 23	eqtri	$$⊢H=\left(n\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-n\right)}^{if\left(n=0,P-1,P\right)}\right)\right)$$
25		oveq2	$$⊢n=J\to x-n=x-J$$
26		eqeq1	$$⊢n=J\to \left(n=0\leftrightarrow J=0\right)$$
27	26	ifbid	$$⊢n=J\to if\left(n=0,P-1,P\right)=if\left(J=0,P-1,P\right)$$
28	25 27	oveq12d	$$⊢n=J\to {\left(x-n\right)}^{if\left(n=0,P-1,P\right)}={\left(x-J\right)}^{if\left(J=0,P-1,P\right)}$$
29	28	mpteq2dv	$$⊢n=J\to \left(x\in X⟼{\left(x-n\right)}^{if\left(n=0,P-1,P\right)}\right)=\left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right)$$
30		cnex	$$⊢ℂ\in \mathrm{V}$$
31	30	ssex	$$⊢X\subseteq ℂ\to X\in \mathrm{V}$$
32		mptexg	$$⊢X\in \mathrm{V}\to \left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right)\in \mathrm{V}$$
33	1 31 32	3syl	$$⊢\phi \to \left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right)\in \mathrm{V}$$
34	24 29 4 33	fvmptd3	$$⊢\phi \to H\left(J\right)=\left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right)$$
35	34	feq1d	$$⊢\phi \to \left(H\left(J\right):X⟶ℂ\leftrightarrow \left(x\in X⟼{\left(x-J\right)}^{if\left(J=0,P-1,P\right)}\right):X⟶ℂ\right)$$
36	17 35	mpbird	$$⊢\phi \to H\left(J\right):X⟶ℂ$$