Metamath Proof Explorer

Axiom ax-hfvmul

Description: Scalar multiplication is an operation on CC and ~H . (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-hfvmul 
|- .h : ( CC X. ~H ) --> ~H

Detailed syntax breakdown

Step Hyp Ref Expression
0 csm 
 |-  .h
1 cc 
 |-  CC
2 chba 
 |-  ~H
3 1 2 cxp 
 |-  ( CC X. ~H )
4 3 2 0 wf 
 |-  .h : ( CC X. ~H ) --> ~H