Definition df-mdet 22520

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22522). 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 22530. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22537, the homogeneity by mdetrsca 22538. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22543) and normalized (see mdet1 22536). Finally, uniqueness is shown by mdetuni 22557. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22522. (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 22519	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3437	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1540	. . . . . 6 class 𝑛
7	3	cv 1540	. . . . . 6 class 𝑟
8		cmat 22342	. . . . . 6 class Mat
9	6, 7, 8	co 7355	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 17127	. . . . 5 class Base
11	9, 10	cfv 6489	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 19289	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6489	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6489	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1540	. . . . . . . 8 class 𝑝
17		czrh 21445	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6489	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 19409	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6489	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5625	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6489	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 20066	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6489	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1540	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6489	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1540	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7355	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5176	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 17351	. . . . . . . 8 class Σg
32	24, 30, 31	co 7355	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 17169	. . . . . . . 8 class .r
34	7, 33	cfv 6489	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7355	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5176	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7355	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5176	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7357	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1541	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  22521