Step |
Hyp |
Ref |
Expression |
1 |
|
nfimdetndef.d |
|- D = ( N maDet R ) |
2 |
|
eqid |
|- ( N Mat R ) = ( N Mat R ) |
3 |
|
eqid |
|- ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) ) |
4 |
|
eqid |
|- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) ) |
5 |
|
eqid |
|- ( ZRHom ` R ) = ( ZRHom ` R ) |
6 |
|
eqid |
|- ( pmSgn ` N ) = ( pmSgn ` N ) |
7 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
8 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
9 |
1 2 3 4 5 6 7 8
|
mdetfval |
|- D = ( m e. ( Base ` ( N Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |
10 |
|
df-nel |
|- ( N e/ Fin <-> -. N e. Fin ) |
11 |
10
|
biimpi |
|- ( N e/ Fin -> -. N e. Fin ) |
12 |
11
|
intnanrd |
|- ( N e/ Fin -> -. ( N e. Fin /\ R e. _V ) ) |
13 |
|
matbas0 |
|- ( -. ( N e. Fin /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) ) |
14 |
12 13
|
syl |
|- ( N e/ Fin -> ( Base ` ( N Mat R ) ) = (/) ) |
15 |
14
|
mpteq1d |
|- ( N e/ Fin -> ( m e. ( Base ` ( N Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. (/) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
16 |
|
mpt0 |
|- ( m e. (/) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) |
17 |
15 16
|
eqtrdi |
|- ( N e/ Fin -> ( m e. ( Base ` ( N Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) ) |
18 |
9 17
|
syl5eq |
|- ( N e/ Fin -> D = (/) ) |