Theorem evlslem6

Description: Lemma for evlseu . Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 26-Jul-2019) (Revised by AV, 11-Apr-2024)

	Ref	Expression
Hypotheses	evlslem1.p	$$⊢P=I\mathrm{mPoly}R$$
	evlslem1.b	$$⊢B={\mathrm{Base}}_P$$
	evlslem1.c	$$⊢C={\mathrm{Base}}_S$$
	evlslem1.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlslem1.t	$$⊢T={\mathrm{mulGrp}}_S$$
	evlslem1.x	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
	evlslem1.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evlslem1.v	$$⊢V=I\mathrm{mVar}R$$
	evlslem1.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)$$
	evlslem1.i	$$⊢\phi \to I\in W$$
	evlslem1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlslem1.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlslem1.f	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$
	evlslem1.g	$$⊢\phi \to G:I⟶C$$
	evlslem6.y	$$⊢\phi \to Y\in B$$
Assertion	evlslem6	$$⊢\phi \to \left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right):D⟶C\wedge {finSupp}_{0_S}\left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlslem1.p	$$⊢P=I\mathrm{mPoly}R$$
2		evlslem1.b	$$⊢B={\mathrm{Base}}_P$$
3		evlslem1.c	$$⊢C={\mathrm{Base}}_S$$
4		evlslem1.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		evlslem1.t	$$⊢T={\mathrm{mulGrp}}_S$$
6		evlslem1.x	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
7		evlslem1.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
8		evlslem1.v	$$⊢V=I\mathrm{mVar}R$$
9		evlslem1.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)$$
10		evlslem1.i	$$⊢\phi \to I\in W$$
11		evlslem1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
12		evlslem1.s	$$⊢\phi \to S\in \mathrm{CRing}$$
13		evlslem1.f	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$
14		evlslem1.g	$$⊢\phi \to G:I⟶C$$
15		evlslem6.y	$$⊢\phi \to Y\in B$$
16		crngring	$$⊢S\in \mathrm{CRing}\to S\in \mathrm{Ring}$$
17	12 16	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
18	17	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{Ring}$$
19		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
20	19 3	rhmf	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F:{\mathrm{Base}}_R⟶C$$
21	13 20	syl	$$⊢\phi \to F:{\mathrm{Base}}_R⟶C$$
22	21	adantr	$$⊢\left(\phi \wedge b\in D\right)\to F:{\mathrm{Base}}_R⟶C$$
23	1 19 2 4 15	mplelf	$$⊢\phi \to Y:D⟶{\mathrm{Base}}_R$$
24	23	ffvelcdmda	$$⊢\left(\phi \wedge b\in D\right)\to Y\left(b\right)\in {\mathrm{Base}}_R$$
25	22 24	ffvelcdmd	$$⊢\left(\phi \wedge b\in D\right)\to F\left(Y\left(b\right)\right)\in C$$
26	5 3	mgpbas	$$⊢C={\mathrm{Base}}_T$$
27	5	crngmgp	$$⊢S\in \mathrm{CRing}\to T\in \mathrm{CMnd}$$
28	12 27	syl	$$⊢\phi \to T\in \mathrm{CMnd}$$
29	28	adantr	$$⊢\left(\phi \wedge b\in D\right)\to T\in \mathrm{CMnd}$$
30		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
31	14	adantr	$$⊢\left(\phi \wedge b\in D\right)\to G:I⟶C$$
32	4 26 6 29 30 31	psrbagev2	$$⊢\left(\phi \wedge b\in D\right)\to {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C$$
33	3 7	ringcl	$$⊢\left(S\in \mathrm{Ring}\wedge F\left(Y\left(b\right)\right)\in C\wedge {\sum }_T\left(b{\underset{\dot{}}{\times }}_{f}G\right)\in C\right)\to F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\in C$$
34	18 25 32 33	syl3anc	$$⊢\left(\phi \wedge b\in D\right)\to F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\in C$$
35	34	fmpttd	$$⊢\phi \to \left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right):D⟶C$$
36		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
37	4 36	rabexd	$$⊢\phi \to D\in \mathrm{V}$$
38	37	mptexd	$$⊢\phi \to \left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\in \mathrm{V}$$
39		funmpt	$$⊢\mathrm{Fun}\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
40	39	a1i	$$⊢\phi \to \mathrm{Fun}\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
41		fvexd	$$⊢\phi \to 0_S\in \mathrm{V}$$
42		eqid	$$⊢0_R=0_R$$
43	1 2 42 15	mplelsfi	$$⊢\phi \to {finSupp}_{0_R}\left(Y\right)$$
44	43	fsuppimpd	$$⊢\phi \to Y\mathrm{supp}{0}_R\in \mathrm{Fin}$$
45	23	feqmptd	$$⊢\phi \to Y=\left(b\in D⟼Y\left(b\right)\right)$$
46	45	oveq1d	$$⊢\phi \to Y\mathrm{supp}{0}_R=\left(b\in D⟼Y\left(b\right)\right)\mathrm{supp}{0}_R$$
47		eqimss2	$$⊢Y\mathrm{supp}{0}_R=\left(b\in D⟼Y\left(b\right)\right)\mathrm{supp}{0}_R\to \left(b\in D⟼Y\left(b\right)\right)\mathrm{supp}{0}_R\subseteq Y\mathrm{supp}{0}_R$$
48	46 47	syl	$$⊢\phi \to \left(b\in D⟼Y\left(b\right)\right)\mathrm{supp}{0}_R\subseteq Y\mathrm{supp}{0}_R$$
49		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
50		eqid	$$⊢0_S=0_S$$
51	42 50	ghmid	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\left(0_R\right)=0_S$$
52	13 49 51	3syl	$$⊢\phi \to F\left(0_R\right)=0_S$$
53		fvexd	$$⊢\left(\phi \wedge b\in D\right)\to Y\left(b\right)\in \mathrm{V}$$
54		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
55	48 52 53 54	suppssfv	$$⊢\phi \to \left(b\in D⟼F\left(Y\left(b\right)\right)\right)\mathrm{supp}{0}_S\subseteq Y\mathrm{supp}{0}_R$$
56	3 7 50	ringlz	$$⊢\left(S\in \mathrm{Ring}\wedge x\in C\right)\to 0_S\underset{\dot{}}{·}x=0_S$$
57	17 56	sylan	$$⊢\left(\phi \wedge x\in C\right)\to 0_S\underset{\dot{}}{·}x=0_S$$
58		fvexd	$$⊢\left(\phi \wedge b\in D\right)\to F\left(Y\left(b\right)\right)\in \mathrm{V}$$
59	55 57 58 32 41	suppssov1	$$⊢\phi \to \left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\mathrm{supp}{0}_S\subseteq Y\mathrm{supp}{0}_R$$
60		suppssfifsupp	$$⊢\left(\left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\wedge 0_S\in \mathrm{V}\right)\wedge \left(Y\mathrm{supp}{0}_R\in \mathrm{Fin}\wedge \left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\mathrm{supp}{0}_S\subseteq Y\mathrm{supp}{0}_R\right)\right)\to {finSupp}_{0_S}\left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)$$
61	38 40 41 44 59 60	syl32anc	$$⊢\phi \to {finSupp}_{0_S}\left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)$$
62	35 61	jca	$$⊢\phi \to \left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right):D⟶C\wedge {finSupp}_{0_S}\left(\left(b\in D⟼F\left(Y\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_T,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)\right)$$