### The Mizar article:

### Banach Space of Bounded Linear Operators

**by****Yasunari Shidama**

- Received December 22, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: LOPBAN_1
- [ MML identifier index ]

environ vocabulary PRE_TOPC, NORMSP_1, RLVECT_1, QC_LANG1, FUNCT_1, ARYTM, ARYTM_1, ARYTM_3, RELAT_1, ABSVALUE, ORDINAL2, BINOP_1, GRCAT_1, UNIALG_1, LATTICES, FUNCOP_1, FUNCSDOM, FUNCT_2, RLSUB_1, SEQ_1, SEQ_2, SEQM_3, BHSP_3, RSSPACE, RSSPACE3, PARTFUN1, LOPBAN_1; notation TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, MCART_1, RELSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, PRE_TOPC, DOMAIN_1, FUNCOP_1, BINOP_1, STRUCT_0, XCMPLX_0, XREAL_0, RAT_1, INT_1, ORDINAL1, ORDINAL2, NUMBERS, MEMBERED, REAL_1, NAT_1, PSCOMP_1, ALG_1, RLVECT_1, VECTSP_1, FRAENKEL, ABSVALUE, RLSUB_1, NORMSP_1, BHSP_1, BHSP_2, BHSP_3, RSSPACE, RSSPACE3, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SERIES_1, FUNCSDOM; constructors MCART_1, FUNCT_3, BINOP_1, ARYTM_0, REAL_1, XREAL_0, NAT_1, SQUARE_1, FUNCT_2, XCMPLX_0, SUBSET_1, MEMBERED, DOMAIN_1, SEQ_1, SEQ_2, SERIES_1, SEQ_4, PSCOMP_1, FUNCOP_1, FUNCSDOM, PREPOWER, RLVECT_1, VECTSP_1, FRAENKEL, PARTFUN1, RLSUB_1, NORMSP_1, BHSP_2, BHSP_3, RSSPACE, RSSPACE3; clusters SUBSET_1, RELSET_1, FINSEQ_1, STRUCT_0, ARYTM_3, RELAT_1, REAL_1, NUMBERS, ORDINAL2, XBOOLE_0, FUNCT_1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCSDOM, RLVECT_1, NORMSP_1, XREAL_0, MEMBERED, VECTSP_1, FRAENKEL, INT_1, SEQ_1, RSSPACE3, BHSP_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions XBOOLE_0, RLVECT_1, STRUCT_0, REAL_1, MEMBERED, XREAL_0, SEQ_4, NORMSP_1, RSSPACE3; theorems XBOOLE_0, REAL_2, AXIOMS, TARSKI, ABSVALUE, REAL_1, RLVECT_1, BINOP_1, FUNCOP_1, FUNCSDOM, XREAL_0, XCMPLX_0, XCMPLX_1, SEQ_1, SEQ_2, SEQM_3, PSCOMP_1, FUNCT_1, NAT_1, FUNCT_2, RLSUB_1, NORMSP_1, SEQ_4, FUNCT_3, ALTCAT_1, RSSPACE, RSSPACE3; schemes BINOP_1, SEQ_1, FUNCT_2, NORMSP_1, XBOOLE_0; begin :: Real Vector Space of Operators definition let X be set; let Y be non empty set; let F be Function of [:REAL, Y:], Y; let a be real number, f be Function of X, Y; redefine func F[;](a,f) -> Element of Funcs(X, Y); coherence proof A0:a in REAL by XREAL_0:def 1; dom f = X by FUNCT_2:def 1; then dom f --> a is Function of X,REAL by A0,FUNCOP_1:57; then A1:<:dom f --> a, f:> is Function of X,[:REAL, Y:] by FUNCT_3:78; F[;](a,f) = F * <:dom f --> a, f:> by FUNCOP_1:def 5; then F[;](a,f) is Function of X, Y by A1,FUNCT_2:19; hence thesis by FUNCT_2:11; end; end; LM00: for X be set for Y be non empty set for f be set holds f is Function of X, Y iff f in Funcs(X,Y) by FUNCT_2:11,121; theorem LM01: for X be non empty set for Y be non empty LoopStr ex ADD be BinOp of Funcs(X,the carrier of Y) st (for f,g being Element of Funcs(X,the carrier of Y) holds ADD.(f,g)=(the add of Y).:(f,g)) proof let X be non empty set; let Y be non empty LoopStr; deffunc F(Element of Funcs(X,the carrier of Y), Element of Funcs(X,the carrier of Y)) = (the add of Y).:($1,$2); consider ADD being BinOp of Funcs(X,the carrier of Y) such that A1: for f,g being Element of Funcs(X,the carrier of Y) holds ADD.(f,g) = F(f,g) from BinOpLambda; take ADD; thus thesis by A1; end; theorem LM02: for X be non empty set, Y be RealLinearSpace ex MULT be Function of [:REAL, Funcs(X,the carrier of Y):], Funcs(X,the carrier of Y) st ( for r be Real, f be Element of Funcs(X,the carrier of Y) holds ( for s be Element of X holds (MULT.[r,f]).s=r*(f.s) ) ) proof let X be non empty set; let Y be RealLinearSpace; deffunc F(Real,Element of Funcs(X,the carrier of Y)) = @((the Mult of Y)[;]($1,$2)); consider F being Function of [:REAL,Funcs(X,the carrier of Y):], Funcs(X,the carrier of Y) such that A1:for a be Real, f being Element of Funcs(X,the carrier of Y) holds F.[a,f] = F(a,f) from Lambda2D; take F; let a be Real,f be Element of Funcs(X,the carrier of Y), x be Element of X; A2:dom (F.[a,f]) = X by ALTCAT_1:6; F.[a,f] = @((the Mult of Y)[;](a,f)) by A1 .= (the Mult of Y) [;](a,f) by FUNCSDOM:def 1; hence (F.[a,f]).x = (the Mult of Y).(a,f.x) by A2,FUNCOP_1:42 .= (the Mult of Y).[a,f.x] by BINOP_1:def 1 .= a*(f.x) by RLVECT_1:def 4; end; definition let X be non empty set; let Y be non empty LoopStr; func FuncAdd(X,Y) -> BinOp of Funcs(X,the carrier of Y) means :Def2: for f,g being Element of Funcs(X,the carrier of Y) holds it.(f,g) = (the add of Y).:(f,g); existence by LM01; uniqueness proof let it1,it2 be BinOp of Funcs(X,the carrier of Y) such that A2: for f,g being Element of Funcs(X,the carrier of Y) holds it1.(f,g) = (the add of Y).:(f,g) and A3: for f,g being Element of Funcs(X,the carrier of Y) holds it2.(f,g) = (the add of Y).:(f,g); now let f,g be Element of Funcs(X,the carrier of Y); thus it1.(f,g) = (the add of Y).:(f,g) by A2 .= it2.(f,g) by A3; end; hence thesis by BINOP_1:2; end; end; definition let X be non empty set; let Y be RealLinearSpace; func FuncExtMult(X,Y) -> Function of [:REAL,Funcs(X,the carrier of Y):], Funcs(X,the carrier of Y) means :Def4: for a being Real, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it.[a,f]).x = a*(f.x); existence by LM02; uniqueness proof let it1,it2 be Function of [:REAL,Funcs(X,the carrier of Y):], Funcs(X,the carrier of Y) such that A2: for a being Real, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it1.[a,f]).x = a*(f.x) and A3: for a being Real, f being Element of Funcs(X,the carrier of Y), x being Element of X holds (it2.[a,f]).x = a*(f.x); now let a be Element of REAL, f be Element of Funcs(X,the carrier of Y); now let x be Element of X; thus (it1.[a,f]).x = a*(f.x) by A2 .= (it2.[a,f]).x by A3; end; hence it1.[a,f] = it2.[a,f] by FUNCT_2:113; end; hence thesis by FUNCT_2:120; end; end; definition let X be set; let Y be non empty ZeroStr; func FuncZero(X,Y) -> Element of Funcs (X,the carrier of Y) equals :Def5: X --> 0.Y; coherence proof X --> 0.Y is Function of X,the carrier of Y by FUNCOP_1:58; hence thesis by FUNCT_2:11; end; end; reserve X,A,B for non empty set; reserve Y for RealLinearSpace; reserve f,g,h for Element of Funcs(X,the carrier of Y); Lm1: for A,B be non empty set for x being Element of A, f being Function of A,B holds x in dom f proof let A,B be non empty set; let x be Element of A, f be Function of A,B; x in A; hence x in dom f by FUNCT_2:def 1; end; theorem Th10:for Y being non empty LoopStr, f,g,h being Element of Funcs(X,the carrier of Y) holds h = (FuncAdd(X,Y)).(f,g) iff for x being Element of X holds h.x = f.x + g.x proof let Y be non empty LoopStr, f,g,h be Element of Funcs(X,the carrier of Y); A1: now assume A2: h = (FuncAdd(X,Y)).(f,g); let x be Element of X; A3: x in dom ((the add of Y).:(f,g)) by Lm1; thus h.x = ((the add of Y).:(f,g)).x by A2,Def2 .= (the add of Y).(f.x,g.x) by A3,FUNCOP_1:28 .= (the add of Y).[f.x,g.x] by BINOP_1:def 1 .= f.x + g.x by RLVECT_1:def 3; end; now assume A4: for x being Element of X holds h.x=f.x + g.x; now let x be Element of X; A5: x in dom ((the add of Y).:(f,g)) by Lm1; thus ((FuncAdd(X,Y)).(f,g)).x = ((the add of Y).:(f,g)).x by Def2 .= (the add of Y).(f.x,g.x) by A5,FUNCOP_1:28 .= (the add of Y).[f.x,g.x] by BINOP_1:def 1 .= f.x + g.x by RLVECT_1:def 3 .= h.x by A4; end; hence h = (FuncAdd(X,Y)).(f,g) by FUNCT_2:113; end; hence thesis by A1; end; theorem Th13: for x being Element of X holds (FuncZero(X,Y)).x = 0.Y proof let x be Element of X; thus (FuncZero(X,Y)).x = (X --> 0.Y).x by Def5 .= 0.Y by FUNCOP_1:13; end; reserve a,b for Real; theorem Th15: h = (FuncExtMult(X,Y)).[a,f] iff for x being Element of X holds h.x = a*(f.x) proof thus h = (FuncExtMult(X,Y)).[a,f] implies (for x being Element of X holds h.x = a*(f.x)) by Def4; now assume A1: for x being Element of X holds h.x = a*(f.x); for x being Element of X holds h.x = ((FuncExtMult(X,Y)).[a,f]).x proof let x be Element of X; thus h.x = a*(f.x) by A1 .= ((FuncExtMult(X,Y)).[a,f]).x by Def4; end; hence h = (FuncExtMult(X,Y)).[a,f] by FUNCT_2:113; end; hence thesis; end; reserve u,v,w for VECTOR of RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#); theorem Th16: (FuncAdd(X,Y)).(f,g) = (FuncAdd(X,Y)).(g,f) proof now let x be Element of X; thus ((FuncAdd(X,Y)).(f,g)).x = g.x + f.x by Th10 .= ((FuncAdd(X,Y)).(g,f)).x by Th10; end; hence thesis by FUNCT_2:113; end; theorem Th17: (FuncAdd(X,Y)).(f,(FuncAdd(X,Y)).(g,h)) = (FuncAdd(X,Y)).((FuncAdd(X,Y)).(f,g),h) proof now let x be Element of X; thus ((FuncAdd(X,Y)).(f,(FuncAdd(X,Y)).(g,h))).x = f.x + ((FuncAdd(X,Y)).(g,h)).x by Th10 .= f.x + (g.x + h.x) by Th10 .= (f.x + g.x) + h.x by RLVECT_1:def 6 .= ((FuncAdd(X,Y)).(f,g)).x + h.x by Th10 .= ((FuncAdd(X,Y)).((FuncAdd(X,Y)).(f,g),h)).x by Th10; end; hence thesis by FUNCT_2:113; end; theorem Th21: (FuncAdd(X,Y)).(FuncZero(X,Y),f) = f proof now let x be Element of X; thus ((FuncAdd(X,Y)).(FuncZero(X,Y),f)).x = (FuncZero(X,Y)).x + f.x by Th10 .= 0.Y + f.x by Th13 .= f.x by RLVECT_1:def 7; end; hence thesis by FUNCT_2:113; end; theorem Th22: (FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[-1,f]) = FuncZero(X,Y) proof now let x be Element of X; set y=f.x; thus ((FuncAdd(X,Y)).(f,(FuncExtMult(X,Y)).[-1,f])).x = f.x + ((FuncExtMult(X,Y)).[-1,f]).x by Th10 .= f.x + ((-1)*y) by Th15 .= f.x + (-y) by RLVECT_1:29 .= 0.Y by RLVECT_1:16 .= (FuncZero(X,Y)).x by Th13; end; hence thesis by FUNCT_2:113; end; theorem Th23: (FuncExtMult(X,Y)).[1,f] = f proof now let x be Element of X; thus ((FuncExtMult(X,Y)).[1 qua Real,f]).x = 1*(f.x) by Th15 .= f.x by RLVECT_1:def 9; end; hence thesis by FUNCT_2:113; end; theorem Th24: (FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,f]] = (FuncExtMult(X,Y)).[a*b,f] proof now let x be Element of X; thus ((FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,f]]).x = a*(((FuncExtMult(X,Y)).[b,f]).x) by Th15 .= a*(b*(f.x)) by Th15 .= (a*b)*(f.x) by RLVECT_1:def 9 .= ((FuncExtMult(X,Y)).[a*b,f]).x by Th15; end; hence thesis by FUNCT_2:113; end; theorem Th25: (FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b,f]) = (FuncExtMult(X,Y)).[a+b,f] proof now let x be Element of X; thus ((FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[b,f])).x = ((FuncExtMult(X,Y)).[a,f]).x + ((FuncExtMult(X,Y)).[b,f]).x by Th10 .= a*(f.x) + ((FuncExtMult(X,Y)).[b,f]).x by Th15 .= a*(f.x) + b*(f.x) by Th15 .= (a+b)*(f.x) by RLVECT_1:def 9 .= ((FuncExtMult(X,Y)).[a+b,f]).x by Th15; end; hence thesis by FUNCT_2:113; end; Lm2: (FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[a,g]) = (FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(f,g)] proof now let x be Element of X; thus ((FuncAdd(X,Y)). ((FuncExtMult(X,Y)).[a,f],(FuncExtMult(X,Y)).[a,g])).x = ((FuncExtMult(X,Y)).[a,f]).x + ((FuncExtMult(X,Y)).[a,g]).x by Th10 .= a*(f.x) + ((FuncExtMult(X,Y)).[a,g]).x by Th15 .= a*(f.x) + a*(g.x) by Th15 .= a*(f.x + g.x) by RLVECT_1:def 9 .= a*(((FuncAdd(X,Y)).(f,g)).x) by Th10 .= ((FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(f,g)]).x by Th15; end; hence thesis by FUNCT_2:113; end; theorem Th34: RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#) is RealLinearSpace proof set IT = RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#); IT is Abelian add-associative right_zeroed right_complementable RealLinearSpace-like proof thus u+v = v+u proof reconsider v' = v, u' = u as Element of Funcs(X,the carrier of Y); thus u+v = (FuncAdd(X,Y)).[u',v'] by RLVECT_1:def 3 .= (FuncAdd(X,Y)).(u',v') by BINOP_1:def 1 .= (FuncAdd(X,Y)).(v',u') by Th16 .= (FuncAdd(X,Y)).[v',u'] by BINOP_1:def 1 .= v+u by RLVECT_1:def 3; end; thus (u+v)+w = u+(v+w) proof reconsider v'=v, u'=u, w'=w as Element of Funcs(X,the carrier of Y); thus (u+v)+w = (FuncAdd(X,Y)).[u+v,w'] by RLVECT_1:def 3 .= (FuncAdd(X,Y)).(u+v,w') by BINOP_1:def 1 .= (FuncAdd(X,Y)).((FuncAdd(X,Y)).[u',v'],w') by RLVECT_1:def 3 .= (FuncAdd(X,Y)).((FuncAdd(X,Y)).(u',v'),w') by BINOP_1:def 1 .= (FuncAdd(X,Y)).(u',(FuncAdd(X,Y)).(v',w')) by Th17 .= (FuncAdd(X,Y)).(u',(FuncAdd(X,Y)).[v',w']) by BINOP_1:def 1 .= (FuncAdd(X,Y)).[u',(FuncAdd(X,Y)).[v',w']] by BINOP_1:def 1 .= (FuncAdd(X,Y)).[u',v+w] by RLVECT_1:def 3 .= u+(v+w) by RLVECT_1:def 3; end; thus u+0.IT = u proof reconsider u'=u as Element of Funcs(X,the carrier of Y); thus u+0.IT = (FuncAdd(X,Y)).[u',0.IT] by RLVECT_1:def 3 .= (FuncAdd(X,Y)).[u',FuncZero(X,Y)] by RLVECT_1:def 2 .= (FuncAdd(X,Y)).(u',FuncZero(X,Y)) by BINOP_1:def 1 .= (FuncAdd(X,Y)).(FuncZero(X,Y),u') by Th16 .= u by Th21; end; thus ex w st u+w = 0.IT proof reconsider u' = u as Element of Funcs(X,the carrier of Y); reconsider w = (FuncExtMult(X,Y)).[-1,u'] as VECTOR of IT; take w; thus u+w = (FuncAdd(X,Y)).[u',(FuncExtMult(X,Y)).[-1,u']] by RLVECT_1:def 3 .= (FuncAdd(X,Y)).(u',(FuncExtMult(X,Y)).[-1,u']) by BINOP_1:def 1 .= FuncZero(X,Y) by Th22 .= 0.IT by RLVECT_1:def 2; end; thus a*(u+v) = a*u + a *v proof reconsider v' = v, u' = u as Element of Funcs(X,the carrier of Y); reconsider w = (FuncExtMult(X,Y)).[a,u'],w' = (FuncExtMult(X,Y)).[a,v'] as VECTOR of IT; thus a*(u+v) = (FuncExtMult(X,Y)).[a,u+v] by RLVECT_1:def 4 .=(FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).[u',v']] by RLVECT_1:def 3 .= (FuncExtMult(X,Y)).[a,(FuncAdd(X,Y)).(u',v')] by BINOP_1:def 1 .=(FuncAdd(X,Y)).(w,w') by Lm2 .= (FuncAdd(X,Y)).[w,w'] by BINOP_1:def 1 .= w + w' by RLVECT_1:def 3 .= w + (a*v) by RLVECT_1:def 4 .= (a*u) + (a*v) by RLVECT_1:def 4; end; thus (a+b)*v = a*v + b*v proof reconsider v' = v as Element of Funcs(X,the carrier of Y); reconsider w = (FuncExtMult(X,Y)).[a,v'],w' = (FuncExtMult(X,Y)).[b,v'] as VECTOR of IT; thus (a+b)*v = (FuncExtMult(X,Y)).[a+b,v'] by RLVECT_1:def 4 .= (FuncAdd(X,Y)).(w,w') by Th25 .= (FuncAdd(X,Y)).[w,w'] by BINOP_1:def 1 .= w + w' by RLVECT_1:def 3 .= w + (b*v) by RLVECT_1:def 4 .= (a*v) + (b*v) by RLVECT_1:def 4; end; thus (a*b)*v = a*(b*v) proof reconsider v'=v as Element of Funcs(X,the carrier of Y); thus (a*b)*v = (FuncExtMult(X,Y)).[a*b,v'] by RLVECT_1:def 4 .= (FuncExtMult(X,Y)).[a,(FuncExtMult(X,Y)).[b,v']] by Th24 .= (FuncExtMult(X,Y)).[a,b*v] by RLVECT_1:def 4 .= a*(b*v) by RLVECT_1:def 4; end; thus 1*v = v proof reconsider v'=v as Element of Funcs(X,the carrier of Y); thus 1*v = (FuncExtMult(X,Y)).[1,v'] by RLVECT_1:def 4 .= v by Th23; end; end; hence thesis; end; definition let X be non empty set; let Y be RealLinearSpace; func RealVectSpace(X,Y) -> RealLinearSpace equals :Def7: RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#); coherence by Th34; end; definition let X be non empty set; let Y be RealLinearSpace; cluster RealVectSpace(X,Y) -> strict; coherence proof RealVectSpace(X,Y) = RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#) by Def7; hence thesis; end; end; theorem LM04: for X be non empty set for Y be RealLinearSpace for f,g,h be VECTOR of RealVectSpace(X,Y) for f',g',h' be Element of Funcs(X, the carrier of Y) st f'=f & g'=g & h'=h holds h = f+g iff for x be Element of X holds h'.x = f'.x + g'.x proof let X be non empty set; let Y be RealLinearSpace; let f,g,h be VECTOR of RealVectSpace(X,Y); let f',g',h' be Element of Funcs(X, the carrier of Y) such that AS1: f'=f and AS2: g'=g and AS3: h'=h; A0: RealVectSpace(X, Y) = RLSStruct(#Funcs(X,the carrier of Y), FuncZero(X,Y), FuncAdd(X,Y), FuncExtMult(X,Y)#) by Def7; P1: now assume R1: h = f+g; let x be Element of X; U1: h= (FuncAdd(X,Y)).[f',g'] by AS1,AS2,A0,R1,RLVECT_1:def 3 .= (FuncAdd(X,Y)).(f',g') by BINOP_1:def 1; thus h'.x = f'.x+g'.x by Th10,U1,AS3; end; now assume R2: for x be Element of X holds h'.x=f'.x+g'.x; f+g = (FuncAdd(X,Y)).[f',g'] by AS1,AS2,A0,RLVECT_1:def 3 .= (FuncAdd(X,Y)).(f',g') by BINOP_1:def 1; hence h = f+g by AS3,Th10,R2; end; hence thesis by P1; end; theorem LM05: for X be non empty set for Y be RealLinearSpace for f,h be VECTOR of RealVectSpace(X,Y) for f',h' be Element of Funcs(X, the carrier of Y) st f'=f & h'=h for a be Real holds h = a*f iff for x be Element of X holds h'.x = a*f'.x proof let X be non empty set; let Y be RealLinearSpace; let f,h be VECTOR of RealVectSpace(X,Y); let f',h' be Element of Funcs(X, the carrier of Y) such that AS1: f'=f and AS2: h'=h; let a be Real; A0: RealVectSpace(X , Y) = RLSStruct(#Funcs(X,the carrier of Y), FuncZero(X,Y), FuncAdd(X,Y), FuncExtMult(X,Y)#) by Def7; P1: now assume R1: h = a*f; let x be Element of X; U1: h= (FuncExtMult(X, Y)).[a,f'] by R1,A0,AS1,RLVECT_1:def 4; thus h'.x = a*f'.x by Th15,U1,AS2; end; now assume R2: for x be Element of X holds h'.x=a*f'.x; h'=(FuncExtMult(X, Y)).[a,f'] by Th15,R2; hence h =a*f by AS2,A0,AS1,RLVECT_1:def 4; end; hence thesis by P1; end; theorem LM06: for X be non empty set for Y be RealLinearSpace holds 0.RealVectSpace(X,Y) = (X --> 0.Y) proof let X be non empty set; let Y be RealLinearSpace; set z=(X -->0.Y); P0: RealVectSpace(X,Y) = RLSStruct(#Funcs(X,the carrier of Y), FuncZero(X,Y),FuncAdd(X,Y),FuncExtMult(X,Y)#) by Def7; 0.RealVectSpace(X,Y) = FuncZero(X,Y) by RLVECT_1:def 2,P0; hence thesis by Def5; end; begin :: Real Vector Space of Linear Operators definition let X be non empty RLSStruct; let Y be non empty LoopStr; let IT be Function of X, Y; attr IT is additive means :Def10: for x,y being VECTOR of X holds IT.(x+y) = IT.x+IT.y; end; definition let X, Y be non empty RLSStruct; let IT be Function of X,Y; attr IT is homogeneous means :Def11: for x being VECTOR of X, r being Real holds IT.(r*x) = r*IT.x; end; definition let X be non empty RLSStruct; let Y be RealLinearSpace; cluster additive homogeneous Function of X,Y; existence proof set f = (the carrier of X) --> 0.Y; reconsider f as Function of X,Y by FUNCOP_1:58; take f; hereby let x,y be VECTOR of X; thus f.(x+y) = 0.Y by FUNCOP_1:13 .= 0.Y+0.Y by RLVECT_1:10 .= f.x+0.Y by FUNCOP_1:13 .= f.x+f.y by FUNCOP_1:13; end; hereby let x be VECTOR of X, r be Real; thus f.(r*x) =0.Y by FUNCOP_1:13 .=r*0.Y by RLVECT_1:23 .= r*f.x by FUNCOP_1:13; end; end; end; definition let X, Y be RealLinearSpace; mode LinearOperator of X,Y is additive homogeneous Function of X,Y; end; definition let X, Y be RealLinearSpace; func LinearOperators(X,Y) -> Subset of RealVectSpace(the carrier of X, Y) means :Def12: for x being set holds x in it iff x is LinearOperator of X,Y; existence proof defpred P[set] means $1 is LinearOperator of X,Y; consider IT being set such that A1:for x being set holds x in IT iff x in Funcs(the carrier of X,the carrier of Y) & P[x] from Separation; B1: IT is Subset of Funcs(the carrier of X,the carrier of Y) proof for x be set st x in IT holds x in Funcs(the carrier of X,the carrier of Y) by A1; hence thesis by TARSKI:def 3; end; B2: the carrier of RealVectSpace(the carrier of X , Y) = Funcs(the carrier of X, the carrier of Y) proof RealVectSpace(the carrier of X , Y) = RLSStruct(#Funcs(the carrier of X,the carrier of Y), FuncZero(the carrier of X,Y), FuncAdd(the carrier of X,Y), FuncExtMult(the carrier of X,Y)#) by Def7; hence thesis; end; take IT; thus IT is Subset of RealVectSpace(the carrier of X, Y) by B1,B2; let x be set; thus x in IT implies x is LinearOperator of X,Y by A1; assume aa: x is LinearOperator of X,Y; then x in Funcs(the carrier of X,the carrier of Y) by FUNCT_2:11; hence thesis by A1,aa; end; uniqueness proof let X1,X2 be Subset of RealVectSpace(the carrier of X, Y); assume that A2: for x being set holds x in X1 iff x is LinearOperator of X,Y and A3: for x being set holds x in X2 iff x is LinearOperator of X,Y; for x being set st x in X1 holds x in X2 proof let x be set; assume x in X1; then x is LinearOperator of X,Y by A2; hence thesis by A3; end; then A4: X1 c= X2 by TARSKI:def 3; for x being set st x in X2 holds x in X1 proof let x be set; assume x in X2; then x is LinearOperator of X,Y by A3; hence thesis by A2; end; then X2 c= X1 by TARSKI:def 3; hence thesis by A4,XBOOLE_0:def 10; end; end; definition let X, Y be RealLinearSpace; cluster LinearOperators(X,Y) -> non empty; coherence proof set f = (the carrier of X) --> 0.Y; reconsider f as Function of X,Y by FUNCOP_1:58; AS3: f is additive proof let x,y be VECTOR of X; thus f.(x+y) = 0.Y by FUNCOP_1:13 .=0.Y+0.Y by RLVECT_1:10 .= f.x+0.Y by FUNCOP_1:13 .= f.x+f.y by FUNCOP_1:13; end; f is homogeneous proof let x be VECTOR of X, r be Real; thus f.(r*x) =0.Y by FUNCOP_1:13 .=r*0.Y by RLVECT_1:23 .= r*f.x by FUNCOP_1:13; end; hence thesis by Def12,AS3; end; end; theorem Th41: for X, Y be RealLinearSpace holds LinearOperators(X,Y) is lineary-closed proof let X, Y be RealLinearSpace; set W = LinearOperators(X,Y); A0: RealVectSpace(the carrier of X, Y) = RLSStruct(#Funcs(the carrier of X,the carrier of Y), FuncZero(the carrier of X,Y), FuncAdd(the carrier of X,Y), FuncExtMult(the carrier of X,Y)#) by Def7; A1:for v,u be VECTOR of RealVectSpace(the carrier of X, Y) st v in LinearOperators(X,Y) & u in LinearOperators(X,Y) holds v + u in LinearOperators(X,Y) proof let v,u be VECTOR of RealVectSpace(the carrier of X ,Y) such that A2: v in W & u in W; v+u is LinearOperator of X,Y proof reconsider f=v+u as Function of X,Y by A0,LM00; f is LinearOperator of X,Y proof Y1: f is additive proof let x,y be VECTOR of X; reconsider v' = v, u' = u as Element of Funcs(the carrier of X,the carrier of Y) by A0; U1: f= (FuncAdd(the carrier of X,Y)).[u',v'] by A0,RLVECT_1:def 3 .= (FuncAdd(the carrier of X,Y)).(u',v') by BINOP_1:def 1; U2: u' is LinearOperator of X,Y by Def12,A2; U3: v' is LinearOperator of X,Y by Def12,A2; thus f.(x+y) =u'.(x+y)+v'.(x+y) by Th10,U1 .=(u'.x+u'.y)+v'.(x+y) by Def10,U2 .=u'.x+u'.y+(v'.x+v'.y) by U3,Def10 .=u'.x+u'.y+v'.x+v'.y by RLVECT_1:def 6 .=u'.x+v'.x+u'.y+v'.y by RLVECT_1:def 6 .= f.x+ u'.y+v'.y by Th10,U1 .= f.x+ (u'.y+v'.y) by RLVECT_1:def 6 .= f.x+f.y by Th10,U1; end; f is homogeneous proof let x be VECTOR of X, s be Real; reconsider v' = v, u' = u as Element of Funcs(the carrier of X,the carrier of Y) by A0; U1: f= (FuncAdd(the carrier of X,Y)).[u',v'] by A0,RLVECT_1:def 3 .= (FuncAdd(the carrier of X,Y)).(u',v') by BINOP_1:def 1; U2: u' is LinearOperator of X,Y by Def12,A2; U3: v' is LinearOperator of X,Y by Def12,A2; thus f.(s*x) =u'.(s*x)+v'.(s*x) by Th10,U1 .=(s*(u'.x))+v'.(s*x) by Def11,U2 .=s*u'.x+s*v'.x by U3,Def11 .=s*(u'.x+v'.x) by RLVECT_1:def 9 .= s*f.x by Th10,U1; end; hence thesis by Y1; end; hence thesis; end; hence v+u in W by Def12; end; for a be Real for v be VECTOR of RealVectSpace(the carrier of X,Y) st v in W holds a * v in W proof let a be Real; let v be VECTOR of RealVectSpace(the carrier of X,Y) such that A12: v in W; a*v is LinearOperator of X,Y proof reconsider f=a*v as Function of X,Y by A0,LM00; f is LinearOperator of X,Y proof Y1: f is additive proof let x,y be VECTOR of X; reconsider v' = v as Element of Funcs(the carrier of X,the carrier of Y) by A0; U1: f= (FuncExtMult(the carrier of X,Y)).[a,v'] by A0,RLVECT_1:def 4; U3: v' is LinearOperator of X,Y by Def12,A12; thus f.(x+y) = a*(v'.(x+y)) by Th15,U1 .=a*(v'.x+v'.y) by U3,Def10 .=a*v'.x+a*v'.y by RLVECT_1:def 9 .=f.x+a*v'.y by Th15,U1 .=f.x+ f.y by Th15,U1; end; f is homogeneous proof let x be VECTOR of X, s be Real; reconsider v' = v as Element of Funcs(the carrier of X,the carrier of Y) by A0; U1: f= (FuncExtMult(the carrier of X,Y)).[a,v'] by A0,RLVECT_1:def 4; U3: v' is LinearOperator of X,Y by Def12,A12; thus f.(s*x) =a*v'.(s*x) by Th15,U1 .=a*(s*(v'.x)) by Def11,U3 .=a*s*v'.x by RLVECT_1:def 9 .=s*(a*v'.x) by RLVECT_1:def 9 .=s*f.x by Th15,U1; end; hence thesis by Y1; end; hence thesis; end; hence thesis by Def12; end; hence thesis by A1,RLSUB_1:def 1; end; theorem Th42: for X, Y be RealLinearSpace holds RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) is Subspace of RealVectSpace(the carrier of X,Y) proof let X, Y be RealLinearSpace; LinearOperators(X,Y) is lineary-closed by Th41; hence thesis by RSSPACE:13; end; definition let X, Y be RealLinearSpace; cluster RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like; coherence by Th42; end; theorem for X, Y be RealLinearSpace holds RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) is RealLinearSpace by Th42; definition let X, Y be RealLinearSpace; func R_VectorSpace_of_LinearOperators(X,Y) -> RealLinearSpace equals:Def15: RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #); coherence; end; definition let X, Y be RealLinearSpace; cluster R_VectorSpace_of_LinearOperators(X,Y) -> strict; coherence proof R_VectorSpace_of_LinearOperators(X,Y) = RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) by Def15; hence thesis; end; end; theorem LM14: for X, Y be RealLinearSpace for f,g,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) for f',g',h' be LinearOperator of X,Y st f'=f & g'=g & h'=h holds (h = f+g iff (for x be VECTOR of X holds h'.x = f'.x + g'.x) ) proof let X, Y be RealLinearSpace; let f,g,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y); let f',g',h' be LinearOperator of X,Y such that AS1: f'=f and AS2: g'=g and AS3: h'=h; R_VectorSpace_of_LinearOperators(X,Y) = RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) by Def15; then A0:R_VectorSpace_of_LinearOperators(X,Y) is Subspace of RealVectSpace(the carrier of X,Y) by Th42; then reconsider f1=f as VECTOR of RealVectSpace(the carrier of X,Y) by RLSUB_1:18; reconsider g1=g as VECTOR of RealVectSpace(the carrier of X,Y) by A0,RLSUB_1:18; reconsider h1=h as VECTOR of RealVectSpace(the carrier of X,Y) by A0,RLSUB_1:18; reconsider f1'=f' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; reconsider g1'=g' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; reconsider h1'=h' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; BS1: f1' = f1 by AS1; BS2: g1' = g1 by AS2; BS3: h1' = h1 by AS3; P1: now assume R1: h = f+g; let x be Element of X; h1=f1+g1 by R1,A0,RLSUB_1:21; hence h'.x=f'.x+g'.x by BS1,BS2,BS3,LM04; end; now assume R2: for x be Element of X holds h'.x=f'.x+g'.x; R3: for x be Element of X holds h1'.x = f1'.x+g1'.x by R2; h1=f1+g1 by BS1,BS2,BS3,LM04,R3; hence h =f+g by A0,RLSUB_1:21; end; hence thesis by P1; end; theorem LM15: for X, Y be RealLinearSpace for f,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) for f',h' be LinearOperator of X,Y st f'=f & h'=h for a be Real holds h = a*f iff for x be VECTOR of X holds h'.x = a*f'.x proof let X, Y be RealLinearSpace; let f,h be VECTOR of R_VectorSpace_of_LinearOperators(X,Y); let f',h' be LinearOperator of X,Y such that AS1: f'=f and AS2: h'=h; let a be Real; R_VectorSpace_of_LinearOperators(X,Y) = RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) by Def15; then A0:R_VectorSpace_of_LinearOperators(X,Y) is Subspace of RealVectSpace(the carrier of X,Y) by Th42; then reconsider f1=f as VECTOR of RealVectSpace(the carrier of X,Y) by RLSUB_1:18; reconsider h1=h as VECTOR of RealVectSpace(the carrier of X,Y) by A0,RLSUB_1:18; reconsider f1'=f' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; reconsider h1'=h' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; BS1: f1' = f1 by AS1; BS2: h1' = h1 by AS2; P1: now assume R1: h = a*f; let x be Element of X; h1=a*f1 by R1,A0,RLSUB_1:22; hence h'.x=a*f'.x by BS1,BS2,LM05; end; now assume R2: for x be Element of X holds h'.x=a*f'.x; R3: for x be Element of X holds h1'.x = a*f1'.x by R2; h1=a*f1 by BS1,BS2,LM05,R3; hence h =a*f by A0,RLSUB_1:22; end; hence thesis by P1; end; theorem LM16: for X, Y be RealLinearSpace holds 0.R_VectorSpace_of_LinearOperators(X,Y) =((the carrier of X) -->0.Y) proof let X, Y be RealLinearSpace; R_VectorSpace_of_LinearOperators(X,Y) = RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) by Def15; then A0:R_VectorSpace_of_LinearOperators(X,Y) is Subspace of RealVectSpace(the carrier of X,Y) by Th42; 0.RealVectSpace(the carrier of X,Y) =((the carrier of X) -->0.Y) by LM06; hence thesis by A0,RLSUB_1:19; end; theorem LM20: for X,Y be RealLinearSpace holds (the carrier of X) --> 0.Y is LinearOperator of X,Y proof let X,Y be RealLinearSpace; set f=(the carrier of X) --> 0.Y; reconsider f as Function of X,Y by FUNCOP_1:58; Y1: f is additive proof let x,y be VECTOR of X; thus f.(x+y) = 0.Y by FUNCOP_1:13 .=0.Y+0.Y by RLVECT_1:10 .= f.x+0.Y by FUNCOP_1:13 .= f.x+f.y by FUNCOP_1:13; end; f is homogeneous proof let x be VECTOR of X, r be Real; thus f.(r*x) =0.Y by FUNCOP_1:13 .=r*0.Y by RLVECT_1:23 .= r*f.x by FUNCOP_1:13; end; hence thesis by Y1; end; begin :: Real Normed Linear Space of Bounded Linear Operators theorem NMLM01: for X be RealNormSpace for seq be sequence of X for g be Point of X holds ( seq is convergent & lim seq = g implies ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) proof let X be RealNormSpace; let seq be sequence of X; let g be Point of X; assume that A1: seq is convergent and A2: lim seq = g; A3: ||.seq.|| is convergent by A1,NORMSP_1:39; now let r be real number; A4: r is Real by XREAL_0:def 1; assume r > 0; then consider m1 be Nat such that A5: for n be Nat st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,NORMSP_1:def 11; take k = m1; now let n be Nat; assume n >= k; then A6: ||.(seq.n) - g.|| < r by A5; abs(||.(seq.n).|| - ||.g.||) <= ||.(seq.n) - g.|| by NORMSP_1:13; then abs(||.(seq.n).|| - ||.g.||) < r by A6,AXIOMS:22; hence abs(||.seq.||.n - ||.g.||) < r by NORMSP_1:def 10; end; hence for n be Nat st k <= n holds abs(||.seq.||.n - ||.g.||) < r; end; hence thesis by A3,SEQ_2:def 7; end; definition let X, Y be RealNormSpace; let IT be LinearOperator of X,Y; attr IT is bounded means :Def16: ex K being Real st 0 <= K & for x being VECTOR of X holds ||. IT.x .|| <= K*||. x .||; end; theorem LM21: for X, Y be RealNormSpace holds for f be LinearOperator of X,Y st (for x be VECTOR of X holds f.x=0.Y) holds f is bounded proof let X, Y be RealNormSpace; let f be LinearOperator of X,Y such that AS1: for x be VECTOR of X holds f.x=0.Y; AS2: now let x be VECTOR of X; thus ||. f.x .|| = ||. 0.Y .|| by AS1 .=0*||. x .|| by NORMSP_1:5; end; take 0; thus thesis by AS2; end; definition let X, Y be RealNormSpace; cluster bounded LinearOperator of X,Y; existence proof set f=(the carrier of X) --> 0.Y; reconsider f as LinearOperator of X,Y by LM20; take f; for x be VECTOR of X holds f.x =0.Y by FUNCOP_1:13; hence thesis by LM21; end; end; definition let X, Y be RealNormSpace; func BoundedLinearOperators(X,Y) -> Subset of R_VectorSpace_of_LinearOperators(X,Y) means :Def17: for x being set holds x in it iff x is bounded LinearOperator of X,Y; existence proof defpred P[set] means $1 is bounded LinearOperator of X,Y; consider IT being set such that A1:for x being set holds x in IT iff x in LinearOperators(X,Y) & P[x] from Separation; B1: IT is Subset of LinearOperators(X,Y) proof for x be set st x in IT holds x in LinearOperators(X,Y) by A1; hence thesis by TARSKI:def 3; end; B2: the carrier of R_VectorSpace_of_LinearOperators(X,Y) = LinearOperators(X,Y) proof R_VectorSpace_of_LinearOperators(X,Y) = RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) by Def15; hence thesis; end; take IT; thus IT is Subset of R_VectorSpace_of_LinearOperators(X,Y) by B1,B2; let x be set; thus x in IT implies x is bounded LinearOperator of X,Y by A1; assume aa: x is bounded LinearOperator of X,Y; then x in LinearOperators(X,Y) by Def12; hence thesis by A1,aa; end; uniqueness proof let X1,X2 be Subset of R_VectorSpace_of_LinearOperators(X,Y); assume that A2: for x being set holds x in X1 iff x is bounded LinearOperator of X,Y and A3: for x being set holds x in X2 iff x is bounded LinearOperator of X,Y; for x being set st x in X1 holds x in X2 proof let x be set; assume x in X1; then x is bounded LinearOperator of X,Y by A2; hence thesis by A3; end; then A4: X1 c= X2 by TARSKI:def 3; for x being set st x in X2 holds x in X1 proof let x be set; assume x in X2; then x is bounded LinearOperator of X,Y by A3; hence thesis by A2; end; then X2 c= X1 by TARSKI:def 3; hence thesis by A4,XBOOLE_0:def 10; end; end; definition let X, Y be RealNormSpace; cluster BoundedLinearOperators(X,Y) -> non empty; coherence proof set f=(the carrier of X) --> 0.Y; reconsider f as LinearOperator of X,Y by LM20; f is bounded proof for x be VECTOR of X holds f.x =0.Y by FUNCOP_1:13; hence thesis by LM21; end; hence thesis by Def17; end; end; theorem Th51: for X, Y be RealNormSpace holds BoundedLinearOperators(X,Y) is lineary-closed proof let X, Y be RealNormSpace; set W = BoundedLinearOperators(X,Y); A0: R_VectorSpace_of_LinearOperators(X,Y) = RLSStruct (# LinearOperators(X,Y), Zero_(LinearOperators(X,Y),RealVectSpace(the carrier of X,Y)), Add_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)), Mult_(LinearOperators(X,Y), RealVectSpace(the carrier of X,Y)) #) by Def15; A1:for v,u be VECTOR of R_VectorSpace_of_LinearOperators(X, Y) st v in W & u in W holds v + u in W proof let v,u be VECTOR of R_VectorSpace_of_LinearOperators(X, Y) such that A2: v in W & u in W; reconsider f=v+u as LinearOperator of X,Y by A0,Def12; f is bounded proof reconsider u1=u as bounded LinearOperator of X,Y by A2,Def17; reconsider v1=v as bounded LinearOperator of X,Y by A2,Def17; consider K1 be Real such that AS1: 0 <= K1 & for x be VECTOR of X holds ||. u1.x .|| <= K1*||. x .|| by Def16; consider K2 be Real such that AS2: 0 <= K2 & for x be VECTOR of X holds ||. v1.x .|| <= K2*||. x .|| by Def16; take K3=K1+K2; 0 + 0 <= K1+K2 by REAL_1:55, AS1, AS2; then AS3: K3 is Real & 0 <= K3; now let x be VECTOR of X; R1: ||. f.x .|| =||. u1.x+v1.x .|| by LM14; R2: ||. u1.x+v1.x .|| <= ||. u1.x .||+ ||. v1.x .|| by NORMSP_1:def 2; R3:||. u1.x .|| <= K1*||. x .|| by AS1; R4:||. v1.x .|| <= K2*||. x .|| by AS2; R5:||. u1.x .|| + ||. v1.x .|| <= K1*||. x .|| +K2*||. x .|| by R3,R4, REAL_1:55; ||. u1.x+v1.x .|| <= K1*||. x .|| +K2*||. x .|| by R5,R2,AXIOMS:22; hence ||. f.x .|| <= K3*||. x .|| by R1,XCMPLX_1:8; end; hence thesis by AS3; end; hence thesis by Def17; end; for a be Real for v be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) st v in W holds a * v in W proof let a be Real; let v be VECTOR of R_VectorSpace_of_LinearOperators(X,Y) such that A5: v in W; reconsider f=a*v as LinearOperator of X,Y by A0,Def12; f is bounded proof reconsider v1=v as bounded LinearOperator of X,Y by A5,Def17; consider K be Real such that AS1: 0 <= K & for x be VECTOR of X holds ||. v1.x .|| <= K*||. x .|| by Def16; take K1=abs(a)*K; 0 <= K & 0 <=abs(a) by AS1,ABSVALUE:5; then AS3: K1 is Real & 0 <= K1 by REAL_2:121; now let x be VECTOR of X; R1: ||. f.x .|| =||. a*v1.x .|| by LM15; R2: ||. a*v1.x .|| = abs(a)* ||. v1.x .|| by NORMSP_1:def 2; R3:||. v1.x .|| <= K*||. x .|| by AS1; RR3:0 <=abs(a) by ABSVALUE:5; abs(a)* ||. v1.x .|| <= abs(a)* (K*||. x .||) by AXIOMS:25,R3,RR3; hence ||. f.x .|| <= abs(a)* K*||. x .|| by R1,R2,XCMPLX_1:4; end; hence thesis by AS3; end; hence thesis by Def17; end; hence thesis by A1,RLSUB_1:def 1; end; theorem Th52: for X, Y be RealNormSpace holds RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) is Subspace of R_VectorSpace_of_LinearOperators(X,Y) proof let X, Y be RealNormSpace; BoundedLinearOperators(X,Y) is lineary-closed by Th51; hence thesis by RSSPACE:13; end; definition let X, Y be RealNormSpace; cluster RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like; coherence by Th52; end; theorem for X, Y be RealNormSpace holds RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) is RealLinearSpace by Th52; definition let X, Y be RealNormSpace; func R_VectorSpace_of_BoundedLinearOperators(X,Y) -> RealLinearSpace equals :Def20: RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #); coherence; end; definition let X, Y be RealNormSpace; cluster R_VectorSpace_of_BoundedLinearOperators(X,Y) -> strict; coherence proof R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; hence thesis; end; end; theorem LM54: for X, Y be RealNormSpace for f,g,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) for f',g',h' be bounded LinearOperator of X,Y st f'=f & g'=g & h'=h holds (h = f+g iff (for x be VECTOR of X holds (h'.x = f'.x + g'.x)) ) proof let X, Y be RealNormSpace; let f,g,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y); let f',g',h' be bounded LinearOperator of X,Y such that AS1: f'=f and AS2: g'=g and AS3: h'=h; R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; then A0:R_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of R_VectorSpace_of_LinearOperators(X,Y) by Th52; then reconsider f1=f as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by RLSUB_1:18; reconsider g1=g as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by A0,RLSUB_1:18; reconsider h1=h as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by A0,RLSUB_1:18; reconsider f1'=f' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; reconsider g1'=g' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; reconsider h1'=h' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; BS1: f1' = f1 by AS1; BS2: g1' = g1 by AS2; BS3: h1' = h1 by AS3; P1: now assume R1: h = f+g; let x be Element of X; h1=f1+g1 by R1,A0,RLSUB_1:21; hence h'.x=f'.x+g'.x by BS1,BS2,BS3,LM14; end; now assume R2: for x be Element of X holds h'.x=f'.x+g'.x; R3: for x be Element of X holds h1'.x = f1'.x+g1'.x by R2; h1=f1+g1 by BS1,BS2,BS3,LM14,R3; hence h =f+g by A0,RLSUB_1:21; end; hence thesis by P1; end; theorem LM55: for X, Y be RealNormSpace for f,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) for f',h' be bounded LinearOperator of X,Y st f'=f & h'=h for a be Real holds h = a*f iff for x be VECTOR of X holds h'.x = a*f'.x proof let X, Y be RealNormSpace; let f,h be VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y); let f',h' be bounded LinearOperator of X,Y such that AS1: f'=f and AS2: h'=h; let a be Real; R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; then A0:R_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of R_VectorSpace_of_LinearOperators(X,Y) by Th52; then reconsider f1=f as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by RLSUB_1:18; reconsider h1=h as VECTOR of R_VectorSpace_of_LinearOperators(X,Y) by A0,RLSUB_1:18; reconsider f1'=f' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; reconsider h1'=h' as Element of Funcs(the carrier of X, the carrier of Y) by LM00; BS1: f1' = f1 by AS1; BS2: h1' = h1 by AS2; P1: now assume R1: h = a*f; let x be Element of X; h1=a*f1 by R1,A0,RLSUB_1:22; hence h'.x=a*f'.x by BS1,BS2,LM15; end; now assume R2: for x be Element of X holds h'.x=a*f'.x; R3: for x be Element of X holds h1'.x = a*f1'.x by R2; h1=a*f1 by BS1,BS2,LM15,R3; hence h =a*f by A0,RLSUB_1:22; end; hence thesis by P1; end; theorem LM56: for X, Y be RealNormSpace holds 0.R_VectorSpace_of_BoundedLinearOperators(X,Y) =((the carrier of X) -->0.Y) proof let X, Y be RealNormSpace; R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20;then A0:R_VectorSpace_of_BoundedLinearOperators(X,Y) is Subspace of R_VectorSpace_of_LinearOperators(X,Y) by Th52; 0.R_VectorSpace_of_LinearOperators(X,Y) =((the carrier of X) -->0.Y) by LM16; hence thesis by A0,RLSUB_1:19; end; definition let X, Y be RealNormSpace; let f be set such that AS1: f in BoundedLinearOperators(X,Y); func modetrans(f,X,Y) -> bounded LinearOperator of X,Y equals:Def21: f; coherence by AS1,Def17; end; definition let X, Y be RealNormSpace; let u be LinearOperator of X,Y; func PreNorms(u) -> non empty Subset of REAL equals :Def22: {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 }; coherence proof now let x be set; now assume AA1: x in {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 }; consider t be VECTOR of X such that PS1: x=||.u.t.|| & ||.t.|| <= 1 by AA1; thus x in REAL by PS1; end; hence x in {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 } implies x in REAL; end; then P2: {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 } c= REAL by TARSKI:def 3; ||.0.X.|| = 0 by NORMSP_1:5; then ||.u.(0.X).|| in {||.u.t.|| where t is VECTOR of X : ||.t.|| <= 1 }; hence thesis by P2; end; end; theorem Lmofnorm0: for X, Y be RealNormSpace for g be bounded LinearOperator of X,Y holds PreNorms(g) is non empty bounded_above proof let X, Y be RealNormSpace; let g be bounded LinearOperator of X,Y; PreNorms(g) is bounded_above proof consider K be Real such that PK1: 0 <= K and PK2: for x be VECTOR of X holds ||. g.x .|| <= K*||. x .|| by Def16; R1:now let r be Real such that AS1: r in PreNorms(g); AS2: r in {||.g.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.g.t.|| & ||.t.|| <= 1 by AS2; PS2: ||.g.t.|| <= K*||. t .|| by PK2; K*||. t .|| <= K *1 by PS1,PK1,AXIOMS:25; hence r <=K by PS1,PS2,AXIOMS:22; end; take K; thus thesis by R1; end; hence thesis; end; theorem for X, Y be RealNormSpace for g be LinearOperator of X,Y holds g is bounded iff PreNorms(g) is bounded_above proof let X, Y be RealNormSpace; let g be LinearOperator of X,Y; Q1: g is bounded implies PreNorms(g) is non empty bounded_above by Lmofnorm0; Q2: now assume P0: PreNorms(g) is bounded_above; reconsider K=sup PreNorms(g) as Real; PP: 0 <= K proof T2:now let r be Real such that AS1: r in PreNorms(g); AS2: r in {||.g.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.g.t.|| & ||.t.|| <= 1 by AS2; thus 0 <= r by PS1,NORMSP_1:8; end; AX1:PreNorms(g) is non empty bounded_above by P0; consider r0 be set such that SS1: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by SS1; 0 <= r0 by T2,SS1; hence thesis by AX1,SEQ_4:def 4,SS1; end; P1: now let t be VECTOR of X; now per cases; case P3: t = 0.X; then g.t = g.(0*0.X) by RLVECT_1:23 .=0*g.(0.X) by Def11 .=0.Y by RLVECT_1:23; then R1: ||.g.t.|| = 0 by NORMSP_1:def 2; ||.t.|| = 0 by P3,NORMSP_1:def 2; hence ||.g.t.|| <= K*||.t.|| by R1; case P4: t <> 0.X; P5:||.t.|| <> 0 by P4,NORMSP_1:def 2; then P50: ||.t.|| > 0 by NORMSP_1:8; P51:abs( ||.t.||") = abs( 1*||.t.||") .=abs( 1/||.t.||) by XCMPLX_0:def 9 .=1/abs( ||.t.||) by ABSVALUE:15 .=1/||.t.|| by P50,ABSVALUE:def 1 .=1*||.t.||" by XCMPLX_0:def 9 .=||.t.||"; reconsider t1= ( ||.t.||")*t as VECTOR of X; P6: ||.t1.|| =abs( ||.t.||")*||.t.|| by NORMSP_1:def 2 .=1 by P5,P51,XCMPLX_0:def 7; P7: ||.g.t.||/||.t.|| = ||.g.t.||*||.t.||" by XCMPLX_0:def 9 .=||. ||.t.||"*g.t.|| by P51,NORMSP_1:def 2 .=||.g.t1.|| by Def11; ||.g.t1.|| in {||.g.s.|| where s is VECTOR of X : ||.s.|| <= 1 } by P6; then ||.g.t.||/||.t.|| in PreNorms(g) by Def22,P7; then ||.g.t.||/||.t.|| <= K by SEQ_4:def 4,P0; then P8: ||.g.t.||/||.t.||*||.t.|| <= K*||.t.|| by P50,AXIOMS:25; ||.g.t.||/||.t.||*||.t.|| = ||.g.t.||*||.t.||"*||.t.|| by XCMPLX_0:def 9 .=||.g.t.||*(||.t.||"*||.t.||) by XCMPLX_1:4 .=||.g.t.||*1 by P5,XCMPLX_0:def 7 .=||.g.t.||; hence ||.g.t.|| <= K *||.t.|| by P8; end; hence ||.g.t.|| <= K*||.t.||; end; take K; thus g is bounded by P1,PP,Def16; end; thus thesis by Q1,Q2; end; theorem LM57: for X, Y be RealNormSpace ex NORM be Function of BoundedLinearOperators(X,Y),REAL st for f be set st f in BoundedLinearOperators(X,Y) holds NORM.f = sup PreNorms(modetrans(f,X,Y)) proof let X, Y be RealNormSpace; deffunc F(set) = sup PreNorms(modetrans($1,X,Y)); A1:for z be set st z in BoundedLinearOperators(X,Y) holds F(z) in REAL; ex f being Function of BoundedLinearOperators(X,Y),REAL st for x being set st x in BoundedLinearOperators(X,Y) holds f.x = F(x) from Lambda1(A1); hence thesis; end; definition let X, Y be RealNormSpace; func BoundedLinearOperatorsNorm(X,Y) -> Function of BoundedLinearOperators(X,Y), REAL means :Def23: for x be set st x in BoundedLinearOperators(X,Y) holds it.x = sup PreNorms(modetrans(x,X,Y)); existence by LM57; uniqueness proof let NORM1,NORM2 be Function of BoundedLinearOperators(X,Y), REAL such that A1: (for x be set st x in BoundedLinearOperators(X,Y) holds NORM1.x = sup PreNorms(modetrans(x,X,Y))) and A2:(for x be set st x in BoundedLinearOperators(X,Y) holds NORM2.x = sup PreNorms(modetrans(x,X,Y))); A3:dom NORM1 = BoundedLinearOperators(X,Y) & dom NORM2 = BoundedLinearOperators(X,Y) by FUNCT_2:def 1; for z be set st z in BoundedLinearOperators(X,Y) holds NORM1.z = NORM2.z proof let z be set such that A4: z in BoundedLinearOperators(X,Y); NORM1.z = sup PreNorms(modetrans(z,X,Y)) by A1,A4; hence thesis by A2,A4; end; hence thesis by A3,FUNCT_1:9; end; end; theorem LM58: for X, Y be RealNormSpace for f be bounded LinearOperator of X,Y holds modetrans(f,X,Y)=f proof let X, Y be RealNormSpace; let f be bounded LinearOperator of X,Y; f in BoundedLinearOperators(X,Y) by Def17; hence thesis by Def21; end; theorem LM59: for X, Y be RealNormSpace for f be bounded LinearOperator of X,Y holds BoundedLinearOperatorsNorm(X,Y).f = sup PreNorms(f) proof let X, Y be RealNormSpace; let f be bounded LinearOperator of X,Y; PS1: f in BoundedLinearOperators(X,Y) by Def17; reconsider f'=f as set; thus BoundedLinearOperatorsNorm(X,Y).f = sup PreNorms(modetrans(f',X,Y)) by Def23,PS1 .= sup PreNorms(f) by LM58; end; definition let X, Y be RealNormSpace; func R_NormSpace_of_BoundedLinearOperators(X,Y) -> non empty NORMSTR equals :Def30: NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #); coherence; end; theorem Lmofnorm1: for X, Y be RealNormSpace holds ((the carrier of X) --> 0.Y) = 0.R_NormSpace_of_BoundedLinearOperators(X,Y) proof let X, Y be RealNormSpace; A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; A1: R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; ((the carrier of X) --> 0.Y) =0.R_VectorSpace_of_BoundedLinearOperators(X,Y) by LM56 .=Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) by A1,RLVECT_1:def 2 .=0.R_NormSpace_of_BoundedLinearOperators(X,Y) by A0,RLVECT_1:def 2; hence thesis; end; theorem Lmofnorm2: for X, Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for g be bounded LinearOperator of X,Y st g=f holds for t be VECTOR of X holds ||.g.t.|| <= ||.f.||*||.t.|| proof let X, Y be RealNormSpace; let f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y); let g be bounded LinearOperator of X,Y such that AS1:g=f; A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; P0: PreNorms(g) is non empty bounded_above by Lmofnorm0; now let t be VECTOR of X; now per cases; case P3: t = 0.X; g.t =g.(0*0.X) by P3,RLVECT_1:23 .=0*g.(0.X) by Def11 .=0.Y by RLVECT_1:23; then R1: ||.g.t.|| = 0 by NORMSP_1:def 2; ||.t.|| = 0 by P3,NORMSP_1:def 2; hence ||.g.t.|| <= ||.f.||*||.t.|| by R1; case P4: t <> 0.X; P5:||.t.|| <> 0 by P4,NORMSP_1:def 2; then P50: ||.t.|| > 0 by NORMSP_1:8; P51:abs( ||.t.||") =abs( 1*||.t.||") .=abs( 1/||.t.||) by XCMPLX_0:def 9 .=1/abs( ||.t.||) by ABSVALUE:15 .=1/||.t.|| by P50,ABSVALUE:def 1 .=1*||.t.||" by XCMPLX_0:def 9 .=||.t.||"; reconsider t1= ( ||.t.||")*t as VECTOR of X; P6: ||.t1.|| =abs( ||.t.||")*||.t.|| by NORMSP_1:def 2 .=1 by P5,P51,XCMPLX_0:def 7; ||.g.t.||/||.t.|| = ||.g.t.||*||.t.||" by XCMPLX_0:def 9 .=||. ||.t.||"*g.t.|| by P51,NORMSP_1:def 2 .=||.g.t1.|| by Def11; then ||.g.t.||/||.t.|| in {||.g.s.|| where s is VECTOR of X : ||.s.|| <= 1 } by P6; then ||.g.t.||/||.t.|| in PreNorms(g) by Def22; then ||.g.t.||/||.t.|| <= sup PreNorms(g) by SEQ_4:def 4,P0; then ||.g.t.||/||.t.|| <= BoundedLinearOperatorsNorm(X,Y).g by LM59; then ||.g.t.||/||.t.|| <= ||.f.|| by AS1,A0,NORMSP_1:def 1; then P8: ||.g.t.||/||.t.||*||.t.|| <= ||.f.||*||.t.|| by P50,AXIOMS:25; ||.g.t.||/||.t.||*||.t.|| = ||.g.t.||*||.t.||"*||.t.|| by XCMPLX_0:def 9 .=||.g.t.||*(||.t.||"*||.t.||) by XCMPLX_1:4 .=||.g.t.||*1 by P5,XCMPLX_0:def 7 .=||.g.t.||; hence ||.g.t.|| <= ||.f.||*||.t.|| by P8; end; hence ||.g.t.|| <= ||.f.||*||.t.||; end; hence thesis; end; theorem Lmofnorm3: for X, Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 <= ||.f.|| proof let X, Y be RealNormSpace; let f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y); A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; reconsider g=f as bounded LinearOperator of X,Y by A0,Def17; Q2: now let r be Real such that AS1: r in PreNorms(g); AS2: r in {||.g.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.g.t.|| & ||.t.|| <= 1 by AS2; thus 0 <= r by PS1,NORMSP_1:8; end; AX1:PreNorms(g) is non empty bounded_above by Lmofnorm0; consider r0 be set such that SS1: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by SS1; 0 <= r0 by Q2,SS1; then SS4: 0 <=sup PreNorms(g) by AX1,SEQ_4:def 4,SS1; BoundedLinearOperatorsNorm(X,Y).f = sup PreNorms(g) by LM59; hence thesis by A0,SS4,NORMSP_1:def 1; end; theorem Lmofnorm4: for X, Y be RealNormSpace for f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y) holds 0 = ||.f.|| proof let X, Y be RealNormSpace; let f being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) such that P211: f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y); A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; thus ||.f.|| = 0 proof set z = (the carrier of X) --> 0.Y; reconsider z as Function of the carrier of X, the carrier of Y by FUNCOP_1:58; reconsider g=f as bounded LinearOperator of X,Y by A0,Def17; Q1: z=g by P211,Lmofnorm1; Q2: now let r be Real such that AS1: r in PreNorms(g); AS2: r in {||.g.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.g.t.|| & ||.t.|| <= 1 by AS2; ||.g.t.|| = ||.0.Y.|| by Q1,FUNCOP_1:13 .= 0 by NORMSP_1:def 2; hence 0 <= r & r <=0 by PS1; end; AX1:PreNorms(g) is non empty bounded_above by Lmofnorm0; consider r0 be set such that SS1: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by SS1; 0 <= r0 & r0<=0 by Q2,SS1; then SS4: 0 <=sup PreNorms(g) by AX1,SEQ_4:def 4,SS1; (for s be real number st s in PreNorms(g) holds s <= 0) implies sup PreNorms(g) <= 0 by PSCOMP_1:10; then SS5: sup PreNorms(g) <=0 by Q2; Q3:sup PreNorms(g) = 0 by SS4,SS5; BoundedLinearOperatorsNorm(X,Y).f=0 by Q3,LM59; hence thesis by A0,NORMSP_1:def 1; end; end; theorem LMB54: for X, Y be RealNormSpace for f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for f',g',h' be bounded LinearOperator of X,Y st f'=f & g'=g & h'=h holds (h = f+g iff (for x be VECTOR of X holds (h'.x = f'.x + g'.x)) ) proof let X, Y be RealNormSpace; let f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y); let f',g',h' be bounded LinearOperator of X,Y such that AS1: f'=f and AS2: g'=g and AS3: h'=h; A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; A1: R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; reconsider f1=f, g1=g, h1=h as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) by A0,A1; P1: (h1 = f1+g1 iff (for x be VECTOR of X holds (h'.x = f'.x + g'.x)) ) by LM54,AS1,AS2,AS3; h=f+g iff h1=f1+g1 proof L: now assume h=f+g; hence h1=Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)).[f,g] by A0,RLVECT_1:def 3 .=f1+g1 by A1,RLVECT_1:def 3; end; now assume h1=f1+g1; hence h=Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) .[f1,g1] by A1,RLVECT_1:def 3 .=f+g by A0,RLVECT_1:def 3; end; hence thesis by L; end; hence thesis by P1; end; theorem LMB55: for X, Y be RealNormSpace for f,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for f',h' be bounded LinearOperator of X,Y st f'=f & h'=h for a be Real holds h = a*f iff for x be VECTOR of X holds h'.x = a*f'.x proof let X, Y be RealNormSpace; let f,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y); let f',h' be bounded LinearOperator of X,Y such that AS1: f'=f and AS2: h'=h; let a be Real; A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; A1: R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; reconsider f1=f as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) by A0,A1; reconsider h1=h as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) by A0,A1; P1: (h1 = a*f1 iff (for x be VECTOR of X holds (h'.x = a*f'.x)) ) by LM55,AS1,AS2; h=a*f iff h1=a*f1 proof L: now assume h=a*f; hence h1=Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)).[a,f] by A0,RLVECT_1:def 4 .=a*f1 by A1,RLVECT_1:def 4; end; now assume h1=a*f1; hence h=Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) .[a,f1] by A1,RLVECT_1:def 4 .=a*f by A0,RLVECT_1:def 4; end; hence thesis by L; end; hence thesis by P1; end; theorem LM60: for X be RealNormSpace for Y be RealNormSpace for f, g being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for a be Real holds ( ||.f.|| = 0 iff f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y) ) & ||.a*f.|| = abs(a) * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.|| proof let X be RealNormSpace; let Y be RealNormSpace; let f, g being Point of R_NormSpace_of_BoundedLinearOperators(X,Y); let a be Real; A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; A1: R_VectorSpace_of_BoundedLinearOperators(X,Y) = RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) by Def20; P1: now assume P11: ||.f.|| = 0; reconsider g=f as bounded LinearOperator of X,Y by A0,Def17; set z = (the carrier of X) --> 0.Y; reconsider z as Function of the carrier of X, the carrier of Y by FUNCOP_1:58; PPP:now let t be VECTOR of X; ||.g.t.|| <= ||.f.|| *||.t.|| by Lmofnorm2; then ||.g.t.|| = 0 by P11,NORMSP_1:8; hence g.t =0.Y by NORMSP_1:def 2 .=z.t by FUNCOP_1:13; end; g=z by PPP,FUNCT_2:113; hence f=0.R_NormSpace_of_BoundedLinearOperators(X,Y) by Lmofnorm1; end; P2: now assume P211: f = 0.R_NormSpace_of_BoundedLinearOperators(X,Y); thus ||.f.|| = 0 proof set z = (the carrier of X) --> 0.Y; reconsider z as Function of the carrier of X, the carrier of Y by FUNCOP_1:58; reconsider g=f as bounded LinearOperator of X,Y by A0,Def17; Q1: z=g by P211,Lmofnorm1; Q2: now let r be Real such that AS1: r in PreNorms(g); AS2: r in {||.g.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.g.t.|| & ||.t.|| <= 1 by AS2; ||.g.t.|| = ||.0.Y.|| by Q1,FUNCOP_1:13 .= 0 by NORMSP_1:def 2; hence 0 <= r & r <=0 by PS1; end; AX1:PreNorms(g) is non empty bounded_above by Lmofnorm0; consider r0 be set such that SS1: r0 in PreNorms(g) by XBOOLE_0:def 1; reconsider r0 as Real by SS1; 0<=r0 by Q2,SS1; then SS4: 0 <=sup PreNorms(g) by AX1,SEQ_4:def 4,SS1; (for s be real number st s in PreNorms(g) holds s <= 0) implies sup PreNorms(g) <= 0 by PSCOMP_1:10; then SS5: sup PreNorms(g) <= 0 by Q2; Q3:sup PreNorms(g) = 0 by SS4,SS5; BoundedLinearOperatorsNorm(X,Y).f =0 by Q3,LM59; hence thesis by A0,NORMSP_1:def 1; end; end; P3: ||.a*f.|| = abs(a) * ||.f.|| proof reconsider f1=f, h1=a*f as bounded LinearOperator of X,Y by A0,Def17; R41: now let t be VECTOR of X such that A41: ||.t.|| <= 1; B1: ||.h1.t.||= ||.a*f1.t.|| by LMB55; B2: ||.a*f1.t.|| =abs(a)*||.f1.t.|| by NORMSP_1:def 2; B3: ||.f1.t.||<= ||.f.||*||.t.|| by Lmofnorm2; 0 <= ||.f.|| by Lmofnorm3; then ||.f.||*||.t.|| <= ||.f.||*1 by A41,AXIOMS:25; then B6: ||.f1.t.|| <= ||.f.|| by B3,AXIOMS:22; 0<= abs(a) by ABSVALUE:5; hence ||.h1.t.|| <= abs(a)*||.f.|| by B1,B2,B6,AXIOMS:25; end; R42: now let r be Real such that AS1: r in PreNorms(h1); AS2: r in {||.h1.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.h1.t.|| & ||.t.|| <= 1 by AS2; thus r <= abs(a)*||.f.|| by PS1,R41; end; AX5: (for s be real number st s in PreNorms(h1) holds s <= abs(a)*||.f.|| ) implies sup PreNorms(h1) <= abs(a)*||.f.|| by PSCOMP_1:10; R43:sup PreNorms(h1) <= abs(a)*||.f.|| by R42,AX5; BoundedLinearOperatorsNorm(X,Y).(a*f) = sup PreNorms(h1) by LM59; then R45: ||.a*f.|| <= abs(a)*||.f.|| by A0,R43,NORMSP_1:def 1; now per cases; case CA1: a <> 0; L41: now let t be VECTOR of X such that A41: ||.t.|| <= 1; h1.t=a*f1.t by LMB55; then a"*h1.t =( a"* a)*f1.t by RLVECT_1:def 9 .=1*f1.t by XCMPLX_0:def 7,CA1 .=f1.t by RLVECT_1:def 9; then B1: ||.f1.t.||= ||.a"*h1.t.||; B2: ||.a"*h1.t.|| =abs(a")*||.h1.t.|| by NORMSP_1:def 2; B3: ||.h1.t.||<= ||.a*f.||*||.t.|| by Lmofnorm2; 0 <= ||.a*f.|| by Lmofnorm3; then ||.a*f.||*||.t.|| <= ||.a*f.||*1 by A41,AXIOMS:25; then B6: ||.h1.t.|| <= ||.a*f.|| by B3,AXIOMS:22; 0<= abs(a") by ABSVALUE:5; then B8: ||.f1.t.|| <=abs(a")*||.a*f.|| by B1,B2,B6,AXIOMS:25; abs(a") =abs(1*a") .=abs( 1/a) by XCMPLX_0:def 9 .=1/abs(a) by ABSVALUE:15 .=1*abs(a)" by XCMPLX_0:def 9 .=abs(a)"; hence ||.f1.t.|| <= abs(a)"*||.a*f.|| by B8; end; L42: now let r be Real such that AS1: r in PreNorms(f1); AS2: r in {||.f1.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.f1.t.|| & ||.t.|| <= 1 by AS2; thus r <= abs(a)"*||.a*f.|| by PS1,L41; end; K0: abs(a) <>0 by CA1,ABSVALUE:6; AX5: (for s be real number st s in PreNorms(f1) holds s <= abs(a)"*||.a*f.|| ) implies sup PreNorms(f1) <= abs(a)"*||.a*f.|| by PSCOMP_1:10; L43:sup PreNorms(f1) <=abs(a)"*||.a*f.|| by L42,AX5; BoundedLinearOperatorsNorm(X,Y).(f) = sup PreNorms(f1) by LM59; then K45: ||.f.|| <=abs(a)"*||.a*f.|| by A0,L43,NORMSP_1:def 1; 0 <= abs(a) by ABSVALUE:5; then abs(a)*||.f.|| <=abs(a)*(abs(a)"*||.a*f.||) by K45,AXIOMS:25; then abs(a)*||.f.|| <=(abs(a)*abs(a)")*||.a*f.|| by XCMPLX_1:4; then abs(a)*||.f.|| <=1*||.a*f.|| by XCMPLX_0:def 7,K0; hence abs(a)* ||.f.|| <=||.a*f.||; case CA2: a=0; reconsider fz=f as VECTOR of R_VectorSpace_of_BoundedLinearOperators(X,Y) by A0,A1; a*f =Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)).[a,f] by A0,RLVECT_1:def 4 .=a*fz by A1,RLVECT_1:def 4 .=0.R_VectorSpace_of_BoundedLinearOperators(X,Y) by CA2,RLVECT_1:23 .=Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) by A1,RLVECT_1:def 2 .=0.R_NormSpace_of_BoundedLinearOperators(X,Y) by A0,RLVECT_1:def 2; then CH1: ||.a*f.||=0 by Lmofnorm4; thus abs(a)* ||.f.|| =0 * ||.f.|| by CA2,ABSVALUE:7 .=||.a*f.|| by CH1; end; hence thesis by R45,AXIOMS:21; end; ||.f+g.|| <= ||.f.|| + ||.g.|| proof reconsider f1=f, g1=g, h1=f+g as bounded LinearOperator of X,Y by A0,Def17; R41: now let t be VECTOR of X such that A41: ||.t.|| <= 1; B1: ||.h1.t.||= ||.f1.t+g1.t.|| by LMB54; B2: ||.f1.t+g1.t.|| <=||.f1.t.||+||.g1.t.|| by NORMSP_1:def 2; B3: ||.f1.t.||<= ||.f.||*||.t.|| by Lmofnorm2; B4: ||.g1.t.||<= ||.g.||*||.t.|| by Lmofnorm2; B6: ||.f1.t.||+||.g1.t.|| <= ||.f.||*||.t.|| + ||.g.||*||.t.|| by B3,B4,REAL_1:55; 0 <= ||.f.|| by Lmofnorm3; then B7: ||.f.||*||.t.|| <= ||.f.||*1 by A41,AXIOMS:25; 0 <= ||.g.|| by Lmofnorm3; then B8: ||.g.||*||.t.|| <= ||.g.||*1 by A41,AXIOMS:25; ||.f.||*||.t.|| + ||.g.||*||.t.|| <= ||.f.||*1 + ||.g.||*1 by B7,B8,REAL_1:55; then ||.f1.t.||+||.g1.t.|| <= ||.f.|| + ||.g.|| by B6,AXIOMS:22; hence ||.h1.t.|| <= ||.f.|| + ||.g.|| by B1,B2,AXIOMS:22; end; R42: now let r be Real such that AS1: r in PreNorms(h1); AS2: r in {||.h1.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.h1.t.|| & ||.t.|| <= 1 by AS2; thus r <= ||.f.|| + ||.g.|| by PS1,R41; end; AX5: (for s be real number st s in PreNorms(h1) holds s <= ||.f.|| + ||.g.||) implies sup PreNorms(h1) <= ||.f.|| + ||.g.|| by PSCOMP_1:10; R43:sup PreNorms(h1) <=||.f.|| + ||.g.|| by R42,AX5; BoundedLinearOperatorsNorm(X,Y).(f+g) = sup PreNorms(h1) by LM59; hence ||.f+g.|| <=||.f.|| + ||.g.|| by A0,R43,NORMSP_1:def 1; end; hence thesis by P1,P2,P3; end; theorem LM61: for X,Y be RealNormSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is RealNormSpace-like proof let X,Y be RealNormSpace; for x, y being Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for a be Real holds ( ||.x.|| = 0 iff x = 0.R_NormSpace_of_BoundedLinearOperators(X,Y) ) & ||.a*x.|| = abs(a) * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by LM60; hence thesis by NORMSP_1:def 2; end; theorem LM62: for X, Y be RealNormSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is RealNormSpace proof let X, Y be RealNormSpace; A1: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; RLSStruct (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)) #) is RealLinearSpace; hence thesis by LM61,RSSPACE3:4,A1; end; definition let X, Y be RealNormSpace; cluster R_NormSpace_of_BoundedLinearOperators(X,Y) -> RealNormSpace-like RealLinearSpace-like Abelian add-associative right_zeroed right_complementable; coherence by LM62; end; theorem LMB54M: for X, Y be RealNormSpace for f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) for f',g',h' be bounded LinearOperator of X,Y st f'=f & g'=g & h'=h holds (h = f-g iff (for x be VECTOR of X holds (h'.x = f'.x - g'.x)) ) proof let X, Y be RealNormSpace; let f,g,h be Point of R_NormSpace_of_BoundedLinearOperators(X,Y); let f',g',h' be bounded LinearOperator of X,Y such that AS1: f'=f and AS2: g'=g and AS3: h'=h; R1: now assume h=f-g; then h+g=f-(g-g) by RLVECT_1:43; then h+g=f-0.R_NormSpace_of_BoundedLinearOperators(X,Y) by RLVECT_1:28; then h+g=f by RLVECT_1:26; then R12: for x be VECTOR of X holds (f'.x=h'.x + g'.x) by AS1,AS2,AS3,LMB54; now let x be VECTOR of X; f'.x=h'.x + g'.x by R12; then f'.x-g'.x=h'.x + (g'.x-g'.x) by RLVECT_1:42; then f'.x-g'.x=h'.x + 0.Y by RLVECT_1:28; hence f'.x-g'.x=h'.x by RLVECT_1:10; end; hence for x be VECTOR of X holds (h'.x = f'.x - g'.x); end; now assume L12: for x be VECTOR of X holds (h'.x = f'.x - g'.x); now let x be VECTOR of X; h'.x = f'.x - g'.x by L12; then h'.x + g'.x= f'.x - (g'.x- g'.x) by RLVECT_1:43; then h'.x + g'.x= f'.x - 0.Y by RLVECT_1:28; hence h'.x + g'.x= f'.x by RLVECT_1:26; end; then f=h+g by AS1,AS2,AS3,LMB54; then f-g=h+(g-g) by RLVECT_1:42; then f-g=h+0.R_NormSpace_of_BoundedLinearOperators(X,Y) by RLVECT_1:28; hence f-g=h by RLVECT_1:10; end; hence thesis by R1; end; begin :: Real Banach Space of Bounded Linear Operators definition let X be RealNormSpace; attr X is complete means :Def40: for seq be sequence of X holds seq is Cauchy_sequence_by_Norm implies seq is convergent; end; definition cluster complete RealNormSpace; existence proof take l1_Space; thus thesis by Def40,RSSPACE3:11; end; end; definition mode RealBanachSpace is complete RealNormSpace; end; RLEM02: for e be Real, seq be Real_Sequence st ( seq is convergent & ex k be Nat st (for i be Nat st k <= i holds seq.i <=e ) ) holds lim seq <=e proof let e be Real; let seq be Real_Sequence such that AS1:seq is convergent and AS2:ex k be Nat st (for i be Nat st k <= i holds seq.i <=e ); deffunc F(set) = e; consider cseq be Real_Sequence such that P1:for n be Nat holds cseq.n=F(n) from ExRealSeq; reconsider e1=e as real number; P3:cseq is constant by SEQM_3:def 6,P1; then P4:cseq is convergent by SEQ_4:39; consider k be Nat such that AS3:for i be Nat st k <= i holds seq.i <=e by AS2; R1:(seq ^\k) is convergent by AS1,SEQ_4:33; R2:lim (seq ^\k)=lim seq by AS1,SEQ_4:33; P5:now let i be Nat; P51: (seq ^\k).i = seq.(k+i) by SEQM_3:def 9; k <= k+i by NAT_1:29; then seq.(k+i) <=e by AS3; hence (seq ^\k) .i <= cseq.i by P1,P51; end; lim cseq = cseq.0 by P3,SEQ_4:41 .= e by P1; hence thesis by P5,R1,P4,SEQ_2:32,R2; end; theorem RLEM03: for X be RealNormSpace for seq be sequence of X st seq is convergent holds ||.seq.|| is convergent & lim ||.seq.|| = ||.lim seq.|| proof let X be RealNormSpace; let seq be sequence of X such that AS1: seq is convergent; now let e1 be real number such that AA2: e1 >0; reconsider e =e1 as Real by XREAL_0:def 1; consider k be Nat such that AA3: for n be Nat st n >= k holds ||.seq.n - lim seq.|| < e by AS1,AA2,NORMSP_1:def 11; AA4: now let m be Nat such that BB4: m >= k; AA7: ||.seq.m.||= ||.seq.||.m by NORMSP_1:def 10; AA8: abs( ||.seq.||.m - ||.lim seq.|| ) <= ||.seq.m - lim seq.|| by NORMSP_1:13,AA7; AA9: ||.seq.m - lim seq.|| <e by AA3,BB4; thus abs( ||.seq.||.m - ||.lim seq.|| ) <e1 by AA9,AA8, AXIOMS:22; end; take k; thus for m be Nat st m >= k holds abs(||.seq.||.m - ||.lim seq.|| ) < e1 by AA4; end; then F1: for s be real number st 0<s ex n be Nat st for m be Nat st n<=m holds abs(||.seq.||.m -||.lim seq.||)<s; ||.seq.|| is convergent by SEQ_2:def 6,F1; hence thesis by SEQ_2:def 7,F1; end; theorem LM63: for X, Y be RealNormSpace st Y is complete for seq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y) st seq is Cauchy_sequence_by_Norm holds seq is convergent proof let X, Y be RealNormSpace such that AS1: Y is complete; let vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y) such that A1: vseq is Cauchy_sequence_by_Norm; AA1: ||.vseq.|| is convergent proof now let e1 be real number such that AA2: e1 >0; reconsider e =e1 as Real by XREAL_0:def 1; consider k be Nat such that AA3: for n, m be Nat st ( n >= k & m >= k ) holds ||.(vseq.n) - (vseq.m).|| < e by A1,AA2,RSSPACE3:10; AA4: now let m be Nat such that BB4: m >= k; AA4: k >=k & m >= k by BB4; AA5: abs( ||.vseq.m.||- ||.vseq.k.|| ) <= ||.(vseq.m) - (vseq.k).|| by NORMSP_1:13; AA6: ||.vseq.k.||= ||.vseq.||.k by NORMSP_1:def 10; AA7: ||.vseq.m.||= ||.vseq.||.m by NORMSP_1:def 10; AA8: abs( ||.vseq.||.m - ||.vseq.||.k ) <= ||.(vseq.m) - (vseq.k).|| by AA5,AA6,AA7; AA9: ||.(vseq.m) - (vseq.k).|| <e by AA4,AA3; thus abs( ||.vseq.||.m - ||.vseq.||.k ) <e1 by AA9,AA8, AXIOMS:22; end; take k; thus for m be Nat st m >= k holds abs(||.vseq.||.m - ||.vseq.||.k ) < e1 by AA4; end; hence ||.vseq.|| is convergent by SEQ_4:58; end; defpred P[set, set] means ex xseq be sequence of Y st (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).$1) & xseq is convergent & $2= lim xseq; A0: R_NormSpace_of_BoundedLinearOperators(X,Y) = NORMSTR (# BoundedLinearOperators(X,Y), Zero_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Add_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), Mult_(BoundedLinearOperators(X,Y), R_VectorSpace_of_LinearOperators(X,Y)), BoundedLinearOperatorsNorm(X,Y) #) by Def30; A2: for x be Element of X ex y be Element of Y st P[x,y] proof let x be Element of X; deffunc F(Nat) = modetrans((vseq.$1),X,Y).x; consider xseq be sequence of Y such that A4: for n be Nat holds xseq.n = F(n) from ExRNSSeq; A40: for m,k be Nat holds ||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| * ||.x.|| proof let m,k be Nat; vseq.m is bounded LinearOperator of X,Y by A0, Def17; then V1: modetrans((vseq.m),X,Y)=vseq.m by LM58; vseq.k is bounded LinearOperator of X,Y by A0, Def17; then V2: modetrans((vseq.k),X,Y)=vseq.k by LM58; vseq.m-vseq.k is bounded LinearOperator of X,Y by A0, Def17; then reconsider h1=vseq.m-vseq.k as bounded LinearOperator of X,Y; B1: xseq.m =modetrans((vseq.m),X,Y).x by A4; B2: xseq.k =modetrans((vseq.k),X,Y).x by A4; xseq.m - xseq.k = h1.x by B1,B2,V1,V2,LMB54M; hence thesis by Lmofnorm2; end; A5: xseq is convergent proof now let e be Real such that A6: e > 0; thus ex k be Nat st for n, m be Nat st ( n >= k & m >= k ) holds ||.xseq.n -xseq.m.|| < e proof now per cases; case C11:x=0.X; take k=0; thus for n, m be Nat st ( n >= k & m >= k ) holds ||.xseq.n -xseq.m.|| < e proof let n, m be Nat such that n >= k & m >= k; C122: xseq.n=modetrans((vseq.n),X,Y).x by A4 .=modetrans((vseq.n),X,Y).(0*x) by RLVECT_1:23,C11 .=0*modetrans((vseq.n),X,Y).x by Def11 .=0.Y by RLVECT_1:23; C123: xseq.m=modetrans((vseq.m),X,Y).x by A4 .=modetrans((vseq.m),X,Y).(0*x) by RLVECT_1:23,C11 .=0*modetrans((vseq.m),X,Y).x by Def11 .=0.Y by RLVECT_1:23; ||.xseq.n -xseq.m.|| = ||.0.Y.|| by C122,C123,RLVECT_1:26 .=0 by NORMSP_1:def 2; hence ||.xseq.n -xseq.m.|| < e by A6; end; case C12:x <>0.X; II: ||.x.|| <> 0 by NORMSP_1:def 2,C12; then JJ: ||.x.|| > 0 by NORMSP_1:8; then KK: e/||.x.||>0 by SEQ_2:6,A6; consider k be Nat such that A8: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) - (vseq.m).|| < e/||.x.|| by A1,KK,RSSPACE3:10; take k; thus for n, m be Nat st ( n >= k & m >= k ) holds ||.xseq.n-xseq.m.|| < e proof let n,m be Nat such that A9: n >=k & m >= k; A91: ||.xseq.n-xseq.m.|| <= ||.(vseq.n) - (vseq.m).|| * ||.x.|| by A40; ||.(vseq.n) - (vseq.m).|| < e/||.x.|| by A8,A9; then A92: ||.(vseq.n) - (vseq.m).|| * ||.x.|| < e/||.x.|| * ||.x.|| by JJ, REAL_1:70; e/||.x.|| * ||.x.|| = e*||.x.||"* ||.x.|| by XCMPLX_0:def 9 .= e*(||.x.||"* ||.x.||) by XCMPLX_1:4 .= e*1 by II,XCMPLX_0:def 7 .=e; hence ||.xseq.n-xseq.m.|| < e by A91,AXIOMS:22,A92; end; end; hence thesis; end; end; then xseq is Cauchy_sequence_by_Norm by RSSPACE3:10; hence thesis by AS1,Def40; end; take y = lim xseq; thus thesis by A4,A5; end; consider f be Function of the carrier of X,the carrier of Y such that A16:for x be Element of X holds P[x,f.x] from FuncExD(A2); reconsider tseq=f as Function of X,Y; A17: for x be Element of X ex xseq be sequence of Y st (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x) & xseq is convergent & tseq.x = lim xseq by A16; tseq is LinearOperator of X,Y proof H1: now let x,y be VECTOR of X; consider xseq be sequence of Y such that H11: (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x) & xseq is convergent & tseq.x = lim xseq by A17; consider yseq be sequence of Y such that H12: (for n be Nat holds yseq.n=modetrans((vseq.n),X,Y).y) & yseq is convergent & tseq.y = lim yseq by A17; consider zseq be sequence of Y such that H13: (for n be Nat holds zseq.n=modetrans((vseq.n),X,Y).(x+y)) & zseq is convergent & tseq.(x+y) = lim zseq by A17; H14: zseq=xseq+yseq proof now let n be Nat; thus zseq.n=modetrans((vseq.n),X,Y).(x+y) by H13 .= modetrans((vseq.n),X,Y).x+modetrans((vseq.n),X,Y).y by Def10 .= xseq.n + modetrans((vseq.n),X,Y).y by H11 .= xseq.n +yseq.n by H12; end; hence thesis by NORMSP_1:def 5; end; thus tseq.(x+y)=tseq.x+tseq.y by H11,H12,H13, H14,NORMSP_1:42; end; now let x be VECTOR of X; let a be Real; consider xseq be sequence of Y such that H21: (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x) & xseq is convergent & tseq.x = lim xseq by A17; consider zseq be sequence of Y such that H23: (for n be Nat holds zseq.n=modetrans((vseq.n),X,Y).(a*x)) & zseq is convergent & tseq.(a*x) = lim zseq by A17; zseq=a*xseq proof now let n be Nat; thus zseq.n=modetrans((vseq.n),X,Y).(a*x) by H23 .= a*modetrans((vseq.n),X,Y).x by Def11 .= a*xseq.n by H21; end; hence thesis by NORMSP_1:def 8; end; hence tseq.(a*x)=a*tseq.x by H21,H23,NORMSP_1:45; end; hence thesis by H1,Def10,Def11; end; then reconsider tseq as LinearOperator of X,Y; BND01: tseq is bounded proof K2: now let x be VECTOR of X; consider xseq be sequence of Y such that K21: (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x) & xseq is convergent & tseq.x = lim xseq by A17; A41: for m be Nat holds ||.xseq.m.|| <= ||.vseq.m.|| * ||.x.|| proof let m be Nat; V0: vseq.m is bounded LinearOperator of X,Y by A0, Def17; then V1: modetrans((vseq.m),X,Y)=vseq.m by LM58; reconsider h1=vseq.m as bounded LinearOperator of X,Y by V0; xseq.m =modetrans((vseq.m),X,Y).x by K21; hence thesis by Lmofnorm2,V1; end; K22: ||.xseq.|| is convergent by K21,NMLM01; K23: ||.tseq.x.|| = lim ||.xseq.|| by K21,NMLM01; K24: for n be Nat holds ||.xseq.||.n <=( ||.x.||(#)||.vseq.||).n proof let n be Nat; K25: ||.xseq.||.n = ||.(xseq.n).|| by NORMSP_1:def 10; K26: ||.(xseq.n).|| <= ||.vseq.n.|| * ||.x.|| by A41; ||.vseq.n.|| = ||.vseq.||.n by NORMSP_1:def 10; hence thesis by K25,SEQ_1:13,K26; end; K30: ||.vseq.|| is convergent by AA1; K31: ||.x.||(#)||.vseq.|| is convergent by K30,SEQ_2:21; K32: lim ( ||.x.||(#)||.vseq.|| ) = lim (||.vseq.|| )* ||.x.|| by K30,SEQ_2:22; lim ||.xseq.|| <= lim (||.vseq.|| )* ||.x.|| by K22,K31,K32,K24,SEQ_2:32; hence ||.tseq.x.|| <= lim (||.vseq.|| )* ||.x.|| by K23; end; take K= lim (||.vseq.|| ); K >=0 proof now let n be Nat; K35: ||.vseq.||.n= ||.vseq.n.|| by NORMSP_1:def 10; K36: ||.vseq.n.|| >=0 by NORMSP_1:8; thus ||.vseq.||.n >=0 by K35,K36; end; hence thesis by AA1,SEQ_2:31; end; hence thesis by K2; end; BND02: for e be Real st e > 0 ex k be Nat st for n be Nat st n >= k holds for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| proof let e be Real such that ND03:e > 0; consider k be Nat such that ND04: for n, m be Nat st ( n >= k & m >= k ) holds ||.(vseq.n) - (vseq.m).|| < e by A1,ND03,RSSPACE3:10; ND05: now let n be Nat such that ND06: n >= k; now let x be VECTOR of X; consider xseq be sequence of Y such that ND07: (for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x) & xseq is convergent & tseq.x = lim xseq by A17; ND08: for m,k be Nat holds ||.xseq.m-xseq.k.|| <= ||.vseq.m - vseq.k.|| * ||.x.|| proof let m,k be Nat; vseq.m is bounded LinearOperator of X,Y by A0, Def17; then V1: modetrans((vseq.m),X,Y)=vseq.m by LM58; vseq.k is bounded LinearOperator of X,Y by A0, Def17; then V2: modetrans((vseq.k),X,Y)=vseq.k by LM58; reconsider h1=vseq.m-vseq.k as bounded LinearOperator of X,Y by A0, Def17; B1: xseq.m =modetrans((vseq.m),X,Y).x by ND07; B2: xseq.k =modetrans((vseq.k),X,Y).x by ND07; xseq.m - xseq.k =h1.x by V1,V2,B1,B2,LMB54M; hence thesis by Lmofnorm2; end; ND09: for m be Nat st m >=k holds ||.xseq.n-xseq.m.|| <= e * ||.x.|| proof let m be Nat such that ND10: m >=k; ND11: ||.xseq.n-xseq.m.|| <= ||.vseq.n - vseq.m.|| * ||.x.|| by ND08; ND12: ||.vseq.n - vseq.m.|| <e by ND10,ND06,ND04; 0 <= ||.x.|| by NORMSP_1:8; then ||.vseq.n - vseq.m.|| * ||.x.|| <= e* ||.x.|| by ND12,AXIOMS:25; hence thesis by ND11,AXIOMS:22; end; ||.xseq.n-tseq.x.|| <= e * ||.x.|| proof deffunc F(Nat) = ||.xseq.$1 - xseq.n.||; consider rseq be Real_Sequence such that P1: for m be Nat holds rseq.m = F(m) from ExRealSeq; SS1: rseq is convergent & lim rseq = ||.tseq.x-xseq.n.|| proof F1: xseq is convergent by ND07; F2: xseq - xseq.n is convergent by F1,NORMSP_1:36; F3: lim (xseq-xseq.n)= tseq.x - xseq.n by ND07,NORMSP_1:44; F4: ||.xseq-xseq.n.|| is convergent by F2,RLEM03; F5: lim ||.xseq-xseq.n.||= ||.tseq.x - xseq.n.|| by F3,F2,RLEM03; F6: rseq = ||.xseq - xseq.n.|| proof now let x be set such that DD: x in NAT; reconsider k=x as Nat by DD; thus rseq.x = ||.xseq.k - xseq.n.|| by P1 .= ||.(xseq - xseq.n).k.|| by NORMSP_1:def 7 .= ||.(xseq - xseq.n).||.x by NORMSP_1:def 10; end; hence thesis by SEQ_1:8; end; thus thesis by F6,F5,F4; end; SS2: for m be Nat st m >= k holds rseq.m <= e * ||.x.|| proof let m be Nat such that I0: m >=k; I1: ||.xseq.n-xseq.m.|| <= e * ||.x.|| by I0,ND09; rseq.m = ||.xseq.m-xseq.n.|| by P1 .= ||.xseq.n-xseq.m.|| by NORMSP_1:11; hence thesis by I1; end; lim rseq <= e * ||.x.|| by RLEM02,SS1,SS2; hence thesis by NORMSP_1:11,SS1; end; hence ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| by ND07; end; hence for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.||; end; take k; thus thesis by ND05; end; reconsider tseq as bounded LinearOperator of X,Y by BND01; reconsider tv=tseq as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by A0,Def17; BND03: for e be Real st e > 0 ex k be Nat st for n be Nat st n >= k holds ||.vseq.n - tv.|| <= e proof let e be Real such that ND15: e > 0; consider k be Nat such that ND16: for n be Nat st n >= k holds for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| by BND02,ND15; now let n be Nat such that ND18: n >= k; set f1=modetrans((vseq.n),X,Y); set g1=tseq; ND19: for x be VECTOR of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e* ||.x.|| by ND18,ND16; reconsider h1=vseq.n-tv as bounded LinearOperator of X,Y by A0,Def17; R41: now let t be VECTOR of X such that A41: ||.t.|| <= 1; vseq.n is bounded LinearOperator of X,Y by A0, Def17; then modetrans((vseq.n),X,Y)=vseq.n by LM58; then B1: ||.h1.t.||= ||.f1.t-g1.t.|| by LMB54M; B2: ||.f1.t-g1.t.|| <=e* ||.t.|| by ND19; e*||.t.|| <= e*1 by A41,AXIOMS:25,ND15; hence ||.h1.t.|| <=e by B1,B2,AXIOMS:22; end; R42: now let r be Real such that AS1: r in PreNorms(h1); AS2: r in {||.h1.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by Def22,AS1; consider t be VECTOR of X such that PS1: r=||.h1.t.|| & ||.t.|| <= 1 by AS2; thus r <=e by PS1,R41; end; AX5: (for s be real number st s in PreNorms(h1) holds s <= e) implies sup PreNorms(h1) <=e by PSCOMP_1:10; R43:sup PreNorms(h1) <=e by R42,AX5; BoundedLinearOperatorsNorm(X,Y).(vseq.n-tv) = sup PreNorms(h1) by LM59; hence ||.vseq.n-tv.|| <=e by A0,R43,NORMSP_1:def 1; end; hence thesis; end; for e be Real st e > 0 ex m be Nat st for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e proof let e be Real such that L1: e > 0; L2: e/2 > 0 by L1,SEQ_2:3; L3: e/2<e by L1,SEQ_2:4; consider m be Nat such that L4: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= e/2 by L2,BND03; now let n be Nat such that L5: n >= m; ||.(vseq.n) - tv.|| <= e/2 by L5,L4; hence ||.(vseq.n) - tv.|| < e by L3,AXIOMS:22; end; hence thesis; end; hence thesis by NORMSP_1:def 9; end; theorem LM64: for X be RealNormSpace for Y be RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators(X,Y) is RealBanachSpace proof let X be RealNormSpace; let Y be RealBanachSpace; for seq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y) st seq is Cauchy_sequence_by_Norm holds seq is convergent by LM63; hence thesis by Def40; end; definition let X be RealNormSpace; let Y be RealBanachSpace; cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> complete; coherence by LM64; end;

Back to top