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

Definition df-lno 22245
 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 22241 . 2
2 vu . . 3
3 vw . . 3
4 cnv 22063 . . 3
5 vx . . . . . . . . . . . 12
65cv 1651 . . . . . . . . . . 11
7 vy . . . . . . . . . . . 12
87cv 1651 . . . . . . . . . . 11
92cv 1651 . . . . . . . . . . . 12
10 cns 22066 . . . . . . . . . . . 12
119, 10cfv 5454 . . . . . . . . . . 11
126, 8, 11co 6081 . . . . . . . . . 10
13 vz . . . . . . . . . . 11
1413cv 1651 . . . . . . . . . 10
15 cpv 22064 . . . . . . . . . . 11
169, 15cfv 5454 . . . . . . . . . 10
1712, 14, 16co 6081 . . . . . . . . 9
18 vt . . . . . . . . . 10
1918cv 1651 . . . . . . . . 9
2017, 19cfv 5454 . . . . . . . 8
218, 19cfv 5454 . . . . . . . . . 10
223cv 1651 . . . . . . . . . . 11
2322, 10cfv 5454 . . . . . . . . . 10
246, 21, 23co 6081 . . . . . . . . 9
2514, 19cfv 5454 . . . . . . . . 9
2622, 15cfv 5454 . . . . . . . . 9
2724, 25, 26co 6081 . . . . . . . 8
2820, 27wceq 1652 . . . . . . 7
29 cba 22065 . . . . . . . 8
309, 29cfv 5454 . . . . . . 7
3128, 13, 30wral 2705 . . . . . 6
3231, 7, 30wral 2705 . . . . 5
33 cc 8988 . . . . 5
3432, 5, 33wral 2705 . . . 4
3522, 29cfv 5454 . . . . 5
36 cmap 7018 . . . . 5
3735, 30, 36co 6081 . . . 4
3834, 18, 37crab 2709 . . 3
392, 3, 4, 4, 38cmpt2 6083 . 2
401, 39wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  lnoval  22253
 Copyright terms: Public domain W3C validator