Definition df-lnop 29612

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

Assertion

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

Distinct variable group:   𝑥,𝑡,𝑦,𝑧

Detailed syntax breakdown of Definition df-lnop

Step	Hyp	Ref	Expression
1		clo 28718	. 2 class LinOp
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1532	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1532	. . . . . . . . . 10 class 𝑦
6		csm 28692	. . . . . . . . . 10 class ·ℎ
7	3, 5, 6	co 7150	. . . . . . . . 9 class (𝑥 ·ℎ 𝑦)
8		vz	. . . . . . . . . 10 setvar 𝑧
9	8	cv 1532	. . . . . . . . 9 class 𝑧
10		cva 28691	. . . . . . . . 9 class +ℎ
11	7, 9, 10	co 7150	. . . . . . . 8 class ((𝑥 ·ℎ 𝑦) +ℎ 𝑧)
12		vt	. . . . . . . . 9 setvar 𝑡
13	12	cv 1532	. . . . . . . 8 class 𝑡
14	11, 13	cfv 6349	. . . . . . 7 class (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧))
15	5, 13	cfv 6349	. . . . . . . . 9 class (𝑡‘𝑦)
16	3, 15, 6	co 7150	. . . . . . . 8 class (𝑥 ·ℎ (𝑡‘𝑦))
17	9, 13	cfv 6349	. . . . . . . 8 class (𝑡‘𝑧)
18	16, 17, 10	co 7150	. . . . . . 7 class ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
19	14, 18	wceq 1533	. . . . . 6 wff (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
20		chba 28690	. . . . . 6 class ℋ
21	19, 8, 20	wral 3138	. . . . 5 wff ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
22	21, 4, 20	wral 3138	. . . 4 wff ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
23		cc 10529	. . . 4 class ℂ
24	22, 2, 23	wral 3138	. . 3 wff ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))
25		cmap 8400	. . . 4 class ↑m
26	20, 20, 25	co 7150	. . 3 class ( ℋ ↑m ℋ)
27	24, 12, 26	crab 3142	. 2 class {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}
28	1, 27	wceq 1533	1 wff LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}

This definition is referenced by:  ellnop  29629  hhlnoi  29671