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

Axiom ax-hvmulass 21512
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 8668 . . . 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 21424 . . . 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 8675 . . . . 5  class  x.
111, 4, 10co 5757 . . . 4  class  ( A  x.  B )
12 csm 21426 . . . 4  class  .h
1311, 6, 12co 5757 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 5757 . . . 4  class  ( B  .h  C )
151, 14, 12co 5757 . . 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  21528  hvmul0or  21529  hvm1neg  21536  hvmulcom  21547  hvmulassi  21550  hvsubdistr2  21554  hilvc  21666  hhssnv  21766  h1de2bi  22058  spansncol  22072  h1datomi  22085  mayete3i  22250  mayete3iOLD  22251  homulass  22307  kbmul  22460  kbass5  22625  strlem1  22755
  Copyright terms: Public domain W3C validator