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 = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdat maDet
1 vn 𝑛
2 cvv V
3 vr 𝑟
4 vm 𝑚
5 cbs Base
6 1 cv 𝑛
7 cmat Mat
8 3 cv 𝑟
9 6 8 7 co ( 𝑛 Mat 𝑟 )
10 9 5 cfv ( Base ‘ ( 𝑛 Mat 𝑟 ) )
11 cgsu Σg
12 vp 𝑝
13 csymg SymGrp
14 6 13 cfv ( SymGrp ‘ 𝑛 )
15 14 5 cfv ( Base ‘ ( SymGrp ‘ 𝑛 ) )
16 czrh ℤRHom
17 8 16 cfv ( ℤRHom ‘ 𝑟 )
18 cpsgn pmSgn
19 6 18 cfv ( pmSgn ‘ 𝑛 )
20 17 19 ccom ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) )
21 12 cv 𝑝
22 21 20 cfv ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 )
23 cmulr .r
24 8 23 cfv ( .r𝑟 )
25 cmgp mulGrp
26 8 25 cfv ( mulGrp ‘ 𝑟 )
27 vx 𝑥
28 27 cv 𝑥
29 28 21 cfv ( 𝑝𝑥 )
30 4 cv 𝑚
31 29 28 30 co ( ( 𝑝𝑥 ) 𝑚 𝑥 )
32 27 6 31 cmpt ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) )
33 26 32 11 co ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) )
34 22 33 24 co ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) )
35 12 15 34 cmpt ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) ) )
36 8 35 11 co ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) ) ) )
37 4 10 36 cmpt ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
38 1 3 2 2 37 cmpo ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
39 0 38 wceq maDet = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑟 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑛 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑟 ) ∘ ( pmSgn ‘ 𝑛 ) ) ‘ 𝑝 ) ( .r𝑟 ) ( ( mulGrp ‘ 𝑟 ) Σg ( 𝑥𝑛 ↦ ( ( 𝑝𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )