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 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion hhph 𝑈 ∈ CPreHilOLD

Proof

Step Hyp Ref Expression
1 hhnv.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
3 2 hhnv ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
4 normpar ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
5 hvsubval ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
6 5 fveq2d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) )
7 6 oveq1d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) = ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) )
8 7 oveq2d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) )
9 hvaddcl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
10 normcl ⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ℝ )
11 9 10 syl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ℂ )
13 12 sqcld ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ∈ ℂ )
14 hvsubcl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 −ℎ 𝑦 ) ∈ ℋ )
15 normcl ⊢ ( ( 𝑥 −ℎ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ∈ ℝ )
16 15 recnd ⊢ ( ( 𝑥 −ℎ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ∈ ℂ )
17 14 16 syl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ∈ ℂ )
18 17 sqcld ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ∈ ℂ )
19 13 18 addcomd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ) )
20 8 19 eqtr3d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ) )
21 normcl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
22 21 recnd ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℂ )
23 22 sqcld ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
24 normcl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
25 24 recnd ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℂ )
26 25 sqcld ⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ∈ ℂ )
27 2cn ⊢ 2 ∈ ℂ
28 adddi ⊢ ( ( 2 ∈ ℂ ∧ ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ∈ ℂ ∧ ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
29 27 28 mp3an1 ⊢ ( ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ∈ ℂ ∧ ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
30 23 26 29 syl2an ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
31 4 20 30 3eqtr4d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
32 31 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 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 ⊢ ( 𝑈 ∈ CPreHilOLD ↔ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ CPreHilOLD )
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ℎ ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
47 40 46 syl5bb ⊢ ( ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) → ( 𝑈 ∈ CPreHilOLD ↔ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
48 34 35 39 47 mp3an ⊢ ( 𝑈 ∈ CPreHilOLD ↔ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) ) )
49 3 32 48 mpbir2an ⊢ 𝑈 ∈ CPreHilOLD