This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipf

Description: Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ipcl.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion ipf ( 𝑈 ∈ NrmCVec → 𝑃 : ( 𝑋 × 𝑋 ) ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 ipcl.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ipcl.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
4 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
5 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
6 1 3 4 5 2 ipval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑃 𝑦 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
7 1 2 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑃 𝑦 ) ∈ ℂ )
8 6 7 eqeltrrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ )
9 8 3expib ⊢ ( 𝑈 ∈ NrmCVec → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ ) )
10 9 ralrimivv ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ )
11 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
12 11 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℂ )
13 10 12 sylib ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℂ )
14 1 3 4 5 2 dipfval ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
15 14 feq1d ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑃 : ( 𝑋 × 𝑋 ) ⟶ ℂ ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℂ ) )
16 13 15 mpbird ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 : ( 𝑋 × 𝑋 ) ⟶ ℂ )