Metamath Proof Explorer


Definition df-lno

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.)

Ref Expression
Assertion df-lno LnOp = u NrmCVec , w NrmCVec t BaseSet w BaseSet u | x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z

Detailed syntax breakdown

Step Hyp Ref Expression
0 clno class LnOp
1 vu setvar u
2 cnv class NrmCVec
3 vw setvar w
4 vt setvar t
5 cba class BaseSet
6 3 cv setvar w
7 6 5 cfv class BaseSet w
8 cmap class 𝑚
9 1 cv setvar u
10 9 5 cfv class BaseSet u
11 7 10 8 co class BaseSet w BaseSet u
12 vx setvar x
13 cc class
14 vy setvar y
15 vz setvar z
16 4 cv setvar t
17 12 cv setvar x
18 cns class 𝑠OLD
19 9 18 cfv class 𝑠OLD u
20 14 cv setvar y
21 17 20 19 co class x 𝑠OLD u y
22 cpv class + v
23 9 22 cfv class + v u
24 15 cv setvar z
25 21 24 23 co class x 𝑠OLD u y + v u z
26 25 16 cfv class t x 𝑠OLD u y + v u z
27 6 18 cfv class 𝑠OLD w
28 20 16 cfv class t y
29 17 28 27 co class x 𝑠OLD w t y
30 6 22 cfv class + v w
31 24 16 cfv class t z
32 29 31 30 co class x 𝑠OLD w t y + v w t z
33 26 32 wceq wff t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
34 33 15 10 wral wff z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
35 34 14 10 wral wff y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
36 35 12 13 wral wff x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
37 36 4 11 crab class t BaseSet w BaseSet u | x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
38 1 3 2 2 37 cmpo class u NrmCVec , w NrmCVec t BaseSet w BaseSet u | x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
39 0 38 wceq wff LnOp = u NrmCVec , w NrmCVec t BaseSet w BaseSet u | x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z