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.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.r
 |-  ( ph -> R e. Mgm )
4 psdcl.x
 |-  ( ph -> X e. I )
5 psdcl.f
 |-  ( ph -> F e. B )
6 fvexd
 |-  ( ph -> ( Base ` R ) e. _V )
7 ovex
 |-  ( NN0 ^m I ) e. _V
8 7 rabex
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
9 8 a1i
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
10 3 adantr
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Mgm )
11 eqid
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
12 11 psrbagf
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> k : I --> NN0 )
13 12 adantl
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k : I --> NN0 )
14 4 adantr
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
15 13 14 ffvelcdmd
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k ` X ) e. NN0 )
16 nn0p1nn
 |-  ( ( k ` X ) e. NN0 -> ( ( k ` X ) + 1 ) e. NN )
17 15 16 syl
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k ` X ) + 1 ) e. NN )
18 eqid
 |-  ( Base ` R ) = ( Base ` R )
19 1 18 11 2 5 psrelbas
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
20 19 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 ) )
21 simpr
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
22 reldmpsr
 |-  Rel dom mPwSer
23 1 2 22 strov2rcl
 |-  ( F e. B -> I e. _V )
24 5 23 syl
 |-  ( ph -> I e. _V )
25 1nn0
 |-  1 e. NN0
26 11 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 } )
27 24 25 26 sylancl
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
28 27 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 } )
29 11 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 } )
30 21 28 29 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 } )
31 20 30 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 ) )
32 eqid
 |-  ( .g ` R ) = ( .g ` R )
33 18 32 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 ) )
34 10 17 31 33 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 ) )
35 34 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 ) )
36 6 9 35 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 } ) )
37 1 2 11 4 5 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 ) ) ) ) ) ) )
38 1 18 11 2 24 psrbas
 |-  ( ph -> B = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
39 36 37 38 3eltr4d
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )