Definition df-mdet 21642

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 21644). 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 21652. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 21659, the homogeneity by mdetrsca 21660. Furthermore, it is shown that the determinant function is alternating (see mdetralt 21665) and normalized (see mdet1 21658). Finally, uniqueness is shown by mdetuni 21679. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 21644. (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 21641	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3422	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1538	. . . . . 6 class 𝑛
7	3	cv 1538	. . . . . 6 class 𝑟
8		cmat 21464	. . . . . 6 class Mat
9	6, 7, 8	co 7255	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 16840	. . . . 5 class Base
11	9, 10	cfv 6418	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 18889	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6418	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6418	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1538	. . . . . . . 8 class 𝑝
17		czrh 20613	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6418	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 19012	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6418	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5584	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6418	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 19635	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6418	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1538	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6418	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1538	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7255	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5153	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 17068	. . . . . . . 8 class Σg
32	24, 30, 31	co 7255	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 16889	. . . . . . . 8 class .r
34	7, 33	cfv 6418	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7255	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5153	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7255	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5153	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7257	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1539	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  21643