This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-iop

Description: Define the Hilbert space identity operator. See dfiop2 for alternate definition. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 chio 
 |-  Iop
1 cpjh 
 |-  projh
2 chba 
 |-  ~H
3 2 1 cfv 
 |-  ( projh ` ~H )
4 0 3 wceq 
 |-  Iop = ( projh ` ~H )