Definition df-mdet 21190

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 21192). 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 21200. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 21207, the homogeneity by mdetrsca 21208. Furthermore, it is shown that the determinant function is alternating (see mdetralt 21213) and normalized (see mdet1 21206). Finally, the uniqueness is shown by mdetuni 21227. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 21192. (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 21189	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3441	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1537	. . . . . 6 class 𝑛
7	3	cv 1537	. . . . . 6 class 𝑟
8		cmat 21012	. . . . . 6 class Mat
9	6, 7, 8	co 7135	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 16475	. . . . 5 class Base
11	9, 10	cfv 6324	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 18487	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6324	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6324	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1537	. . . . . . . 8 class 𝑝
17		czrh 20193	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6324	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 18609	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6324	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5523	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6324	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 19232	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6324	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1537	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6324	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1537	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7135	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5110	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 16706	. . . . . . . 8 class Σg
32	24, 30, 31	co 7135	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 16558	. . . . . . . 8 class .r
34	7, 33	cfv 6324	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7135	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5110	. . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))
37	7, 36, 31	co 7135	. . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))
38	5, 11, 37	cmpt 5110	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
39	2, 3, 4, 4, 38	cmpo 7137	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
40	1, 39	wceq 1538	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  21191