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

Definition df-blo 27441
Description: Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-blo BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})
Distinct variable group:   𝑢,𝑡,𝑤

Detailed syntax breakdown of Definition df-blo
StepHypRef Expression
1 cblo 27437 . 2 class BLnOp
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 27279 . . 3 class NrmCVec
5 vt . . . . . . 7 setvar 𝑡
65cv 1479 . . . . . 6 class 𝑡
72cv 1479 . . . . . . 7 class 𝑢
83cv 1479 . . . . . . 7 class 𝑤
9 cnmoo 27436 . . . . . . 7 class normOpOLD
107, 8, 9co 6605 . . . . . 6 class (𝑢 normOpOLD 𝑤)
116, 10cfv 5850 . . . . 5 class ((𝑢 normOpOLD 𝑤)‘𝑡)
12 cpnf 10016 . . . . 5 class +∞
13 clt 10019 . . . . 5 class <
1411, 12, 13wbr 4618 . . . 4 wff ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞
15 clno 27435 . . . . 5 class LnOp
167, 8, 15co 6605 . . . 4 class (𝑢 LnOp 𝑤)
1714, 5, 16crab 2916 . . 3 class {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞}
182, 3, 4, 4, 17cmpt2 6607 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})
191, 18wceq 1480 1 wff BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})
Colors of variables: wff setvar class
This definition is referenced by:  bloval  27476
  Copyright terms: Public domain W3C validator