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 ⊢ X = BaseSet ⁡ U
ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion ipf ⊢ U ∈ NrmCVec → P : X × X ⟶ ℂ

Proof

Step Hyp Ref Expression
1 ipcl.1 ⊢ X = BaseSet ⁡ U
2 ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
3 eqid ⊢ + v ⁡ U = + v ⁡ U
4 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
5 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
6 1 3 4 5 2 ipval ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → x P y = ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4
7 1 2 dipcl ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → x P y ∈ ℂ
8 6 7 eqeltrrd ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 ∈ ℂ
9 8 3expib ⊢ U ∈ NrmCVec → x ∈ X ∧ y ∈ X → ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 ∈ ℂ
10 9 ralrimivv ⊢ U ∈ NrmCVec → ∀ x ∈ X ∀ y ∈ X ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 ∈ ℂ
11 eqid ⊢ x ∈ X , y ∈ X ⟼ ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 = x ∈ X , y ∈ X ⟼ ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4
12 11 fmpo ⊢ ∀ x ∈ X ∀ y ∈ X ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 ∈ ℂ ↔ x ∈ X , y ∈ X ⟼ ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 : X × X ⟶ ℂ
13 10 12 sylib ⊢ U ∈ NrmCVec → x ∈ X , y ∈ X ⟼ ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 : X × X ⟶ ℂ
14 1 3 4 5 2 dipfval ⊢ U ∈ NrmCVec → P = x ∈ X , y ∈ X ⟼ ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4
15 14 feq1d ⊢ U ∈ NrmCVec → P : X × X ⟶ ℂ ↔ x ∈ X , y ∈ X ⟼ ∑ k = 1 4 i k ⁢ norm CV ⁡ U ⁡ x + v ⁡ U i k ⋅ 𝑠OLD ⁡ U y 2 4 : X × X ⟶ ℂ
16 13 15 mpbird ⊢ U ∈ NrmCVec → P : X × X ⟶ ℂ