HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvmulass Unicode version

Axiom ax-hvmulass 21533
Description: Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvmulass  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  ~H )  ->  (
( A  x.  B
)  .h  C )  =  ( A  .h  ( B  .h  C
) ) )

Detailed syntax breakdown of Axiom ax-hvmulass
StepHypRef Expression
1 cA . . . 4  class  A
2 cc 8689 . . . 4  class  CC
31, 2wcel 1621 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1621 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
7 chil 21445 . . . 4  class  ~H
86, 7wcel 1621 . . 3  wff  C  e. 
~H
93, 5, 8w3a 939 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e. 
~H )
10 cmul 8696 . . . . 5  class  x.
111, 4, 10co 5778 . . . 4  class  ( A  x.  B )
12 csm 21447 . . . 4  class  .h
1311, 6, 12co 5778 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 5778 . . . 4  class  ( B  .h  C )
151, 14, 12co 5778 . . 3  class  ( A  .h  ( B  .h  C ) )
1613, 15wceq 1619 . 2  wff  ( ( A  x.  B )  .h  C )  =  ( A  .h  ( B  .h  C )
)
179, 16wi 6 1  wff  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  ~H )  ->  (
( A  x.  B
)  .h  C )  =  ( A  .h  ( B  .h  C
) ) )
Colors of variables: wff set class
This axiom is referenced by:  hvmul0  21549  hvmul0or  21550  hvm1neg  21557  hvmulcom  21568  hvmulassi  21571  hvsubdistr2  21575  hilvc  21687  hhssnv  21787  h1de2bi  22079  spansncol  22093  h1datomi  22106  mayete3i  22271  mayete3iOLD  22272  homulass  22328  kbmul  22481  kbass5  22646  strlem1  22776
  Copyright terms: Public domain W3C validator