Description: Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1Feb2007) (New usage is discouraged.)
Ref  Expression  

Hypotheses  nvscl.1   X = ( BaseSet ` U ) 

nvscl.4   S = ( .sOLD ` U ) 

Assertion  nvscl   ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) > ( A S B ) e. X ) 
Step  Hyp  Ref  Expression 

1  nvscl.1   X = ( BaseSet ` U ) 

2  nvscl.4   S = ( .sOLD ` U ) 

3  eqid   ( 1st ` U ) = ( 1st ` U ) 

4  3  nvvc   ( U e. NrmCVec > ( 1st ` U ) e. CVecOLD ) 
5  eqid   ( +v ` U ) = ( +v ` U ) 

6  5  vafval   ( +v ` U ) = ( 1st ` ( 1st ` U ) ) 
7  2  smfval   S = ( 2nd ` ( 1st ` U ) ) 
8  1 5  bafval   X = ran ( +v ` U ) 
9  6 7 8  vccl   ( ( ( 1st ` U ) e. CVecOLD /\ A e. CC /\ B e. X ) > ( A S B ) e. X ) 
10  4 9  syl3an1   ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) > ( A S B ) e. X ) 