Description: The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | chpmat0.c | |
|
Assertion | chpmat0d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chpmat0.c | |
|
2 | 0fin | |
|
3 | id | |
|
4 | 0ex | |
|
5 | 4 | snid | |
6 | mat0dimbas0 | |
|
7 | 5 6 | eleqtrrid | |
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | eqid | |
|
17 | eqid | |
|
18 | 1 8 9 10 11 12 13 14 15 16 17 | chpmatval | |
19 | 2 3 7 18 | mp3an2i | |
20 | 10 | ply1ring | |
21 | mdet0pr | |
|
22 | 21 | fveq1d | |
23 | 20 22 | syl | |
24 | 11 | mat0dimid | |
25 | 20 24 | syl | |
26 | 25 | oveq2d | |
27 | eqid | |
|
28 | 14 10 27 | vr1cl | |
29 | 11 | mat0dimscm | |
30 | 20 28 29 | syl2anc | |
31 | 26 30 | eqtrd | |
32 | d0mat2pmat | |
|
33 | 31 32 | oveq12d | |
34 | 11 | matring | |
35 | 2 20 34 | sylancr | |
36 | ringgrp | |
|
37 | 35 36 | syl | |
38 | mat0dimbas0 | |
|
39 | 20 38 | syl | |
40 | 5 39 | eleqtrrid | |
41 | eqid | |
|
42 | eqid | |
|
43 | 41 42 13 | grpsubid | |
44 | 37 40 43 | syl2anc | |
45 | 33 44 | eqtrd | |
46 | 45 | fveq2d | |
47 | 11 | mat0dim0 | |
48 | 20 47 | syl | |
49 | 48 | fveq2d | |
50 | fvex | |
|
51 | 4 50 | fvsn | |
52 | 49 51 | eqtrdi | |
53 | 46 52 | eqtrd | |
54 | 23 53 | eqtrd | |
55 | 19 54 | eqtrd | |