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

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

Detailed syntax breakdown of Definition df-iop
StepHypRef Expression
1 chio 10237 . 2 class Iop
2 chil 10212 . . 3 class ~H
3 cpj 10230 . . 3 class proj
42, 3cfv 3809 . 2 class (proj` ~H)
51, 4wceq 1136 1 wff Iop = (proj` ~H)
Colors of variables: wff set class
This definition is referenced by:  dfiop2 11108  hoival 11110  hoid1i 11144  hoid1ri 11145  pjclem1 11560  pjclem3 11562  pjci 11565
Copyright terms: Public domain