MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ipblnfi Structured version   Visualization version   GIF version

Theorem ipblnfi 28634
Description: A function 𝐹 generated by varying the first argument of an inner product (with its second argument a fixed vector 𝐴) is a bounded linear functional, i.e. a bounded linear operator from the vector space to . (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
ipblnfi.1 𝑋 = (BaseSet‘𝑈)
ipblnfi.7 𝑃 = (·𝑖OLD𝑈)
ipblnfi.9 𝑈 ∈ CPreHilOLD
ipblnfi.c 𝐶 = ⟨⟨ + , · ⟩, abs⟩
ipblnfi.l 𝐵 = (𝑈 BLnOp 𝐶)
ipblnfi.f 𝐹 = (𝑥𝑋 ↦ (𝑥𝑃𝐴))
Assertion
Ref Expression
ipblnfi (𝐴𝑋𝐹𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑈   𝑥,𝑋   𝑥,𝑃
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)

Proof of Theorem ipblnfi
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ipblnfi.9 . . . . . . 7 𝑈 ∈ CPreHilOLD
21phnvi 28595 . . . . . 6 𝑈 ∈ NrmCVec
3 ipblnfi.1 . . . . . . 7 𝑋 = (BaseSet‘𝑈)
4 ipblnfi.7 . . . . . . 7 𝑃 = (·𝑖OLD𝑈)
53, 4dipcl 28491 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝑥𝑋𝐴𝑋) → (𝑥𝑃𝐴) ∈ ℂ)
62, 5mp3an1 1445 . . . . 5 ((𝑥𝑋𝐴𝑋) → (𝑥𝑃𝐴) ∈ ℂ)
76ancoms 462 . . . 4 ((𝐴𝑋𝑥𝑋) → (𝑥𝑃𝐴) ∈ ℂ)
8 ipblnfi.f . . . 4 𝐹 = (𝑥𝑋 ↦ (𝑥𝑃𝐴))
97, 8fmptd 6866 . . 3 (𝐴𝑋𝐹:𝑋⟶ℂ)
10 eqid 2824 . . . . . . . . . . 11 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
113, 10nvscl 28405 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ ℂ ∧ 𝑧𝑋) → (𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
122, 11mp3an1 1445 . . . . . . . . 9 ((𝑦 ∈ ℂ ∧ 𝑧𝑋) → (𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
1312ad2ant2lr 747 . . . . . . . 8 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
14 simprr 772 . . . . . . . 8 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → 𝑤𝑋)
15 simpll 766 . . . . . . . 8 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → 𝐴𝑋)
16 eqid 2824 . . . . . . . . . 10 ( +𝑣𝑈) = ( +𝑣𝑈)
173, 16, 4dipdir 28621 . . . . . . . . 9 ((𝑈 ∈ CPreHilOLD ∧ ((𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋𝑤𝑋𝐴𝑋)) → (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴) = (((𝑦( ·𝑠OLD𝑈)𝑧)𝑃𝐴) + (𝑤𝑃𝐴)))
181, 17mpan 689 . . . . . . . 8 (((𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋𝑤𝑋𝐴𝑋) → (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴) = (((𝑦( ·𝑠OLD𝑈)𝑧)𝑃𝐴) + (𝑤𝑃𝐴)))
1913, 14, 15, 18syl3anc 1368 . . . . . . 7 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴) = (((𝑦( ·𝑠OLD𝑈)𝑧)𝑃𝐴) + (𝑤𝑃𝐴)))
20 simplr 768 . . . . . . . . 9 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → 𝑦 ∈ ℂ)
21 simprl 770 . . . . . . . . 9 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → 𝑧𝑋)
223, 16, 10, 4, 1ipassi 28620 . . . . . . . . 9 ((𝑦 ∈ ℂ ∧ 𝑧𝑋𝐴𝑋) → ((𝑦( ·𝑠OLD𝑈)𝑧)𝑃𝐴) = (𝑦 · (𝑧𝑃𝐴)))
2320, 21, 15, 22syl3anc 1368 . . . . . . . 8 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → ((𝑦( ·𝑠OLD𝑈)𝑧)𝑃𝐴) = (𝑦 · (𝑧𝑃𝐴)))
2423oveq1d 7160 . . . . . . 7 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (((𝑦( ·𝑠OLD𝑈)𝑧)𝑃𝐴) + (𝑤𝑃𝐴)) = ((𝑦 · (𝑧𝑃𝐴)) + (𝑤𝑃𝐴)))
2519, 24eqtrd 2859 . . . . . 6 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴) = ((𝑦 · (𝑧𝑃𝐴)) + (𝑤𝑃𝐴)))
2612adantll 713 . . . . . . . . 9 (((𝐴𝑋𝑦 ∈ ℂ) ∧ 𝑧𝑋) → (𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
273, 16nvgcl 28399 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ (𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋𝑤𝑋) → ((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤) ∈ 𝑋)
282, 27mp3an1 1445 . . . . . . . . 9 (((𝑦( ·𝑠OLD𝑈)𝑧) ∈ 𝑋𝑤𝑋) → ((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤) ∈ 𝑋)
2926, 28sylan 583 . . . . . . . 8 ((((𝐴𝑋𝑦 ∈ ℂ) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤) ∈ 𝑋)
3029anasss 470 . . . . . . 7 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → ((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤) ∈ 𝑋)
31 oveq1 7152 . . . . . . . 8 (𝑥 = ((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤) → (𝑥𝑃𝐴) = (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴))
32 ovex 7178 . . . . . . . 8 (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴) ∈ V
3331, 8, 32fvmpt 6756 . . . . . . 7 (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤) ∈ 𝑋 → (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴))
3430, 33syl 17 . . . . . 6 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = (((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)𝑃𝐴))
35 oveq1 7152 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝑃𝐴) = (𝑧𝑃𝐴))
36 ovex 7178 . . . . . . . . . 10 (𝑧𝑃𝐴) ∈ V
3735, 8, 36fvmpt 6756 . . . . . . . . 9 (𝑧𝑋 → (𝐹𝑧) = (𝑧𝑃𝐴))
3837ad2antrl 727 . . . . . . . 8 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) = (𝑧𝑃𝐴))
3938oveq2d 7161 . . . . . . 7 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (𝑦 · (𝐹𝑧)) = (𝑦 · (𝑧𝑃𝐴)))
40 oveq1 7152 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥𝑃𝐴) = (𝑤𝑃𝐴))
41 ovex 7178 . . . . . . . . 9 (𝑤𝑃𝐴) ∈ V
4240, 8, 41fvmpt 6756 . . . . . . . 8 (𝑤𝑋 → (𝐹𝑤) = (𝑤𝑃𝐴))
4342ad2antll 728 . . . . . . 7 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) = (𝑤𝑃𝐴))
4439, 43oveq12d 7163 . . . . . 6 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → ((𝑦 · (𝐹𝑧)) + (𝐹𝑤)) = ((𝑦 · (𝑧𝑃𝐴)) + (𝑤𝑃𝐴)))
4525, 34, 443eqtr4d 2869 . . . . 5 (((𝐴𝑋𝑦 ∈ ℂ) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = ((𝑦 · (𝐹𝑧)) + (𝐹𝑤)))
4645ralrimivva 3186 . . . 4 ((𝐴𝑋𝑦 ∈ ℂ) → ∀𝑧𝑋𝑤𝑋 (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = ((𝑦 · (𝐹𝑧)) + (𝐹𝑤)))
4746ralrimiva 3177 . . 3 (𝐴𝑋 → ∀𝑦 ∈ ℂ ∀𝑧𝑋𝑤𝑋 (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = ((𝑦 · (𝐹𝑧)) + (𝐹𝑤)))
48 ipblnfi.c . . . . 5 𝐶 = ⟨⟨ + , · ⟩, abs⟩
4948cnnv 28456 . . . 4 𝐶 ∈ NrmCVec
5048cnnvba 28458 . . . . 5 ℂ = (BaseSet‘𝐶)
5148cnnvg 28457 . . . . 5 + = ( +𝑣𝐶)
5248cnnvs 28459 . . . . 5 · = ( ·𝑠OLD𝐶)
53 eqid 2824 . . . . 5 (𝑈 LnOp 𝐶) = (𝑈 LnOp 𝐶)
543, 50, 16, 51, 10, 52, 53islno 28532 . . . 4 ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ NrmCVec) → (𝐹 ∈ (𝑈 LnOp 𝐶) ↔ (𝐹:𝑋⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧𝑋𝑤𝑋 (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = ((𝑦 · (𝐹𝑧)) + (𝐹𝑤)))))
552, 49, 54mp2an 691 . . 3 (𝐹 ∈ (𝑈 LnOp 𝐶) ↔ (𝐹:𝑋⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧𝑋𝑤𝑋 (𝐹‘((𝑦( ·𝑠OLD𝑈)𝑧)( +𝑣𝑈)𝑤)) = ((𝑦 · (𝐹𝑧)) + (𝐹𝑤))))
569, 47, 55sylanbrc 586 . 2 (𝐴𝑋𝐹 ∈ (𝑈 LnOp 𝐶))
57 eqid 2824 . . . 4 (normCV𝑈) = (normCV𝑈)
583, 57nvcl 28440 . . 3 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋) → ((normCV𝑈)‘𝐴) ∈ ℝ)
592, 58mpan 689 . 2 (𝐴𝑋 → ((normCV𝑈)‘𝐴) ∈ ℝ)
603, 57, 4, 1sii 28633 . . . . 5 ((𝑧𝑋𝐴𝑋) → (abs‘(𝑧𝑃𝐴)) ≤ (((normCV𝑈)‘𝑧) · ((normCV𝑈)‘𝐴)))
6160ancoms 462 . . . 4 ((𝐴𝑋𝑧𝑋) → (abs‘(𝑧𝑃𝐴)) ≤ (((normCV𝑈)‘𝑧) · ((normCV𝑈)‘𝐴)))
6237adantl 485 . . . . 5 ((𝐴𝑋𝑧𝑋) → (𝐹𝑧) = (𝑧𝑃𝐴))
6362fveq2d 6662 . . . 4 ((𝐴𝑋𝑧𝑋) → (abs‘(𝐹𝑧)) = (abs‘(𝑧𝑃𝐴)))
6459recnd 10661 . . . . 5 (𝐴𝑋 → ((normCV𝑈)‘𝐴) ∈ ℂ)
653, 57nvcl 28440 . . . . . . 7 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → ((normCV𝑈)‘𝑧) ∈ ℝ)
662, 65mpan 689 . . . . . 6 (𝑧𝑋 → ((normCV𝑈)‘𝑧) ∈ ℝ)
6766recnd 10661 . . . . 5 (𝑧𝑋 → ((normCV𝑈)‘𝑧) ∈ ℂ)
68 mulcom 10615 . . . . 5 ((((normCV𝑈)‘𝐴) ∈ ℂ ∧ ((normCV𝑈)‘𝑧) ∈ ℂ) → (((normCV𝑈)‘𝐴) · ((normCV𝑈)‘𝑧)) = (((normCV𝑈)‘𝑧) · ((normCV𝑈)‘𝐴)))
6964, 67, 68syl2an 598 . . . 4 ((𝐴𝑋𝑧𝑋) → (((normCV𝑈)‘𝐴) · ((normCV𝑈)‘𝑧)) = (((normCV𝑈)‘𝑧) · ((normCV𝑈)‘𝐴)))
7061, 63, 693brtr4d 5084 . . 3 ((𝐴𝑋𝑧𝑋) → (abs‘(𝐹𝑧)) ≤ (((normCV𝑈)‘𝐴) · ((normCV𝑈)‘𝑧)))
7170ralrimiva 3177 . 2 (𝐴𝑋 → ∀𝑧𝑋 (abs‘(𝐹𝑧)) ≤ (((normCV𝑈)‘𝐴) · ((normCV𝑈)‘𝑧)))
7248cnnvnm 28460 . . 3 abs = (normCV𝐶)
73 ipblnfi.l . . 3 𝐵 = (𝑈 BLnOp 𝐶)
743, 57, 72, 53, 73, 2, 49blo3i 28581 . 2 ((𝐹 ∈ (𝑈 LnOp 𝐶) ∧ ((normCV𝑈)‘𝐴) ∈ ℝ ∧ ∀𝑧𝑋 (abs‘(𝐹𝑧)) ≤ (((normCV𝑈)‘𝐴) · ((normCV𝑈)‘𝑧))) → 𝐹𝐵)
7556, 59, 71, 74syl3anc 1368 1 (𝐴𝑋𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  wral 3133  cop 4555   class class class wbr 5052  cmpt 5132  wf 6339  cfv 6343  (class class class)co 7145  cc 10527  cr 10528   + caddc 10532   · cmul 10534  cle 10668  abscabs 14589  NrmCVeccnv 28363   +𝑣 cpv 28364  BaseSetcba 28365   ·𝑠OLD cns 28366  normCVcnmcv 28369  ·𝑖OLDcdip 28479   LnOp clno 28519   BLnOp cblo 28521  CPreHilOLDccphlo 28591
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-inf2 9095  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7399  df-om 7571  df-1st 7679  df-2nd 7680  df-supp 7821  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-oadd 8096  df-er 8279  df-map 8398  df-ixp 8452  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fsupp 8825  df-fi 8866  df-sup 8897  df-inf 8898  df-oi 8965  df-card 9359  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11693  df-3 11694  df-4 11695  df-5 11696  df-6 11697  df-7 11698  df-8 11699  df-9 11700  df-n0 11891  df-z 11975  df-dec 12092  df-uz 12237  df-q 12342  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-icc 12738  df-fz 12891  df-fzo 13034  df-seq 13370  df-exp 13431  df-hash 13692  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-sum 15039  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20530  df-xmet 20531  df-met 20532  df-bl 20533  df-mopn 20534  df-cnfld 20539  df-top 21495  df-topon 21512  df-topsp 21534  df-bases 21547  df-cld 21620  df-ntr 21621  df-cls 21622  df-cn 21828  df-cnp 21829  df-t1 21915  df-haus 21916  df-tx 22163  df-hmeo 22356  df-xms 22923  df-ms 22924  df-tms 22925  df-grpo 28272  df-gid 28273  df-ginv 28274  df-gdiv 28275  df-ablo 28324  df-vc 28338  df-nv 28371  df-va 28374  df-ba 28375  df-sm 28376  df-0v 28377  df-vs 28378  df-nmcv 28379  df-ims 28380  df-dip 28480  df-lno 28523  df-nmoo 28524  df-blo 28525  df-0o 28526  df-ph 28592
This theorem is referenced by:  htthlem  28696
  Copyright terms: Public domain W3C validator