Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > ax-hfi | Structured version Visualization version GIF version |
Description: Inner product maps pairs from ℋ to ℂ. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-hfi | ⊢ ·ih :( ℋ × ℋ)⟶ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chil 27776 | . . 3 class ℋ | |
2 | 1, 1 | cxp 5112 | . 2 class ( ℋ × ℋ) |
3 | cc 9934 | . 2 class ℂ | |
4 | csp 27779 | . 2 class ·ih | |
5 | 2, 3, 4 | wf 5884 | 1 wff ·ih :( ℋ × ℋ)⟶ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: hicl 27937 dfhnorm2 27979 hhip 28034 |
Copyright terms: Public domain | W3C validator |