Theorem mplmonprod

Description: Finite product of monomials. Here the function G maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	mplmonprod.p	$$⊢P=I\mathrm{mPoly}R$$
	mplmonprod.b	$$⊢B={\mathrm{Base}}_P$$
	mplmonprod.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	mplmonprod.i	$$⊢\phi \to I\in V$$
	mplmonprod.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	mplmonprod.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	mplmonprod.f	$$⊢\phi \to F:A⟶D$$
	mplmonprod.1	$$⊢\underset{\dot{}}{1}=1_R$$
	mplmonprod.0	$$⊢\underset{\dot{}}{0}=0_R$$
	mplmonprod.m	$$⊢M={\mathrm{mulGrp}}_P$$
	mplmonprod.g	$$⊢G=\left(y\in D⟼\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
Assertion	mplmonprod	$$⊢\phi \to {\sum }_M\left(G\circ F\right)=G\left(\left(i\in I⟼\underset{x\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}F\left(x\right)\left(i\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplmonprod.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplmonprod.b	$$⊢B={\mathrm{Base}}_P$$
3		mplmonprod.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		mplmonprod.i	$$⊢\phi \to I\in V$$
5		mplmonprod.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
6		mplmonprod.a	$$⊢\phi \to A\in \mathrm{Fin}$$
7		mplmonprod.f	$$⊢\phi \to F:A⟶D$$
8		mplmonprod.1	$$⊢\underset{\dot{}}{1}=1_R$$
9		mplmonprod.0	$$⊢\underset{\dot{}}{0}=0_R$$
10		mplmonprod.m	$$⊢M={\mathrm{mulGrp}}_P$$
11		mplmonprod.g	$$⊢G=\left(y\in D⟼\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
12		eqid	$$⊢{\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}$$
13		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14	12 13	mgpbas	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}}$$
15		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
16		eqid	$$⊢{\cdot }_P={\cdot }_P$$
17	1 15 16	mplmulr	$$⊢{\cdot }_P={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
18	12 17	mgpplusg	$$⊢{\cdot }_P={+}_{{\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}}$$
19		ovex	$$⊢I\mathrm{mPwSer}R\in \mathrm{V}$$
20	2	fvexi	$$⊢B\in \mathrm{V}$$
21	1 15 2	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}B$$
22	21 12	mgpress	$$⊢\left(I\mathrm{mPwSer}R\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to {\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}{\upharpoonright }_{𝑠}B={\mathrm{mulGrp}}_P$$
23	19 20 22	mp2an	$$⊢{\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}{\upharpoonright }_{𝑠}B={\mathrm{mulGrp}}_P$$
24	10 23	eqtr4i	$$⊢M={\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}{\upharpoonright }_{𝑠}B$$
25		fvexd	$$⊢\phi \to {\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}\in \mathrm{V}$$
26	1 15 2 13	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
27	26	a1i	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
28		fvexd	$$⊢\left(\phi \wedge y\in D\right)\to {\mathrm{Base}}_R\in \mathrm{V}$$
29		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
30	5 29	rabex2	$$⊢D\in \mathrm{V}$$
31	30	a1i	$$⊢\left(\phi \wedge y\in D\right)\to D\in \mathrm{V}$$
32		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
33	3	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
34	32 8 33	ringidcld	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
35	3	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
36	32 9	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
37	35 36	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
38	34 37	ifcld	$$⊢\phi \to if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
39	38	ad2antrr	$$⊢\left(\left(\phi \wedge y\in D\right)\wedge z\in D\right)\to if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
40		eqid	$$⊢\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
41	39 40	fmptd	$$⊢\left(\phi \wedge y\in D\right)\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
42	28 31 41	elmapdd	$$⊢\left(\phi \wedge y\in D\right)\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)$$
43	5	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
44	4	adantr	$$⊢\left(\phi \wedge y\in D\right)\to I\in V$$
45	15 32 43 13 44	psrbas	$$⊢\left(\phi \wedge y\in D\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^D$$
46	42 45	eleqtrrd	$$⊢\left(\phi \wedge y\in D\right)\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
47		velsn	$$⊢z\in \left\{y\right\}\leftrightarrow z=y$$
48	47	bicomi	$$⊢z=y\leftrightarrow z\in \left\{y\right\}$$
49	48	a1i	$$⊢z\in D\to \left(z=y\leftrightarrow z\in \left\{y\right\}\right)$$
50	49	ifbid	$$⊢z\in D\to if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(z\in \left\{y\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
51	50	mpteq2ia	$$⊢\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(z\in D⟼if\left(z\in \left\{y\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
52		snfi	$$⊢\left\{y\right\}\in \mathrm{Fin}$$
53	52	a1i	$$⊢\left(\phi \wedge y\in D\right)\to \left\{y\right\}\in \mathrm{Fin}$$
54	8	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
55	54	a1i	$$⊢\left(\left(\phi \wedge y\in D\right)\wedge z\in \left\{y\right\}\right)\to \underset{\dot{}}{1}\in \mathrm{V}$$
56	9	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
57	56	a1i	$$⊢\left(\phi \wedge y\in D\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
58	51 31 53 55 57	mptiffisupp	$$⊢\left(\phi \wedge y\in D\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
59	1 15 13 9 2	mplelbas	$$⊢\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B\leftrightarrow \left(\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(\left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right)$$
60	46 58 59	sylanbrc	$$⊢\left(\phi \wedge y\in D\right)\to \left(z\in D⟼if\left(z=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
61	60 11	fmptd	$$⊢\phi \to G:D⟶B$$
62	61 7	fcod	$$⊢\phi \to \left(G\circ F\right):A⟶B$$
63	15 1 2 4 33	mplsubrg	$$⊢\phi \to B\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)$$
64		eqid	$$⊢1_{\left(I\mathrm{mPwSer}R\right)}=1_{\left(I\mathrm{mPwSer}R\right)}$$
65	64	subrg1cl	$$⊢B\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)\to 1_{\left(I\mathrm{mPwSer}R\right)}\in B$$
66	63 65	syl	$$⊢\phi \to 1_{\left(I\mathrm{mPwSer}R\right)}\in B$$
67	15 4 33	psrring	$$⊢\phi \to I\mathrm{mPwSer}R\in \mathrm{Ring}$$
68	67	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to I\mathrm{mPwSer}R\in \mathrm{Ring}$$
69		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)}$$
70	13 17 64 68 69	ringlidmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to 1_{\left(I\mathrm{mPwSer}R\right)}{\cdot }_{P}x=x$$
71	13 17 64 68 69	ringridmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to x{\cdot }_P{1}_{\left(I\mathrm{mPwSer}R\right)}=x$$
72	70 71	jca	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\right)\to \left(1_{\left(I\mathrm{mPwSer}R\right)}{\cdot }_{P}x=x\wedge x{\cdot }_P{1}_{\left(I\mathrm{mPwSer}R\right)}=x\right)$$
73	14 18 24 25 6 27 62 66 72	gsumress	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}}\left(G\circ F\right)={\sum }_M\left(G\circ F\right)$$
74	15 13 3 4 5 6 7 8 9 12 11	psrmonprod	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{\left(I\mathrm{mPwSer}R\right)}}\left(G\circ F\right)=G\left(\left(i\in I⟼\underset{x\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}F\left(x\right)\left(i\right)\right)\right)$$
75	73 74	eqtr3d	$$⊢\phi \to {\sum }_M\left(G\circ F\right)=G\left(\left(i\in I⟼\underset{x\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}F\left(x\right)\left(i\right)\right)\right)$$