Metamath Proof Explorer

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 
|- .sOLD = ( 2nd o. 1st )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cns 
 |-  .sOLD
1 c2nd 
 |-  2nd
2 c1st 
 |-  1st
3 1 2 ccom 
 |-  ( 2nd o. 1st )
4 0 3 wceq 
 |-  .sOLD = ( 2nd o. 1st )