HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-eigvec Structured version   Visualization version   GIF version

Definition df-eigvec 31601
Description: Define the eigenvector function. Theorem eleigveccl 31707 shows that eigvecโ€˜๐‘‡, the set of eigenvectors of Hilbert space operator ๐‘‡, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-eigvec eigvec = (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)})
Distinct variable group:   ๐‘ฅ,๐‘ก,๐‘ง

Detailed syntax breakdown of Definition df-eigvec
StepHypRef Expression
1 cei 30707 . 2 class eigvec
2 vt . . 3 setvar ๐‘ก
3 chba 30667 . . . 4 class โ„‹
4 cmap 8817 . . . 4 class โ†‘m
53, 3, 4co 7402 . . 3 class ( โ„‹ โ†‘m โ„‹)
6 vx . . . . . . . 8 setvar ๐‘ฅ
76cv 1532 . . . . . . 7 class ๐‘ฅ
82cv 1532 . . . . . . 7 class ๐‘ก
97, 8cfv 6534 . . . . . 6 class (๐‘กโ€˜๐‘ฅ)
10 vz . . . . . . . 8 setvar ๐‘ง
1110cv 1532 . . . . . . 7 class ๐‘ง
12 csm 30669 . . . . . . 7 class ยทโ„Ž
1311, 7, 12co 7402 . . . . . 6 class (๐‘ง ยทโ„Ž ๐‘ฅ)
149, 13wceq 1533 . . . . 5 wff (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)
15 cc 11105 . . . . 5 class โ„‚
1614, 10, 15wrex 3062 . . . 4 wff โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)
17 c0h 30683 . . . . 5 class 0โ„‹
183, 17cdif 3938 . . . 4 class ( โ„‹ โˆ– 0โ„‹)
1916, 6, 18crab 3424 . . 3 class {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)}
202, 5, 19cmpt 5222 . 2 class (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)})
211, 20wceq 1533 1 wff eigvec = (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)})
Colors of variables: wff setvar class
This definition is referenced by:  eigvecval  31644
  Copyright terms: Public domain W3C validator