Theorem evlslem3

Description: Lemma for evlseu . Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015) (Revised by AV, 11-Apr-2024)

	Ref	Expression
Hypotheses	evlslem3.p	$$⊢P=I\mathrm{mPoly}R$$
	evlslem3.b	$$⊢B={\mathrm{Base}}_P$$
	evlslem3.c	$$⊢C={\mathrm{Base}}_S$$
	evlslem3.k	$$⊢K={\mathrm{Base}}_R$$
	evlslem3.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlslem3.t	$$⊢T={\mathrm{mulGrp}}_S$$
	evlslem3.x	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
	evlslem3.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evlslem3.v	$$⊢V=I\mathrm{mVar}R$$
	evlslem3.e	$$⊢E=\left(p\in B⟼\underset{b\in D}{{\sum }_S}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)$$
	evlslem3.i	$$⊢\phi \to I\in W$$
	evlslem3.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlslem3.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlslem3.f	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$
	evlslem3.g	$$⊢\phi \to G:I⟶C$$
	evlslem3.z	$$⊢\underset{\dot{}}{0}=0_R$$
	evlslem3.a	$$⊢\phi \to A\in D$$
	evlslem3.q	$$⊢\phi \to H\in K$$
Assertion	evlslem3	$$⊢\phi \to E\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\right)=F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlslem3.p	$$⊢P=I\mathrm{mPoly}R$$
2		evlslem3.b	$$⊢B={\mathrm{Base}}_P$$
3		evlslem3.c	$$⊢C={\mathrm{Base}}_S$$
4		evlslem3.k	$$⊢K={\mathrm{Base}}_R$$
5		evlslem3.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		evlslem3.t	$$⊢T={\mathrm{mulGrp}}_S$$
7		evlslem3.x	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
8		evlslem3.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
9		evlslem3.v	$$⊢V=I\mathrm{mVar}R$$
10		evlslem3.e	$$⊢E=\left(p\in B⟼\underset{b\in D}{{\sum }_S}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)$$
11		evlslem3.i	$$⊢\phi \to I\in W$$
12		evlslem3.r	$$⊢\phi \to R\in \mathrm{CRing}$$
13		evlslem3.s	$$⊢\phi \to S\in \mathrm{CRing}$$
14		evlslem3.f	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$
15		evlslem3.g	$$⊢\phi \to G:I⟶C$$
16		evlslem3.z	$$⊢\underset{\dot{}}{0}=0_R$$
17		evlslem3.a	$$⊢\phi \to A\in D$$
18		evlslem3.q	$$⊢\phi \to H\in K$$
19		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
20	12 19	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
21	1 5 16 4 11 20 2 18 17	mplmon2cl	$$⊢\phi \to \left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\in B$$
22		fveq1	$$⊢p=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\to p\left(b\right)=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)$$
23	22	fveq2d	$$⊢p=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\to F\left(p\left(b\right)\right)=F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)$$
24	23	oveq1d	$$⊢p=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\to F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
25	24	mpteq2dv	$$⊢p=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\to \left(b\in D⟼F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\left(b\in D⟼F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
26	25	oveq2d	$$⊢p=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\to \underset{b\in D}{{\sum }_S}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\underset{b\in D}{{\sum }_S}\left(F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
27		ovex	$$⊢\underset{b\in D}{{\sum }_S}\left(F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\in \mathrm{V}$$
28	26 10 27	fvmpt	$$⊢\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\in B\to E\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\right)=\underset{b\in D}{{\sum }_S}\left(F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
29	21 28	syl	$$⊢\phi \to E\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\right)=\underset{b\in D}{{\sum }_S}\left(F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
30		eqid	$$⊢\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)=\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)$$
31		eqeq1	$$⊢x=b\to \left(x=A\leftrightarrow b=A\right)$$
32	31	ifbid	$$⊢x=b\to if\left(x=A,H,\underset{\dot{}}{0}\right)=if\left(b=A,H,\underset{\dot{}}{0}\right)$$
33		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
34	16	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
35	34	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
36	18 35	ifexd	$$⊢\phi \to if\left(b=A,H,\underset{\dot{}}{0}\right)\in \mathrm{V}$$
37	36	adantr	$$⊢\left(\phi \wedge b\in D\right)\to if\left(b=A,H,\underset{\dot{}}{0}\right)\in \mathrm{V}$$
38	30 32 33 37	fvmptd3	$$⊢\left(\phi \wedge b\in D\right)\to \left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)=if\left(b=A,H,\underset{\dot{}}{0}\right)$$
39	38	fveq2d	$$⊢\left(\phi \wedge b\in D\right)\to F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)=F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)$$
40	39	oveq1d	$$⊢\left(\phi \wedge b\in D\right)\to F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
41	40	mpteq2dva	$$⊢\phi \to \left(b\in D⟼F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
42	41	oveq2d	$$⊢\phi \to \underset{b\in D}{{\sum }_S}\left(F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\underset{b\in D}{{\sum }_S}\left(F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
43		eqid	$$⊢0_S=0_S$$
44		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
45	13 44	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
46		ringmnd	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Mnd}$$
47	45 46	syl	$$⊢\phi \to S\in \mathrm{Mnd}$$
48		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
49	5 48	rabex2	$$⊢D\in \mathrm{V}$$
50	49	a1i	$$⊢\phi \to D\in \mathrm{V}$$
51	45	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{Ring}$$
52	4 3	rhmf	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F:K⟶C$$
53	14 52	syl	$$⊢\phi \to F:K⟶C$$
54	4 16	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
55	20 54	syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
56	18 55	ifcld	$$⊢\phi \to if\left(b=A,H,\underset{\dot{}}{0}\right)\in K$$
57	53 56	ffvelcdmd	$$⊢\phi \to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\in C$$
58	57	adantr	$$⊢\left(\phi \wedge b\in D\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\in C$$
59	6 3	mgpbas	$$⊢C={\mathrm{Base}}_T$$
60		eqid	$$⊢0_T=0_T$$
61	6	crngmgp	$$⊢S\in \mathrm{CRing}\to T\in \mathrm{CMnd}$$
62	13 61	syl	$$⊢\phi \to T\in \mathrm{CMnd}$$
63	62	adantr	$$⊢\left(\phi \wedge b\in D\right)\to T\in \mathrm{CMnd}$$
64	11	adantr	$$⊢\left(\phi \wedge b\in D\right)\to I\in W$$
65		cmnmnd	$$⊢T\in \mathrm{CMnd}\to T\in \mathrm{Mnd}$$
66	62 65	syl	$$⊢\phi \to T\in \mathrm{Mnd}$$
67	66	ad2antrr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to T\in \mathrm{Mnd}$$
68		simprl	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to y\in {\mathbb{N}}_0$$
69		simprr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to z\in C$$
70	59 7 67 68 69	mulgnn0cld	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to y\underset{\dot{}}{\times }z\in C$$
71	5	psrbagf	$$⊢b\in D\to b:I⟶{\mathbb{N}}_0$$
72	71	adantl	$$⊢\left(\phi \wedge b\in D\right)\to b:I⟶{\mathbb{N}}_0$$
73	15	adantr	$$⊢\left(\phi \wedge b\in D\right)\to G:I⟶C$$
74		inidm	$$⊢I\cap I=I$$
75	70 72 73 64 64 74	off	$$⊢\left(\phi \wedge b\in D\right)\to \left(b{\underset{\dot{}}{\times }}_{f}G\right):I⟶C$$
76		ovex	$$⊢b{\underset{\dot{}}{\times }}_{f}G\in \mathrm{V}$$
77	76	a1i	$$⊢\left(\phi \wedge b\in D\right)\to b{\underset{\dot{}}{\times }}_{f}G\in \mathrm{V}$$
78	75	ffund	$$⊢\left(\phi \wedge b\in D\right)\to \mathrm{Fun}\left(b{\underset{\dot{}}{\times }}_{f}G\right)$$
79		fvexd	$$⊢\left(\phi \wedge b\in D\right)\to 0_T\in \mathrm{V}$$
80	5	psrbag	$$⊢I\in W\to \left(b\in D\leftrightarrow \left(b:I⟶{\mathbb{N}}_0\wedge b^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
81	11 80	syl	$$⊢\phi \to \left(b\in D\leftrightarrow \left(b:I⟶{\mathbb{N}}_0\wedge b^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
82	81	simplbda	$$⊢\left(\phi \wedge b\in D\right)\to b^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
83	72	ffnd	$$⊢\left(\phi \wedge b\in D\right)\to bFnI$$
84	83	adantr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to bFnI$$
85	15	ffnd	$$⊢\phi \to GFnI$$
86	85	ad2antrr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to GFnI$$
87	11	ad2antrr	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to I\in W$$
88		eldifi	$$⊢y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\to y\in I$$
89	88	adantl	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to y\in I$$
90		fnfvof	$$⊢\left(\left(bFnI\wedge GFnI\right)\wedge \left(I\in W\wedge y\in I\right)\right)\to \left(b{\underset{\dot{}}{\times }}_{f}G\right)\left(y\right)=b\left(y\right)\underset{\dot{}}{\times }G\left(y\right)$$
91	84 86 87 89 90	syl22anc	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to \left(b{\underset{\dot{}}{\times }}_{f}G\right)\left(y\right)=b\left(y\right)\underset{\dot{}}{\times }G\left(y\right)$$
92		ffvelcdm	$$⊢\left(b:I⟶{\mathbb{N}}_0\wedge y\in I\right)\to b\left(y\right)\in {\mathbb{N}}_0$$
93	72 88 92	syl2an	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to b\left(y\right)\in {\mathbb{N}}_0$$
94		elnn0	$$⊢b\left(y\right)\in {\mathbb{N}}_0\leftrightarrow \left(b\left(y\right)\in \mathbb{N}\vee b\left(y\right)=0\right)$$
95	93 94	sylib	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to \left(b\left(y\right)\in \mathbb{N}\vee b\left(y\right)=0\right)$$
96		eldifn	$$⊢y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\to \neg y\in b^{-1}\left[\mathbb{N}\right]$$
97	96	adantl	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to \neg y\in b^{-1}\left[\mathbb{N}\right]$$
98	83	ad2antrr	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\wedge b\left(y\right)\in \mathbb{N}\right)\to bFnI$$
99	88	ad2antlr	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\wedge b\left(y\right)\in \mathbb{N}\right)\to y\in I$$
100		simpr	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\wedge b\left(y\right)\in \mathbb{N}\right)\to b\left(y\right)\in \mathbb{N}$$
101	98 99 100	elpreimad	$$⊢\left(\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\wedge b\left(y\right)\in \mathbb{N}\right)\to y\in b^{-1}\left[\mathbb{N}\right]$$
102	97 101	mtand	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to \neg b\left(y\right)\in \mathbb{N}$$
103	95 102	orcnd	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to b\left(y\right)=0$$
104	103	oveq1d	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to b\left(y\right)\underset{\dot{}}{\times }G\left(y\right)=0\underset{\dot{}}{\times }G\left(y\right)$$
105		ffvelcdm	$$⊢\left(G:I⟶C\wedge y\in I\right)\to G\left(y\right)\in C$$
106	73 88 105	syl2an	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to G\left(y\right)\in C$$
107	59 60 7	mulg0	$$⊢G\left(y\right)\in C\to 0\underset{\dot{}}{\times }G\left(y\right)=0_T$$
108	106 107	syl	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to 0\underset{\dot{}}{\times }G\left(y\right)=0_T$$
109	91 104 108	3eqtrd	$$⊢\left(\left(\phi \wedge b\in D\right)\wedge y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\right)\to \left(b{\underset{\dot{}}{\times }}_{f}G\right)\left(y\right)=0_T$$
110	75 109	suppss	$$⊢\left(\phi \wedge b\in D\right)\to \left(b{\underset{\dot{}}{\times }}_{f}G\right)\mathrm{supp}{0}_T\subseteq b^{-1}\left[\mathbb{N}\right]$$
111		suppssfifsupp	$$⊢\left(\left(b{\underset{\dot{}}{\times }}_{f}G\in \mathrm{V}\wedge \mathrm{Fun}\left(b{\underset{\dot{}}{\times }}_{f}G\right)\wedge 0_T\in \mathrm{V}\right)\wedge \left(b^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \left(b{\underset{\dot{}}{\times }}_{f}G\right)\mathrm{supp}{0}_T\subseteq b^{-1}\left[\mathbb{N}\right]\right)\right)\to {finSupp}_{0_T}\left(\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
112	77 78 79 82 110 111	syl32anc	$$⊢\left(\phi \wedge b\in D\right)\to {finSupp}_{0_T}\left(\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
113	59 60 63 64 75 112	gsumcl	$$⊢\left(\phi \wedge b\in D\right)\to {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C$$
114	3 8	ringcl	$$⊢\left(S\in \mathrm{Ring}\wedge F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\in C\wedge {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\in C$$
115	51 58 113 114	syl3anc	$$⊢\left(\phi \wedge b\in D\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\in C$$
116	115	fmpttd	$$⊢\phi \to \left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right):D⟶C$$
117		eldifsnneq	$$⊢b\in \left(D\setminus \left\{A\right\}\right)\to \neg b=A$$
118	117	iffalsed	$$⊢b\in \left(D\setminus \left\{A\right\}\right)\to if\left(b=A,H,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
119	118	adantl	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to if\left(b=A,H,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
120	119	fveq2d	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)=F\left(\underset{\dot{}}{0}\right)$$
121		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
122	14 121	syl	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}S\right)$$
123	16 43	ghmid	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=0_S$$
124	122 123	syl	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=0_S$$
125	124	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to F\left(\underset{\dot{}}{0}\right)=0_S$$
126	120 125	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)=0_S$$
127	126	oveq1d	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=0_S\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
128	45	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to S\in \mathrm{Ring}$$
129		eldifi	$$⊢b\in \left(D\setminus \left\{A\right\}\right)\to b\in D$$
130	129 113	sylan2	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C$$
131	3 8 43	ringlz	$$⊢\left(S\in \mathrm{Ring}\wedge {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C\right)\to 0_S\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=0_S$$
132	128 130 131	syl2anc	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to 0_S\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=0_S$$
133	127 132	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=0_S$$
134	133 50	suppss2	$$⊢\phi \to \left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\mathrm{supp}{0}_S\subseteq \left\{A\right\}$$
135	3 43 47 50 17 116 134	gsumpt	$$⊢\phi \to \underset{b\in D}{{\sum }_S}\left(F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\left(A\right)$$
136	42 135	eqtrd	$$⊢\phi \to \underset{b\in D}{{\sum }_S}\left(F\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\left(A\right)$$
137		iftrue	$$⊢b=A\to if\left(b=A,H,\underset{\dot{}}{0}\right)=H$$
138	137	fveq2d	$$⊢b=A\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)=F\left(H\right)$$
139		oveq1	$$⊢b=A\to b{\underset{\dot{}}{\times }}_{f}G=A{\underset{\dot{}}{\times }}_{f}G$$
140	139	oveq2d	$$⊢b=A\to {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)={\sum }_T\left(A{\underset{\dot{}}{\times }}_{f}G\right)$$
141	138 140	oveq12d	$$⊢b=A\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
142		eqid	$$⊢\left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
143		ovex	$$⊢F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)\in \mathrm{V}$$
144	141 142 143	fvmpt	$$⊢A\in D\to \left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\left(A\right)=F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
145	17 144	syl	$$⊢\phi \to \left(b\in D⟼F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\left(A\right)=F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
146	29 136 145	3eqtrd	$$⊢\phi \to E\left(\left(x\in D⟼if\left(x=A,H,\underset{\dot{}}{0}\right)\right)\right)=F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)$$