df-sm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-sm		Structured version Visualization version GIF version

Definition df-sm 28938

Description: Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)

**Assertion**
Ref	Expression
df-sm	⊢ ·_𝑠OLD = (2^nd ∘ 1^st )

**Detailed syntax breakdown of Definition df-sm**
Step	Hyp	Ref	Expression
1		cns 28928	. 2 class ·_𝑠OLD
2		c2nd 7816	. . 3 class 2^nd
3		c1st 7815	. . 3 class 1^st
4	2, 3	ccom 5592	. 2 class (2^nd ∘ 1^st )
5	1, 4	wceq 1541	1 wff ·_𝑠OLD = (2^nd ∘ 1^st )

Colors of variables: wff setvar class

This definition is referenced by: smfval 28946