MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dipfval Structured version   Visualization version   GIF version
Theorem dipfval 29942
Description: The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
dipfval.1 𝑋 = (BaseSetβ€˜π‘ˆ)
dipfval.2 𝐺 = ( +𝑣 β€˜π‘ˆ)
dipfval.4 𝑆 = ( ·𝑠OLD β€˜π‘ˆ)
dipfval.6 𝑁 = (normCVβ€˜π‘ˆ)
dipfval.7 𝑃 = (·𝑖OLDβ€˜π‘ˆ)
Assertion
Ref Expression
dipfval (π‘ˆ ∈ NrmCVec β†’ 𝑃 = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)) / 4)))
Distinct variable groups:   π‘₯,π‘˜,𝑦,𝐺   π‘˜,𝑁,π‘₯,𝑦   𝑆,π‘˜,π‘₯,𝑦   π‘ˆ,π‘˜,π‘₯,𝑦   π‘˜,𝑋,π‘₯,𝑦
Allowed substitution hints:   𝑃(π‘₯,𝑦,π‘˜)
Proof of Theorem dipfval
Dummy variable 𝑒 is distinct from all other variables.
StepHypRef Expression
1 dipfval.7 . 2 𝑃 = (·𝑖OLDβ€˜π‘ˆ)
2 fveq2 6888 . . . . 5 (𝑒 = π‘ˆ β†’ (BaseSetβ€˜π‘’) = (BaseSetβ€˜π‘ˆ))
3 dipfval.1 . . . . 5 𝑋 = (BaseSetβ€˜π‘ˆ)
42, 3eqtr4di 2790 . . . 4 (𝑒 = π‘ˆ β†’ (BaseSetβ€˜π‘’) = 𝑋)
5 fveq2 6888 . . . . . . . . . 10 (𝑒 = π‘ˆ β†’ (normCVβ€˜π‘’) = (normCVβ€˜π‘ˆ))
6 dipfval.6 . . . . . . . . . 10 𝑁 = (normCVβ€˜π‘ˆ)
75, 6eqtr4di 2790 . . . . . . . . 9 (𝑒 = π‘ˆ β†’ (normCVβ€˜π‘’) = 𝑁)
8 fveq2 6888 . . . . . . . . . . 11 (𝑒 = π‘ˆ β†’ ( +𝑣 β€˜π‘’) = ( +𝑣 β€˜π‘ˆ))
9 dipfval.2 . . . . . . . . . . 11 𝐺 = ( +𝑣 β€˜π‘ˆ)
108, 9eqtr4di 2790 . . . . . . . . . 10 (𝑒 = π‘ˆ β†’ ( +𝑣 β€˜π‘’) = 𝐺)
11 eqidd 2733 . . . . . . . . . 10 (𝑒 = π‘ˆ β†’ π‘₯ = π‘₯)
12 fveq2 6888 . . . . . . . . . . . 12 (𝑒 = π‘ˆ β†’ ( ·𝑠OLD β€˜π‘’) = ( ·𝑠OLD β€˜π‘ˆ))
13 dipfval.4 . . . . . . . . . . . 12 𝑆 = ( ·𝑠OLD β€˜π‘ˆ)
1412, 13eqtr4di 2790 . . . . . . . . . . 11 (𝑒 = π‘ˆ β†’ ( ·𝑠OLD β€˜π‘’) = 𝑆)
1514oveqd 7422 . . . . . . . . . 10 (𝑒 = π‘ˆ β†’ ((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦) = ((iβ†‘π‘˜)𝑆𝑦))
1610, 11, 15oveq123d 7426 . . . . . . . . 9 (𝑒 = π‘ˆ β†’ (π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)) = (π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))
177, 16fveq12d 6895 . . . . . . . 8 (𝑒 = π‘ˆ β†’ ((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦))) = (π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦))))
1817oveq1d 7420 . . . . . . 7 (𝑒 = π‘ˆ β†’ (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2) = ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2))
1918oveq2d 7421 . . . . . 6 (𝑒 = π‘ˆ β†’ ((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) = ((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)))
2019sumeq2sdv 15646 . . . . 5 (𝑒 = π‘ˆ β†’ Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) = Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)))
2120oveq1d 7420 . . . 4 (𝑒 = π‘ˆ β†’ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) / 4) = (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)) / 4))
224, 4, 21mpoeq123dv 7480 . . 3 (𝑒 = π‘ˆ β†’ (π‘₯ ∈ (BaseSetβ€˜π‘’), 𝑦 ∈ (BaseSetβ€˜π‘’) ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) / 4)) = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)) / 4)))
23 df-dip 29941 . . 3 ·𝑖OLD = (𝑒 ∈ NrmCVec ↦ (π‘₯ ∈ (BaseSetβ€˜π‘’), 𝑦 ∈ (BaseSetβ€˜π‘’) ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) / 4)))
243fvexi 6902 . . . 4 𝑋 ∈ V
2524, 24mpoex 8062 . . 3 (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)) / 4)) ∈ V
2622, 23, 25fvmpt 6995 . 2 (π‘ˆ ∈ NrmCVec β†’ (·𝑖OLDβ€˜π‘ˆ) = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)) / 4)))
271, 26eqtrid 2784 1 (π‘ˆ ∈ NrmCVec β†’ 𝑃 = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· ((π‘β€˜(π‘₯𝐺((iβ†‘π‘˜)𝑆𝑦)))↑2)) / 4)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1541   ∈ wcel 2106  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407  1c1 11107  ici 11108   Β· cmul 11111   / cdiv 11867  2c2 12263  4c4 12265  ...cfz 13480  β†‘cexp 14023  Ξ£csu 15628  NrmCVeccnv 29824   +𝑣 cpv 29825  BaseSetcba 29826   ·𝑠OLD cns 29827  normCVcnmcv 29830  Β·π‘–OLDcdip 29940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-seq 13963  df-sum 15629  df-dip 29941
This theorem is referenced by:  ipval  29943  ipf  29953  dipcn  29960
  Copyright terms: Public domain W3C validator