Definition df-mdet 20210

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 20212). 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 20220. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 20227, the homogeneity by mdetrsca 20228. Furthermore, it is shown that the determinant function is alternating (see mdetralt 20233) and normalized (see mdet1 20226). Finally, the uniqueness is shown by mdetuni 20247. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 20212. (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 20209	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3173	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1474	. . . . . 6 class 𝑛
7	3	cv 1474	. . . . . 6 class 𝑟
8		cmat 20032	. . . . . 6 class Mat
9	6, 7, 8	co 6549	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 15695	. . . . 5 class Base
11	9, 10	cfv 5804	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 17620	. . . . . . . 8 class SymGrp
14	6, 13	cfv 5804	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 5804	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1474	. . . . . . . 8 class 𝑝
17		czrh 19667	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 5804	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 17732	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 5804	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5042	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 5804	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 18312	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 5804	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1474	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 5804	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1474	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 6549	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 4643	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 15924	. . . . . . . 8 class Σg
32	24, 30, 31	co 6549	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 15769	. . . . . . . 8 class .r
34	7, 33	cfv 5804	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 6549	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 4643	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 6549	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 4643	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpt2 6551	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1475	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  20211