Definition df-lnop 28084

Description: Define the set of linear operators on Hilbert space. (See df-hosum 27973 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-lnop	⊢ LinOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}

Distinct variable group:   𝑥,𝑡,𝑦,𝑧

Detailed syntax breakdown of Definition df-lnop

Step	Hyp	Ref	Expression
1		clo 27188	. 2 class LinOp
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1474	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1474	. . . . . . . . . 10 class 𝑦
6		csm 27162	. . . . . . . . . 10 class ·ℎ
7	3, 5, 6	co 6549	. . . . . . . . 9 class (𝑥 ·ℎ 𝑦)
8		vz	. . . . . . . . . 10 setvar 𝑧
9	8	cv 1474	. . . . . . . . 9 class 𝑧
10		cva 27161	. . . . . . . . 9 class +ℎ
11	7, 9, 10	co 6549	. . . . . . . 8 class ((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
12		vt	. . . . . . . . 9 setvar 𝑡
13	12	cv 1474	. . . . . . . 8 class 𝑡
14	11, 13	cfv 5804	. . . . . . 7 class (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
15	5, 13	cfv 5804	. . . . . . . . 9 class (𝑡‘𝑦)
16	3, 15, 6	co 6549	. . . . . . . 8 class (𝑥 ·ℎ (𝑡‘𝑦))
17	9, 13	cfv 5804	. . . . . . . 8 class (𝑡‘𝑧)
18	16, 17, 10	co 6549	. . . . . . 7 class ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
19	14, 18	wceq 1475	. . . . . 6 wff (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
20		chil 27160	. . . . . 6 class ℋ
21	19, 8, 20	wral 2896	. . . . 5 wff ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
22	21, 4, 20	wral 2896	. . . 4 wff ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
23		cc 9813	. . . 4 class ℂ
24	22, 2, 23	wral 2896	. . 3 wff ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
25		cmap 7744	. . . 4 class ↑𝑚
26	20, 20, 25	co 6549	. . 3 class ( ℋ ↑𝑚 ℋ)
27	24, 12, 26	crab 2900	. 2 class {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}
28	1, 27	wceq 1475	1 wff LinOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}

This definition is referenced by:  ellnop  28101  hhlnoi  28143