Axiom ax-hfi 8867

Description: Inner product maps pairs from ℋ to ℂ.

Assertion

Ref	Expression
ax-hfi	⊢ ·ih :( ℋ × ℋ )–→ℂ

Detailed syntax breakdown of Axiom ax-hfi

Step	Hyp	Ref	Expression
1		chil 8727	. . 3 class ℋ
2	1, 1	cxp 3158	. 2 class ( ℋ × ℋ )
3		cc 5204	. 2 class ℂ
4		csp 8732	. 2 class ·ih
5	2, 3, 4	wf 3168	1 wff ·ih :( ℋ × ℋ )–→ℂ

This axiom is referenced by:  hiclt 8868  dfhnorm2 8909  hhip 8965

Copyright terms: Public domain