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 ) |
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 ) |