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

Metamath Proof Explorer

Definition df-hfmul

Description: Define the scalar product with a Hilbert space functional. Definition of Beran p. 111. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion df-hfmul ⊢ · fn = f ∈ ℂ , g ∈ ℂ ℋ ⟼ x ∈ ℋ ⟼ f ⁢ g ⁡ x

Detailed syntax breakdown

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