# Metamath Proof Explorer

## Theorem etransclem13

Description: F applied to Y . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem13.x ${⊢}{\phi }\to {X}\subseteq ℂ$
etransclem13.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem13.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem13.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
etransclem13.y ${⊢}{\phi }\to {Y}\in {X}$
Assertion etransclem13 ${⊢}{\phi }\to {F}\left({Y}\right)=\prod _{{j}=0}^{{M}}{\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$

### Proof

Step Hyp Ref Expression
1 etransclem13.x ${⊢}{\phi }\to {X}\subseteq ℂ$
2 etransclem13.p ${⊢}{\phi }\to {P}\in ℕ$
3 etransclem13.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
4 etransclem13.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
5 etransclem13.y ${⊢}{\phi }\to {Y}\in {X}$
6 eqid ${⊢}\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({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)$
7 eqid ${⊢}\left({x}\in {X}⟼\prod _{{j}=0}^{{M}}\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({j}\right)\left({x}\right)\right)=\left({x}\in {X}⟼\prod _{{j}=0}^{{M}}\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({j}\right)\left({x}\right)\right)$
8 1 2 3 4 6 7 etransclem4 ${⊢}{\phi }\to {F}=\left({x}\in {X}⟼\prod _{{j}=0}^{{M}}\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({j}\right)\left({x}\right)\right)$
9 simpr ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
10 cnex ${⊢}ℂ\in \mathrm{V}$
11 10 ssex ${⊢}{X}\subseteq ℂ\to {X}\in \mathrm{V}$
12 mptexg ${⊢}{X}\in \mathrm{V}\to \left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
13 1 11 12 3syl ${⊢}{\phi }\to \left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
14 13 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
15 oveq1 ${⊢}{x}={y}\to {x}-{j}={y}-{j}$
16 15 oveq1d ${⊢}{x}={y}\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
17 16 cbvmptv ${⊢}\left({x}\in {X}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)=\left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
18 17 mpteq2i ${⊢}\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({j}\in \left(0\dots {M}\right)⟼\left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
19 18 fvmpt2 ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge \left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}\right)\to \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({j}\right)=\left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
20 9 14 19 syl2anc ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to \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({j}\right)=\left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
21 20 adantlr ${⊢}\left(\left({\phi }\wedge {x}={Y}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \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({j}\right)=\left({y}\in {X}⟼{\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
22 simpr ${⊢}\left({x}={Y}\wedge {y}={x}\right)\to {y}={x}$
23 simpl ${⊢}\left({x}={Y}\wedge {y}={x}\right)\to {x}={Y}$
24 22 23 eqtrd ${⊢}\left({x}={Y}\wedge {y}={x}\right)\to {y}={Y}$
25 oveq1 ${⊢}{y}={Y}\to {y}-{j}={Y}-{j}$
26 25 oveq1d ${⊢}{y}={Y}\to {\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
27 24 26 syl ${⊢}\left({x}={Y}\wedge {y}={x}\right)\to {\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
28 27 adantll ${⊢}\left(\left({\phi }\wedge {x}={Y}\right)\wedge {y}={x}\right)\to {\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
29 28 adantlr ${⊢}\left(\left(\left({\phi }\wedge {x}={Y}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {y}={x}\right)\to {\left({y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
30 simpr ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {x}={Y}$
31 5 adantr ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {Y}\in {X}$
32 30 31 eqeltrd ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {x}\in {X}$
33 32 adantr ${⊢}\left(\left({\phi }\wedge {x}={Y}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {x}\in {X}$
34 ovexd ${⊢}\left(\left({\phi }\wedge {x}={Y}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\in \mathrm{V}$
35 21 29 33 34 fvmptd ${⊢}\left(\left({\phi }\wedge {x}={Y}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \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({j}\right)\left({x}\right)={\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
36 35 prodeq2dv ${⊢}\left({\phi }\wedge {x}={Y}\right)\to \prod _{{j}=0}^{{M}}\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({j}\right)\left({x}\right)=\prod _{{j}=0}^{{M}}{\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
37 prodex ${⊢}\prod _{{j}=0}^{{M}}{\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\in \mathrm{V}$
38 37 a1i ${⊢}{\phi }\to \prod _{{j}=0}^{{M}}{\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\in \mathrm{V}$
39 8 36 5 38 fvmptd ${⊢}{\phi }\to {F}\left({Y}\right)=\prod _{{j}=0}^{{M}}{\left({Y}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$