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	10	adantr	$⊢ (φ \land b \in D) \to I \in W$
33	4 26 6 29 30 31 32	psrbagev2	$⊢ (φ \land b \in D) \to \sum_{T} (b {\underset{˙}{\times}}_{f} G) \in C$
34	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$
35	18 25 33 34	syl3anc	$⊢ (φ \land b \in D) \to F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) \in C$
36	35	fmpttd	$⊢ φ \to (b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C$
37		ovexd	$⊢ φ \to {ℕ_{0}}^{I} \in V$
38	4 37	rabexd	$⊢ φ \to D \in V$
39	38	mptexd	$⊢ φ \to (b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) \in V$
40		funmpt	$⊢ Fun (b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
41	40	a1i	$⊢ φ \to Fun (b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
42		fvexd	$⊢ φ \to 0_{S} \in V$
43		eqid	$⊢ 0_{R} = 0_{R}$
44	1 2 43 15 11	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (Y)$
45	44	fsuppimpd	$⊢ φ \to Y supp 0_{R} \in Fin$
46	23	feqmptd	$⊢ φ \to Y = (b \in D ⟼ Y (b))$
47	46	oveq1d	$⊢ φ \to Y supp 0_{R} = (b \in D ⟼ Y (b)) supp 0_{R}$
48		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}$
49	47 48	syl	$⊢ φ \to (b \in D ⟼ Y (b)) supp 0_{R} \subseteq Y supp 0_{R}$
50		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
51		eqid	$⊢ 0_{S} = 0_{S}$
52	43 51	ghmid	$⊢ F \in (R GrpHom S) \to F (0_{R}) = 0_{S}$
53	13 50 52	3syl	$⊢ φ \to F (0_{R}) = 0_{S}$
54		fvexd	$⊢ (φ \land b \in D) \to Y (b) \in V$
55		fvexd	$⊢ φ \to 0_{R} \in V$
56	49 53 54 55	suppssfv	$⊢ φ \to (b \in D ⟼ F (Y (b))) supp 0_{S} \subseteq Y supp 0_{R}$
57	3 7 51	ringlz	$⊢ (S \in Ring \land x \in C) \to 0_{S} \underset{˙}{\cdot} x = 0_{S}$
58	17 57	sylan	$⊢ (φ \land x \in C) \to 0_{S} \underset{˙}{\cdot} x = 0_{S}$
59		fvexd	$⊢ (φ \land b \in D) \to F (Y (b)) \in V$
60	56 58 59 33 42	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}$
61		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))))$
62	39 41 42 45 60 61	syl32anc	$⊢ φ \to {finSupp}_{0_{S}} ((b \in D ⟼ F (Y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
63	36 62	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