Metamath Proof Explorer

Definition df-lnfn

Description: Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion df-lnfn ⊢ LinFn = t ∈ ℂ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 clf class LinFn
1 vt setvar t
2 cc class ℂ
3 cmap class ↑ 𝑚
4 chba class ℋ
5 2 4 3 co class ℂ ℋ
6 vx setvar x
7 vy setvar y
8 vz setvar z
9 1 cv setvar t
10 6 cv setvar x
11 csm class ⋅ ℎ
12 7 cv setvar y
13 10 12 11 co class x ⋅ ℎ y
14 cva class + ℎ
15 8 cv setvar z
16 13 15 14 co class x ⋅ ℎ y + ℎ z
17 16 9 cfv class t ⁡ x ⋅ ℎ y + ℎ z
18 cmul class ×
19 12 9 cfv class t ⁡ y
20 10 19 18 co class x ⁢ t ⁡ y
21 caddc class +
22 15 9 cfv class t ⁡ z
23 20 22 21 co class x ⁢ t ⁡ y + t ⁡ z
24 17 23 wceq wff t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z
25 24 8 4 wral wff ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z
26 25 7 4 wral wff ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z
27 26 6 2 wral wff ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z
28 27 1 5 crab class t ∈ ℂ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z
29 0 28 wceq wff LinFn = t ∈ ℂ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z