Step |
Hyp |
Ref |
Expression |
1 |
|
chpmatply1.c |
|- C = ( N CharPlyMat R ) |
2 |
|
chpmatply1.a |
|- A = ( N Mat R ) |
3 |
|
chpmatply1.b |
|- B = ( Base ` A ) |
4 |
|
chpmatply1.p |
|- P = ( Poly1 ` R ) |
5 |
|
chpmatval2.y |
|- Y = ( N Mat P ) |
6 |
|
chpmatval2.m1 |
|- .- = ( -g ` Y ) |
7 |
|
chpmatval2.x |
|- X = ( var1 ` R ) |
8 |
|
chpmatval2.t1 |
|- .x. = ( .s ` Y ) |
9 |
|
chpmatval2.t |
|- T = ( N matToPolyMat R ) |
10 |
|
chpmatval2.i |
|- .1. = ( 1r ` Y ) |
11 |
|
chpmatval2.g |
|- G = ( SymGrp ` N ) |
12 |
|
chpmatval2.h |
|- H = ( Base ` G ) |
13 |
|
chpmatval2.z |
|- Z = ( ZRHom ` P ) |
14 |
|
chpmatval2.s |
|- S = ( pmSgn ` N ) |
15 |
|
chpmatval2.u |
|- U = ( mulGrp ` P ) |
16 |
|
chpmatval2.rm |
|- .X. = ( .r ` P ) |
17 |
|
eqid |
|- ( N maDet P ) = ( N maDet P ) |
18 |
1 2 3 4 5 17 6 7 8 9 10
|
chpmatval |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) ) |
19 |
|
eqid |
|- ( N Mat P ) = ( N Mat P ) |
20 |
5
|
fveq2i |
|- ( -g ` Y ) = ( -g ` ( N Mat P ) ) |
21 |
6 20
|
eqtri |
|- .- = ( -g ` ( N Mat P ) ) |
22 |
5
|
fveq2i |
|- ( .s ` Y ) = ( .s ` ( N Mat P ) ) |
23 |
8 22
|
eqtri |
|- .x. = ( .s ` ( N Mat P ) ) |
24 |
5
|
fveq2i |
|- ( 1r ` Y ) = ( 1r ` ( N Mat P ) ) |
25 |
10 24
|
eqtri |
|- .1. = ( 1r ` ( N Mat P ) ) |
26 |
|
eqid |
|- ( ( X .x. .1. ) .- ( T ` M ) ) = ( ( X .x. .1. ) .- ( T ` M ) ) |
27 |
2 3 4 19 7 9 21 23 25 26
|
chmatcl |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` ( N Mat P ) ) ) |
28 |
5
|
eqcomi |
|- ( N Mat P ) = Y |
29 |
28
|
fveq2i |
|- ( Base ` ( N Mat P ) ) = ( Base ` Y ) |
30 |
11
|
fveq2i |
|- ( Base ` G ) = ( Base ` ( SymGrp ` N ) ) |
31 |
12 30
|
eqtri |
|- H = ( Base ` ( SymGrp ` N ) ) |
32 |
17 5 29 31 13 14 16 15
|
mdetleib |
|- ( ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` ( N Mat P ) ) -> ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) ) |
33 |
27 32
|
syl |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) ) |
34 |
18 33
|
eqtrd |
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( C ` M ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) ) |