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 20439
Description: Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 20441). 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 20449. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 20456, the homogeneity by mdetrsca 20457. Furthermore, it is shown that the determinant function is alternating (see mdetralt 20462) and normalized (see mdet1 20455). Finally, the uniqueness is shown by mdetuni 20476. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 20441. (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 20438 . 2 class maDet
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3231 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1522 . . . . . 6 class 𝑛
73cv 1522 . . . . . 6 class 𝑟
8 cmat 20261 . . . . . 6 class Mat
96, 7, 8co 6690 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 15904 . . . . 5 class Base
119, 10cfv 5926 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vp . . . . . 6 setvar 𝑝
13 csymg 17843 . . . . . . . 8 class SymGrp
146, 13cfv 5926 . . . . . . 7 class (SymGrp‘𝑛)
1514, 10cfv 5926 . . . . . 6 class (Base‘(SymGrp‘𝑛))
1612cv 1522 . . . . . . . 8 class 𝑝
17 czrh 19896 . . . . . . . . . 10 class ℤRHom
187, 17cfv 5926 . . . . . . . . 9 class (ℤRHom‘𝑟)
19 cpsgn 17955 . . . . . . . . . 10 class pmSgn
206, 19cfv 5926 . . . . . . . . 9 class (pmSgn‘𝑛)
2118, 20ccom 5147 . . . . . . . 8 class ((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))
2216, 21cfv 5926 . . . . . . 7 class (((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)
23 cmgp 18535 . . . . . . . . 9 class mulGrp
247, 23cfv 5926 . . . . . . . 8 class (mulGrp‘𝑟)
25 vx . . . . . . . . 9 setvar 𝑥
2625cv 1522 . . . . . . . . . . 11 class 𝑥
2726, 16cfv 5926 . . . . . . . . . 10 class (𝑝𝑥)
285cv 1522 . . . . . . . . . 10 class 𝑚
2927, 26, 28co 6690 . . . . . . . . 9 class ((𝑝𝑥)𝑚𝑥)
3025, 6, 29cmpt 4762 . . . . . . . 8 class (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))
31 cgsu 16148 . . . . . . . 8 class Σg
3224, 30, 31co 6690 . . . . . . 7 class ((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))
33 cmulr 15989 . . . . . . . 8 class .r
347, 33cfv 5926 . . . . . . 7 class (.r𝑟)
3522, 32, 34co 6690 . . . . . 6 class ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))
3612, 15, 35cmpt 4762 . . . . 5 class (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))
377, 36, 31co 6690 . . . 4 class (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))
385, 11, 37cmpt 4762 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥)))))))
392, 3, 4, 4, 38cmpt2 6692 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r𝑟)((mulGrp‘𝑟) Σg (𝑥𝑛 ↦ ((𝑝𝑥)𝑚𝑥))))))))
401, 39wceq 1523 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  20440
  Copyright terms: Public domain W3C validator