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