Metamath Proof Explorer

Theorem psdvsca

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

Ref Expression
Hypotheses psdvsca.s 
|- S = ( I mPwSer R )
psdvsca.b 
|- B = ( Base ` S )
psdvsca.m 
|- .x. = ( .s ` S )
psdvsca.k 
|- K = ( Base ` R )
psdvsca.i 
|- ( ph -> I e. V )
psdvsca.r 
|- ( ph -> R e. CRing )
psdvsca.x 
|- ( ph -> X e. I )
psdvsca.f 
|- ( ph -> F e. B )
psdvsca.c 
|- ( ph -> C e. K )
Assertion psdvsca 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) = ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) )

Proof

Step Hyp Ref Expression
1 psdvsca.s 
 |-  S = ( I mPwSer R )
2 psdvsca.b 
 |-  B = ( Base ` S )
3 psdvsca.m 
 |-  .x. = ( .s ` S )
4 psdvsca.k 
 |-  K = ( Base ` R )
5 psdvsca.i 
 |-  ( ph -> I e. V )
6 psdvsca.r 
 |-  ( ph -> R e. CRing )
7 psdvsca.x 
 |-  ( ph -> X e. I )
8 psdvsca.f 
 |-  ( ph -> F e. B )
9 psdvsca.c 
 |-  ( ph -> C e. K )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
12 6 crngringd 
 |-  ( ph -> R e. Ring )
13 ringmgm 
 |-  ( R e. Ring -> R e. Mgm )
14 12 13 syl 
 |-  ( ph -> R e. Mgm )
15 1 3 4 2 12 9 8 psrvscacl 
 |-  ( ph -> ( C .x. F ) e. B )
16 1 2 5 14 7 15 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) e. B )
17 1 10 11 2 16 psrelbas 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
18 17 ffnd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
19 1 2 5 14 7 8 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
20 1 3 4 2 12 9 19 psrvscacl 
 |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) e. B )
21 1 10 11 2 20 psrelbas 
 |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
22 21 ffnd 
 |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
23 12 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring )
24 11 psrbagf 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 )
25 24 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 )
26 7 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
27 25 26 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d ` X ) e. NN0 )
28 peano2nn0 
 |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. NN0 )
29 28 nn0zd 
 |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. ZZ )
30 27 29 syl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d ` X ) + 1 ) e. ZZ )
31 9 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> C e. K )
32 1 4 11 2 8 psrelbas 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
33 32 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
34 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
35 11 psrbagsn 
 |-  ( I e. V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
36 5 35 syl 
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
37 36 adantr 
 |-  ( ( ph /\ d 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 } )
38 11 psrbagaddcl 
 |-  ( ( d 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 } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
39 34 37 38 syl2anc 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
40 33 39 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. K )
41 eqid 
 |-  ( .g ` R ) = ( .g ` R )
42 eqid 
 |-  ( .r ` R ) = ( .r ` R )
43 4 41 42 mulgass3 
 |-  ( ( R e. Ring /\ ( ( ( d ` X ) + 1 ) e. ZZ /\ C e. K /\ ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. K ) ) -> ( C ( .r ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
44 23 30 31 40 43 syl13anc 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C ( .r ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
45 5 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. V )
46 6 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. CRing )
47 8 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F e. B )
48 1 2 11 45 46 26 47 34 psdcoef 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
49 48 oveq2d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C ( .r ` R ) ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) ) = ( C ( .r ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
50 1 3 4 2 42 11 31 47 39 psrvscaval 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
51 50 oveq2d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
52 44 49 51 3eqtr4rd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( C ( .r ` R ) ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) ) )
53 15 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C .x. F ) e. B )
54 1 2 11 45 46 26 53 34 psdcoef 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) ` d ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
55 19 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
56 1 3 4 2 42 11 31 55 34 psrvscaval 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) ` d ) = ( C ( .r ` R ) ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) ) )
57 52 54 56 3eqtr4d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) ` d ) = ( ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) ` d ) )
58 18 22 57 eqfnfvd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) = ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) )