Metamath Proof Explorer


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 RelCVecOLD

Proof

Step Hyp Ref Expression
1 df-vc CVecOLD=gs|gAbelOps:×rangrangxrang1sx=xyzrangysxgz=ysxgyszzy+zsx=ysxgzsxyzsx=yszsx
2 1 relopabiv RelCVecOLD