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 30837
Description: Define the eigenvector function. Theorem eleigveccl 30943 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 29943 . 2 class eigvec
2 vt . . 3 setvar ๐‘ก
3 chba 29903 . . . 4 class โ„‹
4 cmap 8768 . . . 4 class โ†‘m
53, 3, 4co 7358 . . 3 class ( โ„‹ โ†‘m โ„‹)
6 vx . . . . . . . 8 setvar ๐‘ฅ
76cv 1541 . . . . . . 7 class ๐‘ฅ
82cv 1541 . . . . . . 7 class ๐‘ก
97, 8cfv 6497 . . . . . 6 class (๐‘กโ€˜๐‘ฅ)
10 vz . . . . . . . 8 setvar ๐‘ง
1110cv 1541 . . . . . . 7 class ๐‘ง
12 csm 29905 . . . . . . 7 class ยทโ„Ž
1311, 7, 12co 7358 . . . . . 6 class (๐‘ง ยทโ„Ž ๐‘ฅ)
149, 13wceq 1542 . . . . 5 wff (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)
15 cc 11054 . . . . 5 class โ„‚
1614, 10, 15wrex 3070 . . . 4 wff โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)
17 c0h 29919 . . . . 5 class 0โ„‹
183, 17cdif 3908 . . . 4 class ( โ„‹ โˆ– 0โ„‹)
1916, 6, 18crab 3406 . . 3 class {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)}
202, 5, 19cmpt 5189 . 2 class (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)})
211, 20wceq 1542 1 wff eigvec = (๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ {๐‘ฅ โˆˆ ( โ„‹ โˆ– 0โ„‹) โˆฃ โˆƒ๐‘ง โˆˆ โ„‚ (๐‘กโ€˜๐‘ฅ) = (๐‘ง ยทโ„Ž ๐‘ฅ)})
Colors of variables: wff setvar class
This definition is referenced by:  eigvecval  30880
  Copyright terms: Public domain W3C validator