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

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