Metamath Proof Explorer

Theorem decpmataa0

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is 0 for almost all powers. (Contributed by AV, 3-Nov-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmate.p 
|- P = ( Poly1 ` R )
decpmate.c 
|- C = ( N Mat P )
decpmate.b 
|- B = ( Base ` C )
decpmatcl.a 
|- A = ( N Mat R )
decpmatfsupp.0 
|- .0. = ( 0g ` A )
Assertion decpmataa0 
|- ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( M decompPMat x ) = .0. ) )

Proof

Step Hyp Ref Expression
1 decpmate.p 
 |-  P = ( Poly1 ` R )
2 decpmate.c 
 |-  C = ( N Mat P )
3 decpmate.b 
 |-  B = ( Base ` C )
4 decpmatcl.a 
 |-  A = ( N Mat R )
5 decpmatfsupp.0 
 |-  .0. = ( 0g ` A )
6 2 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ P e. _V ) )
7 6 simpld 
 |-  ( M e. B -> N e. Fin )
8 7 adantl 
 |-  ( ( R e. Ring /\ M e. B ) -> N e. Fin )
9 simpl 
 |-  ( ( R e. Ring /\ M e. B ) -> R e. Ring )
10 simpr 
 |-  ( ( R e. Ring /\ M e. B ) -> M e. B )
11 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
12 1 2 3 11 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 ) = ( 0g ` R ) ) )
13 8 9 10 12 syl3anc 
 |-  ( ( 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 ) = ( 0g ` R ) ) )
14 eqid 
 |-  ( Base ` A ) = ( Base ` A )
15 1 2 3 4 14 decpmatcl 
 |-  ( ( R e. Ring /\ M e. B /\ x e. NN0 ) -> ( M decompPMat x ) e. ( Base ` A ) )
16 15 3expa 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( M decompPMat x ) e. ( Base ` A ) )
17 8 9 jca 
 |-  ( ( R e. Ring /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
18 4 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
19 14 5 ring0cl 
 |-  ( A e. Ring -> .0. e. ( Base ` A ) )
20 17 18 19 3syl 
 |-  ( ( R e. Ring /\ M e. B ) -> .0. e. ( Base ` A ) )
21 20 adantr 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> .0. e. ( Base ` A ) )
22 4 14 eqmat 
 |-  ( ( ( M decompPMat x ) e. ( Base ` A ) /\ .0. e. ( Base ` A ) ) -> ( ( M decompPMat x ) = .0. <-> A. i e. N A. j e. N ( i ( M decompPMat x ) j ) = ( i .0. j ) ) )
23 16 21 22 syl2anc 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( M decompPMat x ) = .0. <-> A. i e. N A. j e. N ( i ( M decompPMat x ) j ) = ( i .0. j ) ) )
24 df-3an 
 |-  ( ( R e. Ring /\ M e. B /\ x e. NN0 ) <-> ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) )
25 1 2 3 decpmate 
 |-  ( ( ( R e. Ring /\ M e. B /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( M decompPMat x ) j ) = ( ( coe1 ` ( i M j ) ) ` x ) )
26 24 25 sylanbr 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( M decompPMat x ) j ) = ( ( coe1 ` ( i M j ) ) ` x ) )
27 17 adantr 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( N e. Fin /\ R e. Ring ) )
28 27 adantr 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( N e. Fin /\ R e. Ring ) )
29 4 11 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( a e. N , b e. N |-> ( 0g ` R ) ) )
30 5 29 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. = ( a e. N , b e. N |-> ( 0g ` R ) ) )
31 28 30 syl 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> .0. = ( a e. N , b e. N |-> ( 0g ` R ) ) )
32 eqidd 
 |-  ( ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) /\ ( a = i /\ b = j ) ) -> ( 0g ` R ) = ( 0g ` R ) )
33 simpl 
 |-  ( ( i e. N /\ j e. N ) -> i e. N )
34 33 adantl 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
35 simpr 
 |-  ( ( i e. N /\ j e. N ) -> j e. N )
36 35 adantl 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
37 fvexd 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( 0g ` R ) e. _V )
38 31 32 34 36 37 ovmpod 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i .0. j ) = ( 0g ` R ) )
39 26 38 eqeq12d 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( ( i ( M decompPMat x ) j ) = ( i .0. j ) <-> ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) )
40 39 2ralbidva 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( A. i e. N A. j e. N ( i ( M decompPMat x ) j ) = ( i .0. j ) <-> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) )
41 23 40 bitrd 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( M decompPMat x ) = .0. <-> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) )
42 41 imbi2d 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ x e. NN0 ) -> ( ( s < x -> ( M decompPMat x ) = .0. ) <-> ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) ) )
43 42 ralbidva 
 |-  ( ( R e. Ring /\ M e. B ) -> ( A. x e. NN0 ( s < x -> ( M decompPMat x ) = .0. ) <-> A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) ) )
44 43 rexbidv 
 |-  ( ( R e. Ring /\ M e. B ) -> ( E. s e. NN0 A. x e. NN0 ( s < x -> ( M decompPMat x ) = .0. ) <-> E. s e. NN0 A. x e. NN0 ( s < x -> A. i e. N A. j e. N ( ( coe1 ` ( i M j ) ) ` x ) = ( 0g ` R ) ) ) )
45 13 44 mpbird 
 |-  ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( M decompPMat x ) = .0. ) )