Step |
Hyp |
Ref |
Expression |
1 |
|
mdetfval1.d |
|- D = ( N maDet R ) |
2 |
|
mdetfval1.a |
|- A = ( N Mat R ) |
3 |
|
mdetfval1.b |
|- B = ( Base ` A ) |
4 |
|
mdetfval1.p |
|- P = ( Base ` ( SymGrp ` N ) ) |
5 |
|
mdetfval1.y |
|- Y = ( ZRHom ` R ) |
6 |
|
mdetfval1.s |
|- S = ( pmSgn ` N ) |
7 |
|
mdetfval1.t |
|- .x. = ( .r ` R ) |
8 |
|
mdetfval1.u |
|- U = ( mulGrp ` R ) |
9 |
1 2 3 4 5 6 7 8
|
mdetfval |
|- D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |
10 |
4 6
|
cofipsgn |
|- ( ( N e. Fin /\ p e. P ) -> ( ( Y o. S ) ` p ) = ( Y ` ( S ` p ) ) ) |
11 |
10
|
oveq1d |
|- ( ( N e. Fin /\ p e. P ) -> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) = ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) |
12 |
11
|
mpteq2dva |
|- ( N e. Fin -> ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) |
13 |
12
|
oveq2d |
|- ( N e. Fin -> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) = ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |
14 |
13
|
mpteq2dv |
|- ( N e. Fin -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
15 |
9 14
|
syl5eq |
|- ( N e. Fin -> D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
16 |
|
df-nel |
|- ( N e/ Fin <-> -. N e. Fin ) |
17 |
1
|
nfimdetndef |
|- ( N e/ Fin -> D = (/) ) |
18 |
2
|
fveq2i |
|- ( Base ` A ) = ( Base ` ( N Mat R ) ) |
19 |
3 18
|
eqtri |
|- B = ( Base ` ( N Mat R ) ) |
20 |
16
|
biimpi |
|- ( N e/ Fin -> -. N e. Fin ) |
21 |
20
|
intnanrd |
|- ( N e/ Fin -> -. ( N e. Fin /\ R e. _V ) ) |
22 |
|
matbas0 |
|- ( -. ( N e. Fin /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) ) |
23 |
21 22
|
syl |
|- ( N e/ Fin -> ( Base ` ( N Mat R ) ) = (/) ) |
24 |
19 23
|
syl5eq |
|- ( N e/ Fin -> B = (/) ) |
25 |
24
|
mpteq1d |
|- ( N e/ Fin -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
26 |
|
mpt0 |
|- ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) |
27 |
25 26
|
eqtrdi |
|- ( N e/ Fin -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) ) |
28 |
17 27
|
eqtr4d |
|- ( N e/ Fin -> D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
29 |
16 28
|
sylbir |
|- ( -. N e. Fin -> D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
30 |
15 29
|
pm2.61i |
|- D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |