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

Axiom ax-hvmulass 21581
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 8732 . . . 4  class  CC
31, 2wcel 1687 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1687 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
7 chil 21493 . . . 4  class  ~H
86, 7wcel 1687 . . 3  wff  C  e. 
~H
93, 5, 8w3a 936 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e. 
~H )
10 cmul 8739 . . . . 5  class  x.
111, 4, 10co 5821 . . . 4  class  ( A  x.  B )
12 csm 21495 . . . 4  class  .h
1311, 6, 12co 5821 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 5821 . . . 4  class  ( B  .h  C )
151, 14, 12co 5821 . . 3  class  ( A  .h  ( B  .h  C ) )
1613, 15wceq 1625 . 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  21597  hvmul0or  21598  hvm1neg  21605  hvmulcom  21616  hvmulassi  21619  hvsubdistr2  21623  hilvc  21735  hhssnv  21835  h1de2bi  22127  spansncol  22141  h1datomi  22154  mayete3i  22301  mayete3iOLD  22302  homulass  22376  kbmul  22529  kbass5  22694  strlem1  22824
  Copyright terms: Public domain W3C validator