Metamath Proof Explorer

Theorem etransclem1

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

Ref Expression
Hypotheses etransclem1.x 
|- ( ph -> X C_ CC )
etransclem1.p 
|- ( ph -> P e. NN )
etransclem1.h 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem1.j 
|- ( ph -> J e. ( 0 ... M ) )
Assertion etransclem1 
|- ( ph -> ( H ` J ) : X --> CC )

Proof

Step Hyp Ref Expression
1 etransclem1.x 
 |-  ( ph -> X C_ CC )
2 etransclem1.p 
 |-  ( ph -> P e. NN )
3 etransclem1.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
4 etransclem1.j 
 |-  ( ph -> J e. ( 0 ... M ) )
5 1 sselda 
 |-  ( ( ph /\ x e. X ) -> x e. CC )
6 4 elfzelzd 
 |-  ( ph -> J e. ZZ )
7 6 zcnd 
 |-  ( ph -> J e. CC )
8 7 adantr 
 |-  ( ( ph /\ x e. X ) -> J e. CC )
9 5 8 subcld 
 |-  ( ( ph /\ x e. X ) -> ( x - J ) e. CC )
10 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
11 2 10 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
12 2 nnnn0d 
 |-  ( ph -> P e. NN0 )
13 11 12 ifcld 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 )
14 13 adantr 
 |-  ( ( ph /\ x e. X ) -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 )
15 9 14 expcld 
 |-  ( ( ph /\ x e. X ) -> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
16 eqid 
 |-  ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) )
17 15 16 fmptd 
 |-  ( ph -> ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) : X --> CC )
18 oveq2 
 |-  ( j = n -> ( x - j ) = ( x - n ) )
19 eqeq1 
 |-  ( j = n -> ( j = 0 <-> n = 0 ) )
20 19 ifbid 
 |-  ( j = n -> if ( j = 0 , ( P - 1 ) , P ) = if ( n = 0 , ( P - 1 ) , P ) )
21 18 20 oveq12d 
 |-  ( j = n -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( x - n ) ^ if ( n = 0 , ( P - 1 ) , P ) ) )
22 21 mpteq2dv 
 |-  ( j = n -> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x - n ) ^ if ( n = 0 , ( P - 1 ) , P ) ) ) )
23 22 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( n e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - n ) ^ if ( n = 0 , ( P - 1 ) , P ) ) ) )
24 3 23 eqtri 
 |-  H = ( n e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - n ) ^ if ( n = 0 , ( P - 1 ) , P ) ) ) )
25 oveq2 
 |-  ( n = J -> ( x - n ) = ( x - J ) )
26 eqeq1 
 |-  ( n = J -> ( n = 0 <-> J = 0 ) )
27 26 ifbid 
 |-  ( n = J -> if ( n = 0 , ( P - 1 ) , P ) = if ( J = 0 , ( P - 1 ) , P ) )
28 25 27 oveq12d 
 |-  ( n = J -> ( ( x - n ) ^ if ( n = 0 , ( P - 1 ) , P ) ) = ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) )
29 28 mpteq2dv 
 |-  ( n = J -> ( x e. X |-> ( ( x - n ) ^ if ( n = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) )
30 cnex 
 |-  CC e. _V
31 30 ssex 
 |-  ( X C_ CC -> X e. _V )
32 mptexg 
 |-  ( X e. _V -> ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) e. _V )
33 1 31 32 3syl 
 |-  ( ph -> ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) e. _V )
34 24 29 4 33 fvmptd3 
 |-  ( ph -> ( H ` J ) = ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) )
35 34 feq1d 
 |-  ( ph -> ( ( H ` J ) : X --> CC <-> ( x e. X |-> ( ( x - J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) : X --> CC ) )
36 17 35 mpbird 
 |-  ( ph -> ( H ` J ) : X --> CC )