Definition df-mdet 22907

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22909). 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 22917. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22924, the homogeneity by mdetrsca 22925. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22930) and normalized (see mdet1 22923). Finally, uniqueness is shown by mdetuni 22944. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22909. (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 22906	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3450	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1568	. . . . . 6 class 𝑛
7	3	cv 1568	. . . . . 6 class 𝑟
8		cmat 22729	. . . . . 6 class Mat
9	6, 7, 8	co 7422	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 17394	. . . . 5 class Base
11	9, 10	cfv 6541	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 19590	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6541	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6541	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1568	. . . . . . . 8 class 𝑝
17		czrh 21812	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6541	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 19710	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6541	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5654	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6541	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 20367	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6541	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1568	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6541	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1568	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7422	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5185	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 17618	. . . . . . . 8 class Σg
32	24, 30, 31	co 7422	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 17436	. . . . . . . 8 class .r
34	7, 33	cfv 6541	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7422	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5185	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7422	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5185	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7424	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1569	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is used by:  mdetfval  22908