Definition df-lno 27599

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 = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )

Distinct variable group:   u, t, w, x, y, z

Detailed syntax breakdown of Definition df-lno

Step	Hyp	Ref	Expression
1		clno 27595	. 2 class LnOp
2		vu	. . 3 setvar u
3		vw	. . 3 setvar w
4		cnv 27439	. . 3 class NrmCVec
5		vx	. . . . . . . . . . . 12 setvar x
6	5	cv 1482	. . . . . . . . . . 11 class x
7		vy	. . . . . . . . . . . 12 setvar y
8	7	cv 1482	. . . . . . . . . . 11 class y
9	2	cv 1482	. . . . . . . . . . . 12 class u
10		cns 27442	. . . . . . . . . . . 12 class .sOLD
11	9, 10	cfv 5888	. . . . . . . . . . 11 class ( .sOLD ` u )
12	6, 8, 11	co 6650	. . . . . . . . . 10 class ( x ( .sOLD ` u ) y )
13		vz	. . . . . . . . . . 11 setvar z
14	13	cv 1482	. . . . . . . . . 10 class z
15		cpv 27440	. . . . . . . . . . 11 class +v
16	9, 15	cfv 5888	. . . . . . . . . 10 class ( +v ` u )
17	12, 14, 16	co 6650	. . . . . . . . 9 class ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z )
18		vt	. . . . . . . . . 10 setvar t
19	18	cv 1482	. . . . . . . . 9 class t
20	17, 19	cfv 5888	. . . . . . . 8 class ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) )
21	8, 19	cfv 5888	. . . . . . . . . 10 class ( t ` y )
22	3	cv 1482	. . . . . . . . . . 11 class w
23	22, 10	cfv 5888	. . . . . . . . . 10 class ( .sOLD ` w )
24	6, 21, 23	co 6650	. . . . . . . . 9 class ( x ( .sOLD ` w ) ( t ` y ) )
25	14, 19	cfv 5888	. . . . . . . . 9 class ( t ` z )
26	22, 15	cfv 5888	. . . . . . . . 9 class ( +v ` w )
27	24, 25, 26	co 6650	. . . . . . . 8 class ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
28	20, 27	wceq 1483	. . . . . . 7 wff ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
29		cba 27441	. . . . . . . 8 class BaseSet
30	9, 29	cfv 5888	. . . . . . 7 class ( BaseSet ` u )
31	28, 13, 30	wral 2912	. . . . . 6 wff A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
32	31, 7, 30	wral 2912	. . . . 5 wff A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
33		cc 9934	. . . . 5 class CC
34	32, 5, 33	wral 2912	. . . 4 wff A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
35	22, 29	cfv 5888	. . . . 5 class ( BaseSet ` w )
36		cmap 7857	. . . . 5 class ^m
37	35, 30, 36	co 6650	. . . 4 class ( ( BaseSet ` w ) ^m ( BaseSet ` u ) )
38	34, 18, 37	crab 2916	. . 3 class { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) }
39	2, 3, 4, 4, 38	cmpt2 6652	. 2 class ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )
40	1, 39	wceq 1483	1 wff LnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )

This definition is referenced by:  lnoval  27607