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 28678

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 28668	. 2 class ·_𝑠OLD
2		c2nd 7760	. . 3 class 2^nd
3		c1st 7759	. . 3 class 1^st
4	2, 3	ccom 5555	. 2 class (2^nd ∘ 1^st )
5	1, 4	wceq 1543	1 wff ·_𝑠OLD = (2^nd ∘ 1^st )

Colors of variables: wff setvar class

This definition is referenced by: smfval 28686