Metamath Proof Explorer
Description: The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypothesis |
hhnv.1 |
|
|
Assertion |
hhsm |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
hhnv.1 |
|
2 |
1
|
hhnv |
|
3 |
1 2
|
h2hsm |
|