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	$$⊢{\cdot }_{\mathrm{ih}}:\mathscr{H}\times \mathscr{H}⟶ℂ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csp	$$class{\cdot }_{\mathrm{ih}}$$
1		chba	$$class\mathscr{H}$$
2	1 1	cxp	$$class\left(\mathscr{H}\times \mathscr{H}\right)$$
3		cc	$$classℂ$$
4	2 3 0	wf	$$wff{\cdot }_{\mathrm{ih}}:\mathscr{H}\times \mathscr{H}⟶ℂ$$