Theorem mplgsum

Description: Finite commutative sums of polynomials are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	mplgsum.p	$$⊢P=I\mathrm{mPoly}R$$
	mplgsum.b	$$⊢B={\mathrm{Base}}_P$$
	mplgsum.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplgsum.i	$$⊢\phi \to I\in V$$
	mplgsum.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	mplgsum.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	mplgsum.f	$$⊢\phi \to F:A⟶B$$
Assertion	mplgsum	$$⊢\phi \to {\sum }_{P}F=\left(y\in D⟼\underset{k\in A}{{\sum }_R}F\left(k\right)\left(y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplgsum.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplgsum.b	$$⊢B={\mathrm{Base}}_P$$
3		mplgsum.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		mplgsum.i	$$⊢\phi \to I\in V$$
5		mplgsum.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
6		mplgsum.a	$$⊢\phi \to A\in \mathrm{Fin}$$
7		mplgsum.f	$$⊢\phi \to F:A⟶B$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
9		eqid	$$⊢{+}_{\left(I\mathrm{mPwSer}R\right)}={+}_{\left(I\mathrm{mPwSer}R\right)}$$
10		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
11	1 10 2	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}B$$
12		ovexd	$$⊢\phi \to I\mathrm{mPwSer}R\in \mathrm{V}$$
13	1 10 2 8	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14	13	a1i	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
15	3	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
16	5	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
17		eqid	$$⊢0_R=0_R$$
18		eqid	$$⊢0_{\left(I\mathrm{mPwSer}R\right)}=0_{\left(I\mathrm{mPwSer}R\right)}$$
19	10 4 15 16 17 18	psr0	$$⊢\phi \to 0_{\left(I\mathrm{mPwSer}R\right)}=D\times \left\{0_R\right\}$$
20		eqid	$$⊢0_P=0_P$$
21	1 16 17 20 4 15	mpl0	$$⊢\phi \to 0_P=D\times \left\{0_R\right\}$$
22	19 21	eqtr4d	$$⊢\phi \to 0_{\left(I\mathrm{mPwSer}R\right)}=0_P$$
23	1	mplgrp	$$⊢\left(I\in V\wedge R\in \mathrm{Grp}\right)\to P\in \mathrm{Grp}$$
24	4 15 23	syl2anc	$$⊢\phi \to P\in \mathrm{Grp}$$
25	2 20	grpidcl	$$⊢P\in \mathrm{Grp}\to 0_P\in B$$
26	24 25	syl	$$⊢\phi \to 0_P\in B$$
27	22 26	eqeltrd	$$⊢\phi \to 0_{\left(I\mathrm{mPwSer}R\right)}\in B$$
28	10 4 15	psrgrp	$$⊢\phi \to I\mathrm{mPwSer}R\in \mathrm{Grp}$$
29	28	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to I\mathrm{mPwSer}R\in \mathrm{Grp}$$
30		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
31	8 9 18 29 30	grplidd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to 0_{\left(I\mathrm{mPwSer}R\right)}{+}_{\left(I\mathrm{mPwSer}R\right)}x=x$$
32	8 9 18 29 30	grpridd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to x{+}_{\left(I\mathrm{mPwSer}R\right)}{0}_{\left(I\mathrm{mPwSer}R\right)}=x$$
33	31 32	jca	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to \left(0_{\left(I\mathrm{mPwSer}R\right)}{+}_{\left(I\mathrm{mPwSer}R\right)}x=x\wedge x{+}_{\left(I\mathrm{mPwSer}R\right)}{0}_{\left(I\mathrm{mPwSer}R\right)}=x\right)$$
34	8 9 11 12 6 14 7 27 33	gsumress	$$⊢\phi \to {\sum }_{I\mathrm{mPwSer}R}F={\sum }_{P}F$$
35	7 14	fssd	$$⊢\phi \to F:A⟶{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
36	10 8 3 4 5 6 35	psrgsum	$$⊢\phi \to {\sum }_{I\mathrm{mPwSer}R}F=\left(y\in D⟼\underset{k\in A}{{\sum }_R}F\left(k\right)\left(y\right)\right)$$
37	34 36	eqtr3d	$$⊢\phi \to {\sum }_{P}F=\left(y\in D⟼\underset{k\in A}{{\sum }_R}F\left(k\right)\left(y\right)\right)$$