This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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