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 , g x f x + g x

Detailed syntax breakdown

Step Hyp Ref Expression
0 chos class + op
1 vf setvar f
2 chba class
3 cmap class 𝑚
4 2 2 3 co class
5 vg setvar g
6 vx setvar x
7 1 cv setvar f
8 6 cv setvar x
9 8 7 cfv class f x
10 cva class +
11 5 cv setvar g
12 8 11 cfv class g x
13 9 12 10 co class f x + g x
14 6 2 13 cmpt class x f x + g x
15 1 5 4 4 14 cmpo class f , g x f x + g x
16 0 15 wceq wff + op = f , g x f x + g x