HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-iop 9806
Description: Define the Hilbert space identity operator. See dfiop2 9810 for alternate definition.
Assertion
Ref Expression
df-iop |- Iop = (proj` H~)

Detailed syntax breakdown of Definition df-iop
StepHypRef Expression
1 chio 8993 . 2 class Iop
2 chil 8968 . . 3 class H~
3 cpj 8986 . . 3 class proj
42, 3cfv 3145 . 2 class (proj` H~)
51, 4wceq 1099 1 wff Iop = (proj` H~)
Colors of variables: wff set class
This definition is referenced by:  dfiop2 9810  hoivalt 9812  hoid1 9846  hoid1r 9847  pjclem1 10247  pjclem3 10249  pjc 10252
Copyright terms: Public domain