Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mdet Unicode version

Definition df-mdet 27588
Description: Determinant of a square matrix... (Contributed by Stefan O'Rear, 9-Sep-2015.)
Assertion
Ref Expression
df-mdet  |- maDet  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( r  gsumg  ( p  e.  ( Base `  ( SymGrp `
 n ) ) 
|->  ( ( ( ZRHom `  r ) `  (
(pmSgn `  n ) `  p ) ) ( .r `  r ) ( (mulGrp `  r
)  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
Distinct variable group:    n, r, m, p, x

Detailed syntax breakdown of Definition df-mdet
StepHypRef Expression
1 cmdat 27586 . 2  class maDet
2 vn . . 3  set  n
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vm . . . 4  set  m
62cv 1631 . . . . . 6  class  n
73cv 1631 . . . . . 6  class  r
8 cmat 27543 . . . . . 6  class Mat
96, 7, 8co 5874 . . . . 5  class  ( n Mat  r )
10 cbs 13164 . . . . 5  class  Base
119, 10cfv 5271 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vp . . . . . 6  set  p
13 csymg 14785 . . . . . . . 8  class  SymGrp
146, 13cfv 5271 . . . . . . 7  class  ( SymGrp `  n )
1514, 10cfv 5271 . . . . . 6  class  ( Base `  ( SymGrp `  n )
)
1612cv 1631 . . . . . . . . 9  class  p
17 cpsgn 27517 . . . . . . . . . 10  class pmSgn
186, 17cfv 5271 . . . . . . . . 9  class  (pmSgn `  n )
1916, 18cfv 5271 . . . . . . . 8  class  ( (pmSgn `  n ) `  p
)
20 czrh 16467 . . . . . . . . 9  class  ZRHom
217, 20cfv 5271 . . . . . . . 8  class  ( ZRHom `  r )
2219, 21cfv 5271 . . . . . . 7  class  ( ( ZRHom `  r ) `  ( (pmSgn `  n
) `  p )
)
23 cmgp 15341 . . . . . . . . 9  class mulGrp
247, 23cfv 5271 . . . . . . . 8  class  (mulGrp `  r )
25 vx . . . . . . . . 9  set  x
2625cv 1631 . . . . . . . . . . 11  class  x
2726, 16cfv 5271 . . . . . . . . . 10  class  ( p `
 x )
285cv 1631 . . . . . . . . . 10  class  m
2927, 26, 28co 5874 . . . . . . . . 9  class  ( ( p `  x ) m x )
3025, 6, 29cmpt 4093 . . . . . . . 8  class  ( x  e.  n  |->  ( ( p `  x ) m x ) )
31 cgsu 13417 . . . . . . . 8  class  gsumg
3224, 30, 31co 5874 . . . . . . 7  class  ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) )
33 cmulr 13225 . . . . . . . 8  class  .r
347, 33cfv 5271 . . . . . . 7  class  ( .r
`  r )
3522, 32, 34co 5874 . . . . . 6  class  ( ( ( ZRHom `  r
) `  ( (pmSgn `  n ) `  p
) ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) )
3612, 15, 35cmpt 4093 . . . . 5  class  ( p  e.  ( Base `  ( SymGrp `
 n ) ) 
|->  ( ( ( ZRHom `  r ) `  (
(pmSgn `  n ) `  p ) ) ( .r `  r ) ( (mulGrp `  r
)  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) )
377, 36, 31co 5874 . . . 4  class  ( r 
gsumg  ( p  e.  ( Base `  ( SymGrp `  n
) )  |->  ( ( ( ZRHom `  r
) `  ( (pmSgn `  n ) `  p
) ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) ) ) )
385, 11, 37cmpt 4093 . . 3  class  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( r  gsumg  ( p  e.  (
Base `  ( SymGrp `  n ) )  |->  ( ( ( ZRHom `  r ) `  (
(pmSgn `  n ) `  p ) ) ( .r `  r ) ( (mulGrp `  r
)  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) ) ) )
392, 3, 4, 4, 38cmpt2 5876 . 2  class  ( n  e.  _V ,  r  e.  _V  |->  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( r  gsumg  ( p  e.  (
Base `  ( SymGrp `  n ) )  |->  ( ( ( ZRHom `  r ) `  (
(pmSgn `  n ) `  p ) ) ( .r `  r ) ( (mulGrp `  r
)  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
401, 39wceq 1632 1  wff maDet  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( r  gsumg  ( p  e.  ( Base `  ( SymGrp `
 n ) ) 
|->  ( ( ( ZRHom `  r ) `  (
(pmSgn `  n ) `  p ) ) ( .r `  r ) ( (mulGrp `  r
)  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  mdetfval  27590
  Copyright terms: Public domain W3C validator