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 )