Metamath Proof Explorer


Theorem hldir

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

Ref Expression
Hypotheses hldi.1
|- X = ( BaseSet ` U )
hldi.2
|- G = ( +v ` U )
hldi.4
|- S = ( .sOLD ` U )
Assertion hldir
|- ( ( U e. CHilOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )

Proof

Step Hyp Ref Expression
1 hldi.1
 |-  X = ( BaseSet ` U )
2 hldi.2
 |-  G = ( +v ` U )
3 hldi.4
 |-  S = ( .sOLD ` U )
4 hlnv
 |-  ( U e. CHilOLD -> U e. NrmCVec )
5 1 2 3 nvdir
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )
6 4 5 sylan
 |-  ( ( U e. CHilOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )