Definition df-sm

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

	Ref	Expression
Assertion	df-sm	$$⊢{\cdot }_{\mathrm{𝑠OLD}}=2^{nd}\circ 1^{st}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cns	$$class{\cdot }_{\mathrm{𝑠OLD}}$$
1		c2nd	$$class{2}^{nd}$$
2		c1st	$$class{1}^{st}$$
3	1 2	ccom	$$class\left(2^{nd}\circ 1^{st}\right)$$
4	0 3	wceq	$$wff{\cdot }_{\mathrm{𝑠OLD}}=2^{nd}\circ 1^{st}$$