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

Definition df-lno 26983
 Description: Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e. the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-lno LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))})
Distinct variable group:   𝑢,𝑡,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-lno
StepHypRef Expression
1 clno 26979 . 2 class LnOp
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 26823 . . 3 class NrmCVec
5 vx . . . . . . . . . . . 12 setvar 𝑥
65cv 1474 . . . . . . . . . . 11 class 𝑥
7 vy . . . . . . . . . . . 12 setvar 𝑦
87cv 1474 . . . . . . . . . . 11 class 𝑦
92cv 1474 . . . . . . . . . . . 12 class 𝑢
10 cns 26826 . . . . . . . . . . . 12 class ·𝑠OLD
119, 10cfv 5804 . . . . . . . . . . 11 class ( ·𝑠OLD𝑢)
126, 8, 11co 6549 . . . . . . . . . 10 class (𝑥( ·𝑠OLD𝑢)𝑦)
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1474 . . . . . . . . . 10 class 𝑧
15 cpv 26824 . . . . . . . . . . 11 class +𝑣
169, 15cfv 5804 . . . . . . . . . 10 class ( +𝑣𝑢)
1712, 14, 16co 6549 . . . . . . . . 9 class ((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)
18 vt . . . . . . . . . 10 setvar 𝑡
1918cv 1474 . . . . . . . . 9 class 𝑡
2017, 19cfv 5804 . . . . . . . 8 class (𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧))
218, 19cfv 5804 . . . . . . . . . 10 class (𝑡𝑦)
223cv 1474 . . . . . . . . . . 11 class 𝑤
2322, 10cfv 5804 . . . . . . . . . 10 class ( ·𝑠OLD𝑤)
246, 21, 23co 6549 . . . . . . . . 9 class (𝑥( ·𝑠OLD𝑤)(𝑡𝑦))
2514, 19cfv 5804 . . . . . . . . 9 class (𝑡𝑧)
2622, 15cfv 5804 . . . . . . . . 9 class ( +𝑣𝑤)
2724, 25, 26co 6549 . . . . . . . 8 class ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))
2820, 27wceq 1475 . . . . . . 7 wff (𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))
29 cba 26825 . . . . . . . 8 class BaseSet
309, 29cfv 5804 . . . . . . 7 class (BaseSet‘𝑢)
3128, 13, 30wral 2896 . . . . . 6 wff 𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))
3231, 7, 30wral 2896 . . . . 5 wff 𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))
33 cc 9813 . . . . 5 class
3432, 5, 33wral 2896 . . . 4 wff 𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))
3522, 29cfv 5804 . . . . 5 class (BaseSet‘𝑤)
36 cmap 7744 . . . . 5 class 𝑚
3735, 30, 36co 6549 . . . 4 class ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢))
3834, 18, 37crab 2900 . . 3 class {𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))}
392, 3, 4, 4, 38cmpt2 6551 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))})
401, 39wceq 1475 1 wff LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD𝑢)𝑦)( +𝑣𝑢)𝑧)) = ((𝑥( ·𝑠OLD𝑤)(𝑡𝑦))( +𝑣𝑤)(𝑡𝑧))})
 Colors of variables: wff setvar class This definition is referenced by:  lnoval  26991
 Copyright terms: Public domain W3C validator