Theorem pmatcoe1fsupp

Description: For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	pmatcoe1fsupp.p	|- P = ( Poly1 ` R )
	pmatcoe1fsupp.c	|- C = ( N Mat P )
	pmatcoe1fsupp.b	|- B = ( Base ` C )
	pmatcoe1fsupp.0	|- .0. = ( 0g ` R )
Assertion	pmatcoe1fsupp	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcoe1fsupp.p	|- P = ( Poly1 ` R )
2		pmatcoe1fsupp.c	|- C = ( N Mat P )
3		pmatcoe1fsupp.b	|- B = ( Base ` C )
4		pmatcoe1fsupp.0	|- .0. = ( 0g ` R )
5		ssrab2	|- { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } C_ ( ( Base ` R ) ^m NN0 )
6	5	a1i	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } C_ ( ( Base ` R ) ^m NN0 ) )
7	6	olcd	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } C_ ( ( Base ` R ) ^m NN0 ) \/ { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } C_ ( ( Base ` R ) ^m NN0 ) ) )
8		inss	|- ( ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } C_ ( ( Base ` R ) ^m NN0 ) \/ { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } C_ ( ( Base ` R ) ^m NN0 ) ) -> ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) C_ ( ( Base ` R ) ^m NN0 ) )
9	7 8	syl	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) C_ ( ( Base ` R ) ^m NN0 ) )
10		xpfi	|- ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
11	10	anidms	|- ( N e. Fin -> ( N X. N ) e. Fin )
12		snfi	|- { ( coe1 ` ( M ` u ) ) } e. Fin
13	12	a1i	|- ( ( N e. Fin /\ u e. ( N X. N ) ) -> { ( coe1 ` ( M ` u ) ) } e. Fin )
14	13	ralrimiva	|- ( N e. Fin -> A. u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } e. Fin )
15	11 14	jca	|- ( N e. Fin -> ( ( N X. N ) e. Fin /\ A. u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } e. Fin ) )
16	15	3ad2ant1	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( N X. N ) e. Fin /\ A. u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } e. Fin ) )
17		iunfi	|- ( ( ( N X. N ) e. Fin /\ A. u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } e. Fin ) -> U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } e. Fin )
18		infi	|- ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } e. Fin -> ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) e. Fin )
19	16 17 18	3syl	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) e. Fin )
20		fvex	|- ( 0g ` R ) e. _V
21	4 20	eqeltri	|- .0. e. _V
22	21	a1i	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .0. e. _V )
23		elin	|- ( w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) <-> ( w e. U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } /\ w e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) )
24		breq1	|- ( v = w -> ( v finSupp .0. <-> w finSupp .0. ) )
25	24	elrab	|- ( w e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } <-> ( w e. ( ( Base ` R ) ^m NN0 ) /\ w finSupp .0. ) )
26	25	simprbi	|- ( w e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } -> w finSupp .0. )
27	23 26	simplbiim	|- ( w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) -> w finSupp .0. )
28	27	rgen	|- A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) w finSupp .0.
29	28	a1i	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) w finSupp .0. )
30		fsuppmapnn0fiub0	|- ( ( ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) C_ ( ( Base ` R ) ^m NN0 ) /\ ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) e. Fin /\ .0. e. _V ) -> ( A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) w finSupp .0. -> E. s e. NN0 A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) ) )
31	30	imp	|- ( ( ( ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) C_ ( ( Base ` R ) ^m NN0 ) /\ ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) e. Fin /\ .0. e. _V ) /\ A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) w finSupp .0. ) -> E. s e. NN0 A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) )
32	9 19 22 29 31	syl31anc	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. s e. NN0 A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) )
33		opelxpi	|- ( ( i e. N /\ j e. N ) -> <. i , j >. e. ( N X. N ) )
34		df-ov	|- ( i M j ) = ( M ` <. i , j >. )
35	34	fveq2i	|- ( coe1 ` ( i M j ) ) = ( coe1 ` ( M ` <. i , j >. ) )
36		fvex	|- ( coe1 ` ( M ` <. i , j >. ) ) e. _V
37	36	snid	|- ( coe1 ` ( M ` <. i , j >. ) ) e. { ( coe1 ` ( M ` <. i , j >. ) ) }
38	35 37	eqeltri	|- ( coe1 ` ( i M j ) ) e. { ( coe1 ` ( M ` <. i , j >. ) ) }
39	38	a1i	|- ( ( i e. N /\ j e. N ) -> ( coe1 ` ( i M j ) ) e. { ( coe1 ` ( M ` <. i , j >. ) ) } )
40		2fveq3	|- ( u = <. i , j >. -> ( coe1 ` ( M ` u ) ) = ( coe1 ` ( M ` <. i , j >. ) ) )
41	40	sneqd	|- ( u = <. i , j >. -> { ( coe1 ` ( M ` u ) ) } = { ( coe1 ` ( M ` <. i , j >. ) ) } )
42	41	eliuni	|- ( ( <. i , j >. e. ( N X. N ) /\ ( coe1 ` ( i M j ) ) e. { ( coe1 ` ( M ` <. i , j >. ) ) } ) -> ( coe1 ` ( i M j ) ) e. U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } )
43	33 39 42	syl2anc	|- ( ( i e. N /\ j e. N ) -> ( coe1 ` ( i M j ) ) e. U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } )
44	43	adantl	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( coe1 ` ( i M j ) ) e. U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } )
45		eqid	|- ( Base ` P ) = ( Base ` P )
46		simprl	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
47		simprr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
48	3	eleq2i	|- ( M e. B <-> M e. ( Base ` C ) )
49	48	biimpi	|- ( M e. B -> M e. ( Base ` C ) )
50	49	3ad2ant3	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M e. ( Base ` C ) )
51	50	ad3antrrr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> M e. ( Base ` C ) )
52	51 3	eleqtrrdi	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> M e. B )
53	2 45 3 46 47 52	matecld	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` P ) )
54		eqid	|- ( coe1 ` ( i M j ) ) = ( coe1 ` ( i M j ) )
55		eqid	|- ( 0g ` R ) = ( 0g ` R )
56		eqid	|- ( Base ` R ) = ( Base ` R )
57	54 45 1 55 56	coe1fsupp	|- ( ( i M j ) e. ( Base ` P ) -> ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp ( 0g ` R ) } )
58	53 57	syl	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp ( 0g ` R ) } )
59	4	a1i	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .0. = ( 0g ` R ) )
60	59	breq2d	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( v finSupp .0. <-> v finSupp ( 0g ` R ) ) )
61	60	rabbidv	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } = { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp ( 0g ` R ) } )
62	61	eleq2d	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } <-> ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp ( 0g ` R ) } ) )
63	62	ad3antrrr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } <-> ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp ( 0g ` R ) } ) )
64	58 63	mpbird	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( coe1 ` ( i M j ) ) e. { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } )
65	44 64	elind	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( coe1 ` ( i M j ) ) e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) )
66		simplr	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> x e. NN0 )
67		fveq1	|- ( w = ( coe1 ` ( i M j ) ) -> ( w ` z ) = ( ( coe1 ` ( i M j ) ) ` z ) )
68	67	eqeq1d	|- ( w = ( coe1 ` ( i M j ) ) -> ( ( w ` z ) = .0. <-> ( ( coe1 ` ( i M j ) ) ` z ) = .0. ) )
69	68	imbi2d	|- ( w = ( coe1 ` ( i M j ) ) -> ( ( s < z -> ( w ` z ) = .0. ) <-> ( s < z -> ( ( coe1 ` ( i M j ) ) ` z ) = .0. ) ) )
70		breq2	|- ( z = x -> ( s < z <-> s < x ) )
71		fveqeq2	|- ( z = x -> ( ( ( coe1 ` ( i M j ) ) ` z ) = .0. <-> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) )
72	70 71	imbi12d	|- ( z = x -> ( ( s < z -> ( ( coe1 ` ( i M j ) ) ` z ) = .0. ) <-> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
73	69 72	rspc2v	|- ( ( ( coe1 ` ( i M j ) ) e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) /\ x e. NN0 ) -> ( A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) -> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
74	65 66 73	syl2anc	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) -> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
75	74	ex	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( i e. N /\ j e. N ) -> ( A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) -> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) ) )
76	75	com23	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) -> ( A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) -> ( ( i e. N /\ j e. N ) -> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) ) )
77	76	impancom	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) ) -> ( x e. NN0 -> ( ( i e. N /\ j e. N ) -> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) ) )
78	77	imp	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) ) /\ x e. NN0 ) -> ( ( i e. N /\ j e. N ) -> ( s < x -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
79	78	com23	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) ) /\ x e. NN0 ) -> ( s < x -> ( ( i e. N /\ j e. N ) -> ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
80	79	ralrimdvv	|- ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) ) /\ x e. NN0 ) -> ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) )
81	80	ralrimiva	|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) ) -> A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) )
82	81	ex	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ s e. NN0 ) -> ( A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) -> A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
83	82	reximdva	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( E. s e. NN0 A. w e. ( U_ u e. ( N X. N ) { ( coe1 ` ( M ` u ) ) } i^i { v e. ( ( Base ` R ) ^m NN0 ) | v finSupp .0. } ) A. z e. NN0 ( s < z -> ( w ` z ) = .0. ) -> E. s e. NN0 A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) ) )
84	32 83	mpd	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = .0. ) )