Metamath Proof Explorer

Theorem mptcoe1matfsupp

Description: The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019) (Proof shortened by AV, 23-Dec-2019)

Ref Expression
Hypotheses mptcoe1matfsupp.a 
|- A = ( N Mat R )
mptcoe1matfsupp.q 
|- Q = ( Poly1 ` A )
mptcoe1matfsupp.l 
|- L = ( Base ` Q )
Assertion mptcoe1matfsupp 
|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( I ( ( coe1 ` O ) ` k ) J ) ) finSupp ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 mptcoe1matfsupp.a 
 |-  A = ( N Mat R )
2 mptcoe1matfsupp.q 
 |-  Q = ( Poly1 ` A )
3 mptcoe1matfsupp.l 
 |-  L = ( Base ` Q )
4 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( 0g ` R ) e. _V )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( Base ` A ) = ( Base ` A )
7 simp2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> I e. N )
8 7 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> I e. N )
9 simp3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> J e. N )
10 9 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> J e. N )
11 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> O e. L )
12 11 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> O e. L )
13 eqid 
 |-  ( coe1 ` O ) = ( coe1 ` O )
14 13 3 2 6 coe1fvalcl 
 |-  ( ( O e. L /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) e. ( Base ` A ) )
15 12 14 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> ( ( coe1 ` O ) ` k ) e. ( Base ` A ) )
16 1 5 6 8 10 15 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> ( I ( ( coe1 ` O ) ` k ) J ) e. ( Base ` R ) )
17 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
18 13 3 2 17 6 coe1fsupp 
 |-  ( O e. L -> ( coe1 ` O ) e. { c e. ( ( Base ` A ) ^m NN0 ) | c finSupp ( 0g ` A ) } )
19 elrabi 
 |-  ( ( coe1 ` O ) e. { c e. ( ( Base ` A ) ^m NN0 ) | c finSupp ( 0g ` A ) } -> ( coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
20 12 18 19 3syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) )
21 fvex 
 |-  ( 0g ` A ) e. _V
22 20 21 jctir 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( ( coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) /\ ( 0g ` A ) e. _V ) )
23 13 3 2 17 coe1sfi 
 |-  ( O e. L -> ( coe1 ` O ) finSupp ( 0g ` A ) )
24 12 23 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( coe1 ` O ) finSupp ( 0g ` A ) )
25 fsuppmapnn0ub 
 |-  ( ( ( coe1 ` O ) e. ( ( Base ` A ) ^m NN0 ) /\ ( 0g ` A ) e. _V ) -> ( ( coe1 ` O ) finSupp ( 0g ` A ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) ) )
26 22 24 25 sylc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) )
27 csbov 
 |-  [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( I [_ x / k ]_ ( ( coe1 ` O ) ` k ) J )
28 csbfv 
 |-  [_ x / k ]_ ( ( coe1 ` O ) ` k ) = ( ( coe1 ` O ) ` x )
29 28 oveqi 
 |-  ( I [_ x / k ]_ ( ( coe1 ` O ) ` k ) J ) = ( I ( ( coe1 ` O ) ` x ) J )
30 27 29 eqtri 
 |-  [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( I ( ( coe1 ` O ) ` x ) J )
31 30 a1i 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) /\ x e. NN0 ) /\ s < x ) /\ ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( I ( ( coe1 ` O ) ` x ) J ) )
32 oveq 
 |-  ( ( ( coe1 ` O ) ` x ) = ( 0g ` A ) -> ( I ( ( coe1 ` O ) ` x ) J ) = ( I ( 0g ` A ) J ) )
33 32 adantl 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) /\ x e. NN0 ) /\ s < x ) /\ ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( I ( ( coe1 ` O ) ` x ) J ) = ( I ( 0g ` A ) J ) )
34 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
35 1 34 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
36 35 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
37 36 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( 0g ` A ) = ( i e. N , j e. N |-> ( 0g ` R ) ) )
38 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ ( i = I /\ j = J ) ) -> ( 0g ` R ) = ( 0g ` R ) )
39 37 38 7 9 4 ovmpod 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( I ( 0g ` A ) J ) = ( 0g ` R ) )
40 39 ad4antr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) /\ x e. NN0 ) /\ s < x ) /\ ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( I ( 0g ` A ) J ) = ( 0g ` R ) )
41 31 33 40 3eqtrd 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) /\ x e. NN0 ) /\ s < x ) /\ ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( 0g ` R ) )
42 41 exp31 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) /\ x e. NN0 ) -> ( s < x -> ( ( ( coe1 ` O ) ` x ) = ( 0g ` A ) -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( 0g ` R ) ) ) )
43 42 a2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> ( s < x -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( 0g ` R ) ) ) )
44 43 ralimdva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> A. x e. NN0 ( s < x -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( 0g ` R ) ) ) )
45 44 reximdva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` O ) ` x ) = ( 0g ` A ) ) -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( 0g ` R ) ) ) )
46 26 45 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ ( I ( ( coe1 ` O ) ` k ) J ) = ( 0g ` R ) ) )
47 4 16 46 mptnn0fsupp 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( I ( ( coe1 ` O ) ` k ) J ) ) finSupp ( 0g ` R ) )