Metamath Proof Explorer

Theorem hhip

Description: The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion hhip ·ih = ( ·𝑖OLD ‘ 𝑈 )

Proof

Step Hyp Ref Expression
1 hhnv.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 polid ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih 𝑦 ) = ( ( ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝑥 +ℎ ( i ·ℎ 𝑦 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝑥 −ℎ ( i ·ℎ 𝑦 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
3 1 hhnv ⊢ 𝑈 ∈ NrmCVec
4 1 hhba ⊢ ℋ = ( BaseSet ‘ 𝑈 )
5 1 hhva ⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
6 1 hhsm ⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
7 1 hhnm ⊢ normℎ = ( normCV ‘ 𝑈 )
8 eqid ⊢ ( ·𝑖OLD ‘ 𝑈 ) = ( ·𝑖OLD ‘ 𝑈 )
9 1 hhvs ⊢ −ℎ = ( −𝑣 ‘ 𝑈 )
10 4 5 6 7 8 9 ipval3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 ) = ( ( ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝑥 +ℎ ( i ·ℎ 𝑦 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝑥 −ℎ ( i ·ℎ 𝑦 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
11 3 10 mp3an1 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 ) = ( ( ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) + ( i · ( ( ( normℎ ‘ ( 𝑥 +ℎ ( i ·ℎ 𝑦 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝑥 −ℎ ( i ·ℎ 𝑦 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
12 2 11 eqtr4d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 ) )
13 12 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 )
14 ax-hfi ⊢ ·ih : ( ℋ × ℋ ) ⟶ ℂ
15 4 8 ipf ⊢ ( 𝑈 ∈ NrmCVec → ( ·𝑖OLD ‘ 𝑈 ) : ( ℋ × ℋ ) ⟶ ℂ )
16 3 15 ax-mp ⊢ ( ·𝑖OLD ‘ 𝑈 ) : ( ℋ × ℋ ) ⟶ ℂ
17 ffn ⊢ ( ·ih : ( ℋ × ℋ ) ⟶ ℂ → ·ih Fn ( ℋ × ℋ ) )
18 ffn ⊢ ( ( ·𝑖OLD ‘ 𝑈 ) : ( ℋ × ℋ ) ⟶ ℂ → ( ·𝑖OLD ‘ 𝑈 ) Fn ( ℋ × ℋ ) )
19 eqfnov2 ⊢ ( ( ·ih Fn ( ℋ × ℋ ) ∧ ( ·𝑖OLD ‘ 𝑈 ) Fn ( ℋ × ℋ ) ) → ( ·ih = ( ·𝑖OLD ‘ 𝑈 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 ) ) )
20 17 18 19 syl2an ⊢ ( ( ·ih : ( ℋ × ℋ ) ⟶ ℂ ∧ ( ·𝑖OLD ‘ 𝑈 ) : ( ℋ × ℋ ) ⟶ ℂ ) → ( ·ih = ( ·𝑖OLD ‘ 𝑈 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 ) ) )
21 14 16 20 mp2an ⊢ ( ·ih = ( ·𝑖OLD ‘ 𝑈 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) 𝑦 ) )
22 13 21 mpbir ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )