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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	evlslem1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlslem1.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	evlslem1.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	evlslem1.t	⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
	evlslem1.x	⊢ ↑ = ( .g ‘ 𝑇 )
	evlslem1.m	⊢ · = ( .r ‘ 𝑆 )
	evlslem1.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	evlslem1.e	⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
	evlslem1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	evlslem1.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evlslem1.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlslem1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
	evlslem1.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
	evlslem6.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	evlslem6	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 ∧ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlslem1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		evlslem1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		evlslem1.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
4		evlslem1.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
5		evlslem1.t	⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
6		evlslem1.x	⊢ ↑ = ( .g ‘ 𝑇 )
7		evlslem1.m	⊢ · = ( .r ‘ 𝑆 )
8		evlslem1.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
9		evlslem1.e	⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
10		evlslem1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
11		evlslem1.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
12		evlslem1.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
13		evlslem1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
14		evlslem1.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
15		evlslem6.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
16		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
17	12 16	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring )
19		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20	19 3	rhmf	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
21	13 20	syl	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
23	1 19 2 4 15	mplelf	⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
24	23	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑌 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
25	22 24	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ∈ 𝐶 )
26	5 3	mgpbas	⊢ 𝐶 = ( Base ‘ 𝑇 )
27	5	crngmgp	⊢ ( 𝑆 ∈ CRing → 𝑇 ∈ CMnd )
28	12 27	syl	⊢ ( 𝜑 → 𝑇 ∈ CMnd )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑇 ∈ CMnd )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
31	14	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐺 : 𝐼 ⟶ 𝐶 )
32	4 26 6 29 30 31	psrbagev2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 )
33	3 7	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
34	18 25 32 33	syl3anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
35	34	fmpttd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 )
36		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
37	4 36	rabexd	⊢ ( 𝜑 → 𝐷 ∈ V )
38	37	mptexd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ∈ V )
39		funmpt	⊢ Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
40	39	a1i	⊢ ( 𝜑 → Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) )
41		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V )
42		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
43	1 2 42 15 11	mplelsfi	⊢ ( 𝜑 → 𝑌 finSupp ( 0g ‘ 𝑅 ) )
44	43	fsuppimpd	⊢ ( 𝜑 → ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ∈ Fin )
45	23	feqmptd	⊢ ( 𝜑 → 𝑌 = ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) )
46	45	oveq1d	⊢ ( 𝜑 → ( 𝑌 supp ( 0g ‘ 𝑅 ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) )
47		eqimss2	⊢ ( ( 𝑌 supp ( 0g ‘ 𝑅 ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
48	46 47	syl	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
49		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
50		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
51	42 50	ghmid	⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
52	13 49 51	3syl	⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
53		fvexd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑌 ‘ 𝑏 ) ∈ V )
54		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
55	48 52 53 54	suppssfv	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
56	3 7 50	ringlz	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑥 ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · 𝑥 ) = ( 0g ‘ 𝑆 ) )
57	17 56	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · 𝑥 ) = ( 0g ‘ 𝑆 ) )
58		fvexd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ∈ V )
59	55 57 58 32 41	suppssov1	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
60		suppssfifsupp	⊢ ( ( ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ∈ V ∧ Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ∧ ( 0g ‘ 𝑆 ) ∈ V ) ∧ ( ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ∧ ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )
61	38 40 41 44 59 60	syl32anc	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )
62	35 61	jca	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 ∧ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) ) )