HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  nmopsetretALT Structured version   Visualization version   GIF version

Theorem nmopsetretALT 29415
Description: The set in the supremum of the operator norm definition df-nmop 29391 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
nmopsetretALT (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦)))} ⊆ ℝ)
Distinct variable group:   𝑥,𝑦,𝑇

Proof of Theorem nmopsetretALT
StepHypRef Expression
1 ffvelrn 6672 . . . . . . . 8 ((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → (𝑇𝑦) ∈ ℋ)
2 normcl 28675 . . . . . . . 8 ((𝑇𝑦) ∈ ℋ → (norm‘(𝑇𝑦)) ∈ ℝ)
31, 2syl 17 . . . . . . 7 ((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → (norm‘(𝑇𝑦)) ∈ ℝ)
4 eleq1 2850 . . . . . . 7 (𝑥 = (norm‘(𝑇𝑦)) → (𝑥 ∈ ℝ ↔ (norm‘(𝑇𝑦)) ∈ ℝ))
53, 4syl5ibr 238 . . . . . 6 (𝑥 = (norm‘(𝑇𝑦)) → ((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → 𝑥 ∈ ℝ))
65impcom 399 . . . . 5 (((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑥 = (norm‘(𝑇𝑦))) → 𝑥 ∈ ℝ)
76adantrl 703 . . . 4 (((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) ∧ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦)))) → 𝑥 ∈ ℝ)
87exp31 412 . . 3 (𝑇: ℋ⟶ ℋ → (𝑦 ∈ ℋ → (((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦))) → 𝑥 ∈ ℝ)))
98rexlimdv 3225 . 2 (𝑇: ℋ⟶ ℋ → (∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦))) → 𝑥 ∈ ℝ))
109abssdv 3934 1 (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦)))} ⊆ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wcel 2048  {cab 2755  wrex 3086  wss 3828   class class class wbr 4927  wf 6182  cfv 6186  cr 10330  1c1 10332  cle 10471  chba 28469  normcno 28473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408  ax-pre-sup 10409  ax-hv0cl 28553  ax-hvmul0 28560  ax-hfi 28629  ax-his1 28632  ax-his3 28634  ax-his4 28635
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-2nd 7499  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-er 8085  df-en 8303  df-dom 8304  df-sdom 8305  df-sup 8697  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-div 11095  df-nn 11436  df-2 11500  df-3 11501  df-n0 11705  df-z 11791  df-uz 12056  df-rp 12202  df-seq 13182  df-exp 13242  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-hnorm 28518
This theorem is referenced by:  nmopub  29460
  Copyright terms: Public domain W3C validator