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 = \{t \in (ℂ^{ℋ}) \| \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)\}$

Step	Hyp	Ref	Expression
0		clf	$class LinFn$
1		vt	$setvar t$
2		cc	$class ℂ$
3		cmap	$class ↑_{𝑚}$
4		chba	$class ℋ$
5	2 4 3	co	$class (ℂ^{ℋ})$
6		vx	$setvar x$
7		vy	$setvar y$
8		vz	$setvar z$
9	1	cv	$setvar t$
10	6	cv	$setvar x$
11		csm	$class \cdot_{ℎ}$
12	7	cv	$setvar y$
13	10 12 11	co	$class (x \cdot_{ℎ} y)$
14		cva	$class +_{ℎ}$
15	8	cv	$setvar z$
16	13 15 14	co	$class ((x \cdot_{ℎ} y) +_{ℎ} z)$
17	16 9	cfv	$class t ((x \cdot_{ℎ} y) +_{ℎ} z)$
18		cmul	$class \times$
19	12 9	cfv	$class t (y)$
20	10 19 18	co	$class x t (y)$
21		caddc	$class +$
22	15 9	cfv	$class t (z)$
23	20 22 21	co	$class (x t (y) + t (z))$
24	17 23	wceq	$wff t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)$
25	24 8 4	wral	$wff \forall z \in ℋ t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)$
26	25 7 4	wral	$wff \forall y \in ℋ \forall z \in ℋ t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)$
27	26 6 2	wral	$wff \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)$
28	27 1 5	crab	$class \{t \in (ℂ^{ℋ}) \| \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)\}$
29	0 28	wceq	$wff LinFn = \{t \in (ℂ^{ℋ}) \| \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ t ((x \cdot_{ℎ} y) +_{ℎ} z) = x t (y) + t (z)\}$

Metamath Proof Explorer