Metamath Proof Explorer

Theorem mdetfval

Description: First substitution for the determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by SO, 9-Jul-2018)

Ref Expression
Hypotheses mdetfval.d 
|- D = ( N maDet R )
mdetfval.a 
|- A = ( N Mat R )
mdetfval.b 
|- B = ( Base ` A )
mdetfval.p 
|- P = ( Base ` ( SymGrp ` N ) )
mdetfval.y 
|- Y = ( ZRHom ` R )
mdetfval.s 
|- S = ( pmSgn ` N )
mdetfval.t 
|- .x. = ( .r ` R )
mdetfval.u 
|- U = ( mulGrp ` R )
Assertion mdetfval 
|- D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )

Proof

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 eqtrid 
 |-  ( -. ( 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 ) ) ) ) ) ) )