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 = t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 clo class LinOp
1 vt setvar t
2 chba class ℋ
3 cmap class ↑ 𝑚
4 2 2 3 co class ℋ ℋ
5 vx setvar x
6 cc class ℂ
7 vy setvar y
8 vz setvar z
9 1 cv setvar t
10 5 cv setvar x
11 csm class ⋅ ℎ
12 7 cv setvar y
13 10 12 11 co class x ⋅ ℎ y
14 cva class + ℎ
15 8 cv setvar z
16 13 15 14 co class x ⋅ ℎ y + ℎ z
17 16 9 cfv class t ⁡ x ⋅ ℎ y + ℎ z
18 12 9 cfv class t ⁡ y
19 10 18 11 co class x ⋅ ℎ t ⁡ y
20 15 9 cfv class t ⁡ z
21 19 20 14 co class x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
22 17 21 wceq wff t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
23 22 8 2 wral wff ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
24 23 7 2 wral wff ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
25 24 5 6 wral wff ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
26 25 1 4 crab class t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z
27 0 26 wceq wff LinOp = t ∈ ℋ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ t ⁡ y + ℎ t ⁡ z