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 20564
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 20566). 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 20574. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 20581, the homogeneity by mdetrsca 20582. Furthermore, it is shown that the determinant function is alternating (see mdetralt 20587) and normalized (see mdet1 20580). Finally, the uniqueness is shown by mdetuni 20601. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 20566. (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 20563 . 2 class maDet
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3328 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1619 . . . . . 6 class 𝑛
73cv 1619 . . . . . 6 class 𝑟
8 cmat 20386 . . . . . 6 class Mat
96, 7, 8co 6801 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 16030 . . . . 5 class Base
119, 10cfv 6037 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vp . . . . . 6 setvar 𝑝
13 csymg 17968 . . . . . . . 8 class SymGrp
146, 13cfv 6037 . . . . . . 7 class (SymGrp‘𝑛)
1514, 10cfv 6037 . . . . . 6 class (Base‘(SymGrp‘𝑛))
1612cv 1619 . . . . . . . 8 class 𝑝
17 czrh 20021 . . . . . . . . . 10 class ℤRHom
187, 17cfv 6037 . . . . . . . . 9 class (ℤRHom‘𝑟)
19 cpsgn 18080 . . . . . . . . . 10 class pmSgn
206, 19cfv 6037 . . . . . . . . 9 class (pmSgn‘𝑛)
2118, 20ccom 5258 . . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
2216, 21cfv 6037 . . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23 cmgp 18660 . . . . . . . . 9 class mulGrp
247, 23cfv 6037 . . . . . . . 8 class (mulGrp‘𝑟)
25 vx . . . . . . . . 9 setvar 𝑥
2625cv 1619 . . . . . . . . . . 11 class 𝑥
2726, 16cfv 6037 . . . . . . . . . 10 class (𝑝𝑥)
285cv 1619 . . . . . . . . . 10 class 𝑚
2927, 26, 28co 6801 . . . . . . . . 9 class ((𝑝𝑥)𝑚𝑥)
3025, 6, 29cmpt 4869 . . . . . . . 8 class (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))
31 cgsu 16274 . . . . . . . 8 class Σg
3224, 30, 31co 6801 . . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))
33 cmulr 16115 . . . . . . . 8 class .r
347, 33cfv 6037 . . . . . . 7 class (.r𝑟)
3522, 32, 34co 6801 . . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))
3612, 15, 35cmpt 4869 . . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))
377, 36, 31co 6801 . . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))
385, 11, 37cmpt 4869 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))))
392, 3, 4, 4, 38cmpt2 6803 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))))
401, 39wceq 1620 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  20565
  Copyright terms: Public domain W3C validator