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

Definition df-mdet 18395
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 18397). 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 18405. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 18408, the homogeneity by mdetrsca 18409. Furthermore, it is shown that the determinant function is alternating (see mdetralt 18413) and normalized (see mdet1 18407). Finally, the uniqueness is shown by mdetuni 18427. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 18397. (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 18394 . 2  class maDet
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 2971 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1368 . . . . . 6  class  n
73cv 1368 . . . . . 6  class  r
8 cmat 18279 . . . . . 6  class Mat
96, 7, 8co 6090 . . . . 5  class  ( n Mat  r )
10 cbs 14173 . . . . 5  class  Base
119, 10cfv 5417 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vp . . . . . 6  setvar  p
13 csymg 15881 . . . . . . . 8  class  SymGrp
146, 13cfv 5417 . . . . . . 7  class  ( SymGrp `  n )
1514, 10cfv 5417 . . . . . 6  class  ( Base `  ( SymGrp `  n )
)
1612cv 1368 . . . . . . . 8  class  p
17 czrh 17930 . . . . . . . . . 10  class  ZRHom
187, 17cfv 5417 . . . . . . . . 9  class  ( ZRHom `  r )
19 cpsgn 15994 . . . . . . . . . 10  class pmSgn
206, 19cfv 5417 . . . . . . . . 9  class  (pmSgn `  n )
2118, 20ccom 4843 . . . . . . . 8  class  ( ( ZRHom `  r )  o.  (pmSgn `  n )
)
2216, 21cfv 5417 . . . . . . 7  class  ( ( ( ZRHom `  r
)  o.  (pmSgn `  n ) ) `  p )
23 cmgp 16590 . . . . . . . . 9  class mulGrp
247, 23cfv 5417 . . . . . . . 8  class  (mulGrp `  r )
25 vx . . . . . . . . 9  setvar  x
2625cv 1368 . . . . . . . . . . 11  class  x
2726, 16cfv 5417 . . . . . . . . . 10  class  ( p `
 x )
285cv 1368 . . . . . . . . . 10  class  m
2927, 26, 28co 6090 . . . . . . . . 9  class  ( ( p `  x ) m x )
3025, 6, 29cmpt 4349 . . . . . . . 8  class  ( x  e.  n  |->  ( ( p `  x ) m x ) )
31 cgsu 14378 . . . . . . . 8  class  gsumg
3224, 30, 31co 6090 . . . . . . 7  class  ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x ) m x ) ) )
33 cmulr 14238 . . . . . . . 8  class  .r
347, 33cfv 5417 . . . . . . 7  class  ( .r
`  r )
3522, 32, 34co 6090 . . . . . 6  class  ( ( ( ( ZRHom `  r )  o.  (pmSgn `  n ) ) `  p ) ( .r
`  r ) ( (mulGrp `  r )  gsumg  ( x  e.  n  |->  ( ( p `  x
) m x ) ) ) )
3612, 15, 35cmpt 4349 . . . . 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 6090 . . . 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 4349 . . 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 6092 . 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 1369 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  18396
  Copyright terms: Public domain W3C validator