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

Axiom ax-hvmulass 21417
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 8615 . . . 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 21329 . . . 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 8622 . . . . 5  class  x.
111, 4, 10co 5710 . . . 4  class  ( A  x.  B )
12 csm 21331 . . . 4  class  .h
1311, 6, 12co 5710 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 5710 . . . 4  class  ( B  .h  C )
151, 14, 12co 5710 . . 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  21433  hvmul0or  21434  hvm1neg  21441  hvmulcom  21452  hvmulassi  21455  hvsubdistr2  21459  hilvc  21571  hhssnv  21671  h1de2bi  21963  spansncol  21977  h1datomi  21990  mayete3i  22155  mayete3iOLD  22156  homulass  22212  kbmul  22365  kbass5  22530  strlem1  22660
  Copyright terms: Public domain W3C validator