Step |
Hyp |
Ref |
Expression |
0 |
|
cchpmat |
|- CharPlyMat |
1 |
|
vn |
|- n |
2 |
|
cfn |
|- Fin |
3 |
|
vr |
|- r |
4 |
|
cvv |
|- _V |
5 |
|
vm |
|- m |
6 |
|
cbs |
|- Base |
7 |
1
|
cv |
|- n |
8 |
|
cmat |
|- Mat |
9 |
3
|
cv |
|- r |
10 |
7 9 8
|
co |
|- ( n Mat r ) |
11 |
10 6
|
cfv |
|- ( Base ` ( n Mat r ) ) |
12 |
|
cmdat |
|- maDet |
13 |
|
cpl1 |
|- Poly1 |
14 |
9 13
|
cfv |
|- ( Poly1 ` r ) |
15 |
7 14 12
|
co |
|- ( n maDet ( Poly1 ` r ) ) |
16 |
|
cv1 |
|- var1 |
17 |
9 16
|
cfv |
|- ( var1 ` r ) |
18 |
|
cvsca |
|- .s |
19 |
7 14 8
|
co |
|- ( n Mat ( Poly1 ` r ) ) |
20 |
19 18
|
cfv |
|- ( .s ` ( n Mat ( Poly1 ` r ) ) ) |
21 |
|
cur |
|- 1r |
22 |
19 21
|
cfv |
|- ( 1r ` ( n Mat ( Poly1 ` r ) ) ) |
23 |
17 22 20
|
co |
|- ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) |
24 |
|
csg |
|- -g |
25 |
19 24
|
cfv |
|- ( -g ` ( n Mat ( Poly1 ` r ) ) ) |
26 |
|
cmat2pmat |
|- matToPolyMat |
27 |
7 9 26
|
co |
|- ( n matToPolyMat r ) |
28 |
5
|
cv |
|- m |
29 |
28 27
|
cfv |
|- ( ( n matToPolyMat r ) ` m ) |
30 |
23 29 25
|
co |
|- ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) |
31 |
30 15
|
cfv |
|- ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) |
32 |
5 11 31
|
cmpt |
|- ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) |
33 |
1 3 2 4 32
|
cmpo |
|- ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) ) |
34 |
0 33
|
wceq |
|- CharPlyMat = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) ) |