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 Rel CVec OLD

Proof

Step Hyp Ref Expression
1 df-vc CVec OLD = g s | g AbelOp s : × ran g ran g x ran g 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x
2 1 relopabiv Rel CVec OLD