Description: Define the sum of two Hilbert space operators. Definition of Beran p. 111. (Contributed by NM, 9-Nov-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | df-hosum | |- +op = ( f e. ( ~H ^m ~H ) , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) +h ( g ` x ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | chos | |- +op |
|
1 | vf | |- f |
|
2 | chba | |- ~H |
|
3 | cmap | |- ^m |
|
4 | 2 2 3 | co | |- ( ~H ^m ~H ) |
5 | vg | |- g |
|
6 | vx | |- x |
|
7 | 1 | cv | |- f |
8 | 6 | cv | |- x |
9 | 8 7 | cfv | |- ( f ` x ) |
10 | cva | |- +h |
|
11 | 5 | cv | |- g |
12 | 8 11 | cfv | |- ( g ` x ) |
13 | 9 12 10 | co | |- ( ( f ` x ) +h ( g ` x ) ) |
14 | 6 2 13 | cmpt | |- ( x e. ~H |-> ( ( f ` x ) +h ( g ` x ) ) ) |
15 | 1 5 4 4 14 | cmpo | |- ( f e. ( ~H ^m ~H ) , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) +h ( g ` x ) ) ) ) |
16 | 0 15 | wceq | |- +op = ( f e. ( ~H ^m ~H ) , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) +h ( g ` x ) ) ) ) |