I propose to use (the new version of) frlmgsum in step 85 and to replace
step 84 by
d7::eqid |- ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
= ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
d13:15:mptex |- ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) )
e. _V
d9:d13:a1i |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) )
e. _V )
d12::snex |- { 0 } e. _V
d11:15,d12:xpex |- ( ( 1 ... N ) X. { 0 } ) e. _V
d10:d11:a1i |- ( ( ph /\ w : ( 0 ... N ) --> QQ )
-> ( ( 1 ... N ) X. { 0 } ) e. _V )
84:d7,45,d9,d10:fsuppmptdm |- ( ( ph /\ w : ( 0 ... N ) --> QQ )
-> ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
finSupp
( ( 1 ... N ) X. { 0 } ) )
On Saturday, April 25, 2020 at 9:24:12 AM UTC+2, Alexander van der Vekens
wrote:
>
> The problem is that the proof uses an old version of frlmgsum: Either
> frlmgsumOLD (deprecated!) must be used in step 85, or step 84 must be
> adapted to comply with the new version of frlmgsum.
>
> Alexander
>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/025c4636-4427-41a6-9069-bc676cb3d0c2%40googlegroups.com.
