Definition df-mdet 22086

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22088). 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 22096. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22103, the homogeneity by mdetrsca 22104. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22109) and normalized (see mdet1 22102). Finally, uniqueness is shown by mdetuni 22123. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22088. (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 22085	. 2 class maDet
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3474	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1540	. . . . . 6 class 𝑛
7	3	cv 1540	. . . . . 6 class 𝑟
8		cmat 21906	. . . . . 6 class Mat
9	6, 7, 8	co 7408	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 17143	. . . . 5 class Base
11	9, 10	cfv 6543	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vp	. . . . . 6 setvar 𝑝
13		csymg 19233	. . . . . . . 8 class SymGrp
14	6, 13	cfv 6543	. . . . . . 7 class (SymGrp‘𝑛)
15	14, 10	cfv 6543	. . . . . 6 class (Base‘(SymGrp‘𝑛))
16	12	cv 1540	. . . . . . . 8 class 𝑝
17		czrh 21048	. . . . . . . . . 10 class ℤRHom
18	7, 17	cfv 6543	. . . . . . . . 9 class (ℤRHom‘𝑟)
19		cpsgn 19356	. . . . . . . . . 10 class pmSgn
20	6, 19	cfv 6543	. . . . . . . . 9 class (pmSgn‘𝑛)
21	18, 20	ccom 5680	. . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
22	16, 21	cfv 6543	. . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23		cmgp 19986	. . . . . . . . 9 class mulGrp
24	7, 23	cfv 6543	. . . . . . . 8 class (mulGrp‘𝑟)
25		vx	. . . . . . . . 9 setvar 𝑥
26	25	cv 1540	. . . . . . . . . . 11 class 𝑥
27	26, 16	cfv 6543	. . . . . . . . . 10 class (𝑝‘𝑥)
28	5	cv 1540	. . . . . . . . . 10 class 𝑚
29	27, 26, 28	co 7408	. . . . . . . . 9 class ((𝑝‘𝑥)𝑚𝑥)
30	25, 6, 29	cmpt 5231	. . . . . . . 8 class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))
31		cgsu 17385	. . . . . . . 8 class Σg
32	24, 30, 31	co 7408	. . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))
33		cmulr 17197	. . . . . . . 8 class .r
34	7, 33	cfv 6543	. . . . . . 7 class (.r‘𝑟)
35	22, 32, 34	co 7408	. . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))
36	12, 15, 35	cmpt 5231	. . . . 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 5231	. . 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 1541	1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))

This definition is referenced by:  mdetfval  22087