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