Definition df-iop 9955

Description: Define the Hilbert space identity operator. See dfiop2 9959 for alternate definition.

Assertion

Ref	Expression
df-iop	|- Iop = (proj` H~)

Detailed syntax breakdown of Definition df-iop

Step	Hyp	Ref	Expression
1		chio 9088	. 2 class Iop
2		chil 9063	. . 3 class H~
3		cpj 9081	. . 3 class proj
4	2, 3	cfv 3263	. 2 class (proj` H~)
5	1, 4	wceq 992	1 wff Iop = (proj` H~)

This definition is referenced by:  dfiop2 9959  hoival 9961  hoid1i 9995  hoid1ri 9996  pjclem1 10404  pjclem3 10406  pjci 10409

Copyright terms: Public domain