Theorem vcrel

Description: The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	vcrel	$$⊢\mathrm{Rel}{CVec}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		df-vc	$$⊢{CVec}_{\mathrm{OLD}}=\left\{⟨g,s⟩|\left(g\in \mathrm{AbelOp}\wedge s:ℂ\times \mathrm{ran}g⟶\mathrm{ran}g\wedge \forall x\in \mathrm{ran}g\left(1sx=x\wedge \forall y\in ℂ\left(\forall z\in \mathrm{ran}gys\left(xgz\right)=\left(ysx\right)g\left(ysz\right)\wedge \forall z\in ℂ\left(\left(y+z\right)sx=\left(ysx\right)g\left(zsx\right)\wedge yzsx=ys\left(zsx\right)\right)\right)\right)\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}{CVec}_{\mathrm{OLD}}$$