MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetfval Structured version   Unicode version

Theorem mdetfval 18412
Description: First substitution for the determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by SO, 9-Jul-2018.)
Hypotheses
Ref Expression
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
Ref Expression
mdetfval  |-  D  =  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )
Distinct variable groups:    B, m    m, p, x, N    P, m    R, m, p, x    S, m    .x. , m    U, m    m, Y
Allowed substitution hints:    A( x, m, p)    B( x, p)    D( x, m, p)    P( x, p)    S( x, p)    .x. ( x, p)    U( x, p)    Y( x, p)

Proof of Theorem mdetfval
Dummy variables  y 
z  n  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetfval.d . 2  |-  D  =  ( N maDet  R )
2 oveq12 6115 . . . . . . . 8  |-  ( ( n  =  N  /\  r  =  R )  ->  ( n Mat  r )  =  ( N Mat  R
) )
3 mdetfval.a . . . . . . . 8  |-  A  =  ( N Mat  R )
42, 3syl6eqr 2493 . . . . . . 7  |-  ( ( n  =  N  /\  r  =  R )  ->  ( n Mat  r )  =  A )
54fveq2d 5710 . . . . . 6  |-  ( ( n  =  N  /\  r  =  R )  ->  ( Base `  (
n Mat  r ) )  =  ( Base `  A
) )
6 mdetfval.b . . . . . 6  |-  B  =  ( Base `  A
)
75, 6syl6eqr 2493 . . . . 5  |-  ( ( n  =  N  /\  r  =  R )  ->  ( Base `  (
n Mat  r ) )  =  B )
8 simpr 461 . . . . . 6  |-  ( ( n  =  N  /\  r  =  R )  ->  r  =  R )
9 simpl 457 . . . . . . . . . 10  |-  ( ( n  =  N  /\  r  =  R )  ->  n  =  N )
109fveq2d 5710 . . . . . . . . 9  |-  ( ( n  =  N  /\  r  =  R )  ->  ( SymGrp `  n )  =  ( SymGrp `  N
) )
1110fveq2d 5710 . . . . . . . 8  |-  ( ( n  =  N  /\  r  =  R )  ->  ( Base `  ( SymGrp `
 n ) )  =  ( Base `  ( SymGrp `
 N ) ) )
12 mdetfval.p . . . . . . . 8  |-  P  =  ( Base `  ( SymGrp `
 N ) )
1311, 12syl6eqr 2493 . . . . . . 7  |-  ( ( n  =  N  /\  r  =  R )  ->  ( Base `  ( SymGrp `
 n ) )  =  P )
14 fveq2 5706 . . . . . . . . . 10  |-  ( r  =  R  ->  ( .r `  r )  =  ( .r `  R
) )
1514adantl 466 . . . . . . . . 9  |-  ( ( n  =  N  /\  r  =  R )  ->  ( .r `  r
)  =  ( .r
`  R ) )
16 mdetfval.t . . . . . . . . 9  |-  .x.  =  ( .r `  R )
1715, 16syl6eqr 2493 . . . . . . . 8  |-  ( ( n  =  N  /\  r  =  R )  ->  ( .r `  r
)  =  .x.  )
188fveq2d 5710 . . . . . . . . . . 11  |-  ( ( n  =  N  /\  r  =  R )  ->  ( ZRHom `  r
)  =  ( ZRHom `  R ) )
19 mdetfval.y . . . . . . . . . . 11  |-  Y  =  ( ZRHom `  R
)
2018, 19syl6eqr 2493 . . . . . . . . . 10  |-  ( ( n  =  N  /\  r  =  R )  ->  ( ZRHom `  r
)  =  Y )
21 fveq2 5706 . . . . . . . . . . . 12  |-  ( n  =  N  ->  (pmSgn `  n )  =  (pmSgn `  N ) )
2221adantr 465 . . . . . . . . . . 11  |-  ( ( n  =  N  /\  r  =  R )  ->  (pmSgn `  n )  =  (pmSgn `  N )
)
23 mdetfval.s . . . . . . . . . . 11  |-  S  =  (pmSgn `  N )
2422, 23syl6eqr 2493 . . . . . . . . . 10  |-  ( ( n  =  N  /\  r  =  R )  ->  (pmSgn `  n )  =  S )
2520, 24coeq12d 5019 . . . . . . . . 9  |-  ( ( n  =  N  /\  r  =  R )  ->  ( ( ZRHom `  r )  o.  (pmSgn `  n ) )  =  ( Y  o.  S
) )
2625fveq1d 5708 . . . . . . . 8  |-  ( ( n  =  N  /\  r  =  R )  ->  ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p )  =  ( ( Y  o.  S
) `  p )
)
27 fveq2 5706 . . . . . . . . . . 11  |-  ( r  =  R  ->  (mulGrp `  r )  =  (mulGrp `  R ) )
2827adantl 466 . . . . . . . . . 10  |-  ( ( n  =  N  /\  r  =  R )  ->  (mulGrp `  r )  =  (mulGrp `  R )
)
29 mdetfval.u . . . . . . . . . 10  |-  U  =  (mulGrp `  R )
3028, 29syl6eqr 2493 . . . . . . . . 9  |-  ( ( n  =  N  /\  r  =  R )  ->  (mulGrp `  r )  =  U )
319mpteq1d 4388 . . . . . . . . 9  |-  ( ( n  =  N  /\  r  =  R )  ->  ( x  e.  n  |->  ( ( p `  x ) m x ) )  =  ( x  e.  N  |->  ( ( p `  x
) m x ) ) )
3230, 31oveq12d 6124 . . . . . . . 8  |-  ( ( n  =  N  /\  r  =  R )  ->  ( (mulGrp `  r
)  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) )  =  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) )
3317, 26, 32oveq123d 6127 . . . . . . 7  |-  ( ( n  =  N  /\  r  =  R )  ->  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n )
) `  p )
( .r `  r
) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) )  =  ( ( ( Y  o.  S ) `
 p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) )
3413, 33mpteq12dv 4385 . . . . . 6  |-  ( ( n  =  N  /\  r  =  R )  ->  ( p  e.  (
Base `  ( SymGrp `  n ) )  |->  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) ) )  =  ( p  e.  P  |->  ( ( ( Y  o.  S ) `
 p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) )
358, 34oveq12d 6124 . . . . 5  |-  ( ( n  =  N  /\  r  =  R )  ->  ( r  gsumg  ( p  e.  (
Base `  ( SymGrp `  n ) )  |->  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) ) ) )  =  ( R 
gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )
367, 35mpteq12dv 4385 . . . 4  |-  ( ( n  =  N  /\  r  =  R )  ->  ( m  e.  (
Base `  ( n Mat  r ) )  |->  ( r  gsumg  ( p  e.  (
Base `  ( SymGrp `  n ) )  |->  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) ) ) ) )  =  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
37 df-mdet 18411 . . . 4  |- maDet  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( r  gsumg  ( p  e.  ( Base `  ( SymGrp `
 n ) ) 
|->  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n )
) `  p )
( .r `  r
) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
38 fvex 5716 . . . . . 6  |-  ( Base `  A )  e.  _V
396, 38eqeltri 2513 . . . . 5  |-  B  e. 
_V
4039mptex 5963 . . . 4  |-  ( m  e.  B  |->  ( R 
gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )  e. 
_V
4136, 37, 40ovmpt2a 6236 . . 3  |-  ( ( N  e.  _V  /\  R  e.  _V )  ->  ( N maDet  R )  =  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S
) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
4237reldmmpt2 6216 . . . . . 6  |-  Rel  dom maDet
4342ovprc 6133 . . . . 5  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( N maDet  R )  =  (/) )
44 mpt0 5553 . . . . 5  |-  ( m  e.  (/)  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S
) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )  =  (/)
4543, 44syl6eqr 2493 . . . 4  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( N maDet  R )  =  ( m  e.  (/)  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S
) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
46 df-mat 18297 . . . . . . . . . 10  |- Mat  =  ( y  e.  Fin , 
z  e.  _V  |->  ( ( z freeLMod  ( y  X.  y ) ) sSet  <. ( .r `  ndx ) ,  ( z maMul  <.
y ,  y ,  y >. ) >. )
)
4746reldmmpt2 6216 . . . . . . . . 9  |-  Rel  dom Mat
4847ovprc 6133 . . . . . . . 8  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( N Mat  R )  =  (/) )
493, 48syl5eq 2487 . . . . . . 7  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  A  =  (/) )
5049fveq2d 5710 . . . . . 6  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( Base `  A
)  =  ( Base `  (/) ) )
51 base0 14228 . . . . . 6  |-  (/)  =  (
Base `  (/) )
5250, 6, 513eqtr4g 2500 . . . . 5  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  B  =  (/) )
5352mpteq1d 4388 . . . 4  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )  =  ( m  e.  (/)  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
5445, 53eqtr4d 2478 . . 3  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( N maDet  R )  =  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S
) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
5541, 54pm2.61i 164 . 2  |-  ( N maDet 
R )  =  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )
561, 55eqtri 2463 1  |-  D  =  ( m  e.  B  |->  ( R  gsumg  ( p  e.  P  |->  ( ( ( Y  o.  S ) `  p )  .x.  ( U  gsumg  ( x  e.  N  |->  ( ( p `  x ) m x ) ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369    = wceq 1369    e. wcel 1756   _Vcvv 2987   (/)c0 3652   <.cop 3898   <.cotp 3900    e. cmpt 4365    X. cxp 4853    o. ccom 4859   ` cfv 5433  (class class class)co 6106   Fincfn 7325   ndxcnx 14186   sSet csts 14187   Basecbs 14189   .rcmulr 14254    gsumg cgsu 14394   SymGrpcsymg 15897  pmSgncpsgn 16010  mulGrpcmgp 16606   ZRHomczrh 17946   freeLMod cfrlm 18186   maMul cmmul 18294   Mat cmat 18295   maDet cmdat 18410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-reu 2737  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-slot 14193  df-base 14194  df-mat 18297  df-mdet 18411
This theorem is referenced by:  mdetleib  18413  nfimdetndef  18415  mdetfval1  18416  mdet0pr  18418  mdetf  18421
  Copyright terms: Public domain W3C validator