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 = ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chfs ⊢ +fn
1 vf ⊢ 𝑓
2 cc ⊢ ℂ
3 cmap ⊢ ↑m
4 chba ⊢ ℋ
5 2 4 3 co ⊢ ( ℂ ↑m ℋ )
6 vg ⊢ 𝑔
7 vx ⊢ 𝑥
8 1 cv ⊢ 𝑓
9 7 cv ⊢ 𝑥
10 9 8 cfv ⊢ ( 𝑓 ‘ 𝑥 )
11 caddc ⊢ +
12 6 cv ⊢ 𝑔
13 9 12 cfv ⊢ ( 𝑔 ‘ 𝑥 )
14 10 13 11 co ⊢ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) )
15 7 4 14 cmpt ⊢ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) )
16 1 6 5 5 15 cmpo ⊢ ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )
17 0 16 wceq ⊢ +fn = ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )