Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfsm  Unicode version 
Description: Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24Apr2007.) (New usage is discouraged.) 
Ref  Expression 

dfsm 
Step  Hyp  Ref  Expression 

1  cns 21986  . 2  
2  c2nd 6301  . . 3  
3  c1st 6300  . . 3  
4  2, 3  ccom 4836  . 2 
5  1, 4  wceq 1649  1 
Colors of variables: wff set class 
This definition is referenced by: smfval 22004 
Copyright terms: Public domain  W3C validator 