Definition df-lnop

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clo	⊢ LinOp
1		vt	⊢ 𝑡
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4	2 2 3	co	⊢ ( ℋ ↑m ℋ )
5		vx	⊢ 𝑥
6		cc	⊢ ℂ
7		vy	⊢ 𝑦
8		vz	⊢ 𝑧
9	1	cv	⊢ 𝑡
10	5	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	12 9	cfv	⊢ ( 𝑡 ‘ 𝑦 )
19	10 18 11	co	⊢ ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) )
20	15 9	cfv	⊢ ( 𝑡 ‘ 𝑧 )
21	19 20 14	co	⊢ ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) )
22	17 21	wceq	⊢ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) )
23	22 8 2	wral	⊢ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) )
24	23 7 2	wral	⊢ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) )
25	24 5 6	wral	⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) )
26	25 1 4	crab	⊢ { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) }
27	0 26	wceq	⊢ LinOp = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) }