Step | Hyp | Ref
| Expression |
1 | | cel 29944 |
. 2
class
eigval |
2 | | vt |
. . 3
setvar π‘ |
3 | | chba 29903 |
. . . 4
class
β |
4 | | cmap 8768 |
. . . 4
class
βm |
5 | 3, 3, 4 | co 7358 |
. . 3
class ( β
βm β) |
6 | | vx |
. . . 4
setvar π₯ |
7 | 2 | cv 1541 |
. . . . 5
class π‘ |
8 | | cei 29943 |
. . . . 5
class
eigvec |
9 | 7, 8 | cfv 6497 |
. . . 4
class
(eigvecβπ‘) |
10 | 6 | cv 1541 |
. . . . . . 7
class π₯ |
11 | 10, 7 | cfv 6497 |
. . . . . 6
class (π‘βπ₯) |
12 | | csp 29906 |
. . . . . 6
class
Β·ih |
13 | 11, 10, 12 | co 7358 |
. . . . 5
class ((π‘βπ₯) Β·ih π₯) |
14 | | cno 29907 |
. . . . . . 7
class
normβ |
15 | 10, 14 | cfv 6497 |
. . . . . 6
class
(normββπ₯) |
16 | | c2 12213 |
. . . . . 6
class
2 |
17 | | cexp 13973 |
. . . . . 6
class
β |
18 | 15, 16, 17 | co 7358 |
. . . . 5
class
((normββπ₯)β2) |
19 | | cdiv 11817 |
. . . . 5
class
/ |
20 | 13, 18, 19 | co 7358 |
. . . 4
class (((π‘βπ₯) Β·ih π₯) /
((normββπ₯)β2)) |
21 | 6, 9, 20 | cmpt 5189 |
. . 3
class (π₯ β (eigvecβπ‘) β¦ (((π‘βπ₯) Β·ih π₯) /
((normββπ₯)β2))) |
22 | 2, 5, 21 | cmpt 5189 |
. 2
class (π‘ β ( β
βm β) β¦ (π₯ β (eigvecβπ‘) β¦ (((π‘βπ₯) Β·ih π₯) /
((normββπ₯)β2)))) |
23 | 1, 22 | wceq 1542 |
1
wff eigval =
(π‘ β ( β
βm β) β¦ (π₯ β (eigvecβπ‘) β¦ (((π‘βπ₯) Β·ih π₯) /
((normββπ₯)β2)))) |