Definition df-lno 9744

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.

Assertion

Ref	Expression
df-lno	|- LnOp = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})}

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

Detailed syntax breakdown of Definition df-lno

Step	Hyp	Ref	Expression
1		clno 9740	. 2 class LnOp
2		vu	. . . . . . 7 set u
3	2	cv 1297	. . . . . 6 class u
4		cnv 9535	. . . . . 6 class NrmCVec
5	3, 4	wcel 1300	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 1297	. . . . . 6 class w
8	7, 4	wcel 1300	. . . . 5 wff w e. NrmCVec
9	5, 8	wa 240	. . . 4 wff (u e. NrmCVec /\ w e. NrmCVec)
10		vo	. . . . . 6 set o
11	10	cv 1297	. . . . 5 class o
12		cba 9537	. . . . . . . . 9 class BaseSet
13	3, 12	cfv 3998	. . . . . . . 8 class (BaseSet` u)
14	7, 12	cfv 3998	. . . . . . . 8 class (BaseSet` w)
15		vt	. . . . . . . . 9 set t
16	15	cv 1297	. . . . . . . 8 class t
17	13, 14, 16	wf 3994	. . . . . . 7 wff t:(BaseSet` u)-->(BaseSet` w)
18		vx	. . . . . . . . . . . . . 14 set x
19	18	cv 1297	. . . . . . . . . . . . 13 class x
20		vy	. . . . . . . . . . . . . . 15 set y
21	20	cv 1297	. . . . . . . . . . . . . 14 class y
22		vz	. . . . . . . . . . . . . . 15 set z
23	22	cv 1297	. . . . . . . . . . . . . 14 class z
24		cns 9538	. . . . . . . . . . . . . . 15 class .s
25	3, 24	cfv 3998	. . . . . . . . . . . . . 14 class (.s` u)
26	21, 23, 25	co 4884	. . . . . . . . . . . . 13 class (y(.s` u)z)
27		cpv 9536	. . . . . . . . . . . . . 14 class +v
28	3, 27	cfv 3998	. . . . . . . . . . . . 13 class (+v` u)
29	19, 26, 28	co 4884	. . . . . . . . . . . 12 class (x(+v` u)(y(.s` u)z))
30	29, 16	cfv 3998	. . . . . . . . . . 11 class (t` (x(+v` u)(y(.s` u)z)))
31	19, 16	cfv 3998	. . . . . . . . . . . 12 class (t` x)
32	23, 16	cfv 3998	. . . . . . . . . . . . 13 class (t` z)
33	7, 24	cfv 3998	. . . . . . . . . . . . 13 class (.s` w)
34	21, 32, 33	co 4884	. . . . . . . . . . . 12 class (y(.s` w)(t` z))
35	7, 27	cfv 3998	. . . . . . . . . . . 12 class (+v` w)
36	31, 34, 35	co 4884	. . . . . . . . . . 11 class ((t` x)(+v` w)(y(.s` w)(t` z)))
37	30, 36	wceq 1298	. . . . . . . . . 10 wff (t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
38	37, 22, 13	wral 2105	. . . . . . . . 9 wff A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
39		cc 6384	. . . . . . . . 9 class CC
40	38, 20, 39	wral 2105	. . . . . . . 8 wff A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
41	40, 18, 13	wral 2105	. . . . . . 7 wff A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
42	17, 41	wa 240	. . . . . 6 wff (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))
43	42, 15	cab 1871	. . . . 5 class {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))}
44	11, 43	wceq 1298	. . . 4 wff o = {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))}
45	9, 44	wa 240	. . 3 wff ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})
46	45, 2, 6, 10	copab2 4885	. 2 class {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})}
47	1, 46	wceq 1298	1 wff LnOp = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})}

This definition is referenced by:  lnoval 9752

Copyright terms: Public domain