Metamath Proof Explorer


Definition df-hosum

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 ) ) ) )

Detailed syntax breakdown

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 ) ) ) )