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 22591
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22593). 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 22601. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22608, the homogeneity by mdetrsca 22609. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22614) and normalized (see mdet1 22607). Finally, uniqueness is shown by mdetuni 22628. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22593. (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 22590 . 2 class maDet
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3480 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1539 . . . . . 6 class 𝑛
73cv 1539 . . . . . 6 class 𝑟
8 cmat 22411 . . . . . 6 class Mat
96, 7, 8co 7431 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 17247 . . . . 5 class Base
119, 10cfv 6561 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vp . . . . . 6 setvar 𝑝
13 csymg 19386 . . . . . . . 8 class SymGrp
146, 13cfv 6561 . . . . . . 7 class (SymGrp‘𝑛)
1514, 10cfv 6561 . . . . . 6 class (Base‘(SymGrp‘𝑛))
1612cv 1539 . . . . . . . 8 class 𝑝
17 czrh 21510 . . . . . . . . . 10 class ℤRHom
187, 17cfv 6561 . . . . . . . . 9 class (ℤRHom‘𝑟)
19 cpsgn 19507 . . . . . . . . . 10 class pmSgn
206, 19cfv 6561 . . . . . . . . 9 class (pmSgn‘𝑛)
2118, 20ccom 5689 . . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
2216, 21cfv 6561 . . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23 cmgp 20137 . . . . . . . . 9 class mulGrp
247, 23cfv 6561 . . . . . . . 8 class (mulGrp‘𝑟)
25 vx . . . . . . . . 9 setvar 𝑥
2625cv 1539 . . . . . . . . . . 11 class 𝑥
2726, 16cfv 6561 . . . . . . . . . 10 class (𝑝𝑥)
285cv 1539 . . . . . . . . . 10 class 𝑚
2927, 26, 28co 7431 . . . . . . . . 9 class ((𝑝𝑥)𝑚𝑥)
3025, 6, 29cmpt 5225 . . . . . . . 8 class (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))
31 cgsu 17485 . . . . . . . 8 class Σg
3224, 30, 31co 7431 . . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))
33 cmulr 17298 . . . . . . . 8 class .r
347, 33cfv 6561 . . . . . . 7 class (.r𝑟)
3522, 32, 34co 7431 . . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))
3612, 15, 35cmpt 5225 . . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))
377, 36, 31co 7431 . . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))
385, 11, 37cmpt 5225 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))))
392, 3, 4, 4, 38cmpo 7433 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))))
401, 39wceq 1540 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  22592
  Copyright terms: Public domain W3C validator