Detailed syntax breakdown of Definition df-eigval
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cel 30980 | . 2
class
eigval | 
| 2 |  | vt | . . 3
setvar 𝑡 | 
| 3 |  | chba 30939 | . . . 4
class 
ℋ | 
| 4 |  | cmap 8867 | . . . 4
class 
↑m | 
| 5 | 3, 3, 4 | co 7432 | . . 3
class ( ℋ
↑m ℋ) | 
| 6 |  | vx | . . . 4
setvar 𝑥 | 
| 7 | 2 | cv 1538 | . . . . 5
class 𝑡 | 
| 8 |  | cei 30979 | . . . . 5
class
eigvec | 
| 9 | 7, 8 | cfv 6560 | . . . 4
class
(eigvec‘𝑡) | 
| 10 | 6 | cv 1538 | . . . . . . 7
class 𝑥 | 
| 11 | 10, 7 | cfv 6560 | . . . . . 6
class (𝑡‘𝑥) | 
| 12 |  | csp 30942 | . . . . . 6
class 
·ih | 
| 13 | 11, 10, 12 | co 7432 | . . . . 5
class ((𝑡‘𝑥) ·ih 𝑥) | 
| 14 |  | cno 30943 | . . . . . . 7
class
normℎ | 
| 15 | 10, 14 | cfv 6560 | . . . . . 6
class
(normℎ‘𝑥) | 
| 16 |  | c2 12322 | . . . . . 6
class
2 | 
| 17 |  | cexp 14103 | . . . . . 6
class
↑ | 
| 18 | 15, 16, 17 | co 7432 | . . . . 5
class
((normℎ‘𝑥)↑2) | 
| 19 |  | cdiv 11921 | . . . . 5
class 
/ | 
| 20 | 13, 18, 19 | co 7432 | . . . 4
class (((𝑡‘𝑥) ·ih 𝑥) /
((normℎ‘𝑥)↑2)) | 
| 21 | 6, 9, 20 | cmpt 5224 | . . 3
class (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) /
((normℎ‘𝑥)↑2))) | 
| 22 | 2, 5, 21 | cmpt 5224 | . 2
class (𝑡 ∈ ( ℋ
↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) /
((normℎ‘𝑥)↑2)))) | 
| 23 | 1, 22 | wceq 1539 | 1
wff eigval =
(𝑡 ∈ ( ℋ
↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) /
((normℎ‘𝑥)↑2)))) |