Metamath Proof Explorer

Theorem pjmf1

Description: The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjmf1 
|- projh : CH -1-1-> ( ~H ^m ~H )

Proof

Step Hyp Ref Expression
1 pjmfn 
 |-  projh Fn CH
2 pjhf 
 |-  ( x e. CH -> ( projh ` x ) : ~H --> ~H )
3 ax-hilex 
 |-  ~H e. _V
4 3 3 elmap 
 |-  ( ( projh ` x ) e. ( ~H ^m ~H ) <-> ( projh ` x ) : ~H --> ~H )
5 2 4 sylibr 
 |-  ( x e. CH -> ( projh ` x ) e. ( ~H ^m ~H ) )
6 5 rgen 
 |-  A. x e. CH ( projh ` x ) e. ( ~H ^m ~H )
7 ffnfv 
 |-  ( projh : CH --> ( ~H ^m ~H ) <-> ( projh Fn CH /\ A. x e. CH ( projh ` x ) e. ( ~H ^m ~H ) ) )
8 1 6 7 mpbir2an 
 |-  projh : CH --> ( ~H ^m ~H )
9 pj11 
 |-  ( ( x e. CH /\ y e. CH ) -> ( ( projh ` x ) = ( projh ` y ) <-> x = y ) )
10 9 biimpd 
 |-  ( ( x e. CH /\ y e. CH ) -> ( ( projh ` x ) = ( projh ` y ) -> x = y ) )
11 10 rgen2 
 |-  A. x e. CH A. y e. CH ( ( projh ` x ) = ( projh ` y ) -> x = y )
12 dff13 
 |-  ( projh : CH -1-1-> ( ~H ^m ~H ) <-> ( projh : CH --> ( ~H ^m ~H ) /\ A. x e. CH A. y e. CH ( ( projh ` x ) = ( projh ` y ) -> x = y ) ) )
13 8 11 12 mpbir2an 
 |-  projh : CH -1-1-> ( ~H ^m ~H )