Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-hmo | Structured version Visualization version GIF version |
Description: Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-hmo | ⊢ HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chmo 28830 | . 2 class HmOp | |
2 | vu | . . 3 setvar 𝑢 | |
3 | cnv 28665 | . . 3 class NrmCVec | |
4 | vt | . . . . . . 7 setvar 𝑡 | |
5 | 4 | cv 1542 | . . . . . 6 class 𝑡 |
6 | 2 | cv 1542 | . . . . . . 7 class 𝑢 |
7 | caj 28829 | . . . . . . 7 class adj | |
8 | 6, 6, 7 | co 7213 | . . . . . 6 class (𝑢adj𝑢) |
9 | 5, 8 | cfv 6380 | . . . . 5 class ((𝑢adj𝑢)‘𝑡) |
10 | 9, 5 | wceq 1543 | . . . 4 wff ((𝑢adj𝑢)‘𝑡) = 𝑡 |
11 | 8 | cdm 5551 | . . . 4 class dom (𝑢adj𝑢) |
12 | 10, 4, 11 | crab 3065 | . . 3 class {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡} |
13 | 2, 3, 12 | cmpt 5135 | . 2 class (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}) |
14 | 1, 13 | wceq 1543 | 1 wff HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}) |
Colors of variables: wff setvar class |
This definition is referenced by: hmoval 28891 |
Copyright terms: Public domain | W3C validator |