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	\|- 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 ) ) ) ) ) ) ) )
	chfacfscmulcl.x	\|- X = ( var1 ` R )
	chfacfscmulcl.m	\|- .x. = ( .s ` Y )
	chfacfscmulcl.e	\|- .^ = ( .g ` ( mulGrp ` P ) )
Assertion	chfacfscmulfsupp	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) finSupp .0. )

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		chfacfscmulcl.x	\|- X = ( var1 ` R )
11		chfacfscmulcl.m	\|- .x. = ( .s ` Y )
12		chfacfscmulcl.e	\|- .^ = ( .g ` ( mulGrp ` P ) )
13	7	fvexi	\|- .0. e. _V
14	13	a1i	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> .0. e. _V )
15		ovexd	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> ( ( i .^ X ) .x. ( G ` i ) ) e. _V )
16		nnnn0	\|- ( s e. NN -> s e. NN0 )
17		peano2nn0	\|- ( s e. NN0 -> ( s + 1 ) e. NN0 )
18	16 17	syl	\|- ( s e. NN -> ( s + 1 ) e. NN0 )
19	18	ad2antrl	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
20		vex	\|- k e. _V
21		csbov12g	\|- ( k e. _V -> [_ k / i ]_ ( ( i .^ X ) .x. ( G ` i ) ) = ( [_ k / i ]_ ( i .^ X ) .x. [_ k / i ]_ ( G ` i ) ) )
22		csbov1g	\|- ( k e. _V -> [_ k / i ]_ ( i .^ X ) = ( [_ k / i ]_ i .^ X ) )
23		csbvarg	\|- ( k e. _V -> [_ k / i ]_ i = k )
24	23	oveq1d	\|- ( k e. _V -> ( [_ k / i ]_ i .^ X ) = ( k .^ X ) )
25	22 24	eqtrd	\|- ( k e. _V -> [_ k / i ]_ ( i .^ X ) = ( k .^ X ) )
26		csbfv	\|- [_ k / i ]_ ( G ` i ) = ( G ` k )
27	26	a1i	\|- ( k e. _V -> [_ k / i ]_ ( G ` i ) = ( G ` k ) )
28	25 27	oveq12d	\|- ( k e. _V -> ( [_ k / i ]_ ( i .^ X ) .x. [_ k / i ]_ ( G ` i ) ) = ( ( k .^ X ) .x. ( G ` k ) ) )
29	21 28	eqtrd	\|- ( k e. _V -> [_ k / i ]_ ( ( i .^ X ) .x. ( G ` i ) ) = ( ( k .^ X ) .x. ( G ` k ) ) )
30	20 29	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 .^ X ) .x. ( G ` i ) ) = ( ( k .^ X ) .x. ( G ` k ) ) )
31		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 ) )
32		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 ) ) ) )
33	16	adantr	\|- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
34	33	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 )
35	34	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 )
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 ) -> s e. ZZ )
37		2z	\|- 2 e. ZZ
38	37	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 )
39	36 38	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 )
40		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 )
41	40	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 )
42	19	nn0zd	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. ZZ )
43		nn0z	\|- ( k e. NN0 -> k e. ZZ )
44		zltp1le	\|- ( ( ( s + 1 ) e. ZZ /\ k e. ZZ ) -> ( ( s + 1 ) < k <-> ( ( s + 1 ) + 1 ) <_ k ) )
45	42 43 44	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 ) )
46	45	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 )
47		nncn	\|- ( s e. NN -> s e. CC )
48		add1p1	\|- ( s e. CC -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
49	47 48	syl	\|- ( s e. NN -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
50	49	breq1d	\|- ( s e. NN -> ( ( ( s + 1 ) + 1 ) <_ k <-> ( s + 2 ) <_ k ) )
51	50	bicomd	\|- ( s e. NN -> ( ( s + 2 ) <_ k <-> ( ( s + 1 ) + 1 ) <_ k ) )
52	51	adantr	\|- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( s + 2 ) <_ k <-> ( ( s + 1 ) + 1 ) <_ k ) )
53	52	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 ) )
54	53	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 ) )
55	46 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 ) -> ( s + 2 ) <_ k )
56		eluz2	\|- ( k e. ( ZZ>= ` ( s + 2 ) ) <-> ( ( s + 2 ) e. ZZ /\ k e. ZZ /\ ( s + 2 ) <_ k ) )
57	39 41 55 56	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 ) ) )
58	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmul0	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ k e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( k .^ X ) .x. ( G ` k ) ) = .0. )
59	31 32 57 58	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 .^ X ) .x. ( G ` k ) ) = .0. )
60	30 59	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 .^ X ) .x. ( G ` i ) ) = .0. )
61	60	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 .^ X ) .x. ( G ` i ) ) = .0. ) )
62	61	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 .^ X ) .x. ( G ` i ) ) = .0. ) )
63		breq1	\|- ( z = ( s + 1 ) -> ( z < k <-> ( s + 1 ) < k ) )
64	63	rspceaimv	\|- ( ( ( s + 1 ) e. NN0 /\ A. k e. NN0 ( ( s + 1 ) < k -> [_ k / i ]_ ( ( i .^ X ) .x. ( G ` i ) ) = .0. ) ) -> E. z e. NN0 A. k e. NN0 ( z < k -> [_ k / i ]_ ( ( i .^ X ) .x. ( G ` i ) ) = .0. ) )
65	19 62 64	syl2anc	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> E. z e. NN0 A. k e. NN0 ( z < k -> [_ k / i ]_ ( ( i .^ X ) .x. ( G ` i ) ) = .0. ) )
66	14 15 65	mptnn0fsupp	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) finSupp .0. )

Metamath Proof Explorer

Theorem chfacfscmulfsupp

Proof