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.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.r 
 |-  ( ph -> R e. CRing )
6 psdvsca.x 
 |-  ( ph -> X e. I )
7 psdvsca.f 
 |-  ( ph -> F e. B )
8 psdvsca.c 
 |-  ( ph -> C e. K )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11 5 crngringd 
 |-  ( ph -> R e. Ring )
12 ringmgm 
 |-  ( R e. Ring -> R e. Mgm )
13 11 12 syl 
 |-  ( ph -> R e. Mgm )
14 1 3 4 2 11 8 7 psrvscacl 
 |-  ( ph -> ( C .x. F ) e. B )
15 1 2 13 6 14 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) e. B )
16 1 9 10 2 15 psrelbas 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
17 16 ffnd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
18 1 2 13 6 7 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
19 1 3 4 2 11 8 18 psrvscacl 
 |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) e. B )
20 1 9 10 2 19 psrelbas 
 |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
21 20 ffnd 
 |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
22 11 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring )
23 10 psrbagf 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 )
24 23 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 )
25 6 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
26 24 25 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d ` X ) e. NN0 )
27 peano2nn0 
 |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. NN0 )
28 27 nn0zd 
 |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. ZZ )
29 26 28 syl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d ` X ) + 1 ) e. ZZ )
30 8 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> C e. K )
31 1 4 10 2 7 psrelbas 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
32 31 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
33 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
34 reldmpsr 
 |-  Rel dom mPwSer
35 1 2 34 strov2rcl 
 |-  ( F e. B -> I e. _V )
36 7 35 syl 
 |-  ( ph -> I e. _V )
37 10 psrbagsn 
 |-  ( I e. _V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
38 36 37 syl 
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
39 38 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 } )
40 10 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 } )
41 33 39 40 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 } )
42 32 41 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 )
43 eqid 
 |-  ( .g ` R ) = ( .g ` R )
44 eqid 
 |-  ( .r ` R ) = ( .r ` R )
45 4 43 44 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 ) ) ) ) ) ) )
46 22 29 30 42 45 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 ) ) ) ) ) ) )
47 7 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F e. B )
48 1 2 10 25 47 33 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 44 10 30 47 41 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 46 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 14 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C .x. F ) e. B )
54 1 2 10 25 53 33 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 18 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 44 10 30 55 33 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 17 21 57 eqfnfvd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) = ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) )