Theorem cncvcOLD

Description: Obsolete version of cncvs . The set of complex numbers is a complex vector space. The vector operation is + , and the scalar product is x. . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	cncvcOLD	⊢ ⟨ + , · ⟩ ∈ CVecOLD

Proof

Step	Hyp	Ref	Expression
1		cnaddabloOLD	⊢ + ∈ AbelOp
2		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
3	2	fdmi	⊢ dom + = ( ℂ × ℂ )
4		ax-mulf	⊢ · : ( ℂ × ℂ ) ⟶ ℂ
5		mulid2	⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
6		adddi	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
7		adddir	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
8		mulass	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
9		eqid	⊢ ⟨ + , · ⟩ = ⟨ + , · ⟩
10	1 3 4 5 6 7 8 9	isvciOLD	⊢ ⟨ + , · ⟩ ∈ CVecOLD