Definition df-iop 9615

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

Assertion

Ref	Expression
df-iop	⊢ Iop = (proj ‘ ℋ )

Detailed syntax breakdown of Definition df-iop

Step	Hyp	Ref	Expression
1		chio 8752	. 2 class Iop
2		chil 8727	. . 3 class ℋ
3		cpj 8745	. . 3 class proj
4	2, 3	cfv 3177	. 2 class (proj ‘ ℋ )
5	1, 4	wceq 954	1 wff Iop = (proj ‘ ℋ )

This definition is referenced by:  dfiop2 9619  hoivalt 9621  hoid1 9655  hoid1r 9656  pjclem1 10061  pjclem3 10063  pjc 10066

Copyright terms: Public domain