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