Theorem mhphf

Description: A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the ( QX ) which corresponds to X ). (Contributed by SN, 28-Jul-2024) (Proof shortened by SN, 8-Mar-2025)

	Ref	Expression
Hypotheses	mhphf.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	mhphf.h	$$⊢H=I\mathrm{mHomP}U$$
	mhphf.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	mhphf.k	$$⊢K={\mathrm{Base}}_S$$
	mhphf.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	mhphf.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	mhphf.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	mhphf.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	mhphf.l	$$⊢\phi \to L\in R$$
	mhphf.x	$$⊢\phi \to X\in H\left(N\right)$$
	mhphf.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	mhphf	$$⊢\phi \to Q\left(X\right)\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}Q\left(X\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhphf.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		mhphf.h	$$⊢H=I\mathrm{mHomP}U$$
3		mhphf.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		mhphf.k	$$⊢K={\mathrm{Base}}_S$$
5		mhphf.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
6		mhphf.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
7		mhphf.s	$$⊢\phi \to S\in \mathrm{CRing}$$
8		mhphf.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
9		mhphf.l	$$⊢\phi \to L\in R$$
10		mhphf.x	$$⊢\phi \to X\in H\left(N\right)$$
11		mhphf.a	$$⊢\phi \to A\in \left(K^I\right)$$
12		elmapi	$$⊢A\in \left(K^I\right)\to A:I⟶K$$
13	11 12	syl	$$⊢\phi \to A:I⟶K$$
14	13	ffnd	$$⊢\phi \to AFnI$$
15	11 14	fndmexd	$$⊢\phi \to I\in \mathrm{V}$$
16	15	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to I\in \mathrm{V}$$
17	9	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to L\in R$$
18	14	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to AFnI$$
19		eqidd	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to A\left(i\right)=A\left(i\right)$$
20	16 17 18 19	ofc1	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to \left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)=L\underset{\dot{}}{·}A\left(i\right)$$
21	20	oveq2d	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)=b\left(i\right)\underset{\dot{}}{\times }\left(L\underset{\dot{}}{·}A\left(i\right)\right)$$
22		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
23	22	crngmgp	$$⊢S\in \mathrm{CRing}\to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
24	7 23	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
25	24	ad2antrr	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
26		elrabi	$$⊢b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\to b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
27		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
28	27	psrbagf	$$⊢b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to b:I⟶{\mathbb{N}}_0$$
29	26 28	syl	$$⊢b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\to b:I⟶{\mathbb{N}}_0$$
30	29	adantl	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to b:I⟶{\mathbb{N}}_0$$
31	30	ffvelcdmda	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to b\left(i\right)\in {\mathbb{N}}_0$$
32	4	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
33	8 32	syl	$$⊢\phi \to R\subseteq K$$
34	33 9	sseldd	$$⊢\phi \to L\in K$$
35	34	ad2antrr	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to L\in K$$
36	13	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to A:I⟶K$$
37	36	ffvelcdmda	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to A\left(i\right)\in K$$
38	22 4	mgpbas	$$⊢K={\mathrm{Base}}_{{\mathrm{mulGrp}}_S}$$
39	22 5	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_S}$$
40	38 6 39	mulgnn0di	$$⊢\left({\mathrm{mulGrp}}_S\in \mathrm{CMnd}\wedge \left(b\left(i\right)\in {\mathbb{N}}_0\wedge L\in K\wedge A\left(i\right)\in K\right)\right)\to b\left(i\right)\underset{\dot{}}{\times }\left(L\underset{\dot{}}{·}A\left(i\right)\right)=\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
41	25 31 35 37 40	syl13anc	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to b\left(i\right)\underset{\dot{}}{\times }\left(L\underset{\dot{}}{·}A\left(i\right)\right)=\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
42	21 41	eqtrd	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)=\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
43	42	mpteq2dva	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)=\left(i\in I⟼\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
44	43	oveq2d	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)=\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
45		eqid	$$⊢1_S=1_S$$
46	22 45	ringidval	$$⊢1_S=0_{{\mathrm{mulGrp}}_S}$$
47	7	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to S\in \mathrm{CRing}$$
48	47 23	syl	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
49	7	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
50	22	ringmgp	$$⊢S\in \mathrm{Ring}\to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
51	49 50	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
52	51	ad2antrr	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
53	38 6 52 31 35	mulgnn0cld	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to b\left(i\right)\underset{\dot{}}{\times }L\in K$$
54	38 6 52 31 37	mulgnn0cld	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge i\in I\right)\to b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\in K$$
55		eqidd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)=\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)$$
56		eqidd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)=\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
57	15	mptexd	$$⊢\phi \to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)\in \mathrm{V}$$
58	57	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)\in \mathrm{V}$$
59		fvexd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to 1_S\in \mathrm{V}$$
60		funmpt	$$⊢\mathrm{Fun}\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)$$
61	60	a1i	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \mathrm{Fun}\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)$$
62	27	psrbagfsupp	$$⊢b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to {finSupp}_0\left(b\right)$$
63	26 62	syl	$$⊢b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\to {finSupp}_0\left(b\right)$$
64	63	adantl	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to {finSupp}_0\left(b\right)$$
65	30	feqmptd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to b=\left(i\in I⟼b\left(i\right)\right)$$
66	65	oveq1d	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to b\mathrm{supp}0=\left(i\in I⟼b\left(i\right)\right)\mathrm{supp}0$$
67	66	eqimsscd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\right)\mathrm{supp}0\subseteq b\mathrm{supp}0$$
68	38 46 6	mulg0	$$⊢k\in K\to 0\underset{\dot{}}{\times }k=1_S$$
69	68	adantl	$$⊢\left(\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\wedge k\in K\right)\to 0\underset{\dot{}}{\times }k=1_S$$
70		0zd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to 0\in \mathbb{Z}$$
71	67 69 31 35 70	suppssov1	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)\mathrm{supp}{1}_S\subseteq b\mathrm{supp}0$$
72	58 59 61 64 71	fsuppsssuppgd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to {finSupp}_{1_S}\left(\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)\right)$$
73	15	mptexd	$$⊢\phi \to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in \mathrm{V}$$
74	73	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in \mathrm{V}$$
75		funmpt	$$⊢\mathrm{Fun}\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
76	75	a1i	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \mathrm{Fun}\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
77	67 69 31 37 70	suppssov1	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\mathrm{supp}{1}_S\subseteq b\mathrm{supp}0$$
78	74 59 76 64 77	fsuppsssuppgd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to {finSupp}_{1_S}\left(\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
79	38 46 39 48 16 53 54 55 56 72 78	gsummptfsadd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)=\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
80		eqid	$$⊢\left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}=\left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
81	2 10	mhprcl	$$⊢\phi \to N\in {\mathbb{N}}_0$$
82	27 80 38 6 15 51 34 81	mhphflem	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(b\left(i\right)\underset{\dot{}}{\times }L\right)=N\underset{\dot{}}{\times }L$$
83	82	oveq1d	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }L\right)\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
84	44 79 83	3eqtrd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
85	84	oveq2d	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)\right)=X\left(b\right)\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
86		eqid	$$⊢I\mathrm{mPoly}U=I\mathrm{mPoly}U$$
87		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
88		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
89	2 86 88 10	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
90	86 87 88 27 89	mplelf	$$⊢\phi \to X:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_U$$
91	3	subrgbas	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R={\mathrm{Base}}_U$$
92	91 32	eqsstrrd	$$⊢R\in \mathrm{SubRing}\left(S\right)\to {\mathrm{Base}}_U\subseteq K$$
93	8 92	syl	$$⊢\phi \to {\mathrm{Base}}_U\subseteq K$$
94	90 93	fssd	$$⊢\phi \to X:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
95	94	ffvelcdmda	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to X\left(b\right)\in K$$
96	26 95	sylan2	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to X\left(b\right)\in K$$
97	38 6 51 81 34	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }L\in K$$
98	97	adantr	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to N\underset{\dot{}}{\times }L\in K$$
99	15	adantr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to I\in \mathrm{V}$$
100	7	adantr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to S\in \mathrm{CRing}$$
101	11	adantr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to A\in \left(K^I\right)$$
102		simpr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
103	27 4 22 6 99 100 101 102	evlsvvvallem	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in K$$
104	26 103	sylan2	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to \underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in K$$
105	4 5 47 96 98 104	crng12d	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to X\left(b\right)\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
106	85 105	eqtrd	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
107	106	mpteq2dva	$$⊢\phi \to \left(b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)\right)\right)=\left(b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}⟼\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
108	107	oveq2d	$$⊢\phi \to \underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)\right)\right)=\underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S}\left(\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
109		eqid	$$⊢0_S=0_S$$
110		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
111	110	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
112	111	rabex	$$⊢\left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\in \mathrm{V}$$
113	112	a1i	$$⊢\phi \to \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\in \mathrm{V}$$
114	49	adantr	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to S\in \mathrm{Ring}$$
115	4 5 114 95 103	ringcld	$$⊢\left(\phi \wedge b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\in K$$
116	26 115	sylan2	$$⊢\left(\phi \wedge b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\to X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\in K$$
117		ssrab2	$$⊢\left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
118		mptss	$$⊢\left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left(b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\subseteq \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
119	117 118	mp1i	$$⊢\phi \to \left(b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\subseteq \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
120	27 86 3 88 4 22 6 5 15 7 8 89 11	evlsvvvallem2	$$⊢\phi \to {finSupp}_{0_S}\left(\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
121	119 120	fsuppss	$$⊢\phi \to {finSupp}_{0_S}\left(\left(b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}⟼X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
122	4 109 5 49 113 97 116 121	gsummulc2	$$⊢\phi \to \underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S}\left(\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S},\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
123	108 122	eqtrd	$$⊢\phi \to \underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)\right)\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S},\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
124	4	fvexi	$$⊢K\in \mathrm{V}$$
125	124	a1i	$$⊢\phi \to K\in \mathrm{V}$$
126	4 5	ringcl	$$⊢\left(S\in \mathrm{Ring}\wedge j\in K\wedge k\in K\right)\to j\underset{\dot{}}{·}k\in K$$
127	49 126	syl3an1	$$⊢\left(\phi \wedge j\in K\wedge k\in K\right)\to j\underset{\dot{}}{·}k\in K$$
128	127	3expb	$$⊢\left(\phi \wedge \left(j\in K\wedge k\in K\right)\right)\to j\underset{\dot{}}{·}k\in K$$
129		fconst6g	$$⊢L\in K\to \left(I\times \left\{L\right\}\right):I⟶K$$
130	34 129	syl	$$⊢\phi \to \left(I\times \left\{L\right\}\right):I⟶K$$
131		inidm	$$⊢I\cap I=I$$
132	128 130 13 15 15 131	off	$$⊢\phi \to \left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right):I⟶K$$
133	125 15 132	elmapdd	$$⊢\phi \to \left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\in \left(K^I\right)$$
134	1 2 3 27 80 4 22 6 5 7 8 10 133	evlsmhpvvval	$$⊢\phi \to Q\left(X\right)\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)=\underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)\left(i\right)\right)\right)\right)$$
135	1 2 3 27 80 4 22 6 5 7 8 10 11	evlsmhpvvval	$$⊢\phi \to Q\left(X\right)\left(A\right)=\underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S}\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
136	135	oveq2d	$$⊢\phi \to \left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}Q\left(X\right)\left(A\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}\left(\underset{b\in \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}}{{\sum }_S},\left(X\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_{{\mathrm{mulGrp}}_S}},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
137	123 134 136	3eqtr4d	$$⊢\phi \to Q\left(X\right)\left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right)=\left(N\underset{\dot{}}{\times }L\right)\underset{\dot{}}{·}Q\left(X\right)\left(A\right)$$