|   | Hilbert Space Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > HSE Home > Th. List > df-iop | Structured version Visualization version GIF version | ||
| Description: Define the Hilbert space identity operator. See dfiop2 31772 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| df-iop | ⊢ Iop = (projℎ‘ ℋ) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | chio 30963 | . 2 class Iop | |
| 2 | chba 30938 | . . 3 class ℋ | |
| 3 | cpjh 30956 | . . 3 class projℎ | |
| 4 | 2, 3 | cfv 6561 | . 2 class (projℎ‘ ℋ) | 
| 5 | 1, 4 | wceq 1540 | 1 wff Iop = (projℎ‘ ℋ) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: dfiop2 31772 hoival 31774 hoid1i 31808 hoid1ri 31809 pjclem1 32214 pjclem3 32216 pjci 32219 | 
| Copyright terms: Public domain | W3C validator |