Description: The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hhnv.1 | |
|
Assertion | hhph | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hhnv.1 | |
|
2 | eqid | |
|
3 | 2 | hhnv | |
4 | normpar | |
|
5 | hvsubval | |
|
6 | 5 | fveq2d | |
7 | 6 | oveq1d | |
8 | 7 | oveq2d | |
9 | hvaddcl | |
|
10 | normcl | |
|
11 | 9 10 | syl | |
12 | 11 | recnd | |
13 | 12 | sqcld | |
14 | hvsubcl | |
|
15 | normcl | |
|
16 | 15 | recnd | |
17 | 14 16 | syl | |
18 | 17 | sqcld | |
19 | 13 18 | addcomd | |
20 | 8 19 | eqtr3d | |
21 | normcl | |
|
22 | 21 | recnd | |
23 | 22 | sqcld | |
24 | normcl | |
|
25 | 24 | recnd | |
26 | 25 | sqcld | |
27 | 2cn | |
|
28 | adddi | |
|
29 | 27 28 | mp3an1 | |
30 | 23 26 29 | syl2an | |
31 | 4 20 30 | 3eqtr4d | |
32 | 31 | rgen2 | |
33 | hilablo | |
|
34 | 33 | elexi | |
35 | hvmulex | |
|
36 | normf | |
|
37 | ax-hilex | |
|
38 | fex | |
|
39 | 36 37 38 | mp2an | |
40 | 1 | eleq1i | |
41 | ablogrpo | |
|
42 | 33 41 | ax-mp | |
43 | ax-hfvadd | |
|
44 | 43 | fdmi | |
45 | 42 44 | grporn | |
46 | 45 | isphg | |
47 | 40 46 | syl5bb | |
48 | 34 35 39 47 | mp3an | |
49 | 3 32 48 | mpbir2an | |