Theorem evlsvvvallem2

Description: Lemma for theorems using evlsvvval . (Contributed by SN, 8-Mar-2025)

	Ref	Expression
Hypotheses	evlsvvvallem2.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	evlsvvvallem2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
	evlsvvvallem2.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsvvvallem2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlsvvvallem2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsvvvallem2.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
	evlsvvvallem2.w	⊢ ↑ = ( .g ‘ 𝑀 )
	evlsvvvallem2.x	⊢ · = ( .r ‘ 𝑆 )
	evlsvvvallem2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsvvvallem2.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvvvallem2.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsvvvallem2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	evlsvvvallem2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlsvvvallem2	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvvvallem2.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2		evlsvvvallem2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsvvvallem2.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evlsvvvallem2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		evlsvvvallem2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		evlsvvvallem2.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
7		evlsvvvallem2.w	⊢ ↑ = ( .g ‘ 𝑀 )
8		evlsvvvallem2.x	⊢ · = ( .r ‘ 𝑆 )
9		evlsvvvallem2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10		evlsvvvallem2.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
11		evlsvvvallem2.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12		evlsvvvallem2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
13		evlsvvvallem2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
14		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
15	1 14	rabex2	⊢ 𝐷 ∈ V
16	15	mptex	⊢ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ∈ V
17	16	a1i	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ∈ V )
18		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V )
19		funmpt	⊢ Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
20	19	a1i	⊢ ( 𝜑 → Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
21		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
22	2 4 21 12	mplelsfi	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑈 ) )
23		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
24	2 23 4 1 12	mplelf	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) )
25		ssidd	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
26		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ V )
27	24 25 12 26	suppssrg	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑈 ) )
28		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
29	3 28	subrg0	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
30	11 29	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
31	30	eqcomd	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑆 ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑆 ) )
33	27 32	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) )
34	33	oveq1d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
35	10	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → 𝑆 ∈ Ring )
37		eldifi	⊢ ( 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) → 𝑏 ∈ 𝐷 )
38	9	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
39	10	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing )
40	13	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
41		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
42	1 5 6 7 38 39 40 41	evlsvvvallem	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
43	37 42	sylan2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
44	5 8 28 36 43	ringlzd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
45	34 44	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
46	15	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
47	45 46	suppss2	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
48	17 18 20 22 47	fsuppsssuppgd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )