Description: The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hhnv.1 | ||
hhims2.2 | |||
Assertion | hhxmet |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hhnv.1 | ||
2 | hhims2.2 | ||
3 | 1 2 | hhmet | |
4 | metxmet | ||
5 | 3 4 | ax-mp |