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

Definition df-mdet 19172
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 19174). 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 19182. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 19189, the homogeneity by mdetrsca 19190. Furthermore, it is shown that the determinant function is alternating (see mdetralt 19195) and normalized (see mdet1 19188). Finally, the uniqueness is shown by mdetuni 19209. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 19174. (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 19171 . 2  class maDet
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3034 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1398 . . . . . 6  class  n
73cv 1398 . . . . . 6  class  r
8 cmat 18994 . . . . . 6  class Mat
96, 7, 8co 6196 . . . . 5  class  ( n Mat  r )
10 cbs 14634 . . . . 5  class  Base
119, 10cfv 5496 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vp . . . . . 6  setvar  p
13 csymg 16519 . . . . . . . 8  class  SymGrp
146, 13cfv 5496 . . . . . . 7  class  ( SymGrp `  n )
1514, 10cfv 5496 . . . . . 6  class  ( Base `  ( SymGrp `  n )
)
1612cv 1398 . . . . . . . 8  class  p
17 czrh 18630 . . . . . . . . . 10  class  ZRHom
187, 17cfv 5496 . . . . . . . . 9  class  ( ZRHom `  r )
19 cpsgn 16631 . . . . . . . . . 10  class pmSgn
206, 19cfv 5496 . . . . . . . . 9  class  (pmSgn `  n )
2118, 20ccom 4917 . . . . . . . 8  class  ( ( ZRHom `  r )  o.  (pmSgn `  n )
)
2216, 21cfv 5496 . . . . . . 7  class  ( ( ( ZRHom `  r
)  o.  (pmSgn `  n ) ) `  p )
23 cmgp 17254 . . . . . . . . 9  class mulGrp
247, 23cfv 5496 . . . . . . . 8  class  (mulGrp `  r )
25 vx . . . . . . . . 9  setvar  x
2625cv 1398 . . . . . . . . . . 11  class  x
2726, 16cfv 5496 . . . . . . . . . 10  class  ( p `
 x )
285cv 1398 . . . . . . . . . 10  class  m
2927, 26, 28co 6196 . . . . . . . . 9  class  ( ( p `  x ) m x )
3025, 6, 29cmpt 4425 . . . . . . . 8  class  ( x  e.  n  |->  ( ( p `  x ) m x ) )
31 cgsu 14848 . . . . . . . 8  class  gsumg
3224, 30, 31co 6196 . . . . . . 7  class  ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) )
33 cmulr 14703 . . . . . . . 8  class  .r
347, 33cfv 5496 . . . . . . 7  class  ( .r
`  r )
3522, 32, 34co 6196 . . . . . 6  class  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) )
3612, 15, 35cmpt 4425 . . . . 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 6196 . . . 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 4425 . . 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 6198 . 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 1399 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  19173
  Copyright terms: Public domain W3C validator