Metamath Proof Explorer

Theorem etransclem13

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

Ref Expression
Hypotheses etransclem13.x ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
etransclem13.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem13.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem13.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem13.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
Assertion etransclem13 ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 etransclem13.x ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
2 etransclem13.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
3 etransclem13.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 etransclem13.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
5 etransclem13.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
6 eqid ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
7 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) ‘ 𝑥 ) )
8 1 2 3 4 6 7 etransclem4 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) ‘ 𝑥 ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
10 cnex ⊢ ℂ ∈ V
11 10 ssex ⊢ ( 𝑋 ⊆ ℂ → 𝑋 ∈ V )
12 mptexg ⊢ ( 𝑋 ∈ V → ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
13 1 11 12 3syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
15 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 − 𝑗 ) = ( 𝑦 − 𝑗 ) )
16 15 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
17 16 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
18 17 mpteq2i ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
19 18 fvmpt2 ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V ) → ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
20 9 14 19 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
21 20 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑌 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
22 simpr ⊢ ( ( 𝑥 = 𝑌 ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
23 simpl ⊢ ( ( 𝑥 = 𝑌 ∧ 𝑦 = 𝑥 ) → 𝑥 = 𝑌 )
24 22 23 eqtrd ⊢ ( ( 𝑥 = 𝑌 ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑌 )
25 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 − 𝑗 ) = ( 𝑌 − 𝑗 ) )
26 25 oveq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
27 24 26 syl ⊢ ( ( 𝑥 = 𝑌 ∧ 𝑦 = 𝑥 ) → ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
28 27 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑌 ) ∧ 𝑦 = 𝑥 ) → ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
29 28 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑌 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑦 = 𝑥 ) → ( ( 𝑦 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑥 = 𝑌 )
31 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑌 ∈ 𝑋 )
32 30 31 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑥 ∈ 𝑋 )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑌 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ 𝑋 )
34 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑌 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ V )
35 21 29 33 34 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑌 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) ‘ 𝑥 ) = ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
36 35 prodeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) ‘ 𝑗 ) ‘ 𝑥 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
37 prodex ⊢ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ V
38 37 a1i ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ V )
39 8 36 5 38 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑌 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )