# 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 ) , 𝑃 ) ) )