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	3	ovexi	⊢ 𝑈 ∈ V
23	22	a1i	⊢ ( 𝜑 → 𝑈 ∈ V )
24	2 4 21 12 23	mplelsfi	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑈 ) )
25		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
26	2 25 4 1 12	mplelf	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) )
27		ssidd	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
28		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ V )
29	26 27 12 28	suppssrg	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑈 ) )
30		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
31	3 30	subrg0	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
32	11 31	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
33	32	eqcomd	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑆 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑆 ) )
35	29 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) )
36	35	oveq1d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
37	10	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → 𝑆 ∈ Ring )
39		eldifi	⊢ ( 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) → 𝑏 ∈ 𝐷 )
40	9	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
41	10	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing )
42	13	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
43		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
44	1 5 6 7 40 41 42 43	evlsvvvallem	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
45	39 44	sylan2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
46	5 8 30 38 45	ringlzd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
47	36 46	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
48	15	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
49	47 48	suppss2	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
50	17 18 20 24 49	fsuppsssuppgd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )