Definition df-lnfn 9714

Description: Define the set of linear functionals on Hilbert space.

Assertion

Ref	Expression
df-lnfn	⊢ LinFn = {t∣(t: ℋ –→ℂ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z)))}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-lnfn

Step	Hyp	Ref	Expression
1		clf 8762	. 2 class LinFn
2		chil 8727	. . . . 5 class ℋ
3		cc 5212	. . . . 5 class ℂ
4		vt	. . . . . 6 set t
5	4	cv 953	. . . . 5 class t
6	2, 3, 5	wf 3173	. . . 4 wff t: ℋ –→ℂ
7		vx	. . . . . . . . . . . 12 set x
8	7	cv 953	. . . . . . . . . . 11 class x
9		vy	. . . . . . . . . . . 12 set y
10	9	cv 953	. . . . . . . . . . 11 class y
11		csm 8729	. . . . . . . . . . 11 class ·h
12	8, 10, 11	co 3954	. . . . . . . . . 10 class (x ·h y)
13		vz	. . . . . . . . . . 11 set z
14	13	cv 953	. . . . . . . . . 10 class z
15		cva 8728	. . . . . . . . . 10 class +h
16	12, 14, 15	co 3954	. . . . . . . . 9 class ((x ·h y) +h z)
17	16, 5	cfv 3177	. . . . . . . 8 class (t ‘((x ·h y) +h z))
18	10, 5	cfv 3177	. . . . . . . . . 10 class (t ‘y)
19		cmul 5219	. . . . . . . . . 10 class ·
20	8, 18, 19	co 3954	. . . . . . . . 9 class (x · (t ‘y))
21	14, 5	cfv 3177	. . . . . . . . 9 class (t ‘z)
22		caddc 5217	. . . . . . . . 9 class +
23	20, 21, 22	co 3954	. . . . . . . 8 class ((x · (t ‘y)) + (t ‘z))
24	17, 23	wceq 954	. . . . . . 7 wff (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z))
25	24, 13, 2	wral 1642	. . . . . 6 wff ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z))
26	25, 9, 2	wral 1642	. . . . 5 wff ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z))
27	26, 7, 3	wral 1642	. . . 4 wff ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z))
28	6, 27	wa 223	. . 3 wff (t: ℋ –→ℂ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z)))
29	28, 4	cab 1461	. 2 class {t∣(t: ℋ –→ℂ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z)))}
30	1, 29	wceq 954	1 wff LinFn = {t∣(t: ℋ –→ℂ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x · (t ‘y)) + (t ‘z)))}

This definition is referenced by:  ellnfnt 9750

Copyright terms: Public domain