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

Metamath Proof Explorer

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 ‘ 𝑆 ) )