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 ) ) )