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 
|- A = ( N Mat R )
cayhamlem1.b 
|- B = ( Base ` A )
cayhamlem1.p 
|- P = ( Poly1 ` R )
cayhamlem1.y 
|- Y = ( N Mat P )
cayhamlem1.r 
|- .X. = ( .r ` Y )
cayhamlem1.s 
|- .- = ( -g ` Y )
cayhamlem1.0 
|- .0. = ( 0g ` Y )
cayhamlem1.t 
|- T = ( N matToPolyMat R )
cayhamlem1.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 ) ) ) ) ) ) ) )
cayhamlem1.e 
|- .^ = ( .g ` ( mulGrp ` Y ) )
Assertion chfacfpmmulfsupp 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 cayhamlem1.a 
 |-  A = ( N Mat R )
2 cayhamlem1.b 
 |-  B = ( Base ` A )
3 cayhamlem1.p 
 |-  P = ( Poly1 ` R )
4 cayhamlem1.y 
 |-  Y = ( N Mat P )
5 cayhamlem1.r 
 |-  .X. = ( .r ` Y )
6 cayhamlem1.s 
 |-  .- = ( -g ` Y )
7 cayhamlem1.0 
 |-  .0. = ( 0g ` Y )
8 cayhamlem1.t 
 |-  T = ( N matToPolyMat R )
9 cayhamlem1.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 cayhamlem1.e 
 |-  .^ = ( .g ` ( mulGrp ` Y ) )
11 7 fvexi 
 |-  .0. e. _V
12 11 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> .0. e. _V )
13 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. _V )
14 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
15 14 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
16 1nn0 
 |-  1 e. NN0
17 16 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. NN0 )
18 15 17 nn0addcld 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
19 vex 
 |-  k e. _V
20 csbov12g 
 |-  ( k e. _V -> [_ k / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( [_ k / i ]_ ( i .^ ( T ` M ) ) .X. [_ k / i ]_ ( G ` i ) ) )
21 nfcvd 
 |-  ( k e. _V -> F/_ i ( k .^ ( T ` M ) ) )
22 oveq1 
 |-  ( i = k -> ( i .^ ( T ` M ) ) = ( k .^ ( T ` M ) ) )
23 21 22 csbiegf 
 |-  ( k e. _V -> [_ k / i ]_ ( i .^ ( T ` M ) ) = ( k .^ ( T ` M ) ) )
24 csbfv 
 |-  [_ k / i ]_ ( G ` i ) = ( G ` k )
25 24 a1i 
 |-  ( k e. _V -> [_ k / i ]_ ( G ` i ) = ( G ` k ) )
26 23 25 oveq12d 
 |-  ( k e. _V -> ( [_ k / i ]_ ( i .^ ( T ` M ) ) .X. [_ k / i ]_ ( G ` i ) ) = ( ( k .^ ( T ` M ) ) .X. ( G ` k ) ) )
27 20 26 eqtrd 
 |-  ( k e. _V -> [_ k / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( k .^ ( T ` M ) ) .X. ( G ` k ) ) )
28 19 27 mp1i 
 |-  ( ( ( ( ( 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 / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( k .^ ( T ` M ) ) .X. ( G ` k ) ) )
29 simplll 
 |-  ( ( ( ( ( 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 e. Fin /\ R e. CRing /\ M e. B ) )
30 simpllr 
 |-  ( ( ( ( ( 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 e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) )
31 14 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
32 31 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 )
33 32 nn0zd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) -> s e. ZZ )
34 33 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 ) -> s e. ZZ )
35 2z 
 |-  2 e. ZZ
36 35 a1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) /\ ( s + 1 ) < k ) -> 2 e. ZZ )
37 34 36 zaddcld 
 |-  ( ( ( ( ( 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 + 2 ) e. ZZ )
38 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 )
39 38 nn0zd 
 |-  ( ( ( ( ( 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. ZZ )
40 peano2nn0 
 |-  ( s e. NN0 -> ( s + 1 ) e. NN0 )
41 14 40 syl 
 |-  ( s e. NN -> ( s + 1 ) e. NN0 )
42 41 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
43 42 nn0zd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. ZZ )
44 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
45 zltp1le 
 |-  ( ( ( s + 1 ) e. ZZ /\ k e. ZZ ) -> ( ( s + 1 ) < k <-> ( ( s + 1 ) + 1 ) <_ k ) )
46 43 44 45 syl2an 
 |-  ( ( ( ( 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 ) + 1 ) <_ k ) )
47 46 biimpa 
 |-  ( ( ( ( ( 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 ) + 1 ) <_ k )
48 nncn 
 |-  ( s e. NN -> s e. CC )
49 add1p1 
 |-  ( s e. CC -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
50 48 49 syl 
 |-  ( s e. NN -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
51 50 breq1d 
 |-  ( s e. NN -> ( ( ( s + 1 ) + 1 ) <_ k <-> ( s + 2 ) <_ k ) )
52 51 bicomd 
 |-  ( s e. NN -> ( ( s + 2 ) <_ k <-> ( ( s + 1 ) + 1 ) <_ k ) )
53 52 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( s + 2 ) <_ k <-> ( ( s + 1 ) + 1 ) <_ k ) )
54 53 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. NN0 ) -> ( ( s + 2 ) <_ k <-> ( ( s + 1 ) + 1 ) <_ k ) )
55 54 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 ) -> ( ( s + 2 ) <_ k <-> ( ( s + 1 ) + 1 ) <_ k ) )
56 47 55 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 ) -> ( s + 2 ) <_ k )
57 eluz2 
 |-  ( k e. ( ZZ>= ` ( s + 2 ) ) <-> ( ( s + 2 ) e. ZZ /\ k e. ZZ /\ ( s + 2 ) <_ k ) )
58 37 39 56 57 syl3anbrc 
 |-  ( ( ( ( ( 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. ( ZZ>= ` ( s + 2 ) ) )
59 1 2 3 4 5 6 7 8 9 10 chfacfpmmul0 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ k e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( k .^ ( T ` M ) ) .X. ( G ` k ) ) = .0. )
60 29 30 58 59 syl3anc 
 |-  ( ( ( ( ( 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 .^ ( T ` M ) ) .X. ( G ` k ) ) = .0. )
61 28 60 eqtrd 
 |-  ( ( ( ( ( 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 / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. )
62 61 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 / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. ) )
63 62 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 / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. ) )
64 breq1 
 |-  ( x = ( s + 1 ) -> ( x < k <-> ( s + 1 ) < k ) )
65 64 rspceaimv 
 |-  ( ( ( s + 1 ) e. NN0 /\ A. k e. NN0 ( ( s + 1 ) < k -> [_ k / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. ) ) -> E. x e. NN0 A. k e. NN0 ( x < k -> [_ k / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. ) )
66 18 63 65 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> E. x e. NN0 A. k e. NN0 ( x < k -> [_ k / i ]_ ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. ) )
67 12 13 66 mptnn0fsupp 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) finSupp .0. )