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

Definition df-hst 31196
Description: Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in [Mayet3] p. 9. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-hst CHStates = {๐‘“ โˆˆ ( โ„‹ โ†‘m Cโ„‹ ) โˆฃ ((normโ„Žโ€˜(๐‘“โ€˜ โ„‹)) = 1 โˆง โˆ€๐‘ฅ โˆˆ Cโ„‹ โˆ€๐‘ฆ โˆˆ Cโ„‹ (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ)))))}
Distinct variable group:   ๐‘ฅ,๐‘“,๐‘ฆ

Detailed syntax breakdown of Definition df-hst
StepHypRef Expression
1 chst 29947 . 2 class CHStates
2 chba 29903 . . . . . . 7 class โ„‹
3 vf . . . . . . . 8 setvar ๐‘“
43cv 1541 . . . . . . 7 class ๐‘“
52, 4cfv 6501 . . . . . 6 class (๐‘“โ€˜ โ„‹)
6 cno 29907 . . . . . 6 class normโ„Ž
75, 6cfv 6501 . . . . 5 class (normโ„Žโ€˜(๐‘“โ€˜ โ„‹))
8 c1 11059 . . . . 5 class 1
97, 8wceq 1542 . . . 4 wff (normโ„Žโ€˜(๐‘“โ€˜ โ„‹)) = 1
10 vx . . . . . . . . 9 setvar ๐‘ฅ
1110cv 1541 . . . . . . . 8 class ๐‘ฅ
12 vy . . . . . . . . . 10 setvar ๐‘ฆ
1312cv 1541 . . . . . . . . 9 class ๐‘ฆ
14 cort 29914 . . . . . . . . 9 class โŠฅ
1513, 14cfv 6501 . . . . . . . 8 class (โŠฅโ€˜๐‘ฆ)
1611, 15wss 3915 . . . . . . 7 wff ๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ)
1711, 4cfv 6501 . . . . . . . . . 10 class (๐‘“โ€˜๐‘ฅ)
1813, 4cfv 6501 . . . . . . . . . 10 class (๐‘“โ€˜๐‘ฆ)
19 csp 29906 . . . . . . . . . 10 class ยทih
2017, 18, 19co 7362 . . . . . . . . 9 class ((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ))
21 cc0 11058 . . . . . . . . 9 class 0
2220, 21wceq 1542 . . . . . . . 8 wff ((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0
23 chj 29917 . . . . . . . . . . 11 class โˆจโ„‹
2411, 13, 23co 7362 . . . . . . . . . 10 class (๐‘ฅ โˆจโ„‹ ๐‘ฆ)
2524, 4cfv 6501 . . . . . . . . 9 class (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ))
26 cva 29904 . . . . . . . . . 10 class +โ„Ž
2717, 18, 26co 7362 . . . . . . . . 9 class ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ))
2825, 27wceq 1542 . . . . . . . 8 wff (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ))
2922, 28wa 397 . . . . . . 7 wff (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ)))
3016, 29wi 4 . . . . . 6 wff (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ))))
31 cch 29913 . . . . . 6 class Cโ„‹
3230, 12, 31wral 3065 . . . . 5 wff โˆ€๐‘ฆ โˆˆ Cโ„‹ (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ))))
3332, 10, 31wral 3065 . . . 4 wff โˆ€๐‘ฅ โˆˆ Cโ„‹ โˆ€๐‘ฆ โˆˆ Cโ„‹ (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ))))
349, 33wa 397 . . 3 wff ((normโ„Žโ€˜(๐‘“โ€˜ โ„‹)) = 1 โˆง โˆ€๐‘ฅ โˆˆ Cโ„‹ โˆ€๐‘ฆ โˆˆ Cโ„‹ (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ)))))
35 cmap 8772 . . . 4 class โ†‘m
362, 31, 35co 7362 . . 3 class ( โ„‹ โ†‘m Cโ„‹ )
3734, 3, 36crab 3410 . 2 class {๐‘“ โˆˆ ( โ„‹ โ†‘m Cโ„‹ ) โˆฃ ((normโ„Žโ€˜(๐‘“โ€˜ โ„‹)) = 1 โˆง โˆ€๐‘ฅ โˆˆ Cโ„‹ โˆ€๐‘ฆ โˆˆ Cโ„‹ (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ)))))}
381, 37wceq 1542 1 wff CHStates = {๐‘“ โˆˆ ( โ„‹ โ†‘m Cโ„‹ ) โˆฃ ((normโ„Žโ€˜(๐‘“โ€˜ โ„‹)) = 1 โˆง โˆ€๐‘ฅ โˆˆ Cโ„‹ โˆ€๐‘ฆ โˆˆ Cโ„‹ (๐‘ฅ โŠ† (โŠฅโ€˜๐‘ฆ) โ†’ (((๐‘“โ€˜๐‘ฅ) ยทih (๐‘“โ€˜๐‘ฆ)) = 0 โˆง (๐‘“โ€˜(๐‘ฅ โˆจโ„‹ ๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) +โ„Ž (๐‘“โ€˜๐‘ฆ)))))}
Colors of variables: wff setvar class
This definition is referenced by:  ishst  31198
  Copyright terms: Public domain W3C validator