Metamath Proof Explorer

Theorem chfacfscmulfsupp

Description: A mapping of scaled values of the "characteristic factor function" is finitely supported. (Contributed by AV, 8-Nov-2019)

Ref Expression
Hypotheses chfacfisf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
chfacfisf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
chfacfisf.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
chfacfisf.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
chfacfisf.r ⊢ × = ( .r ‘ 𝑌 )
chfacfisf.s ⊢ − = ( -g ‘ 𝑌 )
chfacfisf.0 ⊢ 0 = ( 0g ‘ 𝑌 )
chfacfisf.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chfacfisf.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
chfacfscmulcl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
chfacfscmulcl.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
chfacfscmulcl.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
Assertion chfacfscmulfsupp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) finSupp 0 )

Proof

Step Hyp Ref Expression
1 chfacfisf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 chfacfisf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 chfacfisf.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 chfacfisf.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 chfacfisf.r ⊢ × = ( .r ‘ 𝑌 )
6 chfacfisf.s ⊢ − = ( -g ‘ 𝑌 )
7 chfacfisf.0 ⊢ 0 = ( 0g ‘ 𝑌 )
8 chfacfisf.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9 chfacfisf.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10 chfacfscmulcl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
11 chfacfscmulcl.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
12 chfacfscmulcl.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
13 7 fvexi ⊢ 0 ∈ V
14 13 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ V )
15 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ V )
16 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
17 peano2nn0 ⊢ ( 𝑠 ∈ ℕ0 → ( 𝑠 + 1 ) ∈ ℕ0 )
18 16 17 syl ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℕ0 )
19 18 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℕ0 )
20 vex ⊢ 𝑘 ∈ V
21 csbov12g ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = ( ⦋ 𝑘 / 𝑖 ⦌ ( 𝑖 ↑ 𝑋 ) · ⦋ 𝑘 / 𝑖 ⦌ ( 𝐺 ‘ 𝑖 ) ) )
22 csbov1g ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑖 ⦌ ( 𝑖 ↑ 𝑋 ) = ( ⦋ 𝑘 / 𝑖 ⦌ 𝑖 ↑ 𝑋 ) )
23 csbvarg ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑖 ⦌ 𝑖 = 𝑘 )
24 23 oveq1d ⊢ ( 𝑘 ∈ V → ( ⦋ 𝑘 / 𝑖 ⦌ 𝑖 ↑ 𝑋 ) = ( 𝑘 ↑ 𝑋 ) )
25 22 24 eqtrd ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑖 ⦌ ( 𝑖 ↑ 𝑋 ) = ( 𝑘 ↑ 𝑋 ) )
26 csbfv ⊢ ⦋ 𝑘 / 𝑖 ⦌ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑘 )
27 26 a1i ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑖 ⦌ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑘 ) )
28 25 27 oveq12d ⊢ ( 𝑘 ∈ V → ( ⦋ 𝑘 / 𝑖 ⦌ ( 𝑖 ↑ 𝑋 ) · ⦋ 𝑘 / 𝑖 ⦌ ( 𝐺 ‘ 𝑖 ) ) = ( ( 𝑘 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑘 ) ) )
29 21 28 eqtrd ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = ( ( 𝑘 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑘 ) ) )
30 20 29 mp1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = ( ( 𝑘 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑘 ) ) )
31 simplll ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) )
32 simpllr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) )
33 16 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
34 33 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑠 ∈ ℕ0 )
35 34 nn0zd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑠 ∈ ℤ )
36 35 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑠 ∈ ℤ )
37 2z ⊢ 2 ∈ ℤ
38 37 a1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 2 ∈ ℤ )
39 36 38 zaddcld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( 𝑠 + 2 ) ∈ ℤ )
40 simplr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ∈ ℕ0 )
41 40 nn0zd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ∈ ℤ )
42 19 nn0zd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℤ )
43 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
44 zltp1le ⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑠 + 1 ) < 𝑘 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ) )
45 42 43 44 syl2an ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 + 1 ) < 𝑘 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ) )
46 45 biimpa ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 )
47 nncn ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
48 add1p1 ⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
49 47 48 syl ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
50 49 breq1d ⊢ ( 𝑠 ∈ ℕ → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ↔ ( 𝑠 + 2 ) ≤ 𝑘 ) )
51 50 bicomd ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 2 ) ≤ 𝑘 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ) )
52 51 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( 𝑠 + 2 ) ≤ 𝑘 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ) )
53 52 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 + 2 ) ≤ 𝑘 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ) )
54 53 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( ( 𝑠 + 2 ) ≤ 𝑘 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝑘 ) )
55 46 54 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( 𝑠 + 2 ) ≤ 𝑘 )
56 eluz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ↔ ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝑘 ) )
57 39 41 55 56 syl3anbrc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) )
58 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmul0 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝑘 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑘 ) ) = 0 )
59 31 32 57 58 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( ( 𝑘 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑘 ) ) = 0 )
60 30 59 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 )
61 60 ex ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 + 1 ) < 𝑘 → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 ) )
62 61 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝑠 + 1 ) < 𝑘 → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 ) )
63 breq1 ⊢ ( 𝑧 = ( 𝑠 + 1 ) → ( 𝑧 < 𝑘 ↔ ( 𝑠 + 1 ) < 𝑘 ) )
64 63 rspceaimv ⊢ ( ( ( 𝑠 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( ( 𝑠 + 1 ) < 𝑘 → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 ) ) → ∃ 𝑧 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 ( 𝑧 < 𝑘 → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 ) )
65 19 62 64 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∃ 𝑧 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 ( 𝑧 < 𝑘 → ⦋ 𝑘 / 𝑖 ⦌ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 ) )
66 14 15 65 mptnn0fsupp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) finSupp 0 )