MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mdet Structured version   Visualization version   GIF version

Definition df-mdet 21112
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 21114). 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". The functionality is shown by mdetf 21122. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 21129, the homogeneity by mdetrsca 21130. Furthermore, it is shown that the determinant function is alternating (see mdetralt 21135) and normalized (see mdet1 21128). Finally, the uniqueness is shown by mdetuni 21149. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 21114. (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
StepHypRef Expression
1 cmdat 21111 . 2 class maDet
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3499 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1529 . . . . . 6 class 𝑛
73cv 1529 . . . . . 6 class 𝑟
8 cmat 20934 . . . . . 6 class Mat
96, 7, 8co 7151 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 16475 . . . . 5 class Base
119, 10cfv 6351 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vp . . . . . 6 setvar 𝑝
13 csymg 18427 . . . . . . . 8 class SymGrp
146, 13cfv 6351 . . . . . . 7 class (SymGrp‘𝑛)
1514, 10cfv 6351 . . . . . 6 class (Base‘(SymGrp‘𝑛))
1612cv 1529 . . . . . . . 8 class 𝑝
17 czrh 20565 . . . . . . . . . 10 class ℤRHom
187, 17cfv 6351 . . . . . . . . 9 class (ℤRHom‘𝑟)
19 cpsgn 18539 . . . . . . . . . 10 class pmSgn
206, 19cfv 6351 . . . . . . . . 9 class (pmSgn‘𝑛)
2118, 20ccom 5557 . . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
2216, 21cfv 6351 . . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23 cmgp 19161 . . . . . . . . 9 class mulGrp
247, 23cfv 6351 . . . . . . . 8 class (mulGrp‘𝑟)
25 vx . . . . . . . . 9 setvar 𝑥
2625cv 1529 . . . . . . . . . . 11 class 𝑥
2726, 16cfv 6351 . . . . . . . . . 10 class (𝑝𝑥)
285cv 1529 . . . . . . . . . 10 class 𝑚
2927, 26, 28co 7151 . . . . . . . . 9 class ((𝑝𝑥)𝑚𝑥)
3025, 6, 29cmpt 5142 . . . . . . . 8 class (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))
31 cgsu 16706 . . . . . . . 8 class Σg
3224, 30, 31co 7151 . . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))
33 cmulr 16558 . . . . . . . 8 class .r
347, 33cfv 6351 . . . . . . 7 class (.r𝑟)
3522, 32, 34co 7151 . . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))
3612, 15, 35cmpt 5142 . . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))
377, 36, 31co 7151 . . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))
385, 11, 37cmpt 5142 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))))
392, 3, 4, 4, 38cmpo 7153 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))))
401, 39wceq 1530 1 wff maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))))
Colors of variables: wff setvar class
This definition is referenced by:  mdetfval  21113
  Copyright terms: Public domain W3C validator