Definition df-lnfn 31605

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 30711	. 2 class LinFn
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1532	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1532	. . . . . . . . . 10 class 𝑦
6		csm 30678	. . . . . . . . . 10 class ·ℎ
7	3, 5, 6	co 7404	. . . . . . . . 9 class (𝑥 ·ℎ 𝑦)
8		vz	. . . . . . . . . 10 setvar 𝑧
9	8	cv 1532	. . . . . . . . 9 class 𝑧
10		cva 30677	. . . . . . . . 9 class +ℎ
11	7, 9, 10	co 7404	. . . . . . . 8 class ((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
12		vt	. . . . . . . . 9 setvar 𝑡
13	12	cv 1532	. . . . . . . 8 class 𝑡
14	11, 13	cfv 6536	. . . . . . 7 class (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
15	5, 13	cfv 6536	. . . . . . . . 9 class (𝑡‘𝑦)
16		cmul 11114	. . . . . . . . 9 class ·
17	3, 15, 16	co 7404	. . . . . . . 8 class (𝑥 · (𝑡‘𝑦))
18	9, 13	cfv 6536	. . . . . . . 8 class (𝑡‘𝑧)
19		caddc 11112	. . . . . . . 8 class +
20	17, 18, 19	co 7404	. . . . . . 7 class ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
21	14, 20	wceq 1533	. . . . . 6 wff (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
22		chba 30676	. . . . . 6 class ℋ
23	21, 8, 22	wral 3055	. . . . 5 wff ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
24	23, 4, 22	wral 3055	. . . 4 wff ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
25		cc 11107	. . . 4 class ℂ
26	24, 2, 25	wral 3055	. . 3 wff ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))
27		cmap 8819	. . . 4 class ↑m
28	25, 22, 27	co 7404	. . 3 class (ℂ ↑m ℋ)
29	26, 12, 28	crab 3426	. 2 class {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}
30	1, 29	wceq 1533	1 wff LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}

This definition is referenced by:  ellnfn  31640