:: C0SP1 semantic presentation
begin
definition
let V be non empty addLoopStr ;
let V1 be Subset of V;
attrV1 is having-inverse means :Def1: :: C0SP1:def 1
for v being Element of V st v in V1 holds
- v in V1;
end;
:: deftheorem Def1 defines having-inverse C0SP1:def_1_:_
for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is having-inverse iff for v being Element of V st v in V1 holds
- v in V1 );
definition
let V be non empty addLoopStr ;
let V1 be Subset of V;
attrV1 is additively-closed means :Def2: :: C0SP1:def 2
( V1 is add-closed & V1 is having-inverse );
end;
:: deftheorem Def2 defines additively-closed C0SP1:def_2_:_
for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is additively-closed iff ( V1 is add-closed & V1 is having-inverse ) );
Lm1: for V being non empty addLoopStr holds [#] V is add-closed
proof
let V be non empty addLoopStr ; ::_thesis: [#] V is add-closed
for v, u being Element of V st v in [#] V & u in [#] V holds
v + u in [#] V ;
hence [#] V is add-closed by IDEAL_1:def_1; ::_thesis: verum
end;
Lm2: for V being non empty addLoopStr holds [#] V is having-inverse
proof
let V be non empty addLoopStr ; ::_thesis: [#] V is having-inverse
for v being Element of V st v in [#] V holds
- v in [#] V ;
hence [#] V is having-inverse by Def1; ::_thesis: verum
end;
registration
let V be non empty addLoopStr ;
cluster [#] V -> add-closed having-inverse ;
correctness
coherence
( [#] V is add-closed & [#] V is having-inverse );
by Lm1, Lm2;
end;
registration
let V be non empty doubleLoopStr ;
cluster additively-closed -> add-closed having-inverse for Element of bool the carrier of V;
coherence
for b1 being Subset of V st b1 is additively-closed holds
( b1 is add-closed & b1 is having-inverse ) by Def2;
cluster add-closed having-inverse -> additively-closed for Element of bool the carrier of V;
coherence
for b1 being Subset of V st b1 is add-closed & b1 is having-inverse holds
b1 is additively-closed by Def2;
end;
registration
let V be non empty addLoopStr ;
cluster non empty add-closed having-inverse for Element of bool the carrier of V;
correctness
existence
ex b1 being Subset of V st
( b1 is add-closed & b1 is having-inverse & not b1 is empty );
proof
take [#] V ; ::_thesis: ( [#] V is add-closed & [#] V is having-inverse & not [#] V is empty )
thus ( [#] V is add-closed & [#] V is having-inverse & not [#] V is empty ) ; ::_thesis: verum
end;
end;
definition
let V be Ring;
mode Subring of V -> Ring means :Def3: :: C0SP1:def 3
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & 1. it = 1. V & 0. it = 0. V );
existence
ex b1 being Ring st
( the carrier of b1 c= the carrier of V & the addF of b1 = the addF of V || the carrier of b1 & the multF of b1 = the multF of V || the carrier of b1 & 1. b1 = 1. V & 0. b1 = 0. V )
proof
take V ; ::_thesis: ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & 1. V = 1. V & 0. V = 0. V )
thus ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & 1. V = 1. V & 0. V = 0. V ) by RELSET_1:19; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Subring C0SP1:def_3_:_
for V, b2 being Ring holds
( b2 is Subring of V iff ( the carrier of b2 c= the carrier of V & the addF of b2 = the addF of V || the carrier of b2 & the multF of b2 = the multF of V || the carrier of b2 & 1. b2 = 1. V & 0. b2 = 0. V ) );
theorem Th1: :: C0SP1:1
for X being non empty set
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
proof
let X be non empty set ; ::_thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let d1, d2 be Element of X; ::_thesis: for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let A be BinOp of X; ::_thesis: for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let M be Function of [:X,X:],X; ::_thesis: for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let V be Ring; ::_thesis: for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let V1 be Subset of V; ::_thesis: ( V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse implies doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V )
assume that
A1: V1 = X and
A2: A = the addF of V || V1 and
A3: M = the multF of V || V1 and
A4: d1 = 1. V and
A5: d2 = 0. V and
A6: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def_1 ::_thesis: doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
reconsider W = doubleLoopStr(# X,A,M,d1,d2 #) as non empty doubleLoopStr ;
A7: now__::_thesis:_for_a,_x_being_Element_of_W_holds_a_*_x_=_the_multF_of_V_._(a,x)
let a, x be Element of W; ::_thesis: a * x = the multF of V . (a,x)
a * x = the multF of V . [a,x] by A1, A3, FUNCT_1:49;
hence a * x = the multF of V . (a,x) ; ::_thesis: verum
end;
A8: now__::_thesis:_for_x,_y_being_Element_of_W_holds_x_+_y_=_the_addF_of_V_._(x,y)
let x, y be Element of W; ::_thesis: x + y = the addF of V . (x,y)
x + y = the addF of V . [x,y] by A1, A2, FUNCT_1:49;
hence x + y = the addF of V . (x,y) ; ::_thesis: verum
end;
A9: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
proof
set MV = the multF of V;
set Av = the addF of V;
hereby :: according to RLVECT_1:def_2 ::_thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
let x, y be Element of W; ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence x + y = y + x ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_3 ::_thesis: ( W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
let x, y, z be Element of W; ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def_3;
x + (y + z) = the addF of V . (x1,(y + z)) by A8;
then A10: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = the addF of V . ((x + y),z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A10, RLVECT_1:def_3; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_4 ::_thesis: ( W is right_complementable & W is associative & W is well-unital & W is distributive )
let x be Element of W; ::_thesis: x + (0. W) = x
reconsider y = x as Element of V by A1, TARSKI:def_3;
x + (0. W) = y + (0. V) by A5, A8;
hence x + (0. W) = x by RLVECT_1:4; ::_thesis: verum
end;
thus W is right_complementable ::_thesis: ( W is associative & W is well-unital & W is distributive )
proof
let x be Element of W; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
consider v being Element of V such that
A11: x1 + v = 0. V by ALGSTR_0:def_11;
v = - x1 by A11, VECTSP_1:16;
then reconsider y = v as Element of W by A1, A6;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. W
thus x + y = 0. W by A5, A8, A11; ::_thesis: verum
end;
hereby :: according to GROUP_1:def_3 ::_thesis: ( W is well-unital & W is distributive )
let a, b, x be Element of W; ::_thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of V by A1, TARSKI:def_3;
a * (b * x) = the multF of V . (a,(b * x)) by A7;
then A12: a * (b * x) = a1 * (b1 * y) by A7;
a * b = a1 * b1 by A7;
then (a * b) * x = (a1 * b1) * y by A7;
hence (a * b) * x = a * (b * x) by A12, GROUP_1:def_3; ::_thesis: verum
end;
hereby :: according to VECTSP_1:def_6 ::_thesis: W is distributive
let x be Element of W; ::_thesis: ( x * (1. W) = x & (1. W) * x = x )
reconsider y = x as Element of V by A1, TARSKI:def_3;
( x * (1. W) = y * (1. V) & (1. W) * x = (1. V) * y ) by A4, A7;
hence ( x * (1. W) = x & (1. W) * x = x ) by VECTSP_1:def_6; ::_thesis: verum
end;
hereby :: according to VECTSP_1:def_7 ::_thesis: verum
let a, x, y be Element of W; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) )
reconsider x1 = x, y1 = y, a1 = a as Element of V by A1, TARSKI:def_3;
(x + y) * a = the multF of V . ((x + y),a) by A7;
then (x + y) * a = (x1 + y1) * a1 by A8;
then (x + y) * a = (x1 * a1) + (y1 * a1) by VECTSP_1:def_7;
then (x + y) * a = the addF of V . (( the multF of V . (x1,a1)),(y * a)) by A7;
then A13: (x + y) * a = the addF of V . ((x * a),(y * a)) by A7;
a * (x + y) = the multF of V . (a,(x + y)) by A7;
then a * (x + y) = a1 * (x1 + y1) by A8;
then a * (x + y) = (a1 * x1) + (a1 * y1) by VECTSP_1:def_7;
then a * (x + y) = the addF of V . (( the multF of V . (a,x1)),(a * y)) by A7;
then a * (x + y) = the addF of V . ((a * x),(a * y)) by A7;
hence ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) ) by A8, A13; ::_thesis: verum
end;
end;
( 0. W = 0. V & 1. W = 1. V ) by A4, A5;
hence doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V by A1, A2, A3, A9, Def3; ::_thesis: verum
end;
registration
let V be Ring;
cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital for Subring of V;
existence
ex b1 being Subring of V st b1 is strict
proof
set V1 = [#] V;
( the addF of V = the addF of V || ([#] V) & the multF of V = the multF of V || ([#] V) ) by RELSET_1:19;
then doubleLoopStr(# the carrier of V, the addF of V, the multF of V,(1. V),(0. V) #) is Subring of V by Th1;
hence ex b1 being Subring of V st b1 is strict ; ::_thesis: verum
end;
end;
definition
let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
attrV1 is multiplicatively-closed means :Def4: :: C0SP1:def 4
( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) );
end;
:: deftheorem Def4 defines multiplicatively-closed C0SP1:def_4_:_
for V being non empty multLoopStr_0
for V1 being Subset of V holds
( V1 is multiplicatively-closed iff ( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) ) );
definition
let V be non empty addLoopStr ;
let V1 be Subset of V;
assume B1: ( V1 is add-closed & not V1 is empty ) ;
func Add_ (V1,V) -> BinOp of V1 equals :Def5: :: C0SP1:def 5
the addF of V || V1;
correctness
coherence
the addF of V || V1 is BinOp of V1;
proof
A1: dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1;
A2: for z being set st z in [:V1,V1:] holds
( the addF of V || V1) . z in V1
proof
let z be set ; ::_thesis: ( z in [:V1,V1:] implies ( the addF of V || V1) . z in V1 )
assume A3: z in [:V1,V1:] ; ::_thesis: ( the addF of V || V1) . z in V1
then consider r, x being set such that
A4: ( r in V1 & x in V1 ) and
A5: z = [r,x] by ZFMISC_1:def_2;
reconsider y = x, r1 = r as Element of V by A4;
[r,x] in dom ( the addF of V || V1) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then ( the addF of V || V1) . z = r1 + y by A5, FUNCT_1:47;
hence ( the addF of V || V1) . z in V1 by B1, A4, IDEAL_1:def_1; ::_thesis: verum
end;
dom ( the addF of V || V1) = [:V1,V1:] by A1, RELAT_1:62, ZFMISC_1:96;
hence the addF of V || V1 is BinOp of V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Add_ C0SP1:def_5_:_
for V being non empty addLoopStr
for V1 being Subset of V st V1 is add-closed & not V1 is empty holds
Add_ (V1,V) = the addF of V || V1;
definition
let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume B1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func mult_ (V1,V) -> BinOp of V1 equals :Def6: :: C0SP1:def 6
the multF of V || V1;
correctness
coherence
the multF of V || V1 is BinOp of V1;
proof
A1: dom the multF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1;
A2: for z being set st z in [:V1,V1:] holds
( the multF of V || V1) . z in V1
proof
let z be set ; ::_thesis: ( z in [:V1,V1:] implies ( the multF of V || V1) . z in V1 )
assume A3: z in [:V1,V1:] ; ::_thesis: ( the multF of V || V1) . z in V1
then consider r, x being set such that
A4: ( r in V1 & x in V1 ) and
A5: z = [r,x] by ZFMISC_1:def_2;
reconsider y = x, r1 = r as Element of V by A4;
[r,x] in dom ( the multF of V || V1) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then ( the multF of V || V1) . z = r1 * y by A5, FUNCT_1:47;
hence ( the multF of V || V1) . z in V1 by B1, A4, Def4; ::_thesis: verum
end;
dom ( the multF of V || V1) = [:V1,V1:] by A1, RELAT_1:62, ZFMISC_1:96;
hence the multF of V || V1 is BinOp of V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines mult_ C0SP1:def_6_:_
for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
mult_ (V1,V) = the multF of V || V1;
definition
let V be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V1 be Subset of V;
assume A1: ( V1 is add-closed & V1 is having-inverse & not V1 is empty ) ;
func Zero_ (V1,V) -> Element of V1 equals :Def7: :: C0SP1:def 7
0. V;
correctness
coherence
0. V is Element of V1;
proof
set x = the Element of V1;
reconsider x1 = the Element of V1 as Element of V by A1, TARSKI:def_3;
( - x1 in V1 & x1 + (- x1) = 0. V ) by A1, Def1, RLVECT_1:def_10;
hence 0. V is Element of V1 by A1, IDEAL_1:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines Zero_ C0SP1:def_7_:_
for V being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V1 being Subset of V st V1 is add-closed & V1 is having-inverse & not V1 is empty holds
Zero_ (V1,V) = 0. V;
definition
let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func One_ (V1,V) -> Element of V1 equals :Def8: :: C0SP1:def 8
1. V;
correctness
coherence
1. V is Element of V1;
by A1, Def4;
end;
:: deftheorem Def8 defines One_ C0SP1:def_8_:_
for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
One_ (V1,V) = 1. V;
theorem :: C0SP1:2
for V being Ring
for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds
doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring
proof
let V be Ring; ::_thesis: for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds
doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring
let V1 be Subset of V; ::_thesis: ( V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty implies doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring )
assume A1: ( V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty ) ; ::_thesis: doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring
then A2: ( One_ (V1,V) = 1_ V & mult_ (V1,V) = the multF of V || V1 ) by Def6, Def8;
( Zero_ (V1,V) = 0. V & Add_ (V1,V) = the addF of V || V1 ) by A1, Def5, Def7;
hence doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring by A1, A2, Th1; ::_thesis: verum
end;
begin
definition
let V be Algebra;
mode Subalgebra of V -> Algebra means :Def9: :: C0SP1:def 9
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );
existence
ex b1 being Algebra st
( the carrier of b1 c= the carrier of V & the addF of b1 = the addF of V || the carrier of b1 & the multF of b1 = the multF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:REAL, the carrier of b1:] & 1. b1 = 1. V & 0. b1 = 0. V )
proof
take V ; ::_thesis: ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] & 1. V = 1. V & 0. V = 0. V )
thus ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] & 1. V = 1. V & 0. V = 0. V ) by RELSET_1:19; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Subalgebra C0SP1:def_9_:_
for V, b2 being Algebra holds
( b2 is Subalgebra of V iff ( the carrier of b2 c= the carrier of V & the addF of b2 = the addF of V || the carrier of b2 & the multF of b2 = the multF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:REAL, the carrier of b2:] & 1. b2 = 1. V & 0. b2 = 0. V ) );
theorem Th3: :: C0SP1:3
for X being non empty set
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
proof
let X be non empty set ; ::_thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let d1, d2 be Element of X; ::_thesis: for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let A be BinOp of X; ::_thesis: for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let M be Function of [:X,X:],X; ::_thesis: for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let V be Algebra; ::_thesis: for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let V1 be Subset of V; ::_thesis: for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let MR be Function of [:REAL,X:],X; ::_thesis: ( V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V )
assume that
A1: V1 = X and
A2: d1 = 0. V and
A3: d2 = 1. V and
A4: A = the addF of V || V1 and
A5: M = the multF of V || V1 and
A6: MR = the Mult of V | [:REAL,V1:] and
A7: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def_1 ::_thesis: AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
reconsider W = AlgebraStr(# X,M,A,MR,d2,d1 #) as non empty AlgebraStr ;
A8: now__::_thesis:_for_x,_y_being_Element_of_W_holds_x_+_y_=_the_addF_of_V_._(x,y)
let x, y be Element of W; ::_thesis: x + y = the addF of V . (x,y)
x + y = the addF of V . [x,y] by A1, A4, FUNCT_1:49;
hence x + y = the addF of V . (x,y) ; ::_thesis: verum
end;
A9: now__::_thesis:_for_a,_x_being_VECTOR_of_W_holds_a_*_x_=_the_multF_of_V_._(a,x)
let a, x be VECTOR of W; ::_thesis: a * x = the multF of V . (a,x)
a * x = the multF of V . [a,x] by A1, A5, FUNCT_1:49;
hence a * x = the multF of V . (a,x) ; ::_thesis: verum
end;
A10: now__::_thesis:_for_a_being_Real
for_x_being_VECTOR_of_W_holds_a_*_x_=_the_Mult_of_V_._(a,x)
let a be Real; ::_thesis: for x being VECTOR of W holds a * x = the Mult of V . (a,x)
let x be VECTOR of W; ::_thesis: a * x = the Mult of V . (a,x)
a * x = the Mult of V . [a,x] by A1, A6, FUNCT_1:49;
hence a * x = the Mult of V . (a,x) ; ::_thesis: verum
end;
A11: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
set Mv = the multF of V;
set Av = the addF of V;
hereby :: according to RLVECT_1:def_2 ::_thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x, y be VECTOR of W; ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3;
( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence x + y = y + x ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_3 ::_thesis: ( W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x, y, z be VECTOR of W; ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def_3;
x + (y + z) = the addF of V . (x1,(y + z)) by A8;
then A12: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = the addF of V . ((x + y),z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A12, RLVECT_1:def_3; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_4 ::_thesis: ( W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x be VECTOR of W; ::_thesis: x + (0. W) = x
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
thus x + (0. W) = y + (0. V) by A2, A8
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
thus W is right_complementable ::_thesis: ( W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
let x be Element of W; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
consider v being Element of V such that
A13: x1 + v = 0. V by ALGSTR_0:def_11;
v = - x1 by A13, VECTSP_1:16;
then reconsider y = v as Element of W by A1, A7;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. W
thus x + y = 0. W by A2, A8, A13; ::_thesis: verum
end;
hereby :: according to GROUP_1:def_12 ::_thesis: ( W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let v, w be Element of W; ::_thesis: v * w = w * v
reconsider v1 = v, w1 = w as Element of V by A1, TARSKI:def_3;
( v * w = v1 * w1 & w * v = w1 * v1 ) by A9;
hence v * w = w * v ; ::_thesis: verum
end;
hereby :: according to GROUP_1:def_3 ::_thesis: ( W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let a, b, x be Element of W; ::_thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of V by A1, TARSKI:def_3;
a * (b * x) = the multF of V . (a,(b * x)) by A9;
then A14: a * (b * x) = a1 * (b1 * y) by A9;
a * b = a1 * b1 by A9;
then (a * b) * x = (a1 * b1) * y by A9;
hence (a * b) * x = a * (b * x) by A14, GROUP_1:def_3; ::_thesis: verum
end;
hereby :: according to VECTSP_1:def_4 ::_thesis: ( W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let v be Element of W; ::_thesis: v * (1. W) = v
reconsider v1 = v as Element of V by A1, TARSKI:def_3;
v * (1. W) = v1 * (1. V) by A3, A9;
hence v * (1. W) = v by VECTSP_1:def_4; ::_thesis: verum
end;
hereby :: according to VECTSP_1:def_2 ::_thesis: ( W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x, y, z be Element of W; ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def_3;
y + z = y1 + z1 by A8;
then x * (y + z) = x1 * (y1 + z1) by A9;
then A15: x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def_2;
( x * y = x1 * y1 & x * z = x1 * z1 ) by A9;
hence x * (y + z) = (x * y) + (x * z) by A8, A15; ::_thesis: verum
end;
thus W is vector-distributive ::_thesis: ( W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of W holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of W; ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
reconsider aa = a as Real by XREAL_0:def_1;
A16: aa * x = aa * x1 by A10;
x + y = x1 + y1 by A8;
then aa * (x + y) = aa * (x1 + y1) by A10;
then A17: a * (x + y) = (a * x1) + (a * y1) by RLVECT_1:def_5;
aa * y = aa * y1 by A10;
hence a * (x + y) = (a * x) + (a * y) by A8, A16, A17; ::_thesis: verum
end;
thus W is scalar-distributive ::_thesis: ( W is scalar-associative & W is vector-associative )
proof
let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of W holds (a + b) * b1 = (a * b1) + (b * b1)
reconsider aa = a, bb = b as Real by XREAL_0:def_1;
let x be Element of W; ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
A18: aa * x = aa * x1 by A10;
A19: bb * x = bb * x1 by A10;
(aa + bb) * x = (a + b) * x1 by A10;
then (a + b) * x = (a * x1) + (b * x1) by RLVECT_1:def_6;
hence (a + b) * x = (a * x) + (b * x) by A8, A18, A19; ::_thesis: verum
end;
thus W is scalar-associative ::_thesis: W is vector-associative
proof
let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of W holds (a * b) * b1 = a * (b * b1)
let x be Element of W; ::_thesis: (a * b) * x = a * (b * x)
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
reconsider aa = a, bb = b as Real by XREAL_0:def_1;
A20: bb * x = bb * x1 by A10;
(aa * bb) * x = (a * b) * x1 by A10;
then (aa * bb) * x = a * (bb * x1) by RLVECT_1:def_7;
hence (a * b) * x = a * (b * x) by A10, A20; ::_thesis: verum
end;
thus W is vector-associative ::_thesis: verum
proof
let x, y be Element of W; :: according to FUNCSDOM:def_9 ::_thesis: for b1 being Element of REAL holds b1 * (x * y) = (b1 * x) * y
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
A21: a * x = a * x1 by A10;
x * y = x1 * y1 by A9;
then a * (x * y) = a * (x1 * y1) by A10;
then a * (x * y) = (a * x1) * y1 by FUNCSDOM:def_9;
hence a * (x * y) = (a * x) * y by A9, A21; ::_thesis: verum
end;
end;
( 0. W = 0. V & 1. W = 1. V ) by A2, A3;
hence AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V by A1, A4, A5, A6, A11, Def9; ::_thesis: verum
end;
registration
let V be Algebra;
cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital for Subalgebra of V;
existence
ex b1 being Subalgebra of V st b1 is strict
proof
set V1 = [#] V;
A1: the Mult of V = the Mult of V | [:REAL,([#] V):] by RELSET_1:19;
( the addF of V = the addF of V || ([#] V) & the multF of V = the multF of V || ([#] V) ) by RELSET_1:19;
then AlgebraStr(# the carrier of V, the multF of V, the addF of V, the Mult of V,(1. V),(0. V) #) is Subalgebra of V by A1, Th3;
hence ex b1 being Subalgebra of V st b1 is strict ; ::_thesis: verum
end;
end;
definition
let V be Algebra;
let V1 be Subset of V;
attrV1 is additively-linearly-closed means :Def10: :: C0SP1:def 10
( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) );
end;
:: deftheorem Def10 defines additively-linearly-closed C0SP1:def_10_:_
for V being Algebra
for V1 being Subset of V holds
( V1 is additively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) ) );
registration
let V be Algebra;
cluster additively-linearly-closed -> additively-closed for Element of bool the carrier of V;
coherence
for b1 being Subset of V st b1 is additively-linearly-closed holds
b1 is additively-closed
proof
now__::_thesis:_for_V1_being_Subset_of_V_st_V1_is_additively-linearly-closed_holds_
V1_is_additively-closed
let V1 be Subset of V; ::_thesis: ( V1 is additively-linearly-closed implies V1 is additively-closed )
assume V1 is additively-linearly-closed ; ::_thesis: V1 is additively-closed
then ( V1 is add-closed & V1 is having-inverse ) by Def10;
hence V1 is additively-closed ; ::_thesis: verum
end;
hence for b1 being Subset of V st b1 is additively-linearly-closed holds
b1 is additively-closed ; ::_thesis: verum
end;
end;
definition
let V be Algebra;
let V1 be Subset of V;
assume B1: ( V1 is additively-linearly-closed & not V1 is empty ) ;
func Mult_ (V1,V) -> Function of [:REAL,V1:],V1 equals :Def11: :: C0SP1:def 11
the Mult of V | [:REAL,V1:];
correctness
coherence
the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1;
proof
A1: ( [:REAL,V1:] c= [:REAL, the carrier of V:] & dom the Mult of V = [:REAL, the carrier of V:] ) by FUNCT_2:def_1, ZFMISC_1:95;
A2: for z being set st z in [:REAL,V1:] holds
( the Mult of V | [:REAL,V1:]) . z in V1
proof
let z be set ; ::_thesis: ( z in [:REAL,V1:] implies ( the Mult of V | [:REAL,V1:]) . z in V1 )
assume A3: z in [:REAL,V1:] ; ::_thesis: ( the Mult of V | [:REAL,V1:]) . z in V1
consider r, x being set such that
A4: r in REAL and
A5: x in V1 and
A6: z = [r,x] by A3, ZFMISC_1:def_2;
reconsider r = r as Real by A4;
reconsider y = x as VECTOR of V by A5;
[r,x] in dom ( the Mult of V | [:REAL,V1:]) by A1, A3, A6, RELAT_1:62;
then ( the Mult of V | [:REAL,V1:]) . z = r * y by A6, FUNCT_1:47;
hence ( the Mult of V | [:REAL,V1:]) . z in V1 by B1, A5, Def10; ::_thesis: verum
end;
dom ( the Mult of V | [:REAL,V1:]) = [:REAL,V1:] by A1, RELAT_1:62;
hence the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines Mult_ C0SP1:def_11_:_
for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & not V1 is empty holds
Mult_ (V1,V) = the Mult of V | [:REAL,V1:];
definition
let V be non empty RLSStruct ;
attrV is scalar-mult-cancelable means :Def12: :: C0SP1:def 12
for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );
end;
:: deftheorem Def12 defines scalar-mult-cancelable C0SP1:def_12_:_
for V being non empty RLSStruct holds
( V is scalar-mult-cancelable iff for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V ) );
theorem Th4: :: C0SP1:4
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr
for a being Real holds a * (0. V) = 0. V
proof
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ; ::_thesis: for a being Real holds a * (0. V) = 0. V
let a be Real; ::_thesis: a * (0. V) = 0. V
(a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by RLVECT_1:def_5;
then (a * (0. V)) + (a * (0. V)) = a * (0. V) by RLVECT_1:4;
then (a * (0. V)) + (a * (0. V)) = (a * (0. V)) + (0. V) by RLVECT_1:4;
hence a * (0. V) = 0. V by RLVECT_1:8; ::_thesis: verum
end;
theorem :: C0SP1:5
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st V is scalar-mult-cancelable holds
V is RealLinearSpace
proof
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ; ::_thesis: ( V is scalar-mult-cancelable implies V is RealLinearSpace )
assume A1: V is scalar-mult-cancelable ; ::_thesis: V is RealLinearSpace
for v being VECTOR of V holds 1 * v = v
proof
let v be VECTOR of V; ::_thesis: 1 * v = v
(1 * v) + (1 * (- v)) = 1 * (v + (- v)) by RLVECT_1:def_5;
then ( (1 * v) - (1 * v) = 0. V & (1 * v) + (1 * (- v)) = 1 * (0. V) ) by RLVECT_1:5;
then A2: - (1 * v) = 1 * (- v) by Th4, RLVECT_1:8;
1 * v = (1 * 1) * v
.= 1 * (1 * v) by RLVECT_1:def_7 ;
then (1 * (1 * v)) - (1 * v) = 0. V by RLVECT_1:15;
then 1 * ((1 * v) - v) = 0. V by A2, RLVECT_1:def_5;
then (1 * v) - v = 0. V by A1, Def12;
hence 1 * v = v by RLVECT_1:21; ::_thesis: verum
end;
hence V is RealLinearSpace by RLVECT_1:def_8; ::_thesis: verum
end;
Lm3: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace
by RLVECT_1:def_8;
theorem Th6: :: C0SP1:6
for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds
AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V
proof
let V be Algebra; ::_thesis: for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds
AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V
let V1 be Subset of V; ::_thesis: ( V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty implies AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V )
assume A1: ( V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty ) ; ::_thesis: AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V
then A2: Mult_ (V1,V) = the Mult of V | [:REAL,V1:] by Def11;
A3: ( One_ (V1,V) = 1_ V & mult_ (V1,V) = the multF of V || V1 ) by A1, Def6, Def8;
( Zero_ (V1,V) = 0. V & Add_ (V1,V) = the addF of V || V1 ) by A1, Def5, Def7;
hence AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V by A1, A3, A2, Th3; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster RAlgebra X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative commutative right-distributive right_unital ;
correctness
coherence
( RAlgebra X is Abelian & RAlgebra X is add-associative & RAlgebra X is right_zeroed & RAlgebra X is right_complementable & RAlgebra X is commutative & RAlgebra X is associative & RAlgebra X is right_unital & RAlgebra X is right-distributive & RAlgebra X is vector-distributive & RAlgebra X is scalar-distributive & RAlgebra X is scalar-associative & RAlgebra X is vector-associative );
;
end;
theorem Th7: :: C0SP1:7
for X being non empty set holds RAlgebra X is RealLinearSpace
proof
let X be non empty set ; ::_thesis: RAlgebra X is RealLinearSpace
for v being VECTOR of (RAlgebra X) holds 1 * v = v by FUNCSDOM:12;
hence RAlgebra X is RealLinearSpace by Lm3; ::_thesis: verum
end;
theorem Th8: :: C0SP1:8
for V being Algebra
for V1 being Subalgebra of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
proof
let V be Algebra; ::_thesis: for V1 being Subalgebra of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let V1 be Subalgebra of V; ::_thesis: ( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
hereby ::_thesis: ( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let x1, y1 be Element of V1; ::_thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 + y1 = x + y
let x, y be Element of V; ::_thesis: ( x1 = x & y1 = y implies x1 + y1 = x + y )
assume A1: ( x1 = x & y1 = y ) ; ::_thesis: x1 + y1 = x + y
x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by Def9;
hence x1 + y1 = x + y by A1, FUNCT_1:49; ::_thesis: verum
end;
hereby ::_thesis: ( ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let x1, y1 be Element of V1; ::_thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 * y1 = x * y
let x, y be Element of V; ::_thesis: ( x1 = x & y1 = y implies x1 * y1 = x * y )
assume A2: ( x1 = x & y1 = y ) ; ::_thesis: x1 * y1 = x * y
x1 * y1 = ( the multF of V || the carrier of V1) . [x1,y1] by Def9;
hence x1 * y1 = x * y by A2, FUNCT_1:49; ::_thesis: verum
end;
hereby ::_thesis: ( 1_ V1 = 1_ V & 0. V1 = 0. V )
let v1 be Element of V1; ::_thesis: for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v
let v be Element of V; ::_thesis: for a being Real st v1 = v holds
a * v1 = a * v
let a be Real; ::_thesis: ( v1 = v implies a * v1 = a * v )
assume A3: v1 = v ; ::_thesis: a * v1 = a * v
a * v1 = ( the Mult of V | [:REAL, the carrier of V1:]) . [a,v1] by Def9;
hence a * v1 = a * v by A3, FUNCT_1:49; ::_thesis: verum
end;
thus ( 1_ V1 = 1_ V & 0. V1 = 0. V ) by Def9; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
func BoundedFunctions X -> non empty Subset of (RAlgebra X) equals :: C0SP1:def 13
{ f where f is Function of X,REAL : f | X is bounded } ;
correctness
coherence
{ f where f is Function of X,REAL : f | X is bounded } is non empty Subset of (RAlgebra X);
proof
A1: not { f where f is Function of X,REAL : f | X is bounded } is empty
proof
reconsider g = X --> 0 as Function of X,REAL by FUNCOP_1:46;
g | X is bounded ;
then g in { f where f is Function of X,REAL : f | X is bounded } ;
hence not { f where f is Function of X,REAL : f | X is bounded } is empty ; ::_thesis: verum
end;
{ f where f is Function of X,REAL : f | X is bounded } c= Funcs (X,REAL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Function of X,REAL : f | X is bounded } or x in Funcs (X,REAL) )
assume x in { f where f is Function of X,REAL : f | X is bounded } ; ::_thesis: x in Funcs (X,REAL)
then ex f being Function of X,REAL st
( x = f & f | X is bounded ) ;
hence x in Funcs (X,REAL) by FUNCT_2:8; ::_thesis: verum
end;
hence { f where f is Function of X,REAL : f | X is bounded } is non empty Subset of (RAlgebra X) by A1; ::_thesis: verum
end;
end;
:: deftheorem defines BoundedFunctions C0SP1:def_13_:_
for X being non empty set holds BoundedFunctions X = { f where f is Function of X,REAL : f | X is bounded } ;
theorem Th9: :: C0SP1:9
for X being non empty set holds
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )
proof
let X be non empty set ; ::_thesis: ( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )
set W = BoundedFunctions X;
set V = RAlgebra X;
A1: for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v * u in BoundedFunctions X
proof
let v, u be Element of (RAlgebra X); ::_thesis: ( v in BoundedFunctions X & u in BoundedFunctions X implies v * u in BoundedFunctions X )
assume that
A2: v in BoundedFunctions X and
A3: u in BoundedFunctions X ; ::_thesis: v * u in BoundedFunctions X
consider u1 being Function of X,REAL such that
A4: u1 = u and
A5: u1 | X is bounded by A3;
reconsider h = v * u as Element of Funcs (X,REAL) ;
consider v1 being Function of X,REAL such that
A6: v1 = v and
A7: v1 | X is bounded by A2;
dom (v1 (#) u1) = X /\ X by FUNCT_2:def_1;
then A8: (v1 (#) u1) | X is bounded by A7, A5, RFUNCT_1:84;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def_1;
then A9: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & (dom v1) /\ (dom u1) = X /\ X ) by FUNCT_2:def_1, FUNCT_2:def_2;
for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A6, A4, FUNCSDOM:2;
then v * u = v1 (#) u1 by A9, VALUED_1:def_4;
hence v * u in BoundedFunctions X by A8; ::_thesis: verum
end;
reconsider g = RealFuncUnit X as Function of X,REAL ;
for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v + u in BoundedFunctions X
proof
let v, u be Element of (RAlgebra X); ::_thesis: ( v in BoundedFunctions X & u in BoundedFunctions X implies v + u in BoundedFunctions X )
assume that
A10: v in BoundedFunctions X and
A11: u in BoundedFunctions X ; ::_thesis: v + u in BoundedFunctions X
consider u1 being Function of X,REAL such that
A12: u1 = u and
A13: u1 | X is bounded by A11;
reconsider h = v + u as Element of Funcs (X,REAL) ;
consider v1 being Function of X,REAL such that
A14: v1 = v and
A15: v1 | X is bounded by A10;
dom (v1 + u1) = X /\ X by FUNCT_2:def_1;
then A16: (v1 + u1) | X is bounded by A15, A13, RFUNCT_1:83;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def_1;
then A17: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & (dom v1) /\ (dom u1) = X /\ X ) by FUNCT_2:def_1, FUNCT_2:def_2;
for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A14, A12, FUNCSDOM:1;
then v + u = v1 + u1 by A17, VALUED_1:def_1;
hence v + u in BoundedFunctions X by A16; ::_thesis: verum
end;
then A18: BoundedFunctions X is add-closed by IDEAL_1:def_1;
A19: RAlgebra X is RealLinearSpace by Th7;
for v being Element of (RAlgebra X) st v in BoundedFunctions X holds
- v in BoundedFunctions X
proof
let v be Element of (RAlgebra X); ::_thesis: ( v in BoundedFunctions X implies - v in BoundedFunctions X )
assume v in BoundedFunctions X ; ::_thesis: - v in BoundedFunctions X
then consider v1 being Function of X,REAL such that
A20: v1 = v and
A21: v1 | X is bounded ;
A22: (- v1) | X is bounded by A21, RFUNCT_1:82;
reconsider h = - v, v2 = v as Element of Funcs (X,REAL) ;
A23: h = (- 1) * v by A19, RLVECT_1:16;
A24: now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_-_(v1_._x)
let x be set ; ::_thesis: ( x in dom h implies h . x = - (v1 . x) )
assume x in dom h ; ::_thesis: h . x = - (v1 . x)
then reconsider y = x as Element of X ;
h . x = (- 1) * (v2 . y) by A23, FUNCSDOM:4;
hence h . x = - (v1 . x) by A20; ::_thesis: verum
end;
( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & dom v1 = X ) by FUNCT_2:def_1, FUNCT_2:def_2;
then - v = - v1 by A24, VALUED_1:9;
hence - v in BoundedFunctions X by A22; ::_thesis: verum
end;
then A25: BoundedFunctions X is having-inverse by Def1;
for a being Real
for u being Element of (RAlgebra X) st u in BoundedFunctions X holds
a * u in BoundedFunctions X
proof
let a be Real; ::_thesis: for u being Element of (RAlgebra X) st u in BoundedFunctions X holds
a * u in BoundedFunctions X
let u be Element of (RAlgebra X); ::_thesis: ( u in BoundedFunctions X implies a * u in BoundedFunctions X )
assume u in BoundedFunctions X ; ::_thesis: a * u in BoundedFunctions X
then consider u1 being Function of X,REAL such that
A26: u1 = u and
A27: u1 | X is bounded ;
A28: (a (#) u1) | X is bounded by A27, RFUNCT_1:80;
reconsider h = a * u as Element of Funcs (X,REAL) ;
A29: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & dom u1 = X ) by FUNCT_2:def_1, FUNCT_2:def_2;
for x being set st x in dom h holds
h . x = a * (u1 . x) by A26, FUNCSDOM:4;
then a * u = a (#) u1 by A29, VALUED_1:def_5;
hence a * u in BoundedFunctions X by A28; ::_thesis: verum
end;
hence BoundedFunctions X is additively-linearly-closed by A18, A25, Def10; ::_thesis: BoundedFunctions X is multiplicatively-closed
g | X is bounded ;
then 1. (RAlgebra X) in BoundedFunctions X ;
hence BoundedFunctions X is multiplicatively-closed by A1, Def4; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster BoundedFunctions X -> non empty multiplicatively-closed additively-linearly-closed ;
coherence
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed ) by Th9;
end;
definition
let X be non empty set ;
func R_Algebra_of_BoundedFunctions X -> Algebra equals :: C0SP1:def 14
AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);
coherence
AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #) is Algebra by Th6;
end;
:: deftheorem defines R_Algebra_of_BoundedFunctions C0SP1:def_14_:_
for X being non empty set holds R_Algebra_of_BoundedFunctions X = AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);
theorem :: C0SP1:10
for X being non empty set holds R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
theorem :: C0SP1:11
for X being non empty set holds R_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
let X be non empty set ; ::_thesis: R_Algebra_of_BoundedFunctions X is RealLinearSpace
now__::_thesis:_for_v_being_VECTOR_of_(R_Algebra_of_BoundedFunctions_X)_holds_1_*_v_=_v
let v be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: 1 * v = v
reconsider v1 = v as VECTOR of (RAlgebra X) by TARSKI:def_3;
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
then 1 * v = 1 * v1 by Th8;
hence 1 * v = v by FUNCSDOM:12; ::_thesis: verum
end;
hence R_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm3; ::_thesis: verum
end;
theorem Th12: :: C0SP1:12
for X being non empty set
for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof
let X be non empty set ; ::_thesis: for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
let F, G, H be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
let f, g, h be Function of X,REAL; ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (RAlgebra X) by TARSKI:def_3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby ::_thesis: ( ( for x being Element of X holds h . x = (f . x) + (g . x) ) implies H = F + G )
assume A3: H = F + G ; ::_thesis: for x being Element of X holds h . x = (f . x) + (g . x)
let x be Element of X; ::_thesis: h . x = (f . x) + (g . x)
h1 = f1 + g1 by A2, A3, Th8;
hence h . x = (f . x) + (g . x) by A1, FUNCSDOM:1; ::_thesis: verum
end;
assume for x being Element of X holds h . x = (f . x) + (g . x) ; ::_thesis: H = F + G
then h1 = f1 + g1 by A1, FUNCSDOM:1;
hence H = F + G by A2, Th8; ::_thesis: verum
end;
theorem Th13: :: C0SP1:13
for X being non empty set
for a being Real
for F, G being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g being Function of X,REAL st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof
let X be non empty set ; ::_thesis: for a being Real
for F, G being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g being Function of X,REAL st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let a be Real; ::_thesis: for F, G being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g being Function of X,REAL st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let F, G be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: for f, g being Function of X,REAL st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let f, g be Function of X,REAL; ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) )
assume A1: ( f = F & g = G ) ; ::_thesis: ( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
reconsider f1 = F, g1 = G as VECTOR of (RAlgebra X) by TARSKI:def_3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby ::_thesis: ( ( for x being Element of X holds g . x = a * (f . x) ) implies G = a * F )
assume A3: G = a * F ; ::_thesis: for x being Element of X holds g . x = a * (f . x)
let x be Element of X; ::_thesis: g . x = a * (f . x)
g1 = a * f1 by A2, A3, Th8;
hence g . x = a * (f . x) by A1, FUNCSDOM:4; ::_thesis: verum
end;
assume for x being Element of X holds g . x = a * (f . x) ; ::_thesis: G = a * F
then g1 = a * f1 by A1, FUNCSDOM:4;
hence G = a * F by A2, Th8; ::_thesis: verum
end;
theorem Th14: :: C0SP1:14
for X being non empty set
for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
proof
let X be non empty set ; ::_thesis: for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
let F, G, H be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
let f, g, h be Function of X,REAL; ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (RAlgebra X) by TARSKI:def_3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby ::_thesis: ( ( for x being Element of X holds h . x = (f . x) * (g . x) ) implies H = F * G )
assume A3: H = F * G ; ::_thesis: for x being Element of X holds h . x = (f . x) * (g . x)
let x be Element of X; ::_thesis: h . x = (f . x) * (g . x)
h1 = f1 * g1 by A2, A3, Th8;
hence h . x = (f . x) * (g . x) by A1, FUNCSDOM:2; ::_thesis: verum
end;
assume for x being Element of X holds h . x = (f . x) * (g . x) ; ::_thesis: H = F * G
then h1 = f1 * g1 by A1, FUNCSDOM:2;
hence H = F * G by A2, Th8; ::_thesis: verum
end;
theorem Th15: :: C0SP1:15
for X being non empty set holds 0. (R_Algebra_of_BoundedFunctions X) = X --> 0
proof
let X be non empty set ; ::_thesis: 0. (R_Algebra_of_BoundedFunctions X) = X --> 0
( R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 0. (RAlgebra X) = X --> 0 ) by Th6;
hence 0. (R_Algebra_of_BoundedFunctions X) = X --> 0 by Th8; ::_thesis: verum
end;
theorem Th16: :: C0SP1:16
for X being non empty set holds 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1
proof
let X be non empty set ; ::_thesis: 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1
( R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 1_ (RAlgebra X) = X --> 1 ) by Th6;
hence 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1 by Th8; ::_thesis: verum
end;
definition
let X be non empty set ;
let F be set ;
assume A1: F in BoundedFunctions X ;
func modetrans (F,X) -> Function of X,REAL means :Def15: :: C0SP1:def 15
( it = F & it | X is bounded );
correctness
existence
ex b1 being Function of X,REAL st
( b1 = F & b1 | X is bounded );
uniqueness
for b1, b2 being Function of X,REAL st b1 = F & b1 | X is bounded & b2 = F & b2 | X is bounded holds
b1 = b2;
by A1;
end;
:: deftheorem Def15 defines modetrans C0SP1:def_15_:_
for X being non empty set
for F being set st F in BoundedFunctions X holds
for b3 being Function of X,REAL holds
( b3 = modetrans (F,X) iff ( b3 = F & b3 | X is bounded ) );
definition
let X be non empty set ;
let f be Function of X,REAL;
func PreNorms f -> non empty Subset of REAL equals :: C0SP1:def 16
{ (abs (f . x)) where x is Element of X : verum } ;
coherence
{ (abs (f . x)) where x is Element of X : verum } is non empty Subset of REAL
proof
set z = the Element of X;
A1: now__::_thesis:_for_z_being_set_st_z_in__{__(abs_(f_._x))_where_x_is_Element_of_X_:_verum__}__holds_
z_in_REAL
let z be set ; ::_thesis: ( z in { (abs (f . x)) where x is Element of X : verum } implies z in REAL )
now__::_thesis:_(_z_in__{__(abs_(f_._x))_where_x_is_Element_of_X_:_verum__}__implies_z_in_REAL_)
assume z in { (abs (f . x)) where x is Element of X : verum } ; ::_thesis: z in REAL
then ex x being Element of X st z = abs (f . x) ;
hence z in REAL ; ::_thesis: verum
end;
hence ( z in { (abs (f . x)) where x is Element of X : verum } implies z in REAL ) ; ::_thesis: verum
end;
abs (f . the Element of X) in { (abs (f . x)) where x is Element of X : verum } ;
hence { (abs (f . x)) where x is Element of X : verum } is non empty Subset of REAL by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines PreNorms C0SP1:def_16_:_
for X being non empty set
for f being Function of X,REAL holds PreNorms f = { (abs (f . x)) where x is Element of X : verum } ;
theorem Th17: :: C0SP1:17
for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
PreNorms f is bounded_above
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f | X is bounded holds
PreNorms f is bounded_above
let f be Function of X,REAL; ::_thesis: ( f | X is bounded implies PreNorms f is bounded_above )
assume f | X is bounded ; ::_thesis: PreNorms f is bounded_above
then consider K being real number such that
A1: for x being set st x in X /\ (dom f) holds
abs (f . x) <= K by RFUNCT_1:73;
A2: X /\ (dom f) = X /\ X by FUNCT_2:def_1;
take K ; :: according to XXREAL_2:def_10 ::_thesis: K is UpperBound of PreNorms f
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in PreNorms f or r <= K )
assume r in PreNorms f ; ::_thesis: r <= K
then ex t being Element of X st r = abs (f . t) ;
hence r <= K by A1, A2; ::_thesis: verum
end;
theorem :: C0SP1:18
for X being non empty set
for f being Function of X,REAL holds
( f | X is bounded iff PreNorms f is bounded_above )
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL holds
( f | X is bounded iff PreNorms f is bounded_above )
let f be Function of X,REAL; ::_thesis: ( f | X is bounded iff PreNorms f is bounded_above )
now__::_thesis:_(_PreNorms_f_is_bounded_above_implies_ex_K_being_Real_st_f_|_X_is_bounded_)
reconsider K = upper_bound (PreNorms f) as Real ;
assume A1: PreNorms f is bounded_above ; ::_thesis: ex K being Real st f | X is bounded
take K = K; ::_thesis: f | X is bounded
now__::_thesis:_for_t_being_set_st_t_in_X_/\_(dom_f)_holds_
abs_(f_._t)_<=_K
let t be set ; ::_thesis: ( t in X /\ (dom f) implies abs (f . t) <= K )
assume t in X /\ (dom f) ; ::_thesis: abs (f . t) <= K
then abs (f . t) in PreNorms f ;
hence abs (f . t) <= K by A1, SEQ_4:def_1; ::_thesis: verum
end;
hence f | X is bounded by RFUNCT_1:73; ::_thesis: verum
end;
hence ( f | X is bounded iff PreNorms f is bounded_above ) by Th17; ::_thesis: verum
end;
definition
let X be non empty set ;
func BoundedFunctionsNorm X -> Function of (BoundedFunctions X),REAL means :Def17: :: C0SP1:def 17
for x being set st x in BoundedFunctions X holds
it . x = upper_bound (PreNorms (modetrans (x,X)));
existence
ex b1 being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X)))
proof
deffunc H1( set ) -> Element of REAL = upper_bound (PreNorms (modetrans ($1,X)));
A1: for z being set st z in BoundedFunctions X holds
H1(z) in REAL ;
ex f being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (BoundedFunctions X),REAL st ( for x being set st x in BoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in BoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (BoundedFunctions X),REAL; ::_thesis: ( ( for x being set st x in BoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in BoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in BoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) and
A3: for x being set st x in BoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in BoundedFunctions X holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in BoundedFunctions X implies NORM1 . z = NORM2 . z )
assume A5: z in BoundedFunctions X ; ::_thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (PreNorms (modetrans (z,X))) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
( dom NORM1 = BoundedFunctions X & dom NORM2 = BoundedFunctions X ) by FUNCT_2:def_1;
hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def_17_:_
for X being non empty set
for b2 being Function of (BoundedFunctions X),REAL holds
( b2 = BoundedFunctionsNorm X iff for x being set st x in BoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) );
theorem Th19: :: C0SP1:19
for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
modetrans (f,X) = f
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f | X is bounded holds
modetrans (f,X) = f
let f be Function of X,REAL; ::_thesis: ( f | X is bounded implies modetrans (f,X) = f )
assume f | X is bounded ; ::_thesis: modetrans (f,X) = f
then f in BoundedFunctions X ;
hence modetrans (f,X) = f by Def15; ::_thesis: verum
end;
theorem Th20: :: C0SP1:20
for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
let f be Function of X,REAL; ::_thesis: ( f | X is bounded implies (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f) )
reconsider f9 = f as set ;
assume A1: f | X is bounded ; ::_thesis: (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
then f in BoundedFunctions X ;
then (BoundedFunctionsNorm X) . f = upper_bound (PreNorms (modetrans (f9,X))) by Def17;
hence (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f) by A1, Th19; ::_thesis: verum
end;
definition
let X be non empty set ;
func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals :: C0SP1:def 18
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);
correctness
coherence
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #) is Normed_AlgebraStr ;
;
end;
:: deftheorem defines R_Normed_Algebra_of_BoundedFunctions C0SP1:def_18_:_
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X = Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);
registration
let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> non empty ;
correctness
coherence
not R_Normed_Algebra_of_BoundedFunctions X is empty ;
;
end;
Lm4: now__::_thesis:_for_X_being_non_empty_set_
for_x,_e_being_Element_of_(R_Normed_Algebra_of_BoundedFunctions_X)_st_e_=_One__((BoundedFunctions_X),(RAlgebra_X))_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be non empty set ; ::_thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds
( x * e = x & e * x = x )
set F = R_Normed_Algebra_of_BoundedFunctions X;
let x, e be Element of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( e = One_ ((BoundedFunctions X),(RAlgebra X)) implies ( x * e = x & e * x = x ) )
set X1 = BoundedFunctions X;
reconsider f = x as Element of BoundedFunctions X ;
assume A1: e = One_ ((BoundedFunctions X),(RAlgebra X)) ; ::_thesis: ( x * e = x & e * x = x )
then x * e = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (f,(1_ (RAlgebra X))) by Def8;
then A2: x * e = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (f,(1_ (RAlgebra X))) by Def6;
e * x = (mult_ ((BoundedFunctions X),(RAlgebra X))) . ((1_ (RAlgebra X)),f) by A1, Def8;
then A3: e * x = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . ((1_ (RAlgebra X)),f) by Def6;
A4: 1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X) by Th16;
then [f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] by ZFMISC_1:87;
then x * e = f * (1_ (RAlgebra X)) by A2, FUNCT_1:49;
hence x * e = x by VECTSP_1:def_4; ::_thesis: e * x = x
[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] by A4, ZFMISC_1:87;
then e * x = (1_ (RAlgebra X)) * f by A3, FUNCT_1:49;
hence e * x = x by VECTSP_1:def_4; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> unital ;
correctness
coherence
R_Normed_Algebra_of_BoundedFunctions X is unital ;
proof
reconsider e = One_ ((BoundedFunctions X),(RAlgebra X)) as Element of (R_Normed_Algebra_of_BoundedFunctions X) ;
take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions X) holds
( b1 * e = b1 & e * b1 = b1 )
thus for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm4; ::_thesis: verum
end;
end;
theorem Th21: :: C0SP1:21
for W being Normed_AlgebraStr
for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds
W is Algebra
proof
let W be Normed_AlgebraStr ; ::_thesis: for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds
W is Algebra
let V be Algebra; ::_thesis: ( AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V implies W is Algebra )
assume A1: AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V ; ::_thesis: W is Algebra
reconsider W = W as non empty AlgebraStr by A1;
A2: W is right_unital
proof
let x be Element of W; :: according to VECTSP_1:def_4 ::_thesis: x * (1. W) = x
reconsider x1 = x as Element of V by A1;
x * (1. W) = x1 * (1. V) by A1;
hence x * (1. W) = x by VECTSP_1:def_4; ::_thesis: verum
end;
A3: W is right-distributive
proof
let x, y, z be Element of W; :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
x * (y + z) = x1 * (y1 + z1) by A1;
then x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def_2;
hence x * (y + z) = (x * y) + (x * z) by A1; ::_thesis: verum
end;
A4: for x being Element of W holds x is right_complementable
proof
let x be Element of W; ::_thesis: x is right_complementable
reconsider x1 = x as Element of V by A1;
consider v being Element of V such that
A5: x1 + v = 0. V by ALGSTR_0:def_11;
reconsider y = v as Element of W by A1;
x + y = 0. W by A1, A5;
hence x is right_complementable by ALGSTR_0:def_11; ::_thesis: verum
end;
A6: for a, b, x being Element of W holds (a * b) * x = a * (b * x)
proof
let a, b, x be Element of W; ::_thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of V by A1;
(a * b) * x = (a1 * b1) * y by A1;
then (a * b) * x = a1 * (b1 * y) by GROUP_1:def_3;
hence (a * b) * x = a * (b * x) by A1; ::_thesis: verum
end;
A7: for v, w being Element of W holds v * w = w * v
proof
let v, w be Element of W; ::_thesis: v * w = w * v
reconsider v1 = v, w1 = w as Element of V by A1;
v * w = v1 * w1 by A1;
then v * w = w1 * v1 ;
hence v * w = w * v by A1; ::_thesis: verum
end;
A8: for x, y, z being VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x, y, z be VECTOR of W; ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;
(x + y) + z = (x1 + y1) + z1 by A1;
then (x + y) + z = x1 + (y1 + z1) by RLVECT_1:def_3;
hence (x + y) + z = x + (y + z) by A1; ::_thesis: verum
end;
A9: for x, y being VECTOR of W holds x + y = y + x
proof
let x, y be VECTOR of W; ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1;
x + y = x1 + y1 by A1;
then x + y = y1 + x1 ;
hence x + y = y + x by A1; ::_thesis: verum
end;
A10: W is vector-distributive
proof
let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of W holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of W; ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as Element of V by A1;
a * (x + y) = a * (x1 + y1) by A1;
then a * (x + y) = (a * x1) + (a * y1) by RLVECT_1:def_5;
hence a * (x + y) = (a * x) + (a * y) by A1; ::_thesis: verum
end;
A11: W is scalar-distributive
proof
let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of W holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Element of W; ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider x1 = x as Element of V by A1;
(a + b) * x = (a + b) * x1 by A1;
then (a + b) * x = (a * x1) + (b * x1) by RLVECT_1:def_6;
hence (a + b) * x = (a * x) + (b * x) by A1; ::_thesis: verum
thus verum ; ::_thesis: verum
end;
A12: W is scalar-associative
proof
let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of W holds (a * b) * b1 = a * (b * b1)
let x be Element of W; ::_thesis: (a * b) * x = a * (b * x)
reconsider x1 = x as Element of V by A1;
(a * b) * x = (a * b) * x1 by A1;
then (a * b) * x = a * (b * x1) by RLVECT_1:def_7;
hence (a * b) * x = a * (b * x) by A1; ::_thesis: verum
end;
A13: W is vector-associative
proof
let x, y be Element of W; :: according to FUNCSDOM:def_9 ::_thesis: for b1 being Element of REAL holds b1 * (x * y) = (b1 * x) * y
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
a * (x * y) = a * (x1 * y1) by A1;
then a * (x * y) = (a * x1) * y1 by FUNCSDOM:def_9;
hence a * (x * y) = (a * x) * y by A1; ::_thesis: verum
end;
for x being VECTOR of W holds x + (0. W) = x
proof
let x be VECTOR of W; ::_thesis: x + (0. W) = x
reconsider y = x as VECTOR of V by A1;
x + (0. W) = y + (0. V) by A1;
hence x + (0. W) = x by RLVECT_1:4; ::_thesis: verum
end;
hence W is Algebra by A9, A8, A4, A7, A6, A2, A3, A10, A11, A12, A13, ALGSTR_0:def_16, GROUP_1:def_3, GROUP_1:def_12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;
theorem Th22: :: C0SP1:22
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Algebra
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is Algebra
1. (R_Normed_Algebra_of_BoundedFunctions X) = 1_ (R_Algebra_of_BoundedFunctions X) ;
hence R_Normed_Algebra_of_BoundedFunctions X is Algebra by Th21; ::_thesis: verum
end;
theorem Th23: :: C0SP1:23
for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F
proof
let X be non empty set ; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F
set X1 = BoundedFunctions X;
reconsider f1 = F as Element of BoundedFunctions X ;
A1: [1,f1] in [:REAL,(BoundedFunctions X):] by ZFMISC_1:87;
thus (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = ( the Mult of (RAlgebra X) | [:REAL,(BoundedFunctions X):]) . (1,f1) by Def11
.= the Mult of (RAlgebra X) . (1,f1) by A1, FUNCT_1:49
.= F by FUNCSDOM:12 ; ::_thesis: verum
end;
theorem Th24: :: C0SP1:24
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
( ( for v being VECTOR of (R_Normed_Algebra_of_BoundedFunctions X) holds 1 * v = v ) & R_Normed_Algebra_of_BoundedFunctions X is Algebra ) by Th22, Th23;
hence R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm3; ::_thesis: verum
end;
theorem Th25: :: C0SP1:25
for X being non empty set holds X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)
proof
let X be non empty set ; ::_thesis: X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)
X --> 0 = 0. (R_Algebra_of_BoundedFunctions X) by Th15;
hence X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: verum
end;
theorem Th26: :: C0SP1:26
for X being non empty set
for x being Element of X
for f being Function of X,REAL
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
abs (f . x) <= ||.F.||
proof
let X be non empty set ; ::_thesis: for x being Element of X
for f being Function of X,REAL
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
abs (f . x) <= ||.F.||
let x be Element of X; ::_thesis: for f being Function of X,REAL
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
abs (f . x) <= ||.F.||
let f be Function of X,REAL; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
abs (f . x) <= ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & f | X is bounded implies abs (f . x) <= ||.F.|| )
assume that
A1: f = F and
A2: f | X is bounded ; ::_thesis: abs (f . x) <= ||.F.||
A3: abs (f . x) in PreNorms f ;
( not PreNorms f is empty & PreNorms f is bounded_above ) by A2, Th17;
then abs (f . x) <= upper_bound (PreNorms f) by A3, SEQ_4:def_1;
hence abs (f . x) <= ||.F.|| by A1, A2, Th20; ::_thesis: verum
end;
theorem :: C0SP1:27
for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
proof
let X be non empty set ; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: 0 <= ||.F.||
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A1: F = g and
A2: g | X is bounded ;
A3: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A2, Th17;
consider r0 being set such that
A4: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A4;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; ::_thesis: 0 <= r
then ex t being Element of X st r = abs (g . t) ;
hence 0 <= r by COMPLEX1:46; ::_thesis: verum
end;
then 0 <= r0 by A4;
then 0 <= upper_bound (PreNorms g) by A3, A4, SEQ_4:def_1;
hence 0 <= ||.F.|| by A1, A2, Th20; ::_thesis: verum
end;
theorem Th28: :: C0SP1:28
for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
proof
let X be non empty set ; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies 0 = ||.F.|| )
set z = X --> 0;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:46;
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A1: g = F and
A2: g | X is bounded ;
A3: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A2, Th17;
consider r0 being set such that
A4: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A4;
A5: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
assume A6: F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: 0 = ||.F.||
A7: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A8: r = abs (g . t) ;
z = g by A6, A1, Th25;
then abs (g . t) = abs 0 by FUNCOP_1:7;
hence ( 0 <= r & r <= 0 ) by A8, ABSVALUE:2; ::_thesis: verum
end;
then 0 <= r0 by A4;
then upper_bound (PreNorms g) = 0 by A7, A3, A4, A5, SEQ_4:def_1;
hence 0 = ||.F.|| by A1, A2, Th20; ::_thesis: verum
end;
theorem Th29: :: C0SP1:29
for X being non empty set
for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof
let X be non empty set ; ::_thesis: for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
let f, g, h be Function of X,REAL; ::_thesis: for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
let F, G, H be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (R_Algebra_of_BoundedFunctions X) ;
A1: ( H = F + G iff h1 = f1 + g1 ) ;
assume ( f = F & g = G & h = H ) ; ::_thesis: ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
hence ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) by A1, Th12; ::_thesis: verum
end;
theorem Th30: :: C0SP1:30
for X being non empty set
for a being Real
for f, g being Function of X,REAL
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof
let X be non empty set ; ::_thesis: for a being Real
for f, g being Function of X,REAL
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let a be Real; ::_thesis: for f, g being Function of X,REAL
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let f, g be Function of X,REAL; ::_thesis: for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let F, G be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) )
reconsider f1 = F, g1 = G as VECTOR of (R_Algebra_of_BoundedFunctions X) ;
A1: ( G = a * F iff g1 = a * f1 ) ;
assume ( f = F & g = G ) ; ::_thesis: ( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
hence ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) by A1, Th13; ::_thesis: verum
end;
theorem Th31: :: C0SP1:31
for X being non empty set
for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
proof
let X be non empty set ; ::_thesis: for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
let f, g, h be Function of X,REAL; ::_thesis: for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
let F, G, H be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (R_Algebra_of_BoundedFunctions X) ;
A1: ( H = F * G iff h1 = f1 * g1 ) ;
assume ( f = F & g = G & h = H ) ; ::_thesis: ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
hence ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) by A1, Th14; ::_thesis: verum
end;
theorem Th32: :: C0SP1:32
for X being non empty set
for a being Real
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proof
let X be non empty set ; ::_thesis: for a being Real
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let a be Real; ::_thesis: for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1: now__::_thesis:_(_F_=_0._(R_Normed_Algebra_of_BoundedFunctions_X)_implies_||.F.||_=_0_)
set z = X --> 0;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:46;
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A2: F = g and
A3: g | X is bounded ;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A3, Th17;
consider r0 being set such that
A5: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A5;
A6: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
assume F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: ||.F.|| = 0
then A7: z = g by A2, Th25;
A8: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A9: r = abs (g . t) ;
abs (g . t) = abs 0 by A7, FUNCOP_1:7
.= 0 by ABSVALUE:2 ;
hence ( 0 <= r & r <= 0 ) by A9; ::_thesis: verum
end;
then 0 <= r0 by A5;
then upper_bound (PreNorms g) = 0 by A8, A4, A5, A6, SEQ_4:def_1;
hence ||.F.|| = 0 by A2, A3, Th20; ::_thesis: verum
end;
A10: ||.(F + G).|| <= ||.F.|| + ||.G.||
proof
F + G in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A11: h1 = F + G and
A12: h1 | X is bounded ;
G in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A13: g1 = G and
A14: g1 | X is bounded ;
F in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A15: f1 = F and
A16: f1 | X is bounded ;
A17: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(h1_._t)_<=_||.F.||_+_||.G.||
let t be Element of X; ::_thesis: abs (h1 . t) <= ||.F.|| + ||.G.||
( abs (f1 . t) <= ||.F.|| & abs (g1 . t) <= ||.G.|| ) by A15, A16, A13, A14, Th26;
then A18: (abs (f1 . t)) + (abs (g1 . t)) <= ||.F.|| + ||.G.|| by XREAL_1:7;
( abs (h1 . t) = abs ((f1 . t) + (g1 . t)) & abs ((f1 . t) + (g1 . t)) <= (abs (f1 . t)) + (abs (g1 . t)) ) by A15, A13, A11, Th29, COMPLEX1:56;
hence abs (h1 . t) <= ||.F.|| + ||.G.|| by A18, XXREAL_0:2; ::_thesis: verum
end;
A19: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_||.F.||_+_||.G.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= ||.F.|| + ||.G.|| )
assume r in PreNorms h1 ; ::_thesis: r <= ||.F.|| + ||.G.||
then ex t being Element of X st r = abs (h1 . t) ;
hence r <= ||.F.|| + ||.G.|| by A17; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms h1 holds
s <= ||.F.|| + ||.G.|| ) implies upper_bound (PreNorms h1) <= ||.F.|| + ||.G.|| ) by SEQ_4:45;
hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A12, A19, Th20; ::_thesis: verum
end;
A20: ||.(a * F).|| = (abs a) * ||.F.||
proof
F in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A21: f1 = F and
A22: f1 | X is bounded ;
a * F in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A23: h1 = a * F and
A24: h1 | X is bounded ;
A25: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(h1_._t)_<=_(abs_a)_*_||.F.||
let t be Element of X; ::_thesis: abs (h1 . t) <= (abs a) * ||.F.||
abs (h1 . t) = abs (a * (f1 . t)) by A21, A23, Th30;
then A26: abs (h1 . t) = (abs a) * (abs (f1 . t)) by COMPLEX1:65;
0 <= abs a by COMPLEX1:46;
hence abs (h1 . t) <= (abs a) * ||.F.|| by A21, A22, A26, Th26, XREAL_1:64; ::_thesis: verum
end;
A27: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_(abs_a)_*_||.F.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= (abs a) * ||.F.|| )
assume r in PreNorms h1 ; ::_thesis: r <= (abs a) * ||.F.||
then ex t being Element of X st r = abs (h1 . t) ;
hence r <= (abs a) * ||.F.|| by A25; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms h1 holds
s <= (abs a) * ||.F.|| ) implies upper_bound (PreNorms h1) <= (abs a) * ||.F.|| ) by SEQ_4:45;
then A28: ||.(a * F).|| <= (abs a) * ||.F.|| by A23, A24, A27, Th20;
percases ( a <> 0 or a = 0 ) ;
supposeA29: a <> 0 ; ::_thesis: ||.(a * F).|| = (abs a) * ||.F.||
A30: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(f1_._t)_<=_((abs_a)_")_*_||.(a_*_F).||
let t be Element of X; ::_thesis: abs (f1 . t) <= ((abs a) ") * ||.(a * F).||
abs (a ") = abs (1 / a) ;
then A31: abs (a ") = 1 / (abs a) by ABSVALUE:7;
h1 . t = a * (f1 . t) by A21, A23, Th30;
then (a ") * (h1 . t) = ((a ") * a) * (f1 . t) ;
then A32: (a ") * (h1 . t) = 1 * (f1 . t) by A29, XCMPLX_0:def_7;
( abs ((a ") * (h1 . t)) = (abs (a ")) * (abs (h1 . t)) & 0 <= abs (a ") ) by COMPLEX1:46, COMPLEX1:65;
hence abs (f1 . t) <= ((abs a) ") * ||.(a * F).|| by A23, A24, A32, A31, Th26, XREAL_1:64; ::_thesis: verum
end;
A33: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_
r_<=_((abs_a)_")_*_||.(a_*_F).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= ((abs a) ") * ||.(a * F).|| )
assume r in PreNorms f1 ; ::_thesis: r <= ((abs a) ") * ||.(a * F).||
then ex t being Element of X st r = abs (f1 . t) ;
hence r <= ((abs a) ") * ||.(a * F).|| by A30; ::_thesis: verum
end;
A34: 0 <= abs a by COMPLEX1:46;
( ( for s being real number st s in PreNorms f1 holds
s <= ((abs a) ") * ||.(a * F).|| ) implies upper_bound (PreNorms f1) <= ((abs a) ") * ||.(a * F).|| ) by SEQ_4:45;
then ||.F.|| <= ((abs a) ") * ||.(a * F).|| by A21, A22, A33, Th20;
then (abs a) * ||.F.|| <= (abs a) * (((abs a) ") * ||.(a * F).||) by A34, XREAL_1:64;
then A35: (abs a) * ||.F.|| <= ((abs a) * ((abs a) ")) * ||.(a * F).|| ;
abs a <> 0 by A29, COMPLEX1:47;
then (abs a) * ||.F.|| <= 1 * ||.(a * F).|| by A35, XCMPLX_0:def_7;
hence ||.(a * F).|| = (abs a) * ||.F.|| by A28, XXREAL_0:1; ::_thesis: verum
end;
supposeA36: a = 0 ; ::_thesis: ||.(a * F).|| = (abs a) * ||.F.||
reconsider fz = F as VECTOR of (R_Algebra_of_BoundedFunctions X) ;
a * fz = (a + a) * fz by A36
.= (a * fz) + (a * fz) by RLVECT_1:def_6 ;
then 0. (R_Algebra_of_BoundedFunctions X) = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:16;
then 0. (R_Algebra_of_BoundedFunctions X) = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def_3;
then 0. (R_Algebra_of_BoundedFunctions X) = (0. (R_Algebra_of_BoundedFunctions X)) + (a * fz) by VECTSP_1:16;
then A37: a * F = 0. (R_Normed_Algebra_of_BoundedFunctions X) by RLVECT_1:4;
(abs a) * ||.F.|| = 0 * ||.F.|| by A36, ABSVALUE:2;
hence ||.(a * F).|| = (abs a) * ||.F.|| by A37, Th28; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_||.F.||_=_0_implies_F_=_0._(R_Normed_Algebra_of_BoundedFunctions_X)_)
set z = X --> 0;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:46;
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A38: F = g and
A39: g | X is bounded ;
assume A40: ||.F.|| = 0 ; ::_thesis: F = 0. (R_Normed_Algebra_of_BoundedFunctions X)
now__::_thesis:_for_t_being_Element_of_X_holds_g_._t_=_z_._t
let t be Element of X; ::_thesis: g . t = z . t
abs (g . t) <= ||.F.|| by A38, A39, Th26;
then abs (g . t) = 0 by A40, COMPLEX1:46;
hence g . t = 0 by ABSVALUE:2
.= z . t by FUNCOP_1:7 ;
::_thesis: verum
end;
then g = z by FUNCT_2:63;
hence F = 0. (R_Normed_Algebra_of_BoundedFunctions X) by A38, Th25; ::_thesis: verum
end;
hence ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A20, A10; ::_thesis: verum
end;
theorem Th33: :: C0SP1:33
for X being non empty set holds
( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )
proof
let X be non empty set ; ::_thesis: ( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )
thus ||.(0. (R_Normed_Algebra_of_BoundedFunctions X)).|| = 0 by Th32; :: according to NORMSP_0:def_6 ::_thesis: ( R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )
for x, y being Point of (R_Normed_Algebra_of_BoundedFunctions X)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th32;
hence ( R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like & R_Normed_Algebra_of_BoundedFunctions X is vector-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-associative & R_Normed_Algebra_of_BoundedFunctions X is scalar-unital & R_Normed_Algebra_of_BoundedFunctions X is Abelian & R_Normed_Algebra_of_BoundedFunctions X is add-associative & R_Normed_Algebra_of_BoundedFunctions X is right_zeroed & R_Normed_Algebra_of_BoundedFunctions X is right_complementable ) by Th24, Th33;
end;
theorem Th34: :: C0SP1:34
for X being non empty set
for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
proof
let X be non empty set ; ::_thesis: for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
let f, g, h be Function of X,REAL; ::_thesis: for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
let F, G, H be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
A2: now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)_implies_F_-_G_=_H_)
assume A3: for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: F - G = H
now__::_thesis:_for_x_being_Element_of_X_holds_(h_._x)_+_(g_._x)_=_f_._x
let x be Element of X; ::_thesis: (h . x) + (g . x) = f . x
h . x = (f . x) - (g . x) by A3;
hence (h . x) + (g . x) = f . x ; ::_thesis: verum
end;
then F = H + G by A1, Th29;
then F - G = H + (G - G) by RLVECT_1:def_3;
then F - G = H + (0. (R_Normed_Algebra_of_BoundedFunctions X)) by RLVECT_1:15;
hence F - G = H by RLVECT_1:4; ::_thesis: verum
end;
now__::_thesis:_(_H_=_F_-_G_implies_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)
assume H = F - G ; ::_thesis: for x being Element of X holds h . x = (f . x) - (g . x)
then H + G = F - (G - G) by RLVECT_1:29;
then H + G = F - (0. (R_Normed_Algebra_of_BoundedFunctions X)) by RLVECT_1:15;
then A4: H + G = F by RLVECT_1:13;
now__::_thesis:_for_x_being_Element_of_X_holds_(f_._x)_-_(g_._x)_=_h_._x
let x be Element of X; ::_thesis: (f . x) - (g . x) = h . x
f . x = (h . x) + (g . x) by A1, A4, Th29;
hence (f . x) - (g . x) = h . x ; ::_thesis: verum
end;
hence for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: verum
end;
hence ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) by A2; ::_thesis: verum
end;
theorem Th35: :: C0SP1:35
for X being non empty set
for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X be non empty set ; ::_thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
defpred S1[ set , set ] means ex xseq being Real_Sequence st
( ( for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . $1 ) & xseq is convergent & $2 = lim xseq );
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
A2: for x being Element of X ex y being Element of REAL st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Element of REAL st S1[x,y]
deffunc H1( Element of NAT ) -> Element of REAL = (modetrans ((vseq . $1),X)) . x;
consider xseq being Real_Sequence such that
A3: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4();
take lim xseq ; ::_thesis: S1[x, lim xseq]
A4: for m, k being Element of NAT holds abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
(vseq . m) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A5: h1 = (vseq . m) - (vseq . k) and
A6: h1 | X is bounded ;
vseq . m in BoundedFunctions X ;
then ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A7: modetrans ((vseq . m),X) = vseq . m by Th19;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A8: modetrans ((vseq . k),X) = vseq . k by Th19;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A3;
then (xseq . m) - (xseq . k) = h1 . x by A7, A8, A5, Th34;
hence abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by A5, A6, Th26; ::_thesis: verum
end;
now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((xseq_._n)_-_(xseq_._k))_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e )
assume A9: e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e
e is Real by XREAL_0:def_1;
then consider k being Element of NAT such that
A10: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A9, RSSPACE3:8;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= k implies abs ((xseq . n) - (xseq . k)) < e )
assume n >= k ; ::_thesis: abs ((xseq . n) - (xseq . k)) < e
then A11: ||.((vseq . n) - (vseq . k)).|| < e by A10;
abs ((xseq . n) - (xseq . k)) <= ||.((vseq . n) - (vseq . k)).|| by A4;
hence abs ((xseq . n) - (xseq . k)) < e by A11, XXREAL_0:2; ::_thesis: verum
end;
end;
then xseq is convergent by SEQ_4:41;
hence S1[x, lim xseq] by A3; ::_thesis: verum
end;
consider tseq being Function of X,REAL such that
A12: for x being Element of X holds S1[x,tseq . x] from FUNCT_2:sch_3(A2);
now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume A13: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT such that
A14: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A13, RSSPACE3:8;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
A15: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def_4;
assume m >= k ; ::_thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A16: ||.((vseq . m) - (vseq . k)).|| < e by A14;
( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def_4, NORMSP_1:9;
hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A16, A15, XXREAL_0:2; ::_thesis: verum
end;
hence for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ; ::_thesis: verum
end;
then A17: ||.vseq.|| is convergent by SEQ_4:41;
now__::_thesis:_for_x_being_set_st_x_in_X_/\_(dom_tseq)_holds_
abs_(tseq_._x)_<=_lim_||.vseq.||
let x be set ; ::_thesis: ( x in X /\ (dom tseq) implies abs (tseq . x) <= lim ||.vseq.|| )
assume A18: x in X /\ (dom tseq) ; ::_thesis: abs (tseq . x) <= lim ||.vseq.||
then consider xseq being Real_Sequence such that
A19: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A20: ( xseq is convergent & tseq . x = lim xseq ) by A12;
A21: for n being Element of NAT holds (abs xseq) . n <= ||.vseq.|| . n
proof
let n be Element of NAT ; ::_thesis: (abs xseq) . n <= ||.vseq.|| . n
A22: xseq . n = (modetrans ((vseq . n),X)) . x by A19;
vseq . n in BoundedFunctions X ;
then A23: ex h1 being Function of X,REAL st
( vseq . n = h1 & h1 | X is bounded ) ;
then modetrans ((vseq . n),X) = vseq . n by Th19;
then abs (xseq . n) <= ||.(vseq . n).|| by A18, A23, A22, Th26;
then (abs xseq) . n <= ||.(vseq . n).|| by VALUED_1:18;
hence (abs xseq) . n <= ||.vseq.|| . n by NORMSP_0:def_4; ::_thesis: verum
end;
( abs xseq is convergent & abs (tseq . x) = lim (abs xseq) ) by A20, SEQ_4:14;
hence abs (tseq . x) <= lim ||.vseq.|| by A17, A21, SEQ_2:18; ::_thesis: verum
end;
then tseq | X is bounded by RFUNCT_1:73;
then tseq in BoundedFunctions X ;
then reconsider tv = tseq as Point of (R_Normed_Algebra_of_BoundedFunctions X) ;
A24: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
then consider k being Element of NAT such that
A25: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, RSSPACE3:8;
take k ; ::_thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
for_x_being_Element_of_X_holds_abs_(((modetrans_((vseq_._n),X))_._x)_-_(tseq_._x))_<=_e
let n be Element of NAT ; ::_thesis: ( n >= k implies for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e )
assume A26: n >= k ; ::_thesis: for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
now__::_thesis:_for_x_being_Element_of_X_holds_abs_(((modetrans_((vseq_._n),X))_._x)_-_(tseq_._x))_<=_e
let x be Element of X; ::_thesis: abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
consider xseq being Real_Sequence such that
A27: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A28: xseq is convergent and
A29: tseq . x = lim xseq by A12;
reconsider fseq = NAT --> (xseq . n) as Real_Sequence ;
set wseq = xseq - fseq;
deffunc H1( Element of NAT ) -> Element of REAL = abs ((xseq . $1) - (xseq . n));
consider rseq being Real_Sequence such that
A30: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A31: for m, k being Element of NAT holds abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
(vseq . m) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A32: h1 = (vseq . m) - (vseq . k) and
A33: h1 | X is bounded ;
vseq . m in BoundedFunctions X ;
then ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A34: modetrans ((vseq . m),X) = vseq . m by Th19;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A35: modetrans ((vseq . k),X) = vseq . k by Th19;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A27;
then (xseq . m) - (xseq . k) = h1 . x by A34, A35, A32, Th34;
hence abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by A32, A33, Th26; ::_thesis: verum
end;
A36: for m being Element of NAT st m >= k holds
rseq . m <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e )
assume m >= k ; ::_thesis: rseq . m <= e
then A37: ||.((vseq . n) - (vseq . m)).|| < e by A25, A26;
rseq . m = abs ((xseq . m) - (xseq . n)) by A30;
then rseq . m = abs ((xseq . n) - (xseq . m)) by COMPLEX1:60;
then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A31;
hence rseq . m <= e by A37, XXREAL_0:2; ::_thesis: verum
end;
A38: now__::_thesis:_for_m_being_Element_of_NAT_holds_(xseq_-_fseq)_._m_=_(xseq_._m)_-_(xseq_._n)
let m be Element of NAT ; ::_thesis: (xseq - fseq) . m = (xseq . m) - (xseq . n)
(xseq - fseq) . m = (xseq . m) + ((- fseq) . m) by SEQ_1:7;
then (xseq - fseq) . m = (xseq . m) + (- (fseq . m)) by SEQ_1:10;
hence (xseq - fseq) . m = (xseq . m) - (xseq . n) by FUNCOP_1:7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
rseq_._x_=_(abs_(xseq_-_fseq))_._x
let x be set ; ::_thesis: ( x in NAT implies rseq . x = (abs (xseq - fseq)) . x )
assume x in NAT ; ::_thesis: rseq . x = (abs (xseq - fseq)) . x
then reconsider k = x as Element of NAT ;
rseq . x = abs ((xseq . k) - (xseq . n)) by A30;
then rseq . x = abs ((xseq - fseq) . k) by A38;
hence rseq . x = (abs (xseq - fseq)) . x by VALUED_1:18; ::_thesis: verum
end;
then A39: rseq = abs (xseq - fseq) by FUNCT_2:12;
A40: xseq - fseq is convergent by A28, SEQ_2:11;
then rseq is convergent by A39;
then A41: lim rseq <= e by A36, RSSPACE2:5;
lim fseq = fseq . 0 by SEQ_4:26;
then lim fseq = xseq . n by FUNCOP_1:7;
then lim (xseq - fseq) = (tseq . x) - (xseq . n) by A28, A29, SEQ_2:12;
then lim rseq = abs ((tseq . x) - (xseq . n)) by A40, A39, SEQ_4:14;
then abs ((xseq . n) - (tseq . x)) <= e by A41, COMPLEX1:60;
hence abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e by A27; ::_thesis: verum
end;
hence for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e ; ::_thesis: verum
end;
hence for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e ; ::_thesis: verum
end;
A42: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
then consider k being Element of NAT such that
A43: for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e by A24;
take k ; ::_thesis: for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A44: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e
vseq . n in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A45: f1 = vseq . n and
f1 | X is bounded ;
(vseq . n) - tv in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A46: h1 = (vseq . n) - tv and
A47: h1 | X is bounded ;
A48: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(h1_._t)_<=_e
let t be Element of X; ::_thesis: abs (h1 . t) <= e
( modetrans ((vseq . n),X) = f1 & h1 . t = (f1 . t) - (tseq . t) ) by A45, A46, Def15, Th34;
hence abs (h1 . t) <= e by A43, A44; ::_thesis: verum
end;
A49: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_e
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= e )
assume r in PreNorms h1 ; ::_thesis: r <= e
then ex t being Element of X st r = abs (h1 . t) ;
hence r <= e by A48; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
hence ||.((vseq . n) - tv).|| <= e by A46, A47, A49, Th20; ::_thesis: verum
end;
end;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A50: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT such that
A51: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A42, A50, XREAL_1:215;
take m ; ::_thesis: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
A52: e / 2 < e by A50, XREAL_1:216;
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq . n) - tv).|| <= e / 2 by A51;
hence ||.((vseq . n) - tv).|| < e by A52, XXREAL_0:2; ::_thesis: verum
end;
end;
hence vseq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;
theorem Th36: :: C0SP1:36
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace
for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th35;
hence R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace by LOPBAN_1:def_15; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> complete ;
coherence
R_Normed_Algebra_of_BoundedFunctions X is complete by Th36;
end;
theorem :: C0SP1:37
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
set B = R_Normed_Algebra_of_BoundedFunctions X;
reconsider B = R_Normed_Algebra_of_BoundedFunctions X as Normed_Algebra by Th22;
1. B in BoundedFunctions X ;
then consider ONE being Function of X,REAL such that
A1: ONE = 1. B and
A2: ONE | X is bounded ;
1. B = 1_ (R_Algebra_of_BoundedFunctions X) ;
then A3: 1. B = X --> 1 by Th16;
for s being set holds
( s in PreNorms ONE iff s = 1 )
proof
set t = the Element of X;
let s be set ; ::_thesis: ( s in PreNorms ONE iff s = 1 )
A4: (X --> 1) . the Element of X = 1 by FUNCOP_1:7;
hereby ::_thesis: ( s = 1 implies s in PreNorms ONE )
assume s in PreNorms ONE ; ::_thesis: s = 1
then consider t being Element of X such that
A5: s = abs ((X --> 1) . t) by A1, A3;
(X --> 1) . t = 1 by FUNCOP_1:7;
hence s = 1 by A5, COMPLEX1:48; ::_thesis: verum
end;
assume s = 1 ; ::_thesis: s in PreNorms ONE
then s = abs ((X --> 1) . the Element of X) by A4, COMPLEX1:48;
hence s in PreNorms ONE by A1, A3; ::_thesis: verum
end;
then PreNorms ONE = {1} by TARSKI:def_1;
then upper_bound (PreNorms ONE) = 1 by SEQ_4:9;
then A6: ||.(1. B).|| = 1 by A1, A2, Th20;
A7: now__::_thesis:_for_a_being_Real
for_f,_g_being_Element_of_B_holds_a_*_(f_*_g)_=_f_*_(a_*_g)
let a be Real; ::_thesis: for f, g being Element of B holds a * (f * g) = f * (a * g)
let f, g be Element of B; ::_thesis: a * (f * g) = f * (a * g)
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A8: f1 = f and
f1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A9: g1 = g and
g1 | X is bounded ;
a * (f * g) in BoundedFunctions X ;
then consider h3 being Function of X,REAL such that
A10: h3 = a * (f * g) and
h3 | X is bounded ;
f * g in BoundedFunctions X ;
then consider h2 being Function of X,REAL such that
A11: h2 = f * g and
h2 | X is bounded ;
a * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A12: h1 = a * g and
h1 | X is bounded ;
now__::_thesis:_for_x_being_Element_of_X_holds_h3_._x_=_(f1_._x)_*_(h1_._x)
let x be Element of X; ::_thesis: h3 . x = (f1 . x) * (h1 . x)
h3 . x = a * (h2 . x) by A11, A10, Th30;
then h3 . x = a * ((f1 . x) * (g1 . x)) by A8, A9, A11, Th31;
then h3 . x = (f1 . x) * (a * (g1 . x)) ;
hence h3 . x = (f1 . x) * (h1 . x) by A9, A12, Th30; ::_thesis: verum
end;
hence a * (f * g) = f * (a * g) by A8, A12, A10, Th31; ::_thesis: verum
end;
A13: now__::_thesis:_for_f,_g_being_Element_of_B_holds_||.(f_*_g).||_<=_||.f.||_*_||.g.||
let f, g be Element of B; ::_thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A14: f1 = f and
A15: f1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A16: g1 = g and
A17: g1 | X is bounded ;
A18: ( not PreNorms g1 is empty & PreNorms g1 is bounded_above ) by A17, Th17;
f * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A19: h1 = f * g and
A20: h1 | X is bounded ;
A21: ( not PreNorms f1 is empty & PreNorms f1 is bounded_above ) by A15, Th17;
now__::_thesis:_for_s_being_real_number_st_s_in_PreNorms_h1_holds_
s_<=_(upper_bound_(PreNorms_f1))_*_(upper_bound_(PreNorms_g1))
let s be real number ; ::_thesis: ( s in PreNorms h1 implies s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) )
assume s in PreNorms h1 ; ::_thesis: s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
then consider t being Element of X such that
A22: s = abs (h1 . t) ;
abs (g1 . t) in PreNorms g1 ;
then A23: abs (g1 . t) <= upper_bound (PreNorms g1) by A18, SEQ_4:def_1;
abs (f1 . t) in PreNorms f1 ;
then A24: abs (f1 . t) <= upper_bound (PreNorms f1) by A21, SEQ_4:def_1;
then 0 <= upper_bound (PreNorms f1) by COMPLEX1:46;
then A25: (upper_bound (PreNorms f1)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A23, XREAL_1:64;
0 <= abs (g1 . t) by COMPLEX1:46;
then A26: (abs (f1 . t)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (abs (g1 . t)) by A24, XREAL_1:64;
abs (h1 . t) = abs ((f1 . t) * (g1 . t)) by A14, A16, A19, Th31;
then abs (h1 . t) = (abs (f1 . t)) * (abs (g1 . t)) by COMPLEX1:65;
hence s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A22, A26, A25, XXREAL_0:2; ::_thesis: verum
end;
then A27: upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by SEQ_4:45;
A28: ||.g.|| = upper_bound (PreNorms g1) by A16, A17, Th20;
||.f.|| = upper_bound (PreNorms f1) by A14, A15, Th20;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A19, A20, A28, A27, Th20; ::_thesis: verum
end;
A29: now__::_thesis:_for_f,_g,_h_being_Element_of_B_holds_(g_+_h)_*_f_=_(g_*_f)_+_(h_*_f)
let f, g, h be Element of B; ::_thesis: (g + h) * f = (g * f) + (h * f)
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A30: f1 = f and
f1 | X is bounded ;
h in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A31: h1 = h and
h1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A32: g1 = g and
g1 | X is bounded ;
(g + h) * f in BoundedFunctions X ;
then consider F1 being Function of X,REAL such that
A33: F1 = (g + h) * f and
F1 | X is bounded ;
h * f in BoundedFunctions X ;
then consider hf1 being Function of X,REAL such that
A34: hf1 = h * f and
hf1 | X is bounded ;
g * f in BoundedFunctions X ;
then consider gf1 being Function of X,REAL such that
A35: gf1 = g * f and
gf1 | X is bounded ;
g + h in BoundedFunctions X ;
then consider gPh1 being Function of X,REAL such that
A36: gPh1 = g + h and
gPh1 | X is bounded ;
now__::_thesis:_for_x_being_Element_of_X_holds_F1_._x_=_(gf1_._x)_+_(hf1_._x)
let x be Element of X; ::_thesis: F1 . x = (gf1 . x) + (hf1 . x)
F1 . x = (gPh1 . x) * (f1 . x) by A30, A36, A33, Th31;
then F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by A32, A31, A36, Th29;
then F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by A30, A32, A35, Th31;
hence F1 . x = (gf1 . x) + (hf1 . x) by A30, A31, A34, Th31; ::_thesis: verum
end;
hence (g + h) * f = (g * f) + (h * f) by A35, A34, A33, Th29; ::_thesis: verum
end;
for f being Element of B holds (1. B) * f = f by Lm4;
then B is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Algebra by A13, A6, A7, A29, LOPBAN_2:def_9, LOPBAN_2:def_10, LOPBAN_2:def_11, VECTSP_1:def_3, VECTSP_1:def_8;
hence R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra ; ::_thesis: verum
end;