Axiom ax-hfi 10371

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 10212	. . 3 class ~H
2	1, 1	cxp 3795	. 2 class (~H X. ~H)
3		cc 6180	. 2 class CC
4		csp 10217	. 2 class .ih
5	2, 3, 4	wf 3805	1 wff .ih :(~H X. ~H)-->CC

This axiom is referenced by:  hicl 10372  dfhnorm2 10413  hhip 10469

Copyright terms: Public domain