Theorem evlvvvallem

Description: Lemma for theorems using evlvvval . Version of evlsvvvallem2 using df-evl . (Contributed by SN, 11-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		evlvvvallem.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2		evlvvvallem.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		evlvvvallem.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		evlvvvallem.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		evlvvvallem.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
6		evlvvvallem.w	⊢ ↑ = ( .g ‘ 𝑀 )
7		evlvvvallem.x	⊢ · = ( .r ‘ 𝑅 )
8		evlvvvallem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9		evlvvvallem.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
10		evlvvvallem.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11		evlvvvallem.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
12		eqid	⊢ ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) = ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) )
13		eqid	⊢ ( 𝑅 ↾s 𝐾 ) = ( 𝑅 ↾s 𝐾 )
14		eqid	⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) )
15	9	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	4	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑅 ) )
17	15 16	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ 𝑅 ) )
18	4	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐾 ) = 𝑅 )
19	9 18	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐾 ) = 𝑅 )
20	19	oveq2d	⊢ ( 𝜑 → ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) = ( 𝐼 mPoly 𝑅 ) )
21	20 2	eqtr4di	⊢ ( 𝜑 → ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) = 𝑃 )
22	21	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) ) = ( Base ‘ 𝑃 ) )
23	22 3	eqtr4di	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) ) = 𝐵 )
24	10 23	eleqtrrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐾 ) ) ) )
25	1 12 13 14 4 5 6 7 8 9 17 24 11	evlsvvvallem2	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )