Metamath Proof Explorer

Theorem chfacfpmmulfsupp

Description: A mapping of values of the "characteristic factor function" multiplied with a constant polynomial matrix is finitely supported. (Contributed by AV, 23-Nov-2019)

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

Proof

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