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 : ( ℋ × ℋ ) ⟶ ℂ

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csp	⊢ ·ih
1		chba	⊢ ℋ
2	1 1	cxp	⊢ ( ℋ × ℋ )
3		cc	⊢ ℂ
4	2 3 0	wf	⊢ ·ih : ( ℋ × ℋ ) ⟶ ℂ