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

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}$

Step	Hyp	Ref	Expression
1		phnv	$⊢ x \in {CPreHil}_{OLD} \to x \in NrmCVec$
2	1	ssriv	$⊢ {CPreHil}_{OLD} \subseteq NrmCVec$
3		nvrel	$⊢ Rel NrmCVec$
4		relss	$⊢ {CPreHil}_{OLD} \subseteq NrmCVec \to (Rel NrmCVec \to Rel {CPreHil}_{OLD})$
5	2 3 4	mp2	$⊢ Rel {CPreHil}_{OLD}$