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 CPreHil OLD

Proof

Step Hyp Ref Expression
1 phnv x CPreHil OLD x NrmCVec
2 1 ssriv CPreHil OLD NrmCVec
3 nvrel Rel NrmCVec
4 relss CPreHil OLD NrmCVec Rel NrmCVec Rel CPreHil OLD
5 2 3 4 mp2 Rel CPreHil OLD