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

Metamath Proof Explorer

Theorem dfiop2

Description: Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion dfiop2 
|- Iop = ( _I |` ~H )

Proof

Step Hyp Ref Expression
1 df-iop 
 |-  Iop = ( projh ` ~H )
2 helch 
 |-  ~H e. CH
3 2 pjfni 
 |-  ( projh ` ~H ) Fn ~H
4 fnresi 
 |-  ( _I |` ~H ) Fn ~H
5 pjch1 
 |-  ( x e. ~H -> ( ( projh ` ~H ) ` x ) = x )
6 fvresi 
 |-  ( x e. ~H -> ( ( _I |` ~H ) ` x ) = x )
7 5 6 eqtr4d 
 |-  ( x e. ~H -> ( ( projh ` ~H ) ` x ) = ( ( _I |` ~H ) ` x ) )
8 7 rgen 
 |-  A. x e. ~H ( ( projh ` ~H ) ` x ) = ( ( _I |` ~H ) ` x )
9 eqfnfv 
 |-  ( ( ( projh ` ~H ) Fn ~H /\ ( _I |` ~H ) Fn ~H ) -> ( ( projh ` ~H ) = ( _I |` ~H ) <-> A. x e. ~H ( ( projh ` ~H ) ` x ) = ( ( _I |` ~H ) ` x ) ) )
10 8 9 mpbiri 
 |-  ( ( ( projh ` ~H ) Fn ~H /\ ( _I |` ~H ) Fn ~H ) -> ( projh ` ~H ) = ( _I |` ~H ) )
11 3 4 10 mp2an 
 |-  ( projh ` ~H ) = ( _I |` ~H )
12 1 11 eqtri 
 |-  Iop = ( _I |` ~H )