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.i	$$⊢\phi \to I\in V$$
	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.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	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.i	$$⊢\phi \to I\in V$$
8		mhphf.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		mhphf.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		mhphf.l	$$⊢\phi \to L\in R$$
11		mhphf.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12		mhphf.x	$$⊢\phi \to X\in H\left(N\right)$$
13		mhphf.a	$$⊢\phi \to A\in \left(K^I\right)$$
14	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 I\in V$$
15	10	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$$
16		elmapi	$$⊢A\in \left(K^I\right)\to A:I⟶K$$
17	13 16	syl	$$⊢\phi \to A:I⟶K$$
18	17	ffnd	$$⊢\phi \to AFnI$$
19	18	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$$
20		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)$$
21	14 15 19 20	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)$$
22	21	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)$$
23		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
24	23	crngmgp	$$⊢S\in \mathrm{CRing}\to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
25	8 24	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{CMnd}$$
26	25	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}$$
27		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\}$$
28		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\}$$
29	28	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$$
30	27 29	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$$
31	30	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$$
32	31	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$$
33	4	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
34	9 33	syl	$$⊢\phi \to R\subseteq K$$
35	34 10	sseldd	$$⊢\phi \to L\in K$$
36	35	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$$
37	17	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$$
38	37	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$$
39	23 4	mgpbas	$$⊢K={\mathrm{Base}}_{{\mathrm{mulGrp}}_S}$$
40	23 5	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_S}$$
41	39 6 40	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)$$
42	26 32 36 38 41	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)$$
43	22 42	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)$$
44	43	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)$$
45	44	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)$$
46		eqid	$$⊢1_S=1_S$$
47	23 46	ringidval	$$⊢1_S=0_{{\mathrm{mulGrp}}_S}$$
48	8	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}$$
49	48 24	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}$$
50	8	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
51	23	ringmgp	$$⊢S\in \mathrm{Ring}\to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
52	50 51	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
53	52	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}$$
54	39 6 53 32 36	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$$
55	39 6 53 32 38	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$$
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 }L\right)=\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)$$
57		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)$$
58	7	mptexd	$$⊢\phi \to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)\in \mathrm{V}$$
59	58	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}$$
60		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}$$
61		funmpt	$$⊢\mathrm{Fun}\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }L\right)$$
62	61	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)$$
63	28	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)$$
64	27 63	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)$$
65	64	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)$$
66	31	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)$$
67	66	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$$
68	67	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$$
69	39 47 6	mulg0	$$⊢k\in K\to 0\underset{\dot{}}{\times }k=1_S$$
70	69	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$$
71		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}$$
72	68 70 32 36 71	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$$
73	59 60 62 65 72	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)$$
74	7	mptexd	$$⊢\phi \to \left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in \mathrm{V}$$
75	74	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}$$
76		funmpt	$$⊢\mathrm{Fun}\left(i\in I⟼b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)$$
77	76	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)$$
78	68 70 32 38 71	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$$
79	75 60 77 65 78	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)$$
80	39 47 40 49 14 54 55 56 57 73 79	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)$$
81		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\}$$
82	28 81 39 6 7 52 35 11	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	45 80 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	3	ovexi	$$⊢U\in \mathrm{V}$$
90	89	a1i	$$⊢\phi \to U\in \mathrm{V}$$
91	2 86 88 7 90 11 12	mhpmpl	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
92	86 87 88 28 91	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$$
93	3	subrgbas	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R={\mathrm{Base}}_U$$
94	93 33	eqsstrrd	$$⊢R\in \mathrm{SubRing}\left(S\right)\to {\mathrm{Base}}_U\subseteq K$$
95	9 94	syl	$$⊢\phi \to {\mathrm{Base}}_U\subseteq K$$
96	92 95	fssd	$$⊢\phi \to X:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶K$$
97	96	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$$
98	27 97	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$$
99	39 6 52 11 35	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }L\in K$$
100	99	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$$
101	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 I\in V$$
102	8	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}$$
103	13	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)$$
104		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\}$$
105	28 4 23 6 101 102 103 104	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$$
106	27 105	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$$
107	4 5 48 98 100 106	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)$$
108	85 107	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)$$
109	108	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)$$
110	109	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)$$
111		eqid	$$⊢0_S=0_S$$
112		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
113	112	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
114	113	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}$$
115	114	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}$$
116	50	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}$$
117	4 5 116 97 105	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$$
118	27 117	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$$
119		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\}$$
120		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)$$
121	119 120	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)$$
122	28 86 3 88 4 23 6 5 7 8 9 91 13	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)$$
123	121 122	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)$$
124	4 111 5 50 115 99 118 123	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)$$
125	110 124	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)$$
126	4	fvexi	$$⊢K\in \mathrm{V}$$
127	126	a1i	$$⊢\phi \to K\in \mathrm{V}$$
128	4 5	ringcl	$$⊢\left(S\in \mathrm{Ring}\wedge j\in K\wedge k\in K\right)\to j\underset{\dot{}}{·}k\in K$$
129	50 128	syl3an1	$$⊢\left(\phi \wedge j\in K\wedge k\in K\right)\to j\underset{\dot{}}{·}k\in K$$
130	129	3expb	$$⊢\left(\phi \wedge \left(j\in K\wedge k\in K\right)\right)\to j\underset{\dot{}}{·}k\in K$$
131		fconst6g	$$⊢L\in K\to \left(I\times \left\{L\right\}\right):I⟶K$$
132	35 131	syl	$$⊢\phi \to \left(I\times \left\{L\right\}\right):I⟶K$$
133		inidm	$$⊢I\cap I=I$$
134	130 132 17 7 7 133	off	$$⊢\phi \to \left(\left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\right):I⟶K$$
135	127 7 134	elmapdd	$$⊢\phi \to \left(I\times \left\{L\right\}\right){\underset{\dot{}}{·}}_{f}A\in \left(K^I\right)$$
136	1 2 3 28 81 4 23 6 5 7 8 9 11 12 135	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)$$
137	1 2 3 28 81 4 23 6 5 7 8 9 11 12 13	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)$$
138	137	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)$$
139	125 136 138	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)$$