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 classLinOp
1 vt setvart
2 chba classℋ
3 cmap class↑𝑚
4 2 2 3 co classℋℋ
5 vx setvarx
6 cc classℂ
7 vy setvary
8 vz setvarz
9 1 cv setvart
10 5 cv setvarx
11 csm class⋅ℎ
12 7 cv setvary
13 10 12 11 co classx⋅ℎy
14 cva class+ℎ
15 8 cv setvarz
16 13 15 14 co classx⋅ℎy+ℎz
17 16 9 cfv classt⁡x⋅ℎy+ℎz
18 12 9 cfv classt⁡y
19 10 18 11 co classx⋅ℎt⁡y
20 15 9 cfv classt⁡z
21 19 20 14 co classx⋅ℎt⁡y+ℎt⁡z
22 17 21 wceq wfft⁡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 classt∈ℋℋ|∀x∈ℂ∀y∈ℋ∀z∈ℋt⁡x⋅ℎy+ℎz=x⋅ℎt⁡y+ℎt⁡z
27 0 26 wceq wffLinOp=t∈ℋℋ|∀x∈ℂ∀y∈ℋ∀z∈ℋt⁡x⋅ℎy+ℎz=x⋅ℎt⁡y+ℎt⁡z