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