Metamath Proof Explorer

Theorem psdmplcl

Description: The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025)

Ref Expression
Hypotheses psdmplcl.p 
|- P = ( I mPoly R )
psdmplcl.b 
|- B = ( Base ` P )
psdmplcl.i 
|- ( ph -> I e. V )
psdmplcl.r 
|- ( ph -> R e. Mnd )
psdmplcl.x 
|- ( ph -> X e. I )
psdmplcl.f 
|- ( ph -> F e. B )
Assertion psdmplcl 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )

Proof

Step Hyp Ref Expression
1 psdmplcl.p 
 |-  P = ( I mPoly R )
2 psdmplcl.b 
 |-  B = ( Base ` P )
3 psdmplcl.i 
 |-  ( ph -> I e. V )
4 psdmplcl.r 
 |-  ( ph -> R e. Mnd )
5 psdmplcl.x 
 |-  ( ph -> X e. I )
6 psdmplcl.f 
 |-  ( ph -> F e. B )
7 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
8 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
9 mndmgm 
 |-  ( R e. Mnd -> R e. Mgm )
10 4 9 syl 
 |-  ( ph -> R e. Mgm )
11 1 7 2 8 mplbasss 
 |-  B C_ ( Base ` ( I mPwSer R ) )
12 11 6 sselid 
 |-  ( ph -> F e. ( Base ` ( I mPwSer R ) ) )
13 7 8 3 10 5 12 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. ( Base ` ( I mPwSer R ) ) )
14 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
15 7 8 14 3 10 5 12 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 ) ) ) ) ) ) )
16 ovex 
 |-  ( NN0 ^m I ) e. _V
17 16 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
18 17 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
19 18 mptexd 
 |-  ( 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. _V )
20 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
21 funmpt 
 |-  Fun ( 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 ) ) ) ) ) )
22 21 a1i 
 |-  ( ph -> Fun ( 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 ) ) ) ) ) ) )
23 simpr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
24 14 psrbagsn 
 |-  ( I e. V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
25 3 24 syl 
 |-  ( 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 14 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 23 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 eqidd 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
30 eqid 
 |-  ( Base ` R ) = ( Base ` R )
31 1 30 2 14 6 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
32 31 feqmptd 
 |-  ( ph -> F = ( z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` z ) ) )
33 fveq2 
 |-  ( z = ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) -> ( F ` z ) = ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
34 28 29 32 33 fmptco 
 |-  ( ph -> ( F o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
35 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
36 1 2 35 6 4 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
37 28 fmpttd 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
38 ovex 
 |-  ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. _V
39 eqid 
 |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
40 38 39 fnmpti 
 |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
41 40 a1i 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
42 dffn3 
 |-  ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ran ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
43 41 42 sylib 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ran ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
44 43 37 fcod 
 |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ran ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
45 44 ffnd 
 |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
46 fnresi 
 |-  ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
47 46 a1i 
 |-  ( ph -> ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
48 14 psrbagf 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 )
49 48 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 )
50 49 ffvelcdmda 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) e. NN0 )
51 50 nn0cnd 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) e. CC )
52 ax-1cn 
 |-  1 e. CC
53 0cn 
 |-  0 e. CC
54 52 53 ifcli 
 |-  if ( i = X , 1 , 0 ) e. CC
55 54 a1i 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> if ( i = X , 1 , 0 ) e. CC )
56 51 55 pncand 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( ( d ` i ) + if ( i = X , 1 , 0 ) ) - if ( i = X , 1 , 0 ) ) = ( d ` i ) )
57 56 mpteq2dva 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. I |-> ( ( ( d ` i ) + if ( i = X , 1 , 0 ) ) - if ( i = X , 1 , 0 ) ) ) = ( i e. I |-> ( d ` i ) ) )
58 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
59 25 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 } )
60 14 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 } )
61 58 59 60 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 } )
62 14 psrbagf 
 |-  ( ( d oF + ( 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 ) ) ) : I --> NN0 )
63 62 ffnd 
 |-  ( ( d oF + ( 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 ) ) ) Fn I )
64 61 63 syl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) Fn I )
65 1ex 
 |-  1 e. _V
66 c0ex 
 |-  0 e. _V
67 65 66 ifex 
 |-  if ( y = X , 1 , 0 ) e. _V
68 eqid 
 |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) )
69 67 68 fnmpti 
 |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) Fn I
70 69 a1i 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) Fn I )
71 3 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. V )
72 inidm 
 |-  ( I i^i I ) = I
73 48 ffnd 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d Fn I )
74 73 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d Fn I )
75 eqidd 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) = ( d ` i ) )
76 eqeq1 
 |-  ( y = i -> ( y = X <-> i = X ) )
77 76 ifbid 
 |-  ( y = i -> if ( y = X , 1 , 0 ) = if ( i = X , 1 , 0 ) )
78 simpr 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> i e. I )
79 65 66 ifex 
 |-  if ( i = X , 1 , 0 ) e. _V
80 79 a1i 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> if ( i = X , 1 , 0 ) e. _V )
81 68 77 78 80 fvmptd3 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( y e. I |-> if ( y = X , 1 , 0 ) ) ` i ) = if ( i = X , 1 , 0 ) )
82 74 70 71 71 72 75 81 ofval 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` i ) = ( ( d ` i ) + if ( i = X , 1 , 0 ) ) )
83 64 70 71 71 72 82 81 offval 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( i e. I |-> ( ( ( d ` i ) + if ( i = X , 1 , 0 ) ) - if ( i = X , 1 , 0 ) ) ) )
84 49 feqmptd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d = ( i e. I |-> ( d ` i ) ) )
85 57 83 84 3eqtr4d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = d )
86 28 adantlr 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ 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 } )
87 86 fmpttd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
88 87 58 fvco3d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ` d ) = ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` d ) ) )
89 eqid 
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
90 oveq1 
 |-  ( k = d -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
91 ovexd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. _V )
92 89 90 58 91 fvmptd3 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` d ) = ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
93 92 fveq2d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` d ) ) = ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
94 oveq1 
 |-  ( b = ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) -> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
95 ovexd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. _V )
96 39 94 61 95 fvmptd3 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
97 88 93 96 3eqtrd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ` d ) = ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
98 fvresi 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ` d ) = d )
99 98 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ` d ) = d )
100 85 97 99 3eqtr4d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ` d ) = ( ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ` d ) )
101 45 47 100 eqfnfvd 
 |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
102 fcof1 
 |-  ( ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ) -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -1-1-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
103 37 101 102 syl2anc 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -1-1-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
104 36 103 20 6 fsuppco 
 |-  ( ph -> ( F o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) finSupp ( 0g ` R ) )
105 34 104 eqbrtrrd 
 |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) finSupp ( 0g ` R ) )
106 105 fsuppimpd 
 |-  ( ph -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) e. Fin )
107 ssidd 
 |-  ( ph -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) C_ ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) )
108 eqid 
 |-  ( .g ` R ) = ( .g ` R )
109 30 108 35 mulgnn0z 
 |-  ( ( R e. Mnd /\ n e. NN0 ) -> ( n ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
110 4 109 sylan 
 |-  ( ( ph /\ n e. NN0 ) -> ( n ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
111 14 psrbagf 
 |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> k : I --> NN0 )
112 111 adantl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k : I --> NN0 )
113 5 adantr 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
114 112 113 ffvelcdmd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k ` X ) e. NN0 )
115 peano2nn0 
 |-  ( ( k ` X ) e. NN0 -> ( ( k ` X ) + 1 ) e. NN0 )
116 114 115 syl 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k ` X ) + 1 ) e. NN0 )
117 fvexd 
 |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. _V )
118 107 110 116 117 20 suppssov2 
 |-  ( 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 ) ) ) ) ) ) supp ( 0g ` R ) ) C_ ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) )
119 106 118 ssfid 
 |-  ( 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 ) ) ) ) ) ) supp ( 0g ` R ) ) e. Fin )
120 19 20 22 119 isfsuppd 
 |-  ( 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 ) ) ) ) ) ) finSupp ( 0g ` R ) )
121 15 120 eqbrtrd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) finSupp ( 0g ` R ) )
122 1 7 8 35 2 mplelbas 
 |-  ( ( ( ( I mPSDer R ) ` X ) ` F ) e. B <-> ( ( ( ( I mPSDer R ) ` X ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I mPSDer R ) ` X ) ` F ) finSupp ( 0g ` R ) ) )
123 13 121 122 sylanbrc 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )