Definition df-lnfn 28707

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 = {𝑡 ∈ (ℂ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}

Distinct variable group:   𝑥,𝑡,𝑦,𝑧

Detailed syntax breakdown of Definition df-lnfn

Step	Hyp	Ref	Expression
1		clf 27811	. 2 class LinFn
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1482	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1482	. . . . . . . . . 10 class 𝑦
6		csm 27778	. . . . . . . . . 10 class ·ℎ
7	3, 5, 6	co 6650	. . . . . . . . 9 class (𝑥 ·ℎ 𝑦)
8		vz	. . . . . . . . . 10 setvar 𝑧
9	8	cv 1482	. . . . . . . . 9 class 𝑧
10		cva 27777	. . . . . . . . 9 class +ℎ
11	7, 9, 10	co 6650	. . . . . . . 8 class ((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
12		vt	. . . . . . . . 9 setvar 𝑡
13	12	cv 1482	. . . . . . . 8 class 𝑡
14	11, 13	cfv 5888	. . . . . . 7 class (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
15	5, 13	cfv 5888	. . . . . . . . 9 class (𝑡‘𝑦)
16		cmul 9941	. . . . . . . . 9 class ·
17	3, 15, 16	co 6650	. . . . . . . 8 class (𝑥 · (𝑡‘𝑦))
18	9, 13	cfv 5888	. . . . . . . 8 class (𝑡‘𝑧)
19		caddc 9939	. . . . . . . 8 class +
20	17, 18, 19	co 6650	. . . . . . 7 class ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
21	14, 20	wceq 1483	. . . . . 6 wff (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
22		chil 27776	. . . . . 6 class ℋ
23	21, 8, 22	wral 2912	. . . . 5 wff ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
24	23, 4, 22	wral 2912	. . . 4 wff ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
25		cc 9934	. . . 4 class ℂ
26	24, 2, 25	wral 2912	. . 3 wff ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
27		cmap 7857	. . . 4 class ↑𝑚
28	25, 22, 27	co 6650	. . 3 class (ℂ ↑𝑚 ℋ)
29	26, 12, 28	crab 2916	. 2 class {𝑡 ∈ (ℂ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}
30	1, 29	wceq 1483	1 wff LinFn = {𝑡 ∈ (ℂ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}

This definition is referenced by:  ellnfn  28742