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

Axiom ax-hfvmul 21415
Description: Scalar multiplication is an operation on  CC and  ~H. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hfvmul  |-  .h  :
( CC  X.  ~H )
--> ~H

Detailed syntax breakdown of Axiom ax-hfvmul
StepHypRef Expression
1 cc 8615 . . 3  class  CC
2 chil 21329 . . 3  class  ~H
31, 2cxp 4578 . 2  class  ( CC 
X.  ~H )
4 csm 21331 . 2  class  .h
53, 2, 4wf 4588 1  wff  .h  :
( CC  X.  ~H )
--> ~H
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21421  hvmulcl  21423  hilvc  21571  issh2  21618  hhssabloi  21669  hhssnv  21671  hhsssh  21676
  Copyright terms: Public domain W3C validator