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

Step	Hyp	Ref	Expression
1		chio 10237	. 2 class Iop
2		chil 10212	. . 3 class ~H
3		cpj 10230	. . 3 class proj
4	2, 3	cfv 3809	. 2 class (proj` ~H)
5	1, 4	wceq 1136	1 wff Iop = (proj` ~H)

This definition is referenced by:  dfiop2 11108  hoival 11110  hoid1i 11144  hoid1ri 11145  pjclem1 11560  pjclem3 11562  pjci 11565

Copyright terms: Public domain