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	7	adantr	$$⊢\left(\phi \wedge y\in B\right)\to R\in \mathrm{CRing}$$
42	1 2 4 40 41	mplelsfi	$$⊢\left(\phi \wedge y\in B\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(y\right)$$
43	42	fsuppimpd	$$⊢\left(\phi \wedge y\in B\right)\to y\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
44	1 20 2 5 40	mplelf	$$⊢\left(\phi \wedge y\in B\right)\to y:D⟶{\mathrm{Base}}_R$$
45		ssidd	$$⊢\left(\phi \wedge y\in B\right)\to y\mathrm{supp}\underset{\dot{}}{0}\subseteq y\mathrm{supp}\underset{\dot{}}{0}$$
46	14	a1i	$$⊢\left(\phi \wedge y\in B\right)\to D\in \mathrm{V}$$
47	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
48	47	a1i	$$⊢\left(\phi \wedge y\in B\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
49	44 45 46 48	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}$$
50	49	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)$$
51		ifid	$$⊢if\left(k=j,\underset{\dot{}}{0},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
52	50 51	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}$$
53	52	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)$$
54		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
55	17 54	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
56	1 5 4 12 6 55	mpl0	$$⊢\phi \to 0_P=D\times \left\{\underset{\dot{}}{0}\right\}$$
57		fconstmpt	$$⊢D\times \left\{\underset{\dot{}}{0}\right\}=\left(k\in D⟼\underset{\dot{}}{0}\right)$$
58	56 57	eqtrdi	$$⊢\phi \to 0_P=\left(k\in D⟼\underset{\dot{}}{0}\right)$$
59	58	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)$$
60	53 59	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$$
61	60 46	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}$$
62		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)$$
63	39 43 61 62	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)$$
64	63	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)$$
65		fveq1	$$⊢y=x\to y\left(j\right)=x\left(j\right)$$
66	65	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)$$
67	66	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)$$
68	67	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)$$
69	68	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)$$
70	69	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)$$
71	64 70	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)$$
72	71	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)$$
73	72	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)$$
74		equequ2	$$⊢i=j\to \left(k=i\leftrightarrow k=j\right)$$
75		fveq2	$$⊢i=j\to y\left(i\right)=y\left(j\right)$$
76	74 75	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)$$
77	76	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)$$
78	77	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)$$
79	63	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)$$
80	78 79	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)$$
81	2 11 12 15 15 19 27 34 73 80	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)$$
82	81	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)$$
83		ringcmn	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{CMnd}$$
84	18 83	syl	$$⊢\phi \to P\in \mathrm{CMnd}$$
85	84	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to P\in \mathrm{CMnd}$$
86		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
87	8 86	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
88	87	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to S\in \mathrm{Ring}$$
89		ringmnd	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Mnd}$$
90	88 89	syl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to S\in \mathrm{Mnd}$$
91	14 14	xpex	$$⊢D\times D\in \mathrm{V}$$
92	91	a1i	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to D\times D\in \mathrm{V}$$
93		ghmmhm	$$⊢E\in \left(P\mathrm{GrpHom}S\right)\to E\in \left(P\mathrm{MndHom}S\right)$$
94	9 93	syl	$$⊢\phi \to E\in \left(P\mathrm{MndHom}S\right)$$
95	94	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to E\in \left(P\mathrm{MndHom}S\right)$$
96	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}$$
97	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$$
98	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$$
99	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$$
100	96 97 98 99	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$$
101	100	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$$
102		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)$$
103	102	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$$
104	101 103	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$$
105	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}$$
106	102	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)$$
107	105 106 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)$$
108	107	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)$$
109	73	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}$$
110	80	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}$$
111		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}$$
112	109 110 111	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}$$
113	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)$$
114		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)$$
115	108 112 113 114	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)$$
116	2 12 85 90 92 95 104 115	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)$$
117	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$$
118	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}$$
119		eqid	$$⊢{\cdot }_R={\cdot }_R$$
120		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$$
121		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$$
122	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$$
123	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$$
124	1 5 4 20 117 118 11 119 120 121 122 123	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)$$
125	124	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)$$
126	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)$$
127	125 126	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)$$
128	127	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)$$
129	128	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)$$
130	129	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)$$
131		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)$$
132		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
133	2 132	ghmf	$$⊢E\in \left(P\mathrm{GrpHom}S\right)\to E:B⟶{\mathrm{Base}}_S$$
134	9 133	syl	$$⊢\phi \to E:B⟶{\mathrm{Base}}_S$$
135	134	feqmptd	$$⊢\phi \to E=\left(z\in B⟼E\left(z\right)\right)$$
136	135	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)$$
137		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)$$
138	100 131 136 137	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)$$
139	138	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)$$
140		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)$$
141		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)$$
142	27 140 136 141	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)$$
143	142	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)$$
144		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)$$
145		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)$$
146	34 144 136 145	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)$$
147	146	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)$$
148	143 147	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)$$
149		eqid	$$⊢0_S=0_S$$
150	134	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$$
151	150 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$$
152	134	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$$
153	152 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$$
154	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}$$
155		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)$$
156		fvex	$$⊢0_S\in \mathrm{V}$$
157	154 155 156	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)$$
158	157	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)$$
159		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$$
160	12 149	ghmid	$$⊢E\in \left(P\mathrm{GrpHom}S\right)\to E\left(0_P\right)=0_S$$
161	9 160	syl	$$⊢\phi \to E\left(0_P\right)=0_S$$
162	14	mptex	$$⊢\left(k\in D⟼if\left(k=j,x\left(j\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
163	162	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}$$
164	37	a1i	$$⊢\phi \to 0_P\in \mathrm{V}$$
165	159 161 163 164	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$$
166	165	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$$
167		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)$$
168	158 109 166 167	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)$$
169	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}$$
170		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)$$
171	169 170 156	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)$$
172	171	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)$$
173		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$$
174	14	mptex	$$⊢\left(k\in D⟼if\left(k=i,y\left(i\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
175	174	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}$$
176	173 161 175 164	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$$
177	176	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$$
178		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)$$
179	172 110 177 178	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)$$
180	132 3 149 15 15 88 151 153 168 179	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)$$
181	148 180	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)$$
182	130 139 181	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)$$
183	82 116 182	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)$$
184	6	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to I\in W$$
185	17	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to R\in \mathrm{Ring}$$
186	1 5 4 2 184 185 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)$$
187	1 5 4 2 184 185 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)$$
188	186 187	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)$$
189	188	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)$$
190	186	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)$$
191	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$$
192	2 12 85 90 15 95 191 73	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)$$
193	190 192	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)$$
194	187	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)$$
195	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$$
196	2 12 85 90 15 95 195 80	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)$$
197	194 196	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)$$
198	193 197	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)$$
199	183 189 198	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)$$