Definition df-lno 8405

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:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` 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 8401	. 2 class LnOp
2		vu	. . . . . . 7 set u
3	2	cv 955	. . . . . 6 class u
4		cnv 8203	. . . . . 6 class NrmCVec
5	3, 4	wcel 958	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 955	. . . . . 6 class w
8	7, 4	wcel 958	. . . . 5 wff w e. NrmCVec
9	5, 8	wa 223	. . . 4 wff (u e. NrmCVec /\ w e. NrmCVec)
10		vo	. . . . . 6 set o
11	10	cv 955	. . . . 5 class o
12		cba 8205	. . . . . . . . 9 class Base
13	3, 12	cfv 3182	. . . . . . . 8 class (Base` u)
14	7, 12	cfv 3182	. . . . . . . 8 class (Base` w)
15		vt	. . . . . . . . 9 set t
16	15	cv 955	. . . . . . . 8 class t
17	13, 14, 16	wf 3178	. . . . . . 7 wff t:(Base` u)-->(Base` w)
18		vx	. . . . . . . . . . . . . 14 set x
19	18	cv 955	. . . . . . . . . . . . 13 class x
20		vy	. . . . . . . . . . . . . . 15 set y
21	20	cv 955	. . . . . . . . . . . . . 14 class y
22		vz	. . . . . . . . . . . . . . 15 set z
23	22	cv 955	. . . . . . . . . . . . . 14 class z
24		cns 8206	. . . . . . . . . . . . . . 15 class .s
25	3, 24	cfv 3182	. . . . . . . . . . . . . 14 class (.s` u)
26	21, 23, 25	co 3963	. . . . . . . . . . . . 13 class (y(.s` u)z)
27		cpv 8204	. . . . . . . . . . . . . 14 class +v
28	3, 27	cfv 3182	. . . . . . . . . . . . 13 class (+v` u)
29	19, 26, 28	co 3963	. . . . . . . . . . . 12 class (x(+v` u)(y(.s` u)z))
30	29, 16	cfv 3182	. . . . . . . . . . 11 class (t` (x(+v` u)(y(.s` u)z)))
31	19, 16	cfv 3182	. . . . . . . . . . . 12 class (t` x)
32	23, 16	cfv 3182	. . . . . . . . . . . . 13 class (t` z)
33	7, 24	cfv 3182	. . . . . . . . . . . . 13 class (.s` w)
34	21, 32, 33	co 3963	. . . . . . . . . . . 12 class (y(.s` w)(t` z))
35	7, 27	cfv 3182	. . . . . . . . . . . 12 class (+v` w)
36	31, 34, 35	co 3963	. . . . . . . . . . 11 class ((t` x)(+v` w)(y(.s` w)(t` z)))
37	30, 36	wceq 956	. . . . . . . . . 10 wff (t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
38	37, 22, 13	wral 1645	. . . . . . . . 9 wff A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
39		cc 5232	. . . . . . . . 9 class CC
40	38, 20, 39	wral 1645	. . . . . . . 8 wff A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
41	40, 18, 13	wral 1645	. . . . . . 7 wff A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))
42	17, 41	wa 223	. . . . . 6 wff (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))
43	42, 15	cab 1463	. . . . 5 class {t | (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))}
44	11, 43	wceq 956	. . . 4 wff o = {t | (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))}
45	9, 44	wa 223	. . 3 wff ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})
46	45, 2, 6, 10	copab2 3964	. 2 class {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})}
47	1, 46	wceq 956	1 wff LnOp = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})}

This definition is referenced by:  lnoval 8413

Copyright terms: Public domain