Metamath Proof Explorer

Definition df-mdet

Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib ). 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 . Multilineary means "linear for each row" - the additivity is shown by mdetrlin , the homogeneity by mdetrsca . Furthermore, it is shown that the determinant function is alternating (see mdetralt ) and normalized (see mdet1 ). Finally, uniqueness is shown by mdetuni . As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib . (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by SO, 10-Jul-2018)

Ref Expression
Assertion df-mdet ⊢ maDet = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ ∑ r p ∈ Base SymGrp ⁡ n ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdat class maDet
1 vn setvar n
2 cvv class V
3 vr setvar r
4 vm setvar m
5 cbs class Base
6 1 cv setvar n
7 cmat class Mat
8 3 cv setvar r
9 6 8 7 co class n Mat r
10 9 5 cfv class Base n Mat r
11 cgsu class Σ𝑔
12 vp setvar p
13 csymg class SymGrp
14 6 13 cfv class SymGrp ⁡ n
15 14 5 cfv class Base SymGrp ⁡ n
16 czrh class ℤRHom
17 8 16 cfv class ℤRHom ⁡ r
18 cpsgn class pmSgn
19 6 18 cfv class pmSgn ⁡ n
20 17 19 ccom class ℤRHom ⁡ r ∘ pmSgn ⁡ n
21 12 cv setvar p
22 21 20 cfv class ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p
23 cmulr class ⋅ 𝑟
24 8 23 cfv class ⋅ r
25 cmgp class mulGrp
26 8 25 cfv class mulGrp r
27 vx setvar x
28 27 cv setvar x
29 28 21 cfv class p ⁡ x
30 4 cv setvar m
31 29 28 30 co class p ⁡ x m x
32 27 6 31 cmpt class x ∈ n ⟼ p ⁡ x m x
33 26 32 11 co class ∑ mulGrp r x ∈ n p ⁡ x m x
34 22 33 24 co class ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x
35 12 15 34 cmpt class p ∈ Base SymGrp ⁡ n ⟼ ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x
36 8 35 11 co class ∑ r p ∈ Base SymGrp ⁡ n ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x
37 4 10 36 cmpt class m ∈ Base n Mat r ⟼ ∑ r p ∈ Base SymGrp ⁡ n ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x
38 1 3 2 2 37 cmpo class n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ ∑ r p ∈ Base SymGrp ⁡ n ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x
39 0 38 wceq wff maDet = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ ∑ r p ∈ Base SymGrp ⁡ n ℤRHom ⁡ r ∘ pmSgn ⁡ n ⁡ p ⋅ r ∑ mulGrp r x ∈ n p ⁡ x m x