Definition df-lnfn 31096

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

Assertion

Ref	Expression
df-lnfn	⊢ LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}

Distinct variable group:   𝑥,𝑡,𝑦,𝑧

Detailed syntax breakdown of Definition df-lnfn

Step	Hyp	Ref	Expression
1		clf 30202	. 2 class LinFn
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1540	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1540	. . . . . . . . . 10 class 𝑦
6		csm 30169	. . . . . . . . . 10 class ·ℎ
7	3, 5, 6	co 7408	. . . . . . . . 9 class (𝑥 ·ℎ 𝑦)
8		vz	. . . . . . . . . 10 setvar 𝑧
9	8	cv 1540	. . . . . . . . 9 class 𝑧
10		cva 30168	. . . . . . . . 9 class +ℎ
11	7, 9, 10	co 7408	. . . . . . . 8 class ((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
12		vt	. . . . . . . . 9 setvar 𝑡
13	12	cv 1540	. . . . . . . 8 class 𝑡
14	11, 13	cfv 6543	. . . . . . 7 class (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
15	5, 13	cfv 6543	. . . . . . . . 9 class (𝑡‘𝑦)
16		cmul 11114	. . . . . . . . 9 class ·
17	3, 15, 16	co 7408	. . . . . . . 8 class (𝑥 · (𝑡‘𝑦))
18	9, 13	cfv 6543	. . . . . . . 8 class (𝑡‘𝑧)
19		caddc 11112	. . . . . . . 8 class +
20	17, 18, 19	co 7408	. . . . . . 7 class ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
21	14, 20	wceq 1541	. . . . . 6 wff (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
22		chba 30167	. . . . . 6 class ℋ
23	21, 8, 22	wral 3061	. . . . 5 wff ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
24	23, 4, 22	wral 3061	. . . 4 wff ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
25		cc 11107	. . . 4 class ℂ
26	24, 2, 25	wral 3061	. . 3 wff ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
27		cmap 8819	. . . 4 class ↑m
28	25, 22, 27	co 7408	. . 3 class (ℂ ↑m ℋ)
29	26, 12, 28	crab 3432	. 2 class {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}
30	1, 29	wceq 1541	1 wff LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}

This definition is referenced by:  ellnfn  31131