Metamath Proof Explorer


Theorem hlmul0

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

Ref Expression
Hypotheses hlmul0.1
|- X = ( BaseSet ` U )
hlmul0.4
|- S = ( .sOLD ` U )
hlmul0.5
|- Z = ( 0vec ` U )
Assertion hlmul0
|- ( ( U e. CHilOLD /\ A e. X ) -> ( 0 S A ) = Z )

Proof

Step Hyp Ref Expression
1 hlmul0.1
 |-  X = ( BaseSet ` U )
2 hlmul0.4
 |-  S = ( .sOLD ` U )
3 hlmul0.5
 |-  Z = ( 0vec ` U )
4 hlnv
 |-  ( U e. CHilOLD -> U e. NrmCVec )
5 1 2 3 nv0
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 0 S A ) = Z )
6 4 5 sylan
 |-  ( ( U e. CHilOLD /\ A e. X ) -> ( 0 S A ) = Z )