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 | |
|
mptcoe1matfsupp.q | |
||
mptcoe1matfsupp.l | |
||
Assertion | mptcoe1matfsupp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mptcoe1matfsupp.a | |
|
2 | mptcoe1matfsupp.q | |
|
3 | mptcoe1matfsupp.l | |
|
4 | fvexd | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | simp2 | |
|
8 | 7 | adantr | |
9 | simp3 | |
|
10 | 9 | adantr | |
11 | simp3 | |
|
12 | 11 | 3ad2ant1 | |
13 | eqid | |
|
14 | 13 3 2 6 | coe1fvalcl | |
15 | 12 14 | sylan | |
16 | 1 5 6 8 10 15 | matecld | |
17 | eqid | |
|
18 | 13 3 2 17 6 | coe1fsupp | |
19 | elrabi | |
|
20 | 12 18 19 | 3syl | |
21 | fvex | |
|
22 | 20 21 | jctir | |
23 | 13 3 2 17 | coe1sfi | |
24 | 12 23 | syl | |
25 | fsuppmapnn0ub | |
|
26 | 22 24 25 | sylc | |
27 | csbov | |
|
28 | csbfv | |
|
29 | 28 | oveqi | |
30 | 27 29 | eqtri | |
31 | 30 | a1i | |
32 | oveq | |
|
33 | 32 | adantl | |
34 | eqid | |
|
35 | 1 34 | mat0op | |
36 | 35 | 3adant3 | |
37 | 36 | 3ad2ant1 | |
38 | eqidd | |
|
39 | 37 38 7 9 4 | ovmpod | |
40 | 39 | ad4antr | |
41 | 31 33 40 | 3eqtrd | |
42 | 41 | exp31 | |
43 | 42 | a2d | |
44 | 43 | ralimdva | |
45 | 44 | reximdva | |
46 | 26 45 | mpd | |
47 | 4 16 46 | mptnn0fsupp | |