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