![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nmoolb | Structured version Visualization version GIF version |
Description: A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nmoolb.1 | ⊢ 𝑋 = (BaseSet‘𝑈) |
nmoolb.2 | ⊢ 𝑌 = (BaseSet‘𝑊) |
nmoolb.l | ⊢ 𝐿 = (normCV‘𝑈) |
nmoolb.m | ⊢ 𝑀 = (normCV‘𝑊) |
nmoolb.3 | ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
Ref | Expression |
---|---|
nmoolb | ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑀‘(𝑇‘𝐴)) ≤ (𝑁‘𝑇)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmoolb.2 | . . . . . 6 ⊢ 𝑌 = (BaseSet‘𝑊) | |
2 | nmoolb.m | . . . . . 6 ⊢ 𝑀 = (normCV‘𝑊) | |
3 | 1, 2 | nmosetre 28224 | . . . . 5 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))} ⊆ ℝ) |
4 | ressxr 10534 | . . . . 5 ⊢ ℝ ⊆ ℝ* | |
5 | 3, 4 | syl6ss 3903 | . . . 4 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))} ⊆ ℝ*) |
6 | 5 | 3adant1 1123 | . . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))} ⊆ ℝ*) |
7 | fveq2 6541 | . . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝐿‘𝑦) = (𝐿‘𝐴)) | |
8 | 7 | breq1d 4974 | . . . . . . 7 ⊢ (𝑦 = 𝐴 → ((𝐿‘𝑦) ≤ 1 ↔ (𝐿‘𝐴) ≤ 1)) |
9 | 2fveq3 6546 | . . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑀‘(𝑇‘𝑦)) = (𝑀‘(𝑇‘𝐴))) | |
10 | 9 | eqeq2d 2804 | . . . . . . 7 ⊢ (𝑦 = 𝐴 → ((𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦)) ↔ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝐴)))) |
11 | 8, 10 | anbi12d 630 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (((𝐿‘𝑦) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦))) ↔ ((𝐿‘𝐴) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝐴))))) |
12 | eqid 2794 | . . . . . . 7 ⊢ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝐴)) | |
13 | 12 | biantru 530 | . . . . . 6 ⊢ ((𝐿‘𝐴) ≤ 1 ↔ ((𝐿‘𝐴) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝐴)))) |
14 | 11, 13 | syl6bbr 290 | . . . . 5 ⊢ (𝑦 = 𝐴 → (((𝐿‘𝑦) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦))) ↔ (𝐿‘𝐴) ≤ 1)) |
15 | 14 | rspcev 3557 | . . . 4 ⊢ ((𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1) → ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦)))) |
16 | fvex 6554 | . . . . 5 ⊢ (𝑀‘(𝑇‘𝐴)) ∈ V | |
17 | eqeq1 2798 | . . . . . . 7 ⊢ (𝑥 = (𝑀‘(𝑇‘𝐴)) → (𝑥 = (𝑀‘(𝑇‘𝑦)) ↔ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦)))) | |
18 | 17 | anbi2d 628 | . . . . . 6 ⊢ (𝑥 = (𝑀‘(𝑇‘𝐴)) → (((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦))) ↔ ((𝐿‘𝑦) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦))))) |
19 | 18 | rexbidv 3259 | . . . . 5 ⊢ (𝑥 = (𝑀‘(𝑇‘𝐴)) → (∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦))))) |
20 | 16, 19 | elab 3604 | . . . 4 ⊢ ((𝑀‘(𝑇‘𝐴)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ (𝑀‘(𝑇‘𝐴)) = (𝑀‘(𝑇‘𝑦)))) |
21 | 15, 20 | sylibr 235 | . . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1) → (𝑀‘(𝑇‘𝐴)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))}) |
22 | supxrub 12567 | . . 3 ⊢ (({𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ (𝑀‘(𝑇‘𝐴)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))}) → (𝑀‘(𝑇‘𝐴)) ≤ sup({𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))}, ℝ*, < )) | |
23 | 6, 21, 22 | syl2an 595 | . 2 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑀‘(𝑇‘𝐴)) ≤ sup({𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))}, ℝ*, < )) |
24 | nmoolb.1 | . . . 4 ⊢ 𝑋 = (BaseSet‘𝑈) | |
25 | nmoolb.l | . . . 4 ⊢ 𝐿 = (normCV‘𝑈) | |
26 | nmoolb.3 | . . . 4 ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) | |
27 | 24, 1, 25, 2, 26 | nmooval 28223 | . . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))}, ℝ*, < )) |
28 | 27 | adantr 481 | . 2 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑁‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑦)))}, ℝ*, < )) |
29 | 23, 28 | breqtrrd 4992 | 1 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑀‘(𝑇‘𝐴)) ≤ (𝑁‘𝑇)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∈ wcel 2080 {cab 2774 ∃wrex 3105 ⊆ wss 3861 class class class wbr 4964 ⟶wf 6224 ‘cfv 6228 (class class class)co 7019 supcsup 8753 ℝcr 10385 1c1 10387 ℝ*cxr 10523 < clt 10524 ≤ cle 10525 NrmCVeccnv 28044 BaseSetcba 28046 normCVcnmcv 28050 normOpOLD cnmoo 28201 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-rep 5084 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-cnex 10442 ax-resscn 10443 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-mulcom 10450 ax-addass 10451 ax-mulass 10452 ax-distr 10453 ax-i2m1 10454 ax-1ne0 10455 ax-1rid 10456 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 ax-pre-lttri 10460 ax-pre-lttrn 10461 ax-pre-ltadd 10462 ax-pre-mulgt0 10463 ax-pre-sup 10464 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-reu 3111 df-rmo 3112 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-po 5365 df-so 5366 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-1st 7548 df-2nd 7549 df-er 8142 df-map 8261 df-en 8361 df-dom 8362 df-sdom 8363 df-sup 8755 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-sub 10721 df-neg 10722 df-vc 28019 df-nv 28052 df-va 28055 df-ba 28056 df-sm 28057 df-0v 28058 df-nmcv 28060 df-nmoo 28205 |
This theorem is referenced by: nmblolbii 28259 |
Copyright terms: Public domain | W3C validator |