This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑥 ∈ 𝑛 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )