Step |
Hyp |
Ref |
Expression |
1 |
|
mdetfval.d |
|- D = ( N maDet R ) |
2 |
|
mdetfval.a |
|- A = ( N Mat R ) |
3 |
|
mdetfval.b |
|- B = ( Base ` A ) |
4 |
|
mdetfval.p |
|- P = ( Base ` ( SymGrp ` N ) ) |
5 |
|
mdetfval.y |
|- Y = ( ZRHom ` R ) |
6 |
|
mdetfval.s |
|- S = ( pmSgn ` N ) |
7 |
|
mdetfval.t |
|- .x. = ( .r ` R ) |
8 |
|
mdetfval.u |
|- U = ( mulGrp ` R ) |
9 |
|
oveq12 |
|- ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) ) |
10 |
9 2
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( n Mat r ) = A ) |
11 |
10
|
fveq2d |
|- ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = ( Base ` A ) ) |
12 |
11 3
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = B ) |
13 |
|
simpr |
|- ( ( n = N /\ r = R ) -> r = R ) |
14 |
|
simpl |
|- ( ( n = N /\ r = R ) -> n = N ) |
15 |
14
|
fveq2d |
|- ( ( n = N /\ r = R ) -> ( SymGrp ` n ) = ( SymGrp ` N ) ) |
16 |
15
|
fveq2d |
|- ( ( n = N /\ r = R ) -> ( Base ` ( SymGrp ` n ) ) = ( Base ` ( SymGrp ` N ) ) ) |
17 |
16 4
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( Base ` ( SymGrp ` n ) ) = P ) |
18 |
|
fveq2 |
|- ( r = R -> ( .r ` r ) = ( .r ` R ) ) |
19 |
18
|
adantl |
|- ( ( n = N /\ r = R ) -> ( .r ` r ) = ( .r ` R ) ) |
20 |
19 7
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( .r ` r ) = .x. ) |
21 |
13
|
fveq2d |
|- ( ( n = N /\ r = R ) -> ( ZRHom ` r ) = ( ZRHom ` R ) ) |
22 |
21 5
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( ZRHom ` r ) = Y ) |
23 |
|
fveq2 |
|- ( n = N -> ( pmSgn ` n ) = ( pmSgn ` N ) ) |
24 |
23
|
adantr |
|- ( ( n = N /\ r = R ) -> ( pmSgn ` n ) = ( pmSgn ` N ) ) |
25 |
24 6
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( pmSgn ` n ) = S ) |
26 |
22 25
|
coeq12d |
|- ( ( n = N /\ r = R ) -> ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) = ( Y o. S ) ) |
27 |
26
|
fveq1d |
|- ( ( n = N /\ r = R ) -> ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) = ( ( Y o. S ) ` p ) ) |
28 |
|
fveq2 |
|- ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) ) |
29 |
28
|
adantl |
|- ( ( n = N /\ r = R ) -> ( mulGrp ` r ) = ( mulGrp ` R ) ) |
30 |
29 8
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( mulGrp ` r ) = U ) |
31 |
14
|
mpteq1d |
|- ( ( n = N /\ r = R ) -> ( x e. n |-> ( ( p ` x ) m x ) ) = ( x e. N |-> ( ( p ` x ) m x ) ) ) |
32 |
30 31
|
oveq12d |
|- ( ( n = N /\ r = R ) -> ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) = ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) |
33 |
20 27 32
|
oveq123d |
|- ( ( n = N /\ r = R ) -> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) = ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) |
34 |
17 33
|
mpteq12dv |
|- ( ( n = N /\ r = R ) -> ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) |
35 |
13 34
|
oveq12d |
|- ( ( n = N /\ r = 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 ) ) ) ) ) ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |
36 |
12 35
|
mpteq12dv |
|- ( ( n = N /\ r = R ) -> ( 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. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
37 |
|
df-mdet |
|- maDet = ( n e. _V , r e. _V |-> ( 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 ) ) ) ) ) ) ) ) |
38 |
3
|
fvexi |
|- B e. _V |
39 |
38
|
mptex |
|- ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) e. _V |
40 |
36 37 39
|
ovmpoa |
|- ( ( N e. _V /\ R e. _V ) -> ( N maDet R ) = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
41 |
37
|
reldmmpo |
|- Rel dom maDet |
42 |
41
|
ovprc |
|- ( -. ( N e. _V /\ R e. _V ) -> ( N maDet R ) = (/) ) |
43 |
|
mpt0 |
|- ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = (/) |
44 |
42 43
|
eqtr4di |
|- ( -. ( N e. _V /\ R e. _V ) -> ( N maDet R ) = ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
45 |
|
df-mat |
|- Mat = ( y e. Fin , z e. _V |-> ( ( z freeLMod ( y X. y ) ) sSet <. ( .r ` ndx ) , ( z maMul <. y , y , y >. ) >. ) ) |
46 |
45
|
reldmmpo |
|- Rel dom Mat |
47 |
46
|
ovprc |
|- ( -. ( N e. _V /\ R e. _V ) -> ( N Mat R ) = (/) ) |
48 |
2 47
|
syl5eq |
|- ( -. ( N e. _V /\ R e. _V ) -> A = (/) ) |
49 |
48
|
fveq2d |
|- ( -. ( N e. _V /\ R e. _V ) -> ( Base ` A ) = ( Base ` (/) ) ) |
50 |
|
base0 |
|- (/) = ( Base ` (/) ) |
51 |
49 3 50
|
3eqtr4g |
|- ( -. ( N e. _V /\ R e. _V ) -> B = (/) ) |
52 |
51
|
mpteq1d |
|- ( -. ( N e. _V /\ R e. _V ) -> ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. (/) |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
53 |
44 52
|
eqtr4d |
|- ( -. ( N e. _V /\ R e. _V ) -> ( N maDet R ) = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) ) |
54 |
40 53
|
pm2.61i |
|- ( N maDet R ) = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |
55 |
1 54
|
eqtri |
|- D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) ) |