Definition df-mdet 21285

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

Assertion

Ref	Expression
df-mdet	⊢ maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

Distinct variable group:   𝑛,𝑟,𝑚,𝑝,𝑥

Detailed syntax breakdown of Definition df-mdet

Step	Hyp	Ref	Expression
1		cmdat 21284	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3409	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1537	. . . . . 6 class 𝑛
7	3	cv 1537	. . . . . 6 class 𝑟
8		cmat 21107	. . . . . 6 class Mat
9	6, 7, 8	co 7150	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 16541	. . . . 5 class Base
11	9, 10	cfv 6335	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 18562	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6335	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6335	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1537	. . . . . . . 8 class 𝑝
17		czrh 20269	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6335	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 18684	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6335	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5528	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6335	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 19307	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6335	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1537	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6335	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1537	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7150	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5112	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 16772	. . . . . . . 8 class Σg
32	24, 30, 31	co 7150	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 16624	. . . . . . . 8 class .r
34	7, 33	cfv 6335	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7150	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5112	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7150	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5112	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7152	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1538	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  21286