Detailed syntax breakdown of Definition df-mdet
| Step | Hyp | Ref
| 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 𝑚 |
| 6 | 2 | cv 1539 |
. . . . . 6
class 𝑛 |
| 7 | 3 | cv 1539 |
. . . . . 6
class 𝑟 |
| 8 | | cmat 22411 |
. . . . . 6
class
Mat |
| 9 | 6, 7, 8 | co 7431 |
. . . . 5
class (𝑛 Mat 𝑟) |
| 10 | | cbs 17247 |
. . . . 5
class
Base |
| 11 | 9, 10 | cfv 6561 |
. . . 4
class
(Base‘(𝑛 Mat
𝑟)) |
| 12 | | vp |
. . . . . 6
setvar 𝑝 |
| 13 | | csymg 19386 |
. . . . . . . 8
class
SymGrp |
| 14 | 6, 13 | cfv 6561 |
. . . . . . 7
class
(SymGrp‘𝑛) |
| 15 | 14, 10 | cfv 6561 |
. . . . . 6
class
(Base‘(SymGrp‘𝑛)) |
| 16 | 12 | cv 1539 |
. . . . . . . 8
class 𝑝 |
| 17 | | czrh 21510 |
. . . . . . . . . 10
class
ℤRHom |
| 18 | 7, 17 | cfv 6561 |
. . . . . . . . 9
class
(ℤRHom‘𝑟) |
| 19 | | cpsgn 19507 |
. . . . . . . . . 10
class
pmSgn |
| 20 | 6, 19 | cfv 6561 |
. . . . . . . . 9
class
(pmSgn‘𝑛) |
| 21 | 18, 20 | ccom 5689 |
. . . . . . . 8
class
((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛)) |
| 22 | 16, 21 | cfv 6561 |
. . . . . . 7
class
(((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝) |
| 23 | | cmgp 20137 |
. . . . . . . . 9
class
mulGrp |
| 24 | 7, 23 | cfv 6561 |
. . . . . . . 8
class
(mulGrp‘𝑟) |
| 25 | | vx |
. . . . . . . . 9
setvar 𝑥 |
| 26 | 25 | cv 1539 |
. . . . . . . . . . 11
class 𝑥 |
| 27 | 26, 16 | cfv 6561 |
. . . . . . . . . 10
class (𝑝‘𝑥) |
| 28 | 5 | cv 1539 |
. . . . . . . . . 10
class 𝑚 |
| 29 | 27, 26, 28 | co 7431 |
. . . . . . . . 9
class ((𝑝‘𝑥)𝑚𝑥) |
| 30 | 25, 6, 29 | cmpt 5225 |
. . . . . . . 8
class (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)) |
| 31 | | cgsu 17485 |
. . . . . . . 8
class
Σg |
| 32 | 24, 30, 31 | co 7431 |
. . . . . . 7
class
((mulGrp‘𝑟)
Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))) |
| 33 | | cmulr 17298 |
. . . . . . . 8
class
.r |
| 34 | 7, 33 | cfv 6561 |
. . . . . . 7
class
(.r‘𝑟) |
| 35 | 22, 32, 34 | co 7431 |
. . . . . 6
class
((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))) |
| 36 | 12, 15, 35 | cmpt 5225 |
. . . . 5
class (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))) |
| 37 | 7, 36, 31 | co 7431 |
. . . 4
class (𝑟 Σg
(𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))) |
| 38 | 5, 11, 37 | cmpt 5225 |
. . 3
class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) |
| 39 | 2, 3, 4, 4, 38 | cmpo 7433 |
. 2
class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |
| 40 | 1, 39 | wceq 1540 |
1
wff maDet =
(𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) |