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

Axiom ax-hvmulass 21587
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 8735 . . . 4  class  CC
31, 2wcel 1684 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1684 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
7 chil 21499 . . . 4  class  ~H
86, 7wcel 1684 . . 3  wff  C  e. 
~H
93, 5, 8w3a 934 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e. 
~H )
10 cmul 8742 . . . . 5  class  x.
111, 4, 10co 5858 . . . 4  class  ( A  x.  B )
12 csm 21501 . . . 4  class  .h
1311, 6, 12co 5858 . . 3  class  ( ( A  x.  B )  .h  C )
144, 6, 12co 5858 . . . 4  class  ( B  .h  C )
151, 14, 12co 5858 . . 3  class  ( A  .h  ( B  .h  C ) )
1613, 15wceq 1623 . 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  21603  hvmul0or  21604  hvm1neg  21611  hvmulcom  21622  hvmulassi  21625  hvsubdistr2  21629  hilvc  21741  hhssnv  21841  h1de2bi  22133  spansncol  22147  h1datomi  22160  mayete3i  22307  mayete3iOLD  22308  homulass  22382  kbmul  22535  kbass5  22700  strlem1  22830
  Copyright terms: Public domain W3C validator