Metamath Proof Explorer


Axiom ax-hfi

Description: Inner product maps pairs from ~H to CC . (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Assertion ax-hfi
|- .ih : ( ~H X. ~H ) --> CC

Detailed syntax breakdown

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