Theorem evlslem2

Description: A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 11-Apr-2024)

	Ref	Expression
Hypotheses	evlslem2.p	$$⊢P=I\mathrm{mPoly}R$$
	evlslem2.b	$$⊢B={\mathrm{Base}}_P$$
	evlslem2.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evlslem2.z	$$⊢\underset{\dot{}}{0}=0_R$$
	evlslem2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlslem2.i	$$⊢\phi \to I\in W$$
	evlslem2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlslem2.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlslem2.e1	$$⊢\phi \to E\in \left(P\mathrm{GrpHom}S\right)$$
	evlslem2.e2	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge y\in B\right)\wedge \left(j\in D\wedge i\in D\right)\right)\right)\to E\left(\left(k\in D⟼if\left(k=j{+}_{f}i,x\left(j\right){\cdot }_{R}y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
Assertion	evlslem2	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(x{\cdot }_{P}y\right)=E\left(x\right)\underset{\dot{}}{·}E\left(y\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlslem2.p	$$⊢P=I\mathrm{mPoly}R$$
2		evlslem2.b	$$⊢B={\mathrm{Base}}_P$$
3		evlslem2.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
4		evlslem2.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		evlslem2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		evlslem2.i	$$⊢\phi \to I\in W$$
7		evlslem2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
8		evlslem2.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evlslem2.e1	$$⊢\phi \to E\in \left(P\mathrm{GrpHom}S\right)$$
10		evlslem2.e2	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge y\in B\right)\wedge \left(j\in D\wedge i\in D\right)\right)\right)\to E\left(\left(k\in D⟼if\left(k=j{+}_{f}i,x\left(j\right){\cdot }_{R}y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
11		eqid	$$⊢{\cdot }_P={\cdot }_P$$
12		eqid	$$⊢0_P=0_P$$
13		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
14	5 13	rabex2	$$⊢D\in \mathrm{V}$$
15	14	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to D\in \mathrm{V}$$
16		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
17	7 16	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
18	1 6 17	mplringd	$$⊢\phi \to P\in \mathrm{Ring}$$
19	18	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to P\in \mathrm{Ring}$$
20		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
21	6	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to I\in W$$
22	17	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to R\in \mathrm{Ring}$$
23		simprl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\in B$$
24	1 20 2 5 23	mplelf	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x:D⟶{\mathrm{Base}}_R$$
25	24	ffvelcdmda	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to x\left(j\right)\in {\mathrm{Base}}_R$$
26		simpr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to j\in D$$
27	1 5 4 20 21 22 2 25 26	mplmon2cl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\in B$$
28	6	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to I\in W$$
29	17	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to R\in \mathrm{Ring}$$
30		simprr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to y\in B$$
31	1 20 2 5 30	mplelf	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to y:D⟶{\mathrm{Base}}_R$$
32	31	ffvelcdmda	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to y\left(i\right)\in {\mathrm{Base}}_R$$
33		simpr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to i\in D$$
34	1 5 4 20 28 29 2 32 33	mplmon2cl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to \left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B$$
35	14	mptex	$$⊢\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
36		funmpt	$$⊢\mathrm{Fun}\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
37		fvex	$$⊢0_P\in \mathrm{V}$$
38	35 36 37	3pm3.2i	$$⊢\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)$$
39	38	a1i	$$⊢\left(\phi \wedge y\in B\right)\to \left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)$$
40		simpr	$$⊢\left(\phi \wedge y\in B\right)\to y\in B$$
41	1 2 4 40	mplelsfi	$$⊢\left(\phi \wedge y\in B\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(y\right)$$
42	41	fsuppimpd	$$⊢\left(\phi \wedge y\in B\right)\to y\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
43	1 20 2 5 40	mplelf	$$⊢\left(\phi \wedge y\in B\right)\to y:D⟶{\mathrm{Base}}_R$$
44		ssidd	$$⊢\left(\phi \wedge y\in B\right)\to y\mathrm{supp}\underset{\dot{}}{0}\subseteq y\mathrm{supp}\underset{\dot{}}{0}$$
45	14	a1i	$$⊢\left(\phi \wedge y\in B\right)\to D\in \mathrm{V}$$
46	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
47	46	a1i	$$⊢\left(\phi \wedge y\in B\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
48	43 44 45 47	suppssr	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge j\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(y\right)\right)\right)\to y\left(j\right)=\underset{\dot{}}{0}$$
49	48	ifeq1d	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge j\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(y\right)\right)\right)\to if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)=if\left(k=j,\underset{\dot{}}{0},\underset{\dot{}}{0}\right)$$
50		ifid	$$⊢if\left(k=j,\underset{\dot{}}{0},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
51	49 50	eqtrdi	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge j\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(y\right)\right)\right)\to if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
52	51	mpteq2dv	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge j\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(y\right)\right)\right)\to \left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼\underset{\dot{}}{0}\right)$$
53		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
54	17 53	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
55	1 5 4 12 6 54	mpl0	$$⊢\phi \to 0_P=D\times \left\{\underset{\dot{}}{0}\right\}$$
56		fconstmpt	$$⊢D\times \left\{\underset{\dot{}}{0}\right\}=\left(k\in D⟼\underset{\dot{}}{0}\right)$$
57	55 56	eqtrdi	$$⊢\phi \to 0_P=\left(k\in D⟼\underset{\dot{}}{0}\right)$$
58	57	ad2antrr	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge j\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(y\right)\right)\right)\to 0_P=\left(k\in D⟼\underset{\dot{}}{0}\right)$$
59	52 58	eqtr4d	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge j\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(y\right)\right)\right)\to \left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)=0_P$$
60	59 45	suppss2	$$⊢\left(\phi \wedge y\in B\right)\to \left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq y\mathrm{supp}\underset{\dot{}}{0}$$
61		suppssfifsupp	$$⊢\left(\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)\wedge \left(y\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\wedge \left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq y\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to {finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
62	39 42 60 61	syl12anc	$$⊢\left(\phi \wedge y\in B\right)\to {finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
63	62	ralrimiva	$$⊢\phi \to \forall y\in B{finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
64		fveq1	$$⊢y=x\to y\left(j\right)=x\left(j\right)$$
65	64	ifeq1d	$$⊢y=x\to if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)=if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)$$
66	65	mpteq2dv	$$⊢y=x\to \left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)$$
67	66	mpteq2dv	$$⊢y=x\to \left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
68	67	breq1d	$$⊢y=x\to \left({finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow {finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
69	68	cbvralvw	$$⊢\forall y\in B{finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow \forall x\in B{finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
70	63 69	sylib	$$⊢\phi \to \forall x\in B{finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
71	70	r19.21bi	$$⊢\left(\phi \wedge x\in B\right)\to {finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
72	71	adantrr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
73		equequ2	$$⊢i=j\to \left(k=i\leftrightarrow k=j\right)$$
74		fveq2	$$⊢i=j\to y\left(i\right)=y\left(j\right)$$
75	73 74	ifbieq1d	$$⊢i=j\to if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)=if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)$$
76	75	mpteq2dv	$$⊢i=j\to \left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)$$
77	76	cbvmptv	$$⊢\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
78	62	adantrl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {finSupp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,y\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
79	77 78	eqbrtrid	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {finSupp}_{0_P}\left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
80	2 11 12 15 15 19 27 34 72 79	gsumdixp	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\underset{j\in D}{{\sum }_P},\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right){\cdot }_P\left(\underset{i\in D}{{\sum }_P},\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)={\sum }_P\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
81	80	fveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(\left(\underset{j\in D}{{\sum }_P},\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right){\cdot }_P\left(\underset{i\in D}{{\sum }_P},\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=E\left({\sum }_P\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
82		ringcmn	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{CMnd}$$
83	18 82	syl	$$⊢\phi \to P\in \mathrm{CMnd}$$
84	83	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to P\in \mathrm{CMnd}$$
85		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
86	8 85	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
87	86	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to S\in \mathrm{Ring}$$
88		ringmnd	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Mnd}$$
89	87 88	syl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to S\in \mathrm{Mnd}$$
90	14 14	xpex	$$⊢D\times D\in \mathrm{V}$$
91	90	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to D\times D\in \mathrm{V}$$
92		ghmmhm	$$⊢E\in \left(P\mathrm{GrpHom}S\right)\to E\in \left(P\mathrm{MndHom}S\right)$$
93	9 92	syl	$$⊢\phi \to E\in \left(P\mathrm{MndHom}S\right)$$
94	93	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\in \left(P\mathrm{MndHom}S\right)$$
95	18	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to P\in \mathrm{Ring}$$
96	27	adantrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\in B$$
97	34	adantrl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to \left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B$$
98	2 11	ringcl	$$⊢\left(P\in \mathrm{Ring}\wedge \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\in B\wedge \left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B\right)\to \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B$$
99	95 96 97 98	syl3anc	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B$$
100	99	ralrimivva	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \forall j\in D\forall i\in D\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B$$
101		eqid	$$⊢\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
102	101	fmpo	$$⊢\forall j\in D\forall i\in D\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in B\leftrightarrow \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right):D\times D⟶B$$
103	100 102	sylib	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right):D\times D⟶B$$
104	14 14	mpoex	$$⊢\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
105	101	mpofun	$$⊢\mathrm{Fun}\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
106	104 105 37	3pm3.2i	$$⊢\left(\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)$$
107	106	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)$$
108	72	fsuppimpd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\in \mathrm{Fin}$$
109	79	fsuppimpd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\in \mathrm{Fin}$$
110		xpfi	$$⊢\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\in \mathrm{Fin}\wedge \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\in \mathrm{Fin}\right)\to {supp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\times {supp}_{0_P}\left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{Fin}$$
111	108 109 110	syl2anc	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {supp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\times {supp}_{0_P}\left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{Fin}$$
112	2 12 11 19 27 34 15 15	evlslem4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq {supp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\times {supp}_{0_P}\left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
113		suppssfifsupp	$$⊢\left(\left(\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)\wedge \left({supp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\times {supp}_{0_P}\left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{Fin}\wedge \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq {supp}_{0_P}\left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\times {supp}_{0_P}\left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)\right)\to {finSupp}_{0_P}\left(\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
114	107 111 112 113	syl12anc	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {finSupp}_{0_P}\left(\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
115	2 12 84 89 91 94 103 114	gsummhm	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=E\left({\sum }_P\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
116	6	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to I\in W$$
117	7	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to R\in \mathrm{CRing}$$
118		eqid	$$⊢{\cdot }_R={\cdot }_R$$
119		simprl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to j\in D$$
120		simprr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to i\in D$$
121	25	adantrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to x\left(j\right)\in {\mathrm{Base}}_R$$
122	32	adantrl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to y\left(i\right)\in {\mathrm{Base}}_R$$
123	1 5 4 20 116 117 11 118 119 120 121 122	mplmon2mul	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼if\left(k=j{+}_{f}i,x\left(j\right){\cdot }_{R}y\left(i\right),\underset{\dot{}}{0}\right)\right)$$
124	123	fveq2d	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=E\left(\left(k\in D⟼if\left(k=j{+}_{f}i,x\left(j\right){\cdot }_{R}y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
125	10	anassrs	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to E\left(\left(k\in D⟼if\left(k=j{+}_{f}i,x\left(j\right){\cdot }_{R}y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
126	124 125	eqtrd	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge \left(j\in D\wedge i\in D\right)\right)\to E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
127	126	3impb	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\wedge i\in D\right)\to E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
128	127	mpoeq3dva	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
129	128	oveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)={\sum }_S\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
130		eqidd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
131		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
132	2 131	ghmf	$$⊢E\in \left(P\mathrm{GrpHom}S\right)\to E:B⟶{\mathrm{Base}}_S$$
133	9 132	syl	$$⊢\phi \to E:B⟶{\mathrm{Base}}_S$$
134	133	feqmptd	$$⊢\phi \to E=\left(z\in B⟼E\left(z\right)\right)$$
135	134	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E=\left(z\in B⟼E\left(z\right)\right)$$
136		fveq2	$$⊢z=\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\to E\left(z\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
137	99 130 135 136	fmpoco	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\circ \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
138	137	oveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)={\sum }_S\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
139		eqidd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
140		fveq2	$$⊢z=\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\to E\left(z\right)=E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
141	27 139 135 140	fmptco	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)=\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
142	141	oveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)=\underset{j\in D}{{\sum }_S}E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
143		eqidd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
144		fveq2	$$⊢z=\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\to E\left(z\right)=E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
145	34 143 135 144	fmptco	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)=\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
146	145	oveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=\underset{i\in D}{{\sum }_S}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
147	142 146	oveq12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left({\sum }_S,\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)\underset{\dot{}}{·}\left({\sum }_S,\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)=\left(\underset{j\in D}{{\sum }_S},E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\underset{\dot{}}{·}\left(\underset{i\in D}{{\sum }_S},E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
148		eqid	$$⊢0_S=0_S$$
149	133	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to E:B⟶{\mathrm{Base}}_S$$
150	149 27	ffvelcdmd	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge j\in D\right)\to E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\in {\mathrm{Base}}_S$$
151	133	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to E:B⟶{\mathrm{Base}}_S$$
152	151 34	ffvelcdmd	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge i\in D\right)\to E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\in {\mathrm{Base}}_S$$
153	14	mptex	$$⊢\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}$$
154		funmpt	$$⊢\mathrm{Fun}\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
155		fvex	$$⊢0_S\in \mathrm{V}$$
156	153 154 155	3pm3.2i	$$⊢\left(\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)$$
157	156	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)$$
158		ssidd	$$⊢\phi \to \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P$$
159	12 148	ghmid	$$⊢E\in \left(P\mathrm{GrpHom}S\right)\to E\left(0_P\right)=0_S$$
160	9 159	syl	$$⊢\phi \to E\left(0_P\right)=0_S$$
161	14	mptex	$$⊢\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
162	161	a1i	$$⊢\left(\phi \wedge j\in D\right)\to \left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
163	37	a1i	$$⊢\phi \to 0_P\in \mathrm{V}$$
164	158 160 162 163	suppssfv	$$⊢\phi \to \left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P$$
165	164	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P$$
166		suppssfifsupp	$$⊢\left(\left(\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)\wedge \left(\left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\in \mathrm{Fin}\wedge \left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\right)\right)\to {finSupp}_{0_S}\left(\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
167	157 108 165 166	syl12anc	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {finSupp}_{0_S}\left(\left(j\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
168	14	mptex	$$⊢\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}$$
169		funmpt	$$⊢\mathrm{Fun}\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
170	168 169 155	3pm3.2i	$$⊢\left(\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)$$
171	170	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)$$
172		ssidd	$$⊢\phi \to \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P$$
173	14	mptex	$$⊢\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
174	173	a1i	$$⊢\left(\phi \wedge i\in D\right)\to \left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
175	172 160 174 163	suppssfv	$$⊢\phi \to \left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P$$
176	175	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P$$
177		suppssfifsupp	$$⊢\left(\left(\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)\wedge \left(\left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\in \mathrm{Fin}\wedge \left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\right)\right)\to {finSupp}_{0_S}\left(\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
178	171 109 176 177	syl12anc	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {finSupp}_{0_S}\left(\left(i\in D⟼E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
179	131 3 148 15 15 87 150 152 167 178	gsumdixp	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\underset{j\in D}{{\sum }_S},E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\underset{\dot{}}{·}\left(\underset{i\in D}{{\sum }_S},E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)={\sum }_S\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
180	147 179	eqtrd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left({\sum }_S,\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)\underset{\dot{}}{·}\left({\sum }_S,\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)={\sum }_S\left(j\in D,i\in D⟼E\left(\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{·}E\left(\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
181	129 138 180	3eqtr4d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(j\in D,i\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right){\cdot }_P\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=\left({\sum }_S,\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)\underset{\dot{}}{·}\left({\sum }_S,\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
182	81 115 181	3eqtr2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(\left(\underset{j\in D}{{\sum }_P},\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right){\cdot }_P\left(\underset{i\in D}{{\sum }_P},\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=\left({\sum }_S,\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)\underset{\dot{}}{·}\left({\sum }_S,\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
183	6	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to I\in W$$
184	17	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to R\in \mathrm{Ring}$$
185	1 5 4 2 183 184 23	mplcoe4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x=\underset{j\in D}{{\sum }_P}\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)$$
186	1 5 4 2 183 184 30	mplcoe4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to y=\underset{i\in D}{{\sum }_P}\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)$$
187	185 186	oveq12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{P}y=\left(\underset{j\in D}{{\sum }_P},\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right){\cdot }_P\left(\underset{i\in D}{{\sum }_P},\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
188	187	fveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(x{\cdot }_{P}y\right)=E\left(\left(\underset{j\in D}{{\sum }_P},\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right){\cdot }_P\left(\underset{i\in D}{{\sum }_P},\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
189	185	fveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(x\right)=E\left(\underset{j\in D}{{\sum }_P}\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
190	27	fmpttd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right):D⟶B$$
191	2 12 84 89 15 94 190 72	gsummhm	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)=E\left(\underset{j\in D}{{\sum }_P}\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)$$
192	189 191	eqtr4d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(x\right)={\sum }_S\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
193	186	fveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(y\right)=E\left(\underset{i\in D}{{\sum }_P}\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
194	34	fmpttd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right):D⟶B$$
195	2 12 84 89 15 94 194 79	gsummhm	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\sum }_S\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)=E\left(\underset{i\in D}{{\sum }_P}\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)$$
196	193 195	eqtr4d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(y\right)={\sum }_S\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
197	192 196	oveq12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(x\right)\underset{\dot{}}{·}E\left(y\right)=\left({\sum }_S,\left(E\circ \left(j\in D⟼\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)\underset{\dot{}}{·}\left({\sum }_S,\left(E\circ \left(i\in D⟼\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
198	182 188 197	3eqtr4d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\left(x{\cdot }_{P}y\right)=E\left(x\right)\underset{\dot{}}{·}E\left(y\right)$$