This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mdet

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib ). 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". Functionality is shown by mdetf . Multilineary means "linear for each row" - the additivity is shown by mdetrlin , the homogeneity by mdetrsca . Furthermore, it is shown that the determinant function is alternating (see mdetralt ) and normalized (see mdet1 ). Finally, uniqueness is shown by mdetuni . As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib . (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by SO, 10-Jul-2018)

Ref Expression
Assertion df-mdet 
|- maDet = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( r gsum ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdat 
 |-  maDet
1 vn 
 |-  n
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vm 
 |-  m
5 cbs 
 |-  Base
6 1 cv 
 |-  n
7 cmat 
 |-  Mat
8 3 cv 
 |-  r
9 6 8 7 co 
 |-  ( n Mat r )
10 9 5 cfv 
 |-  ( Base ` ( n Mat r ) )
11 cgsu 
 |-  gsum
12 vp 
 |-  p
13 csymg 
 |-  SymGrp
14 6 13 cfv 
 |-  ( SymGrp ` n )
15 14 5 cfv 
 |-  ( Base ` ( SymGrp ` n ) )
16 czrh 
 |-  ZRHom
17 8 16 cfv 
 |-  ( ZRHom ` r )
18 cpsgn 
 |-  pmSgn
19 6 18 cfv 
 |-  ( pmSgn ` n )
20 17 19 ccom 
 |-  ( ( ZRHom ` r ) o. ( pmSgn ` n ) )
21 12 cv 
 |-  p
22 21 20 cfv 
 |-  ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p )
23 cmulr 
 |-  .r
24 8 23 cfv 
 |-  ( .r ` r )
25 cmgp 
 |-  mulGrp
26 8 25 cfv 
 |-  ( mulGrp ` r )
27 vx 
 |-  x
28 27 cv 
 |-  x
29 28 21 cfv 
 |-  ( p ` x )
30 4 cv 
 |-  m
31 29 28 30 co 
 |-  ( ( p ` x ) m x )
32 27 6 31 cmpt 
 |-  ( x e. n |-> ( ( p ` x ) m x ) )
33 26 32 11 co 
 |-  ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) )
34 22 33 24 co 
 |-  ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) )
35 12 15 34 cmpt 
 |-  ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) )
36 8 35 11 co 
 |-  ( r gsum ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) ) )
37 4 10 36 cmpt 
 |-  ( m e. ( Base ` ( n Mat r ) ) |-> ( r gsum ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) ) ) )
38 1 3 2 2 37 cmpo 
 |-  ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( r gsum ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
39 0 38 wceq 
 |-  maDet = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( r gsum ( p e. ( Base ` ( SymGrp ` n ) ) |-> ( ( ( ( ZRHom ` r ) o. ( pmSgn ` n ) ) ` p ) ( .r ` r ) ( ( mulGrp ` r ) gsum ( x e. n |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )