Metamath Proof Explorer

Theorem phrel

Description: The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion phrel 
|- Rel CPreHilOLD

Proof

Step Hyp Ref Expression
1 phnv 
 |-  ( x e. CPreHilOLD -> x e. NrmCVec )
2 1 ssriv 
 |-  CPreHilOLD C_ NrmCVec
3 nvrel 
 |-  Rel NrmCVec
4 relss 
 |-  ( CPreHilOLD C_ NrmCVec -> ( Rel NrmCVec -> Rel CPreHilOLD ) )
5 2 3 4 mp2 
 |-  Rel CPreHilOLD