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

Definition df-lno 26230
 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
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-lno
StepHypRef Expression
1 clno 26226 . 2
2 vu . . 3
3 vw . . 3
4 cnv 26048 . . 3
5 vx . . . . . . . . . . . 12
65cv 1436 . . . . . . . . . . 11
7 vy . . . . . . . . . . . 12
87cv 1436 . . . . . . . . . . 11
92cv 1436 . . . . . . . . . . . 12
10 cns 26051 . . . . . . . . . . . 12
119, 10cfv 5601 . . . . . . . . . . 11
126, 8, 11co 6305 . . . . . . . . . 10
13 vz . . . . . . . . . . 11
1413cv 1436 . . . . . . . . . 10
15 cpv 26049 . . . . . . . . . . 11
169, 15cfv 5601 . . . . . . . . . 10
1712, 14, 16co 6305 . . . . . . . . 9
18 vt . . . . . . . . . 10
1918cv 1436 . . . . . . . . 9
2017, 19cfv 5601 . . . . . . . 8
218, 19cfv 5601 . . . . . . . . . 10
223cv 1436 . . . . . . . . . . 11
2322, 10cfv 5601 . . . . . . . . . 10
246, 21, 23co 6305 . . . . . . . . 9
2514, 19cfv 5601 . . . . . . . . 9
2622, 15cfv 5601 . . . . . . . . 9
2724, 25, 26co 6305 . . . . . . . 8
2820, 27wceq 1437 . . . . . . 7
29 cba 26050 . . . . . . . 8
309, 29cfv 5601 . . . . . . 7
3128, 13, 30wral 2782 . . . . . 6
3231, 7, 30wral 2782 . . . . 5
33 cc 9536 . . . . 5
3432, 5, 33wral 2782 . . . 4
3522, 29cfv 5601 . . . . 5
36 cmap 7480 . . . . 5
3735, 30, 36co 6305 . . . 4
3834, 18, 37crab 2786 . . 3
392, 3, 4, 4, 38cmpt2 6307 . 2
401, 39wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  lnoval  26238
 Copyright terms: Public domain W3C validator