Definition df-mdet 22707

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22709). 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 22717. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22724, the homogeneity by mdetrsca 22725. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22730) and normalized (see mdet1 22723). Finally, uniqueness is shown by mdetuni 22744. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22709. (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 22706	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3463	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1566	. . . . . 6 class 𝑛
7	3	cv 1566	. . . . . 6 class 𝑟
8		cmat 22529	. . . . . 6 class Mat
9	6, 7, 8	co 7408	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 17265	. . . . 5 class Base
11	9, 10	cfv 6534	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 19435	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6534	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6534	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1566	. . . . . . . 8 class 𝑝
17		czrh 21614	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6534	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 19555	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6534	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5663	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6534	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 20212	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6534	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1566	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6534	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1566	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7408	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5193	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 17489	. . . . . . . 8 class Σg
32	24, 30, 31	co 7408	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 17307	. . . . . . . 8 class .r
34	7, 33	cfv 6534	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7408	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5193	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7408	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5193	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7410	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1567	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  22708