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 mPoly R$
	evlslem1.b	$⊢ B = {Base}_{P}$
	evlslem1.c	$⊢ C = {Base}_{S}$
	evlslem1.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	evlslem1.t	$⊢ T = {mulGrp}_{S}$
	evlslem1.x	$⊢ \underset{˙}{\times} = \cdot_{T}$
	evlslem1.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	evlslem1.v	$⊢ V = I mVar R$
	evlslem1.e	$⊢ E = (p \in B ⟼ \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
	evlslem1.i	$⊢ φ \to I \in W$
	evlslem1.r	$⊢ φ \to R \in CRing$
	evlslem1.s	$⊢ φ \to S \in CRing$
	evlslem1.f	$⊢ φ \to F \in (R RingHom S)$
	evlslem1.g	$⊢ φ \to G : I ⟶ C$
	evlslem6.y	$⊢ φ \to Y \in B$
Assertion	evlslem6	$⊢ φ \to ((b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C \land {finSupp}_{0_{S}} ((b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))))$

Proof

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

Metamath Proof Explorer

Theorem evlslem6

Proof