This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-hfsum

Description: Define the sum of two Hilbert space functionals. Definition of Beran p. 111. Note that unlike some authors, we define a functional as any function from ~H to CC , not just linear (or bounded linear) ones. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion df-hfsum ⊢ + fn = f ∈ ℂ ℋ , g ∈ ℂ ℋ ⟼ x ∈ ℋ ⟼ f ⁡ x + g ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 chfs class + fn
1 vf setvar f
2 cc class ℂ
3 cmap class ↑ 𝑚
4 chba class ℋ
5 2 4 3 co class ℂ ℋ
6 vg setvar g
7 vx setvar x
8 1 cv setvar f
9 7 cv setvar x
10 9 8 cfv class f ⁡ x
11 caddc class +
12 6 cv setvar g
13 9 12 cfv class g ⁡ x
14 10 13 11 co class f ⁡ x + g ⁡ x
15 7 4 14 cmpt class x ∈ ℋ ⟼ f ⁡ x + g ⁡ x
16 1 6 5 5 15 cmpo class f ∈ ℂ ℋ , g ∈ ℂ ℋ ⟼ x ∈ ℋ ⟼ f ⁡ x + g ⁡ x
17 0 16 wceq wff + fn = f ∈ ℂ ℋ , g ∈ ℂ ℋ ⟼ x ∈ ℋ ⟼ f ⁡ x + g ⁡ x