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

Definition df-homul 30502
Description: Define the scalar product with a Hilbert space operator. Definition of [Beran] p. 111. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-homul ยทop = (๐‘“ โˆˆ โ„‚, ๐‘” โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ (๐‘ฅ โˆˆ โ„‹ โ†ฆ (๐‘“ ยทโ„Ž (๐‘”โ€˜๐‘ฅ))))
Distinct variable group:   ๐‘“,๐‘”,๐‘ฅ

Detailed syntax breakdown of Definition df-homul
StepHypRef Expression
1 chot 29710 . 2 class ยทop
2 vf . . 3 setvar ๐‘“
3 vg . . 3 setvar ๐‘”
4 cc 11007 . . 3 class โ„‚
5 chba 29690 . . . 4 class โ„‹
6 cmap 8723 . . . 4 class โ†‘m
75, 5, 6co 7351 . . 3 class ( โ„‹ โ†‘m โ„‹)
8 vx . . . 4 setvar ๐‘ฅ
92cv 1540 . . . . 5 class ๐‘“
108cv 1540 . . . . . 6 class ๐‘ฅ
113cv 1540 . . . . . 6 class ๐‘”
1210, 11cfv 6493 . . . . 5 class (๐‘”โ€˜๐‘ฅ)
13 csm 29692 . . . . 5 class ยทโ„Ž
149, 12, 13co 7351 . . . 4 class (๐‘“ ยทโ„Ž (๐‘”โ€˜๐‘ฅ))
158, 5, 14cmpt 5186 . . 3 class (๐‘ฅ โˆˆ โ„‹ โ†ฆ (๐‘“ ยทโ„Ž (๐‘”โ€˜๐‘ฅ)))
162, 3, 4, 7, 15cmpo 7353 . 2 class (๐‘“ โˆˆ โ„‚, ๐‘” โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ (๐‘ฅ โˆˆ โ„‹ โ†ฆ (๐‘“ ยทโ„Ž (๐‘”โ€˜๐‘ฅ))))
171, 16wceq 1541 1 wff ยทop = (๐‘“ โˆˆ โ„‚, ๐‘” โˆˆ ( โ„‹ โ†‘m โ„‹) โ†ฆ (๐‘ฅ โˆˆ โ„‹ โ†ฆ (๐‘“ ยทโ„Ž (๐‘”โ€˜๐‘ฅ))))
Colors of variables: wff setvar class
This definition is referenced by:  hommval  30507
  Copyright terms: Public domain W3C validator