This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
evlvvvallem.p ⊢ P = I mPoly R
evlvvvallem.b ⊢ B = Base P
evlvvvallem.k ⊢ K = Base R
evlvvvallem.m ⊢ M = mulGrp R
evlvvvallem.w ⊢ × ˙ = ⋅ M
evlvvvallem.x ⊢ · ˙ = ⋅ R
evlvvvallem.i ⊢ φ → I ∈ V
evlvvvallem.r ⊢ φ → R ∈ CRing
evlvvvallem.f ⊢ φ → F ∈ B
evlvvvallem.a ⊢ φ → A ∈ K I
Assertion evlvvvallem ⊢ φ → finSupp 0 R⁡ b ∈ D ⟼ F ⁡ b · ˙ ∑ M v ∈ I b ⁡ v × ˙ A ⁡ v

Proof

Step Hyp Ref Expression
1 evlvvvallem.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
2 evlvvvallem.p ⊢ P = I mPoly R
3 evlvvvallem.b ⊢ B = Base P
4 evlvvvallem.k ⊢ K = Base R
5 evlvvvallem.m ⊢ M = mulGrp R
6 evlvvvallem.w ⊢ × ˙ = ⋅ M
7 evlvvvallem.x ⊢ · ˙ = ⋅ R
8 evlvvvallem.i ⊢ φ → I ∈ V
9 evlvvvallem.r ⊢ φ → R ∈ CRing
10 evlvvvallem.f ⊢ φ → F ∈ B
11 evlvvvallem.a ⊢ φ → A ∈ K I
12 eqid ⊢ I mPoly R ↾ 𝑠 K = I mPoly R ↾ 𝑠 K
13 eqid ⊢ R ↾ 𝑠 K = R ↾ 𝑠 K
14 eqid ⊢ Base I mPoly R ↾ 𝑠 K = Base I mPoly R ↾ 𝑠 K
15 9 crngringd ⊢ φ → R ∈ Ring
16 4 subrgid ⊢ R ∈ Ring → K ∈ SubRing ⁡ R
17 15 16 syl ⊢ φ → K ∈ SubRing ⁡ R
18 4 ressid ⊢ R ∈ CRing → R ↾ 𝑠 K = R
19 9 18 syl ⊢ φ → R ↾ 𝑠 K = R
20 19 oveq2d ⊢ φ → I mPoly R ↾ 𝑠 K = I mPoly R
21 20 2 eqtr4di ⊢ φ → I mPoly R ↾ 𝑠 K = P
22 21 fveq2d ⊢ φ → Base I mPoly R ↾ 𝑠 K = Base P
23 22 3 eqtr4di ⊢ φ → Base I mPoly R ↾ 𝑠 K = B
24 10 23 eleqtrrd ⊢ φ → F ∈ Base I mPoly R ↾ 𝑠 K
25 1 12 13 14 4 5 6 7 8 9 17 24 11 evlsvvvallem2 ⊢ φ → finSupp 0 R⁡ b ∈ D ⟼ F ⁡ b · ˙ ∑ M v ∈ I b ⁡ v × ˙ A ⁡ v