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

Axiom ax-hvmulass 21603
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 8751 . . . 4  class  CC
31, 2wcel 1696 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1696 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
7 chil 21515 . . . 4  class  ~H
86, 7wcel 1696 . . 3  wff  C  e. 
~H
93, 5, 8w3a 934 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e. 
~H )
10 cmul 8758 . . . . 5  class  x.
111, 4, 10co 5874 . . . 4  class  ( A  x.  B )
12 csm 21517 . . . 4  class  .h
1311, 6, 12co 5874 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 5874 . . . 4  class  ( B  .h  C )
151, 14, 12co 5874 . . 3  class  ( A  .h  ( B  .h  C ) )
1613, 15wceq 1632 . 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  21619  hvmul0or  21620  hvm1neg  21627  hvmulcom  21638  hvmulassi  21641  hvsubdistr2  21645  hilvc  21757  hhssnv  21857  h1de2bi  22149  spansncol  22163  h1datomi  22176  mayete3i  22323  mayete3iOLD  22324  homulass  22398  kbmul  22551  kbass5  22716  strlem1  22846
  Copyright terms: Public domain W3C validator