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