Metamath Proof Explorer

Theorem psdcl

Description: The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025)

Ref Expression
Hypotheses psdcl.s 
|- S = ( I mPwSer R )
psdcl.b 
|- B = ( Base ` S )
psdcl.i 
|- ( ph -> I e. V )
psdcl.r 
|- ( ph -> R e. Mgm )
psdcl.x 
|- ( ph -> X e. I )
psdcl.f 
|- ( ph -> F e. B )
Assertion psdcl 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )

Proof

Step Hyp Ref Expression
1 psdcl.s 
 |-  S = ( I mPwSer R )
2 psdcl.b 
 |-  B = ( Base ` S )
3 psdcl.i 
 |-  ( ph -> I e. V )
4 psdcl.r 
 |-  ( ph -> R e. Mgm )
5 psdcl.x 
 |-  ( ph -> X e. I )
6 psdcl.f 
 |-  ( ph -> F e. B )
7 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
8 ovex 
 |-  ( NN0 ^m I ) e. _V
9 8 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
10 9 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
11 4 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Mgm )
12 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
13 12 psrbagf 
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> k : I --> NN0 )
14 13 adantl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k : I --> NN0 )
15 5 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
16 14 15 ffvelcdmd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k ` X ) e. NN0 )
17 nn0p1nn 
 |-  ( ( k ` X ) e. NN0 -> ( ( k ` X ) + 1 ) e. NN )
18 16 17 syl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k ` X ) + 1 ) e. NN )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 1 19 12 2 6 psrelbas 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
21 20 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
22 simpr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
23 1nn0 
 |-  1 e. NN0
24 12 snifpsrbag 
 |-  ( ( I e. V /\ 1 e. NN0 ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
25 3 23 24 sylancl 
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
26 25 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
27 12 psrbagaddcl 
 |-  ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
28 22 26 27 syl2anc 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
29 21 28 ffvelcdmd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. ( Base ` R ) )
30 eqid 
 |-  ( .g ` R ) = ( .g ` R )
31 19 30 mulgnncl 
 |-  ( ( R e. Mgm /\ ( ( k ` X ) + 1 ) e. NN /\ ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. ( Base ` R ) ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. ( Base ` R ) )
32 11 18 29 31 syl3anc 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. ( Base ` R ) )
33 32 fmpttd 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
34 7 10 33 elmapdd 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
35 1 2 12 3 4 5 6 psdval 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
36 1 19 12 2 3 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
37 34 35 36 3eltr4d 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )