etransclem13

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

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

Proof

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

Metamath Proof Explorer

Theorem etransclem13

Proof