Metamath Proof Explorer

Theorem hhph

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 ⊢ U = + ℎ ⋅ ℎ norm ℎ
Assertion hhph ⊢ U ∈ CPreHil OLD

Proof

Step Hyp Ref Expression
1 hhnv.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
3 2 hhnv ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec
4 normpar ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x - ℎ y 2 + norm ℎ ⁡ x + ℎ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + 2 ⁢ norm ℎ ⁡ y 2
5 hvsubval ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y = x + ℎ -1 ⋅ ℎ y
6 5 fveq2d ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x - ℎ y = norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y
7 6 oveq1d ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x - ℎ y 2 = norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2
8 7 oveq2d ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x - ℎ y 2 = norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2
9 hvaddcl ⊢ x ∈ ℋ ∧ y ∈ ℋ → x + ℎ y ∈ ℋ
10 normcl ⊢ x + ℎ y ∈ ℋ → norm ℎ ⁡ x + ℎ y ∈ ℝ
11 9 10 syl ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y ∈ ℝ
12 11 recnd ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y ∈ ℂ
13 12 sqcld ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y 2 ∈ ℂ
14 hvsubcl ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ∈ ℋ
15 normcl ⊢ x - ℎ y ∈ ℋ → norm ℎ ⁡ x - ℎ y ∈ ℝ
16 15 recnd ⊢ x - ℎ y ∈ ℋ → norm ℎ ⁡ x - ℎ y ∈ ℂ
17 14 16 syl ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x - ℎ y ∈ ℂ
18 17 sqcld ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x - ℎ y 2 ∈ ℂ
19 13 18 addcomd ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x - ℎ y 2 = norm ℎ ⁡ x - ℎ y 2 + norm ℎ ⁡ x + ℎ y 2
20 8 19 eqtr3d ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2 = norm ℎ ⁡ x - ℎ y 2 + norm ℎ ⁡ x + ℎ y 2
21 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
22 21 recnd ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℂ
23 22 sqcld ⊢ x ∈ ℋ → norm ℎ ⁡ x 2 ∈ ℂ
24 normcl ⊢ y ∈ ℋ → norm ℎ ⁡ y ∈ ℝ
25 24 recnd ⊢ y ∈ ℋ → norm ℎ ⁡ y ∈ ℂ
26 25 sqcld ⊢ y ∈ ℋ → norm ℎ ⁡ y 2 ∈ ℂ
27 2cn ⊢ 2 ∈ ℂ
28 adddi ⊢ 2 ∈ ℂ ∧ norm ℎ ⁡ x 2 ∈ ℂ ∧ norm ℎ ⁡ y 2 ∈ ℂ → 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + 2 ⁢ norm ℎ ⁡ y 2
29 27 28 mp3an1 ⊢ norm ℎ ⁡ x 2 ∈ ℂ ∧ norm ℎ ⁡ y 2 ∈ ℂ → 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + 2 ⁢ norm ℎ ⁡ y 2
30 23 26 29 syl2an ⊢ x ∈ ℋ ∧ y ∈ ℋ → 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + 2 ⁢ norm ℎ ⁡ y 2
31 4 20 30 3eqtr4d ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2
32 31 rgen2 ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2
33 hilablo ⊢ + ℎ ∈ AbelOp
34 33 elexi ⊢ + ℎ ∈ V
35 hvmulex ⊢ ⋅ ℎ ∈ V
36 normf ⊢ norm ℎ : ℋ ⟶ ℝ
37 ax-hilex ⊢ ℋ ∈ V
38 fex ⊢ norm ℎ : ℋ ⟶ ℝ ∧ ℋ ∈ V → norm ℎ ∈ V
39 36 37 38 mp2an ⊢ norm ℎ ∈ V
40 1 eleq1i ⊢ U ∈ CPreHil OLD ↔ + ℎ ⋅ ℎ norm ℎ ∈ CPreHil OLD
41 ablogrpo ⊢ + ℎ ∈ AbelOp → + ℎ ∈ GrpOp
42 33 41 ax-mp ⊢ + ℎ ∈ GrpOp
43 ax-hfvadd ⊢ + ℎ : ℋ × ℋ ⟶ ℋ
44 43 fdmi ⊢ dom ⁡ + ℎ = ℋ × ℋ
45 42 44 grporn ⊢ ℋ = ran ⁡ + ℎ
46 45 isphg ⊢ + ℎ ∈ V ∧ ⋅ ℎ ∈ V ∧ norm ℎ ∈ V → + ℎ ⋅ ℎ norm ℎ ∈ CPreHil OLD ↔ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2
47 40 46 bitrid ⊢ + ℎ ∈ V ∧ ⋅ ℎ ∈ V ∧ norm ℎ ∈ V → U ∈ CPreHil OLD ↔ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2
48 34 35 39 47 mp3an ⊢ U ∈ CPreHil OLD ↔ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ norm ℎ ⁡ x + ℎ y 2 + norm ℎ ⁡ x + ℎ -1 ⋅ ℎ y 2 = 2 ⁢ norm ℎ ⁡ x 2 + norm ℎ ⁡ y 2
49 3 32 48 mpbir2an ⊢ U ∈ CPreHil OLD