Definition df-sm 8212

Description: Define scalar multiplication on a normed complex vector space.

Assertion

Ref	Expression
df-sm	|- .s = (2nd o. 1st)

Detailed syntax breakdown of Definition df-sm

Step	Hyp	Ref	Expression
1		cns 8202	. 2 class .s
2		c2nd 4084	. . 3 class 2nd
3		c1st 4083	. . 3 class 1st
4	2, 3	ccom 3180	. 2 class (2nd o. 1st)
5	1, 4	wceq 958	1 wff .s = (2nd o. 1st)

This definition is referenced by:  smfval 8220

Copyright terms: Public domain