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

Axiom ax-hvmulass 22463
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 8944 . . . 4  class  CC
31, 2wcel 1721 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1721 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
7 chil 22375 . . . 4  class  ~H
86, 7wcel 1721 . . 3  wff  C  e. 
~H
93, 5, 8w3a 936 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e. 
~H )
10 cmul 8951 . . . . 5  class  x.
111, 4, 10co 6040 . . . 4  class  ( A  x.  B )
12 csm 22377 . . . 4  class  .h
1311, 6, 12co 6040 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 6040 . . . 4  class  ( B  .h  C )
151, 14, 12co 6040 . . 3  class  ( A  .h  ( B  .h  C ) )
1613, 15wceq 1649 . 2  wff  ( ( A  x.  B )  .h  C )  =  ( A  .h  ( B  .h  C )
)
179, 16wi 4 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  22479  hvmul0or  22480  hvm1neg  22487  hvmulcom  22498  hvmulassi  22501  hvsubdistr2  22505  hilvc  22617  hhssnv  22717  h1de2bi  23009  spansncol  23023  h1datomi  23036  mayete3i  23183  mayete3iOLD  23184  homulass  23258  kbmul  23411  kbass5  23576  strlem1  23706
  Copyright terms: Public domain W3C validator