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

Step	Hyp	Ref	Expression
1		chio 8993	. 2 class Iop
2		chil 8968	. . 3 class H~
3		cpj 8986	. . 3 class proj
4	2, 3	cfv 3145	. 2 class (proj` H~)
5	1, 4	wceq 1099	1 wff Iop = (proj` H~)

This definition is referenced by:  dfiop2 9810  hoivalt 9812  hoid1 9846  hoid1r 9847  pjclem1 10247  pjclem3 10249  pjc 10252

Copyright terms: Public domain