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 )