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	$⊢ ⟨+ \times⟩ \in {CVec}_{OLD}$

Proof

Step	Hyp	Ref	Expression
1		cnaddabloOLD	$⊢ + \in AbelOp$
2		ax-addf	$⊢ + : ℂ \times ℂ ⟶ ℂ$
3	2	fdmi	$⊢ dom + = ℂ \times ℂ$
4		ax-mulf	$⊢ \times : ℂ \times ℂ ⟶ ℂ$
5		mullid	$⊢ x \in ℂ \to 1 x = x$
6		adddi	$⊢ (y \in ℂ \land x \in ℂ \land z \in ℂ) \to y (x + z) = y x + y z$
7		adddir	$⊢ (y \in ℂ \land z \in ℂ \land x \in ℂ) \to (y + z) x = y x + z x$
8		mulass	$⊢ (y \in ℂ \land z \in ℂ \land x \in ℂ) \to y z x = y z x$
9		eqid	$⊢ ⟨+ \times⟩ = ⟨+ \times⟩$
10	1 3 4 5 6 7 8 9	isvciOLD	$⊢ ⟨+ \times⟩ \in {CVec}_{OLD}$

Metamath Proof Explorer

Theorem cncvcOLD

Proof