Metamath Proof Explorer


Theorem hlmulid

Description: Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlmulf.1
|- X = ( BaseSet ` U )
hlmulf.4
|- S = ( .sOLD ` U )
Assertion hlmulid
|- ( ( U e. CHilOLD /\ A e. X ) -> ( 1 S A ) = A )

Proof

Step Hyp Ref Expression
1 hlmulf.1
 |-  X = ( BaseSet ` U )
2 hlmulf.4
 |-  S = ( .sOLD ` U )
3 hlnv
 |-  ( U e. CHilOLD -> U e. NrmCVec )
4 1 2 nvsid
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )
5 3 4 sylan
 |-  ( ( U e. CHilOLD /\ A e. X ) -> ( 1 S A ) = A )