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 20152
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 20154). 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 20162. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 20169, the homogeneity by mdetrsca 20170. Furthermore, it is shown that the determinant function is alternating (see mdetralt 20175) and normalized (see mdet1 20168). Finally, the uniqueness is shown by mdetuni 20189. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 20154. (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 20151 . 2 class maDet
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3172 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1473 . . . . . 6 class 𝑛
73cv 1473 . . . . . 6 class 𝑟
8 cmat 19974 . . . . . 6 class Mat
96, 7, 8co 6527 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 15641 . . . . 5 class Base
119, 10cfv 5790 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vp . . . . . 6 setvar 𝑝
13 csymg 17566 . . . . . . . 8 class SymGrp
146, 13cfv 5790 . . . . . . 7 class (SymGrp‘𝑛)
1514, 10cfv 5790 . . . . . 6 class (Base‘(SymGrp‘𝑛))
1612cv 1473 . . . . . . . 8 class 𝑝
17 czrh 19612 . . . . . . . . . 10 class ℤRHom
187, 17cfv 5790 . . . . . . . . 9 class (ℤRHom‘𝑟)
19 cpsgn 17678 . . . . . . . . . 10 class pmSgn
206, 19cfv 5790 . . . . . . . . 9 class (pmSgn‘𝑛)
2118, 20ccom 5032 . . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
2216, 21cfv 5790 . . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23 cmgp 18258 . . . . . . . . 9 class mulGrp
247, 23cfv 5790 . . . . . . . 8 class (mulGrp‘𝑟)
25 vx . . . . . . . . 9 setvar 𝑥
2625cv 1473 . . . . . . . . . . 11 class 𝑥
2726, 16cfv 5790 . . . . . . . . . 10 class (𝑝𝑥)
285cv 1473 . . . . . . . . . 10 class 𝑚
2927, 26, 28co 6527 . . . . . . . . 9 class ((𝑝𝑥)𝑚𝑥)
3025, 6, 29cmpt 4637 . . . . . . . 8 class (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))
31 cgsu 15870 . . . . . . . 8 class Σg
3224, 30, 31co 6527 . . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))
33 cmulr 15715 . . . . . . . 8 class .r
347, 33cfv 5790 . . . . . . 7 class (.r𝑟)
3522, 32, 34co 6527 . . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))
3612, 15, 35cmpt 4637 . . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))
377, 36, 31co 6527 . . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))
385, 11, 37cmpt 4637 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))))
392, 3, 4, 4, 38cmpt2 6529 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))))
401, 39wceq 1474 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  20153
  Copyright terms: Public domain W3C validator