Definition df-mdet 20391

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 20393). 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 20401. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 20408, the homogeneity by mdetrsca 20409. Furthermore, it is shown that the determinant function is alternating (see mdetralt 20414) and normalized (see mdet1 20407). Finally, the uniqueness is shown by mdetuni 20428. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 20393. (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 20390	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3200	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1482	. . . . . 6 class 𝑛
7	3	cv 1482	. . . . . 6 class 𝑟
8		cmat 20213	. . . . . 6 class Mat
9	6, 7, 8	co 6650	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 15857	. . . . 5 class Base
11	9, 10	cfv 5888	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 17797	. . . . . . . 8 class SymGrp
14	6, 13	cfv 5888	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 5888	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1482	. . . . . . . 8 class 𝑝
17		czrh 19848	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 5888	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 17909	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 5888	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5118	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 5888	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 18489	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 5888	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1482	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 5888	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1482	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 6650	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 4729	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 16101	. . . . . . . 8 class Σg
32	24, 30, 31	co 6650	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 15942	. . . . . . . 8 class .r
34	7, 33	cfv 5888	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 6650	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 4729	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 6650	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 4729	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpt2 6652	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1483	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  20392