Step | Hyp | Ref
| Expression |
1 | | chpmatfval.c |
. 2
CharPlyMat
|
2 | | df-chpmat 20632 |
. . . 4
CharPlyMat Mat maDet Poly1var1 Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
|
3 | 2 | a1i 11 |
. . 3
CharPlyMat
Mat maDet Poly1var1 Mat
Poly1 Mat Poly1 Mat Poly1 matToPolyMat
|
4 | | oveq12 6659 |
. . . . . . . 8
Mat Mat |
5 | | chpmatfval.a |
. . . . . . . 8
Mat |
6 | 4, 5 | syl6eqr 2674 |
. . . . . . 7
Mat |
7 | 6 | fveq2d 6195 |
. . . . . 6
Mat |
8 | | chpmatfval.b |
. . . . . 6
|
9 | 7, 8 | syl6eqr 2674 |
. . . . 5
Mat |
10 | | simpl 473 |
. . . . . . . 8
|
11 | | simpr 477 |
. . . . . . . . . 10
|
12 | 11 | fveq2d 6195 |
. . . . . . . . 9
Poly1 Poly1 |
13 | | chpmatfval.p |
. . . . . . . . 9
Poly1 |
14 | 12, 13 | syl6eqr 2674 |
. . . . . . . 8
Poly1 |
15 | 10, 14 | oveq12d 6668 |
. . . . . . 7
maDet Poly1 maDet |
16 | | chpmatfval.d |
. . . . . . 7
maDet |
17 | 15, 16 | syl6eqr 2674 |
. . . . . 6
maDet Poly1 |
18 | | fveq2 6191 |
. . . . . . . . . . . . 13
Poly1 Poly1 |
19 | 18 | adantl 482 |
. . . . . . . . . . . 12
Poly1 Poly1 |
20 | 19, 13 | syl6eqr 2674 |
. . . . . . . . . . 11
Poly1 |
21 | 10, 20 | oveq12d 6668 |
. . . . . . . . . 10
Mat Poly1 Mat |
22 | | chpmatfval.y |
. . . . . . . . . 10
Mat |
23 | 21, 22 | syl6eqr 2674 |
. . . . . . . . 9
Mat Poly1 |
24 | 23 | fveq2d 6195 |
. . . . . . . 8
Mat Poly1 |
25 | | chpmatfval.s |
. . . . . . . 8
|
26 | 24, 25 | syl6eqr 2674 |
. . . . . . 7
Mat Poly1 |
27 | 23 | fveq2d 6195 |
. . . . . . . . 9
Mat Poly1 |
28 | | chpmatfval.m |
. . . . . . . . 9
|
29 | 27, 28 | syl6eqr 2674 |
. . . . . . . 8
Mat Poly1 |
30 | | fveq2 6191 |
. . . . . . . . . 10
var1 var1 |
31 | | chpmatfval.x |
. . . . . . . . . 10
var1 |
32 | 30, 31 | syl6eqr 2674 |
. . . . . . . . 9
var1 |
33 | 32 | adantl 482 |
. . . . . . . 8
var1 |
34 | 23 | fveq2d 6195 |
. . . . . . . . 9
Mat Poly1 |
35 | | chpmatfval.i |
. . . . . . . . 9
|
36 | 34, 35 | syl6eqr 2674 |
. . . . . . . 8
Mat Poly1 |
37 | 29, 33, 36 | oveq123d 6671 |
. . . . . . 7
var1 Mat Poly1 Mat
Poly1 |
38 | | oveq12 6659 |
. . . . . . . . 9
matToPolyMat
matToPolyMat |
39 | | chpmatfval.t |
. . . . . . . . 9
matToPolyMat |
40 | 38, 39 | syl6eqr 2674 |
. . . . . . . 8
matToPolyMat
|
41 | 40 | fveq1d 6193 |
. . . . . . 7
matToPolyMat |
42 | 26, 37, 41 | oveq123d 6671 |
. . . . . 6
var1 Mat
Poly1 Mat Poly1 Mat Poly1 matToPolyMat
|
43 | 17, 42 | fveq12d 6197 |
. . . . 5
maDet Poly1var1 Mat
Poly1 Mat Poly1 Mat Poly1 matToPolyMat
|
44 | 9, 43 | mpteq12dv 4733 |
. . . 4
Mat maDet Poly1var1 Mat Poly1 Mat
Poly1 Mat Poly1 matToPolyMat
|
45 | 44 | adantl 482 |
. . 3
Mat maDet Poly1var1 Mat Poly1 Mat
Poly1 Mat Poly1 matToPolyMat
|
46 | | simpl 473 |
. . 3
|
47 | | elex 3212 |
. . . 4
|
48 | 47 | adantl 482 |
. . 3
|
49 | | fvex 6201 |
. . . . 5
|
50 | 8, 49 | eqeltri 2697 |
. . . 4
|
51 | | mptexg 6484 |
. . . 4
|
52 | 50, 51 | mp1i 13 |
. . 3
|
53 | 3, 45, 46, 48, 52 | ovmpt2d 6788 |
. 2
CharPlyMat
|
54 | 1, 53 | syl5eq 2668 |
1
|