Definition df-iop 9675

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

Assertion

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

Detailed syntax breakdown of Definition df-iop

Step	Hyp	Ref	Expression
1		chio 8813	. 2 class Iop
2		chil 8788	. . 3 class H~
3		cpj 8806	. . 3 class proj
4	2, 3	cfv 3182	. 2 class (proj` H~)
5	1, 4	wceq 956	1 wff Iop = (proj` H~)

This definition is referenced by:  dfiop2 9679  hoivalt 9681  hoid1 9715  hoid1r 9716  pjclem1 10123  pjclem3 10125  pjc 10128

Copyright terms: Public domain