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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clf	⊢ LinFn
1		vt	⊢ 𝑡
2		cc	⊢ ℂ
3		cmap	⊢ ↑m
4		chba	⊢ ℋ
5	2 4 3	co	⊢ ( ℂ ↑m ℋ )
6		vx	⊢ 𝑥
7		vy	⊢ 𝑦
8		vz	⊢ 𝑧
9	1	cv	⊢ 𝑡
10	6	cv	⊢ 𝑥
11		csm	⊢ ·ℎ
12	7	cv	⊢ 𝑦
13	10 12 11	co	⊢ ( 𝑥 ·ℎ 𝑦 )
14		cva	⊢ +ℎ
15	8	cv	⊢ 𝑧
16	13 15 14	co	⊢ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 )
17	16 9	cfv	⊢ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) )
18		cmul	⊢ ·
19	12 9	cfv	⊢ ( 𝑡 ‘ 𝑦 )
20	10 19 18	co	⊢ ( 𝑥 · ( 𝑡 ‘ 𝑦 ) )
21		caddc	⊢ +
22	15 9	cfv	⊢ ( 𝑡 ‘ 𝑧 )
23	20 22 21	co	⊢ ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
24	17 23	wceq	⊢ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
25	24 8 4	wral	⊢ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
26	25 7 4	wral	⊢ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
27	26 6 2	wral	⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) )
28	27 1 5	crab	⊢ { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) ) }
29	0 28	wceq	⊢ LinFn = { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑡 ‘ 𝑦 ) ) + ( 𝑡 ‘ 𝑧 ) ) }