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	ffvelrnd	$$⊢\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	mulgnn0cl	$$⊢\left(T\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge z\in C\right)\to y\underset{\dot{}}{\times }z\in C$$
71	67 68 69 70	syl3anc	$$⊢\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$$
72	5	psrbagf	$$⊢b\in D\to b:I⟶{\mathbb{N}}_0$$
73	72	adantl	$$⊢\left(\phi \wedge b\in D\right)\to b:I⟶{\mathbb{N}}_0$$
74	15	adantr	$$⊢\left(\phi \wedge b\in D\right)\to G:I⟶C$$
75		inidm	$$⊢I\cap I=I$$
76	71 73 74 64 64 75	off	$$⊢\left(\phi \wedge b\in D\right)\to \left(b{\underset{\dot{}}{\times }}_{f}G\right):I⟶C$$
77		ovex	$$⊢b{\underset{\dot{}}{\times }}_{f}G\in \mathrm{V}$$
78	77	a1i	$$⊢\left(\phi \wedge b\in D\right)\to b{\underset{\dot{}}{\times }}_{f}G\in \mathrm{V}$$
79	76	ffund	$$⊢\left(\phi \wedge b\in D\right)\to \mathrm{Fun}\left(b{\underset{\dot{}}{\times }}_{f}G\right)$$
80		fvexd	$$⊢\left(\phi \wedge b\in D\right)\to 0_T\in \mathrm{V}$$
81	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)$$
82	11 81	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)$$
83	82	simplbda	$$⊢\left(\phi \wedge b\in D\right)\to b^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
84	73	ffnd	$$⊢\left(\phi \wedge b\in D\right)\to bFnI$$
85	84	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$$
86	15	ffnd	$$⊢\phi \to GFnI$$
87	86	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$$
88	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$$
89		eldifi	$$⊢y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\to y\in I$$
90	89	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$$
91		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)$$
92	85 87 88 90 91	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)$$
93		ffvelrn	$$⊢\left(b:I⟶{\mathbb{N}}_0\wedge y\in I\right)\to b\left(y\right)\in {\mathbb{N}}_0$$
94	73 89 93	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$$
95		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)$$
96	94 95	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)$$
97		eldifn	$$⊢y\in \left(I\setminus b^{-1}\left[\mathbb{N}\right]\right)\to \neg y\in b^{-1}\left[\mathbb{N}\right]$$
98	97	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]$$
99	84	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$$
100	89	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$$
101		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}$$
102	99 100 101	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]$$
103	98 102	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}$$
104	96 103	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$$
105	104	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)$$
106		ffvelrn	$$⊢\left(G:I⟶C\wedge y\in I\right)\to G\left(y\right)\in C$$
107	74 89 106	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$$
108	59 60 7	mulg0	$$⊢G\left(y\right)\in C\to 0\underset{\dot{}}{\times }G\left(y\right)=0_T$$
109	107 108	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$$
110	92 105 109	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$$
111	76 110	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]$$
112		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)$$
113	78 79 80 83 111 112	syl32anc	$$⊢\left(\phi \wedge b\in D\right)\to {finSupp}_{0_T}\left(\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
114	59 60 63 64 76 113	gsumcl	$$⊢\left(\phi \wedge b\in D\right)\to {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C$$
115	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$$
116	51 58 114 115	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$$
117	116	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$$
118		eldifsnneq	$$⊢b\in \left(D\setminus \left\{A\right\}\right)\to \neg b=A$$
119	118	iffalsed	$$⊢b\in \left(D\setminus \left\{A\right\}\right)\to if\left(b=A,H,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
120	119	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}$$
121	120	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)$$
122		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
123	14 122	syl	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}S\right)$$
124	16 43	ghmid	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=0_S$$
125	123 124	syl	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=0_S$$
126	125	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to F\left(\underset{\dot{}}{0}\right)=0_S$$
127	121 126	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$$
128	127	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)$$
129	45	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus \left\{A\right\}\right)\right)\to S\in \mathrm{Ring}$$
130		eldifi	$$⊢b\in \left(D\setminus \left\{A\right\}\right)\to b\in D$$
131	130 114	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$$
132	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$$
133	129 131 132	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$$
134	128 133	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$$
135	134 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\}$$
136	3 43 47 50 17 117 135	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)$$
137	42 136	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)$$
138		iftrue	$$⊢b=A\to if\left(b=A,H,\underset{\dot{}}{0}\right)=H$$
139	138	fveq2d	$$⊢b=A\to F\left(if\left(b=A,H,\underset{\dot{}}{0}\right)\right)=F\left(H\right)$$
140		oveq1	$$⊢b=A\to b{\underset{\dot{}}{\times }}_{f}G=A{\underset{\dot{}}{\times }}_{f}G$$
141	140	oveq2d	$$⊢b=A\to {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)={\sum }_T\left(A{\underset{\dot{}}{\times }}_{f}G\right)$$
142	139 141	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)$$
143		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)$$
144		ovex	$$⊢F\left(H\right)\underset{\dot{}}{·}\left({\sum }_T,\left(A{\underset{\dot{}}{\times }}_{f}G\right)\right)\in \mathrm{V}$$
145	142 143 144	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)$$
146	17 145	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)$$
147	29 137 146	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)$$