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 ) ) ) ) ) ) ) )