Step | Hyp | Ref
| Expression |
1 | | cei 29943 |
. 2
class
eigvec |
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 |
. . . . . . . 8
setvar ๐ฅ |
7 | 6 | cv 1541 |
. . . . . . 7
class ๐ฅ |
8 | 2 | cv 1541 |
. . . . . . 7
class ๐ก |
9 | 7, 8 | cfv 6497 |
. . . . . 6
class (๐กโ๐ฅ) |
10 | | vz |
. . . . . . . 8
setvar ๐ง |
11 | 10 | cv 1541 |
. . . . . . 7
class ๐ง |
12 | | csm 29905 |
. . . . . . 7
class
ยทโ |
13 | 11, 7, 12 | co 7358 |
. . . . . 6
class (๐ง
ยทโ ๐ฅ) |
14 | 9, 13 | wceq 1542 |
. . . . 5
wff (๐กโ๐ฅ) = (๐ง ยทโ ๐ฅ) |
15 | | cc 11054 |
. . . . 5
class
โ |
16 | 14, 10, 15 | wrex 3070 |
. . . 4
wff
โ๐ง โ
โ (๐กโ๐ฅ) = (๐ง ยทโ ๐ฅ) |
17 | | c0h 29919 |
. . . . 5
class
0โ |
18 | 3, 17 | cdif 3908 |
. . . 4
class ( โ
โ 0โ) |
19 | 16, 6, 18 | crab 3406 |
. . 3
class {๐ฅ โ ( โ โ
0โ) โฃ โ๐ง โ โ (๐กโ๐ฅ) = (๐ง ยทโ ๐ฅ)} |
20 | 2, 5, 19 | cmpt 5189 |
. 2
class (๐ก โ ( โ
โm โ) โฆ {๐ฅ โ ( โ โ
0โ) โฃ โ๐ง โ โ (๐กโ๐ฅ) = (๐ง ยทโ ๐ฅ)}) |
21 | 1, 20 | wceq 1542 |
1
wff eigvec =
(๐ก โ ( โ
โm โ) โฆ {๐ฅ โ ( โ โ
0โ) โฃ โ๐ง โ โ (๐กโ๐ฅ) = (๐ง ยทโ ๐ฅ)}) |