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

Metamath Proof Explorer

Definition df-homul

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

Ref Expression
Assertion df-homul ⊢ · op = f ∈ ℂ , g ∈ ℋ ℋ ⟼ x ∈ ℋ ⟼ f ⋅ ℎ g ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 chot class · op
1 vf setvar f
2 cc class ℂ
3 vg setvar g
4 chba class ℋ
5 cmap class ↑ 𝑚
6 4 4 5 co class ℋ ℋ
7 vx setvar x
8 1 cv setvar f
9 csm 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 4 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 · op = f ∈ ℂ , g ∈ ℋ ℋ ⟼ x ∈ ℋ ⟼ f ⋅ ℎ g ⁡ x