Description: Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hvmulcom.1 | |- A e. CC |
|
hvmulcom.2 | |- B e. CC |
||
hvmulcom.3 | |- C e. ~H |
||
Assertion | hvmulassi | |- ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hvmulcom.1 | |- A e. CC |
|
2 | hvmulcom.2 | |- B e. CC |
|
3 | hvmulcom.3 | |- C e. ~H |
|
4 | ax-hvmulass | |- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) ) |
|
5 | 1 2 3 4 | mp3an | |- ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) |