Metamath Proof Explorer

Theorem chfacffsupp

Description: The "characteristic factor function" is finitely supported. (Contributed by AV, 20-Nov-2019) (Proof shortened by AV, 23-Dec-2019)

Ref Expression
Hypotheses chfacfisf.a 
|- A = ( N Mat R )
chfacfisf.b 
|- B = ( Base ` A )
chfacfisf.p 
|- P = ( Poly1 ` R )
chfacfisf.y 
|- Y = ( N Mat P )
chfacfisf.r 
|- .X. = ( .r ` Y )
chfacfisf.s 
|- .- = ( -g ` Y )
chfacfisf.0 
|- .0. = ( 0g ` Y )
chfacfisf.t 
|- T = ( N matToPolyMat R )
chfacfisf.g 
|- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
Assertion chfacffsupp 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G finSupp ( 0g ` Y ) )

Proof

Step Hyp Ref Expression
1 chfacfisf.a 
 |-  A = ( N Mat R )
2 chfacfisf.b 
 |-  B = ( Base ` A )
3 chfacfisf.p 
 |-  P = ( Poly1 ` R )
4 chfacfisf.y 
 |-  Y = ( N Mat P )
5 chfacfisf.r 
 |-  .X. = ( .r ` Y )
6 chfacfisf.s 
 |-  .- = ( -g ` Y )
7 chfacfisf.0 
 |-  .0. = ( 0g ` Y )
8 chfacfisf.t 
 |-  T = ( N matToPolyMat R )
9 chfacfisf.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
10 fvexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0g ` Y ) e. _V )
11 ovex 
 |-  ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. _V
12 fvex 
 |-  ( T ` ( b ` s ) ) e. _V
13 7 fvexi 
 |-  .0. e. _V
14 ovex 
 |-  ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. _V
15 13 14 ifex 
 |-  if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) e. _V
16 12 15 ifex 
 |-  if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) e. _V
17 11 16 ifex 
 |-  if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) e. _V
18 17 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) e. _V )
19 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
20 peano2nn0 
 |-  ( s e. NN0 -> ( s + 1 ) e. NN0 )
21 19 20 syl 
 |-  ( s e. NN -> ( s + 1 ) e. NN0 )
22 21 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
23 simplr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> k e. NN0 )
24 0red 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> 0 e. RR )
25 nnre 
 |-  ( s e. NN -> s e. RR )
26 peano2re 
 |-  ( s e. RR -> ( s + 1 ) e. RR )
27 25 26 syl 
 |-  ( s e. NN -> ( s + 1 ) e. RR )
28 27 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( s + 1 ) e. RR )
29 28 ad3antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> ( s + 1 ) e. RR )
30 nn0re 
 |-  ( k e. NN0 -> k e. RR )
31 30 ad2antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> k e. RR )
32 19 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
33 32 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) -> s e. NN0 )
34 nn0p1gt0 
 |-  ( s e. NN0 -> 0 < ( s + 1 ) )
35 33 34 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) -> 0 < ( s + 1 ) )
36 35 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> 0 < ( s + 1 ) )
37 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> ( s + 1 ) < k )
38 24 29 31 36 37 lttrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> 0 < k )
39 38 gt0ne0d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> k =/= 0 )
40 39 neneqd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> -. k = 0 )
41 40 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> -. k = 0 )
42 eqeq1 
 |-  ( n = k -> ( n = 0 <-> k = 0 ) )
43 42 notbid 
 |-  ( n = k -> ( -. n = 0 <-> -. k = 0 ) )
44 43 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> ( -. n = 0 <-> -. k = 0 ) )
45 41 44 mpbird 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> -. n = 0 )
46 45 iffalsed 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) )
47 28 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) -> ( s + 1 ) e. RR )
48 ltne 
 |-  ( ( ( s + 1 ) e. RR /\ ( s + 1 ) < k ) -> k =/= ( s + 1 ) )
49 47 48 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> k =/= ( s + 1 ) )
50 49 neneqd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> -. k = ( s + 1 ) )
51 50 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> -. k = ( s + 1 ) )
52 eqeq1 
 |-  ( n = k -> ( n = ( s + 1 ) <-> k = ( s + 1 ) ) )
53 52 notbid 
 |-  ( n = k -> ( -. n = ( s + 1 ) <-> -. k = ( s + 1 ) ) )
54 53 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> ( -. n = ( s + 1 ) <-> -. k = ( s + 1 ) ) )
55 51 54 mpbird 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> -. n = ( s + 1 ) )
56 55 iffalsed 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) = if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) )
57 simplr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> ( s + 1 ) < k )
58 breq2 
 |-  ( n = k -> ( ( s + 1 ) < n <-> ( s + 1 ) < k ) )
59 58 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> ( ( s + 1 ) < n <-> ( s + 1 ) < k ) )
60 57 59 mpbird 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> ( s + 1 ) < n )
61 60 iftrued 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) = .0. )
62 61 7 eqtrdi 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) = ( 0g ` Y ) )
63 46 56 62 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) /\ n = k ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) )
64 23 63 csbied 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> [_ k / n ]_ if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) )
65 64 ex 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) -> ( ( s + 1 ) < k -> [_ k / n ]_ if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) ) )
66 65 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. k e. NN0 ( ( s + 1 ) < k -> [_ k / n ]_ if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) ) )
67 breq1 
 |-  ( l = ( s + 1 ) -> ( l < k <-> ( s + 1 ) < k ) )
68 67 rspceaimv 
 |-  ( ( ( s + 1 ) e. NN0 /\ A. k e. NN0 ( ( s + 1 ) < k -> [_ k / n ]_ if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) ) ) -> E. l e. NN0 A. k e. NN0 ( l < k -> [_ k / n ]_ if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) ) )
69 22 66 68 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> E. l e. NN0 A. k e. NN0 ( l < k -> [_ k / n ]_ if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( 0g ` Y ) ) )
70 10 18 69 mptnn0fsupp 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) ) finSupp ( 0g ` Y ) )
71 9 70 eqbrtrid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G finSupp ( 0g ` Y ) )