Metamath Proof Explorer


Theorem nvsid

Description: Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvscl.1
|- X = ( BaseSet ` U )
nvscl.4
|- S = ( .sOLD ` U )
Assertion nvsid
|- ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )

Proof

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 vcidOLD
 |-  ( ( ( 1st ` U ) e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )
10 4 9 sylan
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )