Definition df-iop 9592

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

Assertion

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

Detailed syntax breakdown of Definition df-iop

Step	Hyp	Ref	Expression
1		chio 8752	. 2 class Iop
2		chil 8727	. . 3 class H~
3		cpj 8745	. . 3 class proj
4	2, 3	cfv 3172	. 2 class (proj` H~)
5	1, 4	wceq 953	1 wff Iop = (proj` H~)

This definition is referenced by:  dfiop2 9596  hoivalt 9598  hoid1 9632  hoid1r 9633  pjclem1 10033  pjclem3 10035  pjc 10038

Copyright terms: Public domain