Axiom ax-hfi 8901

Description: Inner product maps pairs from H~ to CC.

Assertion

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

Detailed syntax breakdown of Axiom ax-hfi

Step	Hyp	Ref	Expression
1		chil 8743	. . 3 class H~
2	1, 1	cxp 3166	. 2 class (H~ X. H~)
3		cc 5220	. 2 class CC
4		csp 8748	. 2 class .ih
5	2, 3, 4	wf 3176	1 wff .ih :(H~ X. H~)-->CC

This axiom is referenced by:  hiclt 8902  dfhnorm2 8943  hhip 8999

Copyright terms: Public domain