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	$$⊢{+}_{\mathrm{op}}=\left(f\in \left({\mathscr{H}}^{\mathscr{H}}\right),g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right){+}_{ℎ}g\left(x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chos	$$class{+}_{\mathrm{op}}$$
1		vf	$$setvarf$$
2		chba	$$class\mathscr{H}$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4	2 2 3	co	$$class\left({\mathscr{H}}^{\mathscr{H}}\right)$$
5		vg	$$setvarg$$
6		vx	$$setvarx$$
7	1	cv	$$setvarf$$
8	6	cv	$$setvarx$$
9	8 7	cfv	$$classf\left(x\right)$$
10		cva	$$class{+}_{ℎ}$$
11	5	cv	$$setvarg$$
12	8 11	cfv	$$classg\left(x\right)$$
13	9 12 10	co	$$class\left(f\left(x\right){+}_{ℎ}g\left(x\right)\right)$$
14	6 2 13	cmpt	$$class\left(x\in \mathscr{H}⟼f\left(x\right){+}_{ℎ}g\left(x\right)\right)$$
15	1 5 4 4 14	cmpo	$$class\left(f\in \left({\mathscr{H}}^{\mathscr{H}}\right),g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right){+}_{ℎ}g\left(x\right)\right)\right)$$
16	0 15	wceq	$$wff{+}_{\mathrm{op}}=\left(f\in \left({\mathscr{H}}^{\mathscr{H}}\right),g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right){+}_{ℎ}g\left(x\right)\right)\right)$$