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 CVecOLD

Proof

Step	Hyp	Ref	Expression
1		df-vc	⊢ CVecOLD = { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ AbelOp ∧ 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) }
2	1	relopabiv	⊢ Rel CVecOLD