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

Axiom ax-hvmulass 22502
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 8980 . . . 4  class  CC
31, 2wcel 1725 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1725 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
7 chil 22414 . . . 4  class  ~H
86, 7wcel 1725 . . 3  wff  C  e. 
~H
93, 5, 8w3a 936 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e. 
~H )
10 cmul 8987 . . . . 5  class  x.
111, 4, 10co 6073 . . . 4  class  ( A  x.  B )
12 csm 22416 . . . 4  class  .h
1311, 6, 12co 6073 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 6073 . . . 4  class  ( B  .h  C )
151, 14, 12co 6073 . . 3  class  ( A  .h  ( B  .h  C ) )
1613, 15wceq 1652 . 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  22518  hvmul0or  22519  hvm1neg  22526  hvmulcom  22537  hvmulassi  22540  hvsubdistr2  22544  hilvc  22656  hhssnv  22756  h1de2bi  23048  spansncol  23062  h1datomi  23075  mayete3i  23222  mayete3iOLD  23223  homulass  23297  kbmul  23450  kbass5  23615  strlem1  23745
  Copyright terms: Public domain W3C validator