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	$$⊢\mathrm{maDet}=\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}}{{\sum }_r}\left(\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmdat	$$class\mathrm{maDet}$$
1		vn	$$setvarn$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vm	$$setvarm$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvarn$$
7		cmat	$$class\mathrm{Mat}$$
8	3	cv	$$setvarr$$
9	6 8 7	co	$$class\left(n\mathrm{Mat}r\right)$$
10	9 5	cfv	$$class{\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}$$
11		cgsu	$$class{\Sigma }_{𝑔}$$
12		vp	$$setvarp$$
13		csymg	$$class\mathrm{SymGrp}$$
14	6 13	cfv	$$class\mathrm{SymGrp}\left(n\right)$$
15	14 5	cfv	$$class{\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}$$
16		czrh	$$class\mathrm{\mathbb{Z}RHom}$$
17	8 16	cfv	$$class\mathrm{\mathbb{Z}RHom}\left(r\right)$$
18		cpsgn	$$class\mathrm{pmSgn}$$
19	6 18	cfv	$$class\mathrm{pmSgn}\left(n\right)$$
20	17 19	ccom	$$class\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)$$
21	12	cv	$$setvarp$$
22	21 20	cfv	$$class\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right)$$
23		cmulr	$$class{\cdot }_{𝑟}$$
24	8 23	cfv	$$class{\cdot }_r$$
25		cmgp	$$class\mathrm{mulGrp}$$
26	8 25	cfv	$$class{\mathrm{mulGrp}}_r$$
27		vx	$$setvarx$$
28	27	cv	$$setvarx$$
29	28 21	cfv	$$classp\left(x\right)$$
30	4	cv	$$setvarm$$
31	29 28 30	co	$$class\left(p\left(x\right)mx\right)$$
32	27 6 31	cmpt	$$class\left(x\in n⟼p\left(x\right)mx\right)$$
33	26 32 11	co	$$class\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)$$
34	22 33 24	co	$$class\left(\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)$$
35	12 15 34	cmpt	$$class\left(p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}⟼\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)$$
36	8 35 11	co	$$class\left(\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}}{{\sum }_r},\left(\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)\right)$$
37	4 10 36	cmpt	$$class\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}}{{\sum }_r}\left(\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)\right)$$
38	1 3 2 2 37	cmpo	$$class\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}}{{\sum }_r}\left(\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)\right)\right)$$
39	0 38	wceq	$$wff\mathrm{maDet}=\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(n\right)}}{{\sum }_r}\left(\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ \mathrm{pmSgn}\left(n\right)\right)\left(p\right){\cdot }_r\left(\underset{x\in n}{{\sum }_{{\mathrm{mulGrp}}_r}},\left(p\left(x\right)mx\right)\right)\right)\right)\right)$$