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

Definition df-mdet 18849
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 18851). The properties of the axiomatic definition of a determinant according to [Weierstrass] p. 272 are derived from this definition as theorems: "The determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring". The functionality is shown by mdetf 18859. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 18866, the homogeneity by mdetrsca 18867. Furthermore, it is shown that the determinant function is alternating (see mdetralt 18872) and normalized (see mdet1 18865). Finally, the uniqueness is shown by mdetuni 18886. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 18851. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by SO, 10-Jul-2018.)
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 )  o.  (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 18848 . 2  class maDet
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3108 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1373 . . . . . 6  class  n
73cv 1373 . . . . . 6  class  r
8 cmat 18671 . . . . . 6  class Mat
96, 7, 8co 6277 . . . . 5  class  ( n Mat  r )
10 cbs 14481 . . . . 5  class  Base
119, 10cfv 5581 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vp . . . . . 6  setvar  p
13 csymg 16192 . . . . . . . 8  class  SymGrp
146, 13cfv 5581 . . . . . . 7  class  ( SymGrp `  n )
1514, 10cfv 5581 . . . . . 6  class  ( Base `  ( SymGrp `  n )
)
1612cv 1373 . . . . . . . 8  class  p
17 czrh 18299 . . . . . . . . . 10  class  ZRHom
187, 17cfv 5581 . . . . . . . . 9  class  ( ZRHom `  r )
19 cpsgn 16305 . . . . . . . . . 10  class pmSgn
206, 19cfv 5581 . . . . . . . . 9  class  (pmSgn `  n )
2118, 20ccom 4998 . . . . . . . 8  class  ( ( ZRHom `  r )  o.  (pmSgn `  n )
)
2216, 21cfv 5581 . . . . . . 7  class  ( ( ( ZRHom `  r
)  o.  (pmSgn `  n ) ) `  p )
23 cmgp 16926 . . . . . . . . 9  class mulGrp
247, 23cfv 5581 . . . . . . . 8  class  (mulGrp `  r )
25 vx . . . . . . . . 9  setvar  x
2625cv 1373 . . . . . . . . . . 11  class  x
2726, 16cfv 5581 . . . . . . . . . 10  class  ( p `
 x )
285cv 1373 . . . . . . . . . 10  class  m
2927, 26, 28co 6277 . . . . . . . . 9  class  ( ( p `  x ) m x )
3025, 6, 29cmpt 4500 . . . . . . . 8  class  ( x  e.  n  |->  ( ( p `  x ) m x ) )
31 cgsu 14687 . . . . . . . 8  class  gsumg
3224, 30, 31co 6277 . . . . . . 7  class  ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) )
33 cmulr 14547 . . . . . . . 8  class  .r
347, 33cfv 5581 . . . . . . 7  class  ( .r
`  r )
3522, 32, 34co 6277 . . . . . 6  class  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) )
3612, 15, 35cmpt 4500 . . . . 5  class  ( p  e.  ( Base `  ( SymGrp `
 n ) ) 
|->  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n )
) `  p )
( .r `  r
) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) ) ) )
377, 36, 31co 6277 . . . 4  class  ( 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 ) ) ) ) ) )
385, 11, 37cmpt 4500 . . 3  class  ( 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 ) ) ) ) ) ) )
392, 3, 4, 4, 38cmpt2 6279 . 2  class  ( 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 ) ) ) ) ) ) ) )
401, 39wceq 1374 1  wff 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 ) ) ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mdetfval  18850
  Copyright terms: Public domain W3C validator