Theorem evlsbagval

Description: Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since .0. and .1. using U instead of S is convenient for its sole use case mhphf , but may not be convenient for other uses. (Contributed by SN, 29-Jul-2024)

	Ref	Expression
Hypotheses	evlsbagval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsbagval.p	$$⊢P=I\mathrm{mPoly}U$$
	evlsbagval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsbagval.w	$$⊢W={\mathrm{Base}}_P$$
	evlsbagval.k	$$⊢K={\mathrm{Base}}_S$$
	evlsbagval.m	$$⊢M={\mathrm{mulGrp}}_S$$
	evlsbagval.e	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlsbagval.z	$$⊢\underset{\dot{}}{0}=0_U$$
	evlsbagval.o	$$⊢\underset{\dot{}}{1}=1_U$$
	evlsbagval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlsbagval.f	$$⊢F=\left(s\in D⟼if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
	evlsbagval.i	$$⊢\phi \to I\in V$$
	evlsbagval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsbagval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsbagval.a	$$⊢\phi \to A\in \left(K^I\right)$$
	evlsbagval.b	$$⊢\phi \to B\in D$$
Assertion	evlsbagval	$$⊢\phi \to \left(F\in W\wedge Q\left(F\right)\left(A\right)=\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlsbagval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		evlsbagval.p	$$⊢P=I\mathrm{mPoly}U$$
3		evlsbagval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evlsbagval.w	$$⊢W={\mathrm{Base}}_P$$
5		evlsbagval.k	$$⊢K={\mathrm{Base}}_S$$
6		evlsbagval.m	$$⊢M={\mathrm{mulGrp}}_S$$
7		evlsbagval.e	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
8		evlsbagval.z	$$⊢\underset{\dot{}}{0}=0_U$$
9		evlsbagval.o	$$⊢\underset{\dot{}}{1}=1_U$$
10		evlsbagval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		evlsbagval.f	$$⊢F=\left(s\in D⟼if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
12		evlsbagval.i	$$⊢\phi \to I\in V$$
13		evlsbagval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
14		evlsbagval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
15		evlsbagval.a	$$⊢\phi \to A\in \left(K^I\right)$$
16		evlsbagval.b	$$⊢\phi \to B\in D$$
17		fvexd	$$⊢\phi \to {\mathrm{Base}}_U\in \mathrm{V}$$
18		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
19	10 18	rabexd	$$⊢\phi \to D\in \mathrm{V}$$
20	3	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
21	14 20	syl	$$⊢\phi \to U\in \mathrm{Ring}$$
22		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
23	22 9	ringidcl	$$⊢U\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_U$$
24	21 23	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_U$$
25	22 8	ring0cl	$$⊢U\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_U$$
26	21 25	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_U$$
27	24 26	ifcld	$$⊢\phi \to if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_U$$
28	27	adantr	$$⊢\left(\phi \wedge s\in D\right)\to if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_U$$
29	28 11	fmptd	$$⊢\phi \to F:D⟶{\mathrm{Base}}_U$$
30	17 19 29	elmapdd	$$⊢\phi \to F\in \left({{\mathrm{Base}}_U}^D\right)$$
31		eqid	$$⊢I\mathrm{mPwSer}U=I\mathrm{mPwSer}U$$
32		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}U\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}U\right)}$$
33	31 22 10 32 12	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}U\right)}={{\mathrm{Base}}_U}^D$$
34	30 33	eleqtrrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}U\right)}$$
35	19 26 11	sniffsupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
36	2 31 32 8 4	mplelbas	$$⊢F\in W\leftrightarrow \left(F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}U\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
37	34 35 36	sylanbrc	$$⊢\phi \to F\in W$$
38		fveq1	$$⊢g=A\to g\left(v\right)=A\left(v\right)$$
39	38	oveq2d	$$⊢g=A\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)=B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)$$
40	39	mpteq2dv	$$⊢g=A\to \left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)=\left(v\in I⟼B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)$$
41	40	oveq2d	$$⊢g=A\to \underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)=\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)$$
42		fveq1	$$⊢p=F\to p\left(b\right)=F\left(b\right)$$
43	42	fveq2d	$$⊢p=F\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)$$
44	43	oveq1d	$$⊢p=F\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
45	44	mpteq2dv	$$⊢p=F\to \left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
46	45	oveq2d	$$⊢p=F\to \underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
47		eqid	$$⊢S{\uparrow }_{𝑠}\left(K^I\right)=S{\uparrow }_{𝑠}\left(K^I\right)$$
48		eqid	$$⊢{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
49		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}$$
50		eqid	$$⊢{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
51		eqid	$$⊢\left(p\in W⟼\underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\right)=\left(p\in W⟼\underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\right)$$
52		eqid	$$⊢\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)$$
53		eqid	$$⊢\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)=\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)$$
54	1 2 4 10 5 3 47 48 49 50 51 52 53 12 13 14	evlsval3	$$⊢\phi \to Q=\left(p\in W⟼\underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(p\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\right)$$
55		ovexd	$$⊢\phi \to \underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\in \mathrm{V}$$
56	46 54 37 55	fvmptd4	$$⊢\phi \to Q\left(F\right)=\underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
57		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
58		eqid	$$⊢0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
59	13	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
60		ovexd	$$⊢\phi \to K^I\in \mathrm{V}$$
61	47	pwsring	$$⊢\left(S\in \mathrm{Ring}\wedge K^I\in \mathrm{V}\right)\to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Ring}$$
62	59 60 61	syl2anc	$$⊢\phi \to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Ring}$$
63	62	ringcmnd	$$⊢\phi \to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{CMnd}$$
64	62	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Ring}$$
65	13	ad2antrr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in R\right)\to S\in \mathrm{CRing}$$
66		ovexd	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in R\right)\to K^I\in \mathrm{V}$$
67	5	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
68	14 67	syl	$$⊢\phi \to R\subseteq K$$
69	68	adantr	$$⊢\left(\phi \wedge b\in D\right)\to R\subseteq K$$
70	69	sselda	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in R\right)\to x\in K$$
71		fconst6g	$$⊢x\in K\to \left(\left(K^I\right)\times \left\{x\right\}\right):K^I⟶K$$
72	70 71	syl	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in R\right)\to \left(\left(K^I\right)\times \left\{x\right\}\right):K^I⟶K$$
73	47 5 57 65 66 72	pwselbasr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in R\right)\to \left(K^I\right)\times \left\{x\right\}\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
74	73	fmpttd	$$⊢\left(\phi \wedge b\in D\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right):R⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
75		eqid	$$⊢1_S=1_S$$
76	3 75	subrg1	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 1_S=1_U$$
77	14 76	syl	$$⊢\phi \to 1_S=1_U$$
78	75	subrg1cl	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 1_S\in R$$
79	14 78	syl	$$⊢\phi \to 1_S\in R$$
80	77 79	eqeltrrd	$$⊢\phi \to 1_U\in R$$
81	9 80	eqeltrid	$$⊢\phi \to \underset{\dot{}}{1}\in R$$
82	3	subrgbas	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R={\mathrm{Base}}_U$$
83	14 82	syl	$$⊢\phi \to R={\mathrm{Base}}_U$$
84	26 83	eleqtrrd	$$⊢\phi \to \underset{\dot{}}{0}\in R$$
85	81 84	ifcld	$$⊢\phi \to if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in R$$
86	85	adantr	$$⊢\left(\phi \wedge s\in D\right)\to if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in R$$
87	86 11	fmptd	$$⊢\phi \to F:D⟶R$$
88	87	ffvelrnda	$$⊢\left(\phi \wedge b\in D\right)\to F\left(b\right)\in R$$
89	74 88	ffvelrnd	$$⊢\left(\phi \wedge b\in D\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
90	48 57	mgpbas	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}$$
91	47	pwscrng	$$⊢\left(S\in \mathrm{CRing}\wedge K^I\in \mathrm{V}\right)\to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{CRing}$$
92	13 60 91	syl2anc	$$⊢\phi \to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{CRing}$$
93	48	crngmgp	$$⊢S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{CMnd}$$
94	92 93	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{CMnd}$$
95	94	adantr	$$⊢\left(\phi \wedge b\in D\right)\to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{CMnd}$$
96		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
97	13	ad2antrr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\to S\in \mathrm{CRing}$$
98		ovexd	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\to K^I\in \mathrm{V}$$
99		elmapi	$$⊢a\in \left(K^I\right)\to a:I⟶K$$
100	99	adantl	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to a:I⟶K$$
101		simplr	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to x\in I$$
102	100 101	ffvelrnd	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to a\left(x\right)\in K$$
103	102	fmpttd	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right):K^I⟶K$$
104	47 5 57 97 98 103	pwselbasr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge x\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
105	104	fmpttd	$$⊢\left(\phi \wedge b\in D\right)\to \left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right):I⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
106	10 90 49 95 96 105	psrbagev2	$$⊢\left(\phi \wedge b\in D\right)\to {\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
107	57 50 64 89 106	ringcld	$$⊢\left(\phi \wedge b\in D\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
108	107	fmpttd	$$⊢\phi \to \left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right):D⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
109		eqeq1	$$⊢s=b\to \left(s=B\leftrightarrow b=B\right)$$
110	109	ifbid	$$⊢s=b\to if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(b=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
111		eldifi	$$⊢b\in \left(D\setminus \left\{B\right\}\right)\to b\in D$$
112	111	adantl	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to b\in D$$
113	9	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
114	8	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
115	113 114	ifex	$$⊢if\left(b=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
116	115	a1i	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to if\left(b=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
117	11 110 112 116	fvmptd3	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to F\left(b\right)=if\left(b=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
118		eldifsnneq	$$⊢b\in \left(D\setminus \left\{B\right\}\right)\to \neg b=B$$
119	118	adantl	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \neg b=B$$
120	119	iffalsed	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to if\left(b=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
121	117 120	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to F\left(b\right)=\underset{\dot{}}{0}$$
122	121	fveq2d	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(\underset{\dot{}}{0}\right)$$
123		sneq	$$⊢x=\underset{\dot{}}{0}\to \left\{x\right\}=\left\{\underset{\dot{}}{0}\right\}$$
124	123	xpeq2d	$$⊢x=\underset{\dot{}}{0}\to \left(K^I\right)\times \left\{x\right\}=\left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}$$
125	84	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \underset{\dot{}}{0}\in R$$
126		ovex	$$⊢K^I\in \mathrm{V}$$
127		snex	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
128	126 127	xpex	$$⊢\left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
129	128	a1i	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
130	52 124 125 129	fvmptd3	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(\underset{\dot{}}{0}\right)=\left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}$$
131		eqid	$$⊢0_S=0_S$$
132	3 131	subrg0	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 0_S=0_U$$
133	14 132	syl	$$⊢\phi \to 0_S=0_U$$
134	133 8	eqtr4di	$$⊢\phi \to 0_S=\underset{\dot{}}{0}$$
135	134	sneqd	$$⊢\phi \to \left\{0_S\right\}=\left\{\underset{\dot{}}{0}\right\}$$
136	135	xpeq2d	$$⊢\phi \to \left(K^I\right)\times \left\{0_S\right\}=\left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}$$
137	59	ringgrpd	$$⊢\phi \to S\in \mathrm{Grp}$$
138	137	grpmndd	$$⊢\phi \to S\in \mathrm{Mnd}$$
139	47 131	pws0g	$$⊢\left(S\in \mathrm{Mnd}\wedge K^I\in \mathrm{V}\right)\to \left(K^I\right)\times \left\{0_S\right\}=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
140	138 60 139	syl2anc	$$⊢\phi \to \left(K^I\right)\times \left\{0_S\right\}=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
141	136 140	eqtr3d	$$⊢\phi \to \left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
142	141	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(K^I\right)\times \left\{\underset{\dot{}}{0}\right\}=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
143	122 130 142	3eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
144	143	oveq1d	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
145	94	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{CMnd}$$
146	13	ad2antrr	$$⊢\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\to S\in \mathrm{CRing}$$
147		ovexd	$$⊢\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\to K^I\in \mathrm{V}$$
148	99	adantl	$$⊢\left(\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to a:I⟶K$$
149		simplr	$$⊢\left(\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to x\in I$$
150	148 149	ffvelrnd	$$⊢\left(\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to a\left(x\right)\in K$$
151	150	fmpttd	$$⊢\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right):K^I⟶K$$
152	47 5 57 146 147 151	pwselbasr	$$⊢\left(\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\wedge x\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
153	152	fmpttd	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right):I⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
154	10 90 49 145 112 153	psrbagev2	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to {\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
155	57 50 58	ringlz	$$⊢\left(S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Ring}\wedge {\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\right)\to 0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
156	62 154 155	syl2an2r	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to 0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
157	144 156	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{B\right\}\right)\right)\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
158	157 19	suppss2	$$⊢\phi \to \left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\mathrm{supp}{0}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\subseteq \left\{B\right\}$$
159	19	mptexd	$$⊢\phi \to \left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\in \mathrm{V}$$
160		fvexd	$$⊢\phi \to 0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{V}$$
161		funmpt	$$⊢\mathrm{Fun}\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
162	161	a1i	$$⊢\phi \to \mathrm{Fun}\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
163		snfi	$$⊢\left\{B\right\}\in \mathrm{Fin}$$
164	163	a1i	$$⊢\phi \to \left\{B\right\}\in \mathrm{Fin}$$
165	164 158	ssfid	$$⊢\phi \to \left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\mathrm{supp}{0}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{Fin}$$
166	159 160 162 165	isfsuppd	$$⊢\phi \to {finSupp}_{0_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\right)$$
167	57 58 63 19 108 158 166	gsumres	$$⊢\phi \to {\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}\left({\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\upharpoonright }_{\left\{B\right\}}\right)=\underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
168	16	snssd	$$⊢\phi \to \left\{B\right\}\subseteq D$$
169	168	resmptd	$$⊢\phi \to {\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\upharpoonright }_{\left\{B\right\}}=\left(b\in \left\{B\right\}⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
170	169	oveq2d	$$⊢\phi \to {\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}\left({\left(b\in D⟼\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)\upharpoonright }_{\left\{B\right\}}\right)=\underset{b\in \left\{B\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
171	167 170	eqtr3d	$$⊢\phi \to \underset{b\in D}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\underset{b\in \left\{B\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)$$
172	62	ringgrpd	$$⊢\phi \to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Grp}$$
173	172	grpmndd	$$⊢\phi \to S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Mnd}$$
174		iftrue	$$⊢s=B\to if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$
175	113	a1i	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{V}$$
176	11 174 16 175	fvmptd3	$$⊢\phi \to F\left(B\right)=\underset{\dot{}}{1}$$
177	176	fveq2d	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(\underset{\dot{}}{1}\right)$$
178	9 77	eqtr4id	$$⊢\phi \to \underset{\dot{}}{1}=1_S$$
179	178	fveq2d	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(\underset{\dot{}}{1}\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(1_S\right)$$
180		sneq	$$⊢x=1_S\to \left\{x\right\}=\left\{1_S\right\}$$
181	180	xpeq2d	$$⊢x=1_S\to \left(K^I\right)\times \left\{x\right\}=\left(K^I\right)\times \left\{1_S\right\}$$
182		snex	$$⊢\left\{1_S\right\}\in \mathrm{V}$$
183	182	a1i	$$⊢\phi \to \left\{1_S\right\}\in \mathrm{V}$$
184	60 183	xpexd	$$⊢\phi \to \left(K^I\right)\times \left\{1_S\right\}\in \mathrm{V}$$
185	52 181 79 184	fvmptd3	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(1_S\right)=\left(K^I\right)\times \left\{1_S\right\}$$
186	179 185	eqtrd	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(\underset{\dot{}}{1}\right)=\left(K^I\right)\times \left\{1_S\right\}$$
187	47 75	pws1	$$⊢\left(S\in \mathrm{Ring}\wedge K^I\in \mathrm{V}\right)\to \left(K^I\right)\times \left\{1_S\right\}=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
188	59 60 187	syl2anc	$$⊢\phi \to \left(K^I\right)\times \left\{1_S\right\}=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
189	177 186 188	3eqtrd	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right)=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
190	189	oveq1d	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
191		eqid	$$⊢1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
192	13	adantr	$$⊢\left(\phi \wedge x\in I\right)\to S\in \mathrm{CRing}$$
193		ovexd	$$⊢\left(\phi \wedge x\in I\right)\to K^I\in \mathrm{V}$$
194	99	adantl	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to a:I⟶K$$
195		simplr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to x\in I$$
196	194 195	ffvelrnd	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge a\in \left(K^I\right)\right)\to a\left(x\right)\in K$$
197	196	fmpttd	$$⊢\left(\phi \wedge x\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right):K^I⟶K$$
198	47 5 57 192 193 197	pwselbasr	$$⊢\left(\phi \wedge x\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
199	198	fmpttd	$$⊢\phi \to \left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right):I⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
200	10 90 49 94 16 199	psrbagev2	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
201	57 50 191 62 200	ringlidmd	$$⊢\phi \to 1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)={\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)$$
202	190 201	eqtrd	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)={\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)$$
203	202 200	eqeltrd	$$⊢\phi \to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
204		2fveq3	$$⊢b=B\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right)$$
205		oveq1	$$⊢b=B\to b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)=B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)$$
206	205	oveq2d	$$⊢b=B\to {\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)={\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)$$
207	204 206	oveq12d	$$⊢b=B\to \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
208	57 207	gsumsn	$$⊢\left(S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Mnd}\wedge B\in D\wedge \left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\right)\to \underset{b\in \left\{B\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
209	173 16 203 208	syl3anc	$$⊢\phi \to \underset{b\in \left\{B\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(B\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)$$
210	10	psrbagf	$$⊢B\in D\to B:I⟶{\mathbb{N}}_0$$
211	16 210	syl	$$⊢\phi \to B:I⟶{\mathbb{N}}_0$$
212	211	ffnd	$$⊢\phi \to BFnI$$
213	126	mptex	$$⊢\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\in \mathrm{V}$$
214	213 53	fnmpti	$$⊢\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)FnI$$
215	214	a1i	$$⊢\phi \to \left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)FnI$$
216		inidm	$$⊢I\cap I=I$$
217		eqidd	$$⊢\left(\phi \wedge v\in I\right)\to B\left(v\right)=B\left(v\right)$$
218		fveq2	$$⊢x=v\to a\left(x\right)=a\left(v\right)$$
219	218	mpteq2dv	$$⊢x=v\to \left(a\in \left(K^I\right)⟼a\left(x\right)\right)=\left(a\in \left(K^I\right)⟼a\left(v\right)\right)$$
220		simpr	$$⊢\left(\phi \wedge v\in I\right)\to v\in I$$
221	126	mptex	$$⊢\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in \mathrm{V}$$
222	221	a1i	$$⊢\left(\phi \wedge v\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in \mathrm{V}$$
223	53 219 220 222	fvmptd3	$$⊢\left(\phi \wedge v\in I\right)\to \left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\left(v\right)=\left(a\in \left(K^I\right)⟼a\left(v\right)\right)$$
224	212 215 12 12 216 217 223	offval	$$⊢\phi \to B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)=\left(v\in I⟼B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\right)$$
225	13	adantr	$$⊢\left(\phi \wedge v\in I\right)\to S\in \mathrm{CRing}$$
226		ovexd	$$⊢\left(\phi \wedge v\in I\right)\to K^I\in \mathrm{V}$$
227	48	ringmgp	$$⊢S{\uparrow }_{𝑠}\left(K^I\right)\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{Mnd}$$
228	62 227	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{Mnd}$$
229	228	adantr	$$⊢\left(\phi \wedge v\in I\right)\to {\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{Mnd}$$
230	211	ffvelrnda	$$⊢\left(\phi \wedge v\in I\right)\to B\left(v\right)\in {\mathbb{N}}_0$$
231	99	adantl	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge a\in \left(K^I\right)\right)\to a:I⟶K$$
232		simplr	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge a\in \left(K^I\right)\right)\to v\in I$$
233	231 232	ffvelrnd	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge a\in \left(K^I\right)\right)\to a\left(v\right)\in K$$
234	233	fmpttd	$$⊢\left(\phi \wedge v\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(v\right)\right):K^I⟶K$$
235	47 5 57 225 226 234	pwselbasr	$$⊢\left(\phi \wedge v\in I\right)\to \left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
236	90 49	mulgnn0cl	$$⊢\left({\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{Mnd}\wedge B\left(v\right)\in {\mathbb{N}}_0\wedge \left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\right)\to B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
237	229 230 235 236	syl3anc	$$⊢\left(\phi \wedge v\in I\right)\to B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
238	47 5 57 225 226 237	pwselbas	$$⊢\left(\phi \wedge v\in I\right)\to \left(B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\right):K^I⟶K$$
239	238	ffnd	$$⊢\left(\phi \wedge v\in I\right)\to \left(B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\right)Fn\left(K^I\right)$$
240		ovex	$$⊢B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\in \mathrm{V}$$
241		eqid	$$⊢\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)=\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)$$
242	240 241	fnmpti	$$⊢\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)Fn\left(K^I\right)$$
243	242	a1i	$$⊢\left(\phi \wedge v\in I\right)\to \left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)Fn\left(K^I\right)$$
244		eqid	$$⊢\left(a\in \left(K^I\right)⟼a\left(v\right)\right)=\left(a\in \left(K^I\right)⟼a\left(v\right)\right)$$
245		fveq1	$$⊢a=l\to a\left(v\right)=l\left(v\right)$$
246		simpr	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to l\in \left(K^I\right)$$
247		fvexd	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to l\left(v\right)\in \mathrm{V}$$
248	244 245 246 247	fvmptd3	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to \left(a\in \left(K^I\right)⟼a\left(v\right)\right)\left(l\right)=l\left(v\right)$$
249	248	oveq2d	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\left(l\right)=B\left(v\right)\underset{\dot{}}{\times }l\left(v\right)$$
250	59	ad2antrr	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to S\in \mathrm{Ring}$$
251		ovexd	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to K^I\in \mathrm{V}$$
252	230	adantr	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to B\left(v\right)\in {\mathbb{N}}_0$$
253	235	adantr	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to \left(a\in \left(K^I\right)⟼a\left(v\right)\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
254	47 57 48 6 49 7 250 251 252 253 246	pwsexpg	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to \left(B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\right)\left(l\right)=B\left(v\right)\underset{\dot{}}{\times }\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\left(l\right)$$
255		fveq1	$$⊢g=l\to g\left(v\right)=l\left(v\right)$$
256	255	oveq2d	$$⊢g=l\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)=B\left(v\right)\underset{\dot{}}{\times }l\left(v\right)$$
257		ovexd	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }l\left(v\right)\in \mathrm{V}$$
258	241 256 246 257	fvmptd3	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to \left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\left(l\right)=B\left(v\right)\underset{\dot{}}{\times }l\left(v\right)$$
259	249 254 258	3eqtr4d	$$⊢\left(\left(\phi \wedge v\in I\right)\wedge l\in \left(K^I\right)\right)\to \left(B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\right)\left(l\right)=\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\left(l\right)$$
260	239 243 259	eqfnfvd	$$⊢\left(\phi \wedge v\in I\right)\to B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)=\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)$$
261	260	mpteq2dva	$$⊢\phi \to \left(v\in I⟼B\left(v\right){\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(a\in \left(K^I\right)⟼a\left(v\right)\right)\right)=\left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
262	224 261	eqtrd	$$⊢\phi \to B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)=\left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
263	262	oveq2d	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)=\underset{v\in I}{{\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)$$
264	6	crngmgp	$$⊢S\in \mathrm{CRing}\to M\in \mathrm{CMnd}$$
265	13 264	syl	$$⊢\phi \to M\in \mathrm{CMnd}$$
266	265	cmnmndd	$$⊢\phi \to M\in \mathrm{Mnd}$$
267	266	adantr	$$⊢\left(\phi \wedge \left(g\in \left(K^I\right)\wedge v\in I\right)\right)\to M\in \mathrm{Mnd}$$
268	230	adantrl	$$⊢\left(\phi \wedge \left(g\in \left(K^I\right)\wedge v\in I\right)\right)\to B\left(v\right)\in {\mathbb{N}}_0$$
269		elmapi	$$⊢g\in \left(K^I\right)\to g:I⟶K$$
270	269	ad2antrl	$$⊢\left(\phi \wedge \left(g\in \left(K^I\right)\wedge v\in I\right)\right)\to g:I⟶K$$
271		simprr	$$⊢\left(\phi \wedge \left(g\in \left(K^I\right)\wedge v\in I\right)\right)\to v\in I$$
272	270 271	ffvelrnd	$$⊢\left(\phi \wedge \left(g\in \left(K^I\right)\wedge v\in I\right)\right)\to g\left(v\right)\in K$$
273	6 5	mgpbas	$$⊢K={\mathrm{Base}}_M$$
274	273 7	mulgnn0cl	$$⊢\left(M\in \mathrm{Mnd}\wedge B\left(v\right)\in {\mathbb{N}}_0\wedge g\left(v\right)\in K\right)\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\in K$$
275	267 268 272 274	syl3anc	$$⊢\left(\phi \wedge \left(g\in \left(K^I\right)\wedge v\in I\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\in K$$
276	12	mptexd	$$⊢\phi \to \left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)\in \mathrm{V}$$
277		fvexd	$$⊢\phi \to 1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{V}$$
278		funmpt	$$⊢\mathrm{Fun}\left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
279	278	a1i	$$⊢\phi \to \mathrm{Fun}\left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
280	10	psrbagfsupp	$$⊢B\in D\to {finSupp}_0\left(B\right)$$
281	16 280	syl	$$⊢\phi \to {finSupp}_0\left(B\right)$$
282	281	fsuppimpd	$$⊢\phi \to B\mathrm{supp}0\in \mathrm{Fin}$$
283		ssidd	$$⊢\phi \to B\mathrm{supp}0\subseteq B\mathrm{supp}0$$
284		c0ex	$$⊢0\in \mathrm{V}$$
285	284	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
286	211 283 12 285	suppssr	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to B\left(v\right)=0$$
287	286	oveq1d	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)=0\underset{\dot{}}{\times }g\left(v\right)$$
288	287	adantr	$$⊢\left(\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\wedge g\in \left(K^I\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)=0\underset{\dot{}}{\times }g\left(v\right)$$
289	269	adantl	$$⊢\left(\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\wedge g\in \left(K^I\right)\right)\to g:I⟶K$$
290		eldifi	$$⊢v\in \left(I\setminus {supp}_0\left(B\right)\right)\to v\in I$$
291	290	ad2antlr	$$⊢\left(\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\wedge g\in \left(K^I\right)\right)\to v\in I$$
292	289 291	ffvelrnd	$$⊢\left(\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\wedge g\in \left(K^I\right)\right)\to g\left(v\right)\in K$$
293	6 75	ringidval	$$⊢1_S=0_M$$
294	273 293 7	mulg0	$$⊢g\left(v\right)\in K\to 0\underset{\dot{}}{\times }g\left(v\right)=1_S$$
295	292 294	syl	$$⊢\left(\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\wedge g\in \left(K^I\right)\right)\to 0\underset{\dot{}}{\times }g\left(v\right)=1_S$$
296	288 295	eqtrd	$$⊢\left(\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\wedge g\in \left(K^I\right)\right)\to B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)=1_S$$
297	296	mpteq2dva	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to \left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)=\left(g\in \left(K^I\right)⟼1_S\right)$$
298		fconstmpt	$$⊢\left(K^I\right)\times \left\{1_S\right\}=\left(g\in \left(K^I\right)⟼1_S\right)$$
299		ovexd	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to K^I\in \mathrm{V}$$
300	59 299 187	syl2an2r	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to \left(K^I\right)\times \left\{1_S\right\}=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
301	298 300	eqtr3id	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to \left(g\in \left(K^I\right)⟼1_S\right)=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
302	297 301	eqtrd	$$⊢\left(\phi \wedge v\in \left(I\setminus {supp}_0\left(B\right)\right)\right)\to \left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)=1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
303	302 12	suppss2	$$⊢\phi \to \left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)\mathrm{supp}{1}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\subseteq B\mathrm{supp}0$$
304	282 303	ssfid	$$⊢\phi \to \left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)\mathrm{supp}{1}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\in \mathrm{Fin}$$
305	276 277 279 304	isfsuppd	$$⊢\phi \to {finSupp}_{1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}\left(\left(v\in I⟼\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)\right)$$
306	47 5 191 48 6 60 12 13 275 305	pwsgprod	$$⊢\phi \to \underset{v\in I}{{\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}\left(g\in \left(K^I\right)⟼B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)=\left(g\in \left(K^I\right)⟼\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
307	201 263 306	3eqtrd	$$⊢\phi \to 1_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}{\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(B{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)=\left(g\in \left(K^I\right)⟼\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
308	209 190 307	3eqtrd	$$⊢\phi \to \underset{b\in \left\{B\right\}}{{\sum }_{S{\uparrow }_{𝑠}\left(K^I\right)}}\left(\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)\left(F\left(b\right)\right){\cdot }_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}\left({\sum }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}},\left(b{{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}}_f\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)\right)\right)\right)=\left(g\in \left(K^I\right)⟼\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
309	56 171 308	3eqtrd	$$⊢\phi \to Q\left(F\right)=\left(g\in \left(K^I\right)⟼\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }g\left(v\right)\right)\right)$$
310		ovexd	$$⊢\phi \to \underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\in \mathrm{V}$$
311	41 309 15 310	fvmptd4	$$⊢\phi \to Q\left(F\right)\left(A\right)=\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)$$
312	37 311	jca	$$⊢\phi \to \left(F\in W\wedge Q\left(F\right)\left(A\right)=\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)$$