Definition df-mdet 22472

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22474). 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 22482. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22489, the homogeneity by mdetrsca 22490. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22495) and normalized (see mdet1 22488). Finally, uniqueness is shown by mdetuni 22509. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22474. (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 22471	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3447	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1539	. . . . . 6 class 𝑛
7	3	cv 1539	. . . . . 6 class 𝑟
8		cmat 22294	. . . . . 6 class Mat
9	6, 7, 8	co 7387	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 17179	. . . . 5 class Base
11	9, 10	cfv 6511	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 19299	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6511	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6511	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1539	. . . . . . . 8 class 𝑝
17		czrh 21409	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6511	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 19419	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6511	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5642	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6511	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 20049	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6511	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1539	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6511	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1539	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7387	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5188	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 17403	. . . . . . . 8 class Σg
32	24, 30, 31	co 7387	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 17221	. . . . . . . 8 class .r
34	7, 33	cfv 6511	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7387	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5188	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7387	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5188	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7389	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1540	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  22473