:: CC0SP1 semantic presentation
begin
definition
let V be ComplexAlgebra;
mode ComplexSubAlgebra of V -> ComplexAlgebra means :Def1: :: CC0SP1:def 1
( 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 | [:COMPLEX, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );
existence
ex b1 being ComplexAlgebra 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 | [:COMPLEX, 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 | [:COMPLEX, 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 | [:COMPLEX, the carrier of V:] & 1. V = 1. V & 0. V = 0. V ) by RELSET_1:19; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines ComplexSubAlgebra CC0SP1:def_1_:_
for V, b2 being ComplexAlgebra holds
( b2 is ComplexSubAlgebra 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 | [:COMPLEX, the carrier of b2:] & 1. b2 = 1. V & 0. b2 = 0. V ) );
Lm1: now__::_thesis:_for_z_being_Complex
for_X_being_non_empty_set_
for_V_being_ComplexAlgebra
for_V1_being_non_empty_Subset_of_V
for_d1,_d2_being_Element_of_X
for_A_being_BinOp_of_X
for_M_being_Function_of_[:X,X:],X
for_MR_being_Function_of_[:COMPLEX,X:],X_st_V1_=_X_&_MR_=_the_Mult_of_V_|_[:COMPLEX,V1:]_holds_
for_W_being_non_empty_ComplexAlgebraStr_st_W_=_ComplexAlgebraStr(#_X,M,A,MR,d2,d1_#)_holds_
for_w_being_VECTOR_of_W
for_v_being_Element_of_V_st_w_=_v_holds_
z_*_w_=_z_*_v
let z be Complex; ::_thesis: for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let X be non empty set ; ::_thesis: for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let V be ComplexAlgebra; ::_thesis: for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let V1 be non empty Subset of V; ::_thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let d1, d2 be Element of X; ::_thesis: for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let A be BinOp of X; ::_thesis: for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let M be Function of [:X,X:],X; ::_thesis: for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let MR be Function of [:COMPLEX,X:],X; ::_thesis: ( V1 = X & MR = the Mult of V | [:COMPLEX,V1:] implies for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v )
assume that
A1: V1 = X and
A2: MR = the Mult of V | [:COMPLEX,V1:] ; ::_thesis: for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let W be non empty ComplexAlgebraStr ; ::_thesis: ( W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) implies for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v )
assume A3: W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) ; ::_thesis: for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let w be VECTOR of W; ::_thesis: for v being Element of V st w = v holds
z * w = z * v
let v be Element of V; ::_thesis: ( w = v implies z * w = z * v )
assume A4: w = v ; ::_thesis: z * w = z * v
z in COMPLEX by XCMPLX_0:def_2;
then [z,w] in [:COMPLEX,V1:] by A1, A3, ZFMISC_1:def_2;
hence z * w = z * v by A4, A2, A3, FUNCT_1:49; ::_thesis: verum
end;
theorem Th1: :: CC0SP1:1
for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
proof
let X be non empty set ; ::_thesis: for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
let V be ComplexAlgebra; ::_thesis: for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
let V1 be non empty Subset of V; ::_thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra 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 MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
let A be BinOp of X; ::_thesis: for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
let M be Function of [:X,X:],X; ::_thesis: for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
let MR be Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse implies ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra 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 | [:COMPLEX,V1:] and
A7: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def_1 ::_thesis: ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
reconsider W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) as non empty ComplexAlgebraStr ;
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)
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
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: ( 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 MV = the Mult 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 A11: 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 A11, 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, z = 0. W 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
A12: x1 + v = 0. V by ALGSTR_0:def_11;
v = - x1 by A12, 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, A12; ::_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 A13: 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 A13, 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 A14: 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, A14; ::_thesis: verum
end;
thus for a being Complex
for x, y being VECTOR of W holds a * (x + y) = (a * x) + (a * y) :: according to CLVECT_1:def_2 ::_thesis: ( W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
let a be Complex; ::_thesis: for x, y being VECTOR of W holds a * (x + y) = (a * x) + (a * y)
let x, y be VECTOR of W; ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
A15: a * x = a * x1 by A1, A6, Lm1;
A16: a * y = a * y1 by A1, A6, Lm1;
x + y = x1 + y1 by A8;
then a * (x + y) = a * (x1 + y1) by A1, A6, Lm1;
then a * (x + y) = (a * x1) + (a * y1) by CLVECT_1:def_2;
hence a * (x + y) = (a * x) + (a * y) by A8, A15, A16; ::_thesis: verum
end;
thus for a, b being Complex
for v being VECTOR of W holds (a + b) * v = (a * v) + (b * v) :: according to CLVECT_1:def_3 ::_thesis: ( W is scalar-associative & W is vector-associative )
proof
let a, b be Complex; ::_thesis: for v being VECTOR of W holds (a + b) * v = (a * v) + (b * v)
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;
A17: a * x = a * x1 by A1, A6, Lm1;
A18: b * x = b * x1 by A1, A6, Lm1;
(a + b) * x = (a + b) * x1 by A1, A6, Lm1;
then (a + b) * x = (a * x1) + (b * x1) by CLVECT_1:def_3;
hence (a + b) * x = (a * x) + (b * x) by A8, A17, A18; ::_thesis: verum
end;
thus for a, b being Complex
for v being VECTOR of W holds (a * b) * v = a * (b * v) :: according to CLVECT_1:def_4 ::_thesis: W is vector-associative
proof
let a, b be Complex; ::_thesis: for v being VECTOR of W holds (a * b) * v = a * (b * v)
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 y = b * x as Element of W ;
reconsider y1 = b * x1 as Element of V ;
A19: b * x = b * x1 by A1, A6, Lm1;
A20: a * (b * x) = a * (b * x1) by A1, A6, A19, Lm1;
(a * b) * x = (a * b) * x1 by A1, A6, Lm1;
hence (a * b) * x = a * (b * x) by A20, CLVECT_1:def_4; ::_thesis: verum
end;
thus for x, y being Element of W
for a being Element of COMPLEX holds a * (x * y) = (a * x) * y :: according to CFUNCDOM:def_9 ::_thesis: verum
proof
let x, y be Element of W; ::_thesis: for a being Element of COMPLEX holds a * (x * y) = (a * x) * y
let a be Element of COMPLEX ; ::_thesis: a * (x * y) = (a * x) * y
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
A21: a * x = a * x1 by A1, A6, Lm1;
A22: a * (x * y) = a * (x1 * y1) by A1, A6, Lm1, A9;
a * (x1 * y1) = (a * x1) * y1 by CFUNCDOM:def_9;
hence a * (x * y) = (a * x) * y by A9, A21, A22; ::_thesis: verum
end;
thus verum ; ::_thesis: verum
end;
( 0. W = 0. V & 1. W = 1. V ) by A2, A3;
hence ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V by A1, A4, A5, A6, A10, Def1; ::_thesis: verum
end;
registration
let V be ComplexAlgebra;
cluster non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative for ComplexSubAlgebra of V;
existence
ex b1 being ComplexSubAlgebra of V st b1 is strict
proof
set V1 = [#] V;
A1: the Mult of V = the Mult of V | [:COMPLEX,([#] 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 ComplexAlgebraStr(# the carrier of V, the multF of V, the addF of V, the Mult of V,(1. V),(0. V) #) is ComplexSubAlgebra of V by A1, Th1;
hence ex b1 being ComplexSubAlgebra of V st b1 is strict ; ::_thesis: verum
end;
end;
definition
let V be ComplexAlgebra;
let V1 be Subset of V;
attrV1 is Cadditively-linearly-closed means :Def2: :: CC0SP1:def 2
( V1 is add-closed & V1 is having-inverse & ( for a being Complex
for v being Element of V st v in V1 holds
a * v in V1 ) );
end;
:: deftheorem Def2 defines Cadditively-linearly-closed CC0SP1:def_2_:_
for V being ComplexAlgebra
for V1 being Subset of V holds
( V1 is Cadditively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Complex
for v being Element of V st v in V1 holds
a * v in V1 ) ) );
definition
let V be ComplexAlgebra;
let V1 be Subset of V;
assume B1: ( V1 is Cadditively-linearly-closed & not V1 is empty ) ;
func Mult_ (V1,V) -> Function of [:COMPLEX,V1:],V1 equals :Def3: :: CC0SP1:def 3
the Mult of V | [:COMPLEX,V1:];
correctness
coherence
the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1;
proof
A1: ( [:COMPLEX,V1:] c= [:COMPLEX, the carrier of V:] & dom the Mult of V = [:COMPLEX, the carrier of V:] ) by FUNCT_2:def_1, ZFMISC_1:95;
A2: for z being set st z in [:COMPLEX,V1:] holds
( the Mult of V | [:COMPLEX,V1:]) . z in V1
proof
let z be set ; ::_thesis: ( z in [:COMPLEX,V1:] implies ( the Mult of V | [:COMPLEX,V1:]) . z in V1 )
assume A3: z in [:COMPLEX,V1:] ; ::_thesis: ( the Mult of V | [:COMPLEX,V1:]) . z in V1
consider r, x being set such that
A4: r in COMPLEX and
A5: x in V1 and
A6: z = [r,x] by A3, ZFMISC_1:def_2;
reconsider r = r as Complex by A4;
reconsider y = x as VECTOR of V by A5;
[r,x] in dom ( the Mult of V | [:COMPLEX,V1:]) by A1, A3, A6, RELAT_1:62;
then ( the Mult of V | [:COMPLEX,V1:]) . z = r * y by A6, FUNCT_1:47;
hence ( the Mult of V | [:COMPLEX,V1:]) . z in V1 by B1, A5, Def2; ::_thesis: verum
end;
dom ( the Mult of V | [:COMPLEX,V1:]) = [:COMPLEX,V1:] by A1, RELAT_1:62;
hence the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Mult_ CC0SP1:def_3_:_
for V being ComplexAlgebra
for V1 being Subset of V st V1 is Cadditively-linearly-closed & not V1 is empty holds
Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:];
definition
let X be non empty set ;
func ComplexBoundedFunctions X -> non empty Subset of (CAlgebra X) equals :: CC0SP1:def 4
{ f where f is Function of X,COMPLEX : f | X is bounded } ;
correctness
coherence
{ f where f is Function of X,COMPLEX : f | X is bounded } is non empty Subset of (CAlgebra X);
proof
A1: { f where f is Function of X,COMPLEX : f | X is bounded } c= Funcs (X,COMPLEX)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Function of X,COMPLEX : f | X is bounded } or x in Funcs (X,COMPLEX) )
assume x in { f where f is Function of X,COMPLEX : f | X is bounded } ; ::_thesis: x in Funcs (X,COMPLEX)
then ex f being Function of X,COMPLEX st
( x = f & f | X is bounded ) ;
hence x in Funcs (X,COMPLEX) by FUNCT_2:8; ::_thesis: verum
end;
not { f where f is Function of X,COMPLEX : f | X is bounded } is empty
proof
reconsider g = X --> 0c as Function of X,COMPLEX ;
g | X is bounded ;
then g in { f where f is Function of X,COMPLEX : f | X is bounded } ;
hence not { f where f is Function of X,COMPLEX : f | X is bounded } is empty ; ::_thesis: verum
end;
hence { f where f is Function of X,COMPLEX : f | X is bounded } is non empty Subset of (CAlgebra X) by A1; ::_thesis: verum
end;
end;
:: deftheorem defines ComplexBoundedFunctions CC0SP1:def_4_:_
for X being non empty set holds ComplexBoundedFunctions X = { f where f is Function of X,COMPLEX : f | X is bounded } ;
registration
let X be non empty set ;
cluster CAlgebra X -> scalar-unital ;
coherence
CAlgebra X is scalar-unital
proof
for v being Element of (CAlgebra X) holds 1r * v = v by CFUNCDOM:12;
hence CAlgebra X is scalar-unital by CLVECT_1:def_5; ::_thesis: verum
end;
end;
registration
let X be non empty set ;
cluster ComplexBoundedFunctions X -> non empty multiplicatively-closed Cadditively-linearly-closed ;
coherence
( ComplexBoundedFunctions X is Cadditively-linearly-closed & ComplexBoundedFunctions X is multiplicatively-closed )
proof
set W = ComplexBoundedFunctions X;
set V = CAlgebra X;
for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v + u in ComplexBoundedFunctions X
proof
let v, u be Element of (CAlgebra X); ::_thesis: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v + u in ComplexBoundedFunctions X )
assume A1: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; ::_thesis: v + u in ComplexBoundedFunctions X
consider v1 being Function of X,COMPLEX such that
A2: ( v1 = v & v1 | X is bounded ) by A1;
consider u1 being Function of X,COMPLEX such that
A3: ( u1 = u & u1 | X is bounded ) by A1;
dom (v1 + u1) = X /\ X by FUNCT_2:def_1;
then A4: ( v1 + u1 is Function of X,COMPLEX & (v1 + u1) | X is bounded ) by A2, A3, CFUNCT_1:75;
reconsider h = v + u as Element of Funcs (X,COMPLEX) ;
A5: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def_2;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def_1;
then A6: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def_1;
for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A2, A3, CFUNCDOM:1;
then v + u = v1 + u1 by A6, A5, VALUED_1:def_1;
hence v + u in ComplexBoundedFunctions X by A4; ::_thesis: verum
end;
then A7: ComplexBoundedFunctions X is add-closed by IDEAL_1:def_1;
for v being Element of (CAlgebra X) st v in ComplexBoundedFunctions X holds
- v in ComplexBoundedFunctions X
proof
let v be Element of (CAlgebra X); ::_thesis: ( v in ComplexBoundedFunctions X implies - v in ComplexBoundedFunctions X )
assume A8: v in ComplexBoundedFunctions X ; ::_thesis: - v in ComplexBoundedFunctions X
consider v1 being Function of X,COMPLEX such that
A9: ( v1 = v & v1 | X is bounded ) by A8;
A10: ( - v1 is Function of X,COMPLEX & (- v1) | X is bounded ) by A9, CFUNCT_1:74;
reconsider h = - v, v2 = v as Element of Funcs (X,COMPLEX) ;
A11: h = (- 1r) * v by CLVECT_1:3;
A12: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def_2;
A13: dom v1 = X by FUNCT_2:def_1;
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 = (- 1r) * (v2 . y) by A11, CFUNCDOM:4;
hence h . x = - (v1 . x) by A9; ::_thesis: verum
end;
then - v = - v1 by A13, A12, VALUED_1:9;
hence - v in ComplexBoundedFunctions X by A10; ::_thesis: verum
end;
then A14: ComplexBoundedFunctions X is having-inverse by C0SP1:def_1;
for a being Complex
for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X
proof
let a be Complex; ::_thesis: for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X
let u be Element of (CAlgebra X); ::_thesis: ( u in ComplexBoundedFunctions X implies a * u in ComplexBoundedFunctions X )
assume A15: u in ComplexBoundedFunctions X ; ::_thesis: a * u in ComplexBoundedFunctions X
consider u1 being Function of X,COMPLEX such that
A16: ( u1 = u & u1 | X is bounded ) by A15;
A17: a in COMPLEX by XCMPLX_0:def_2;
then A18: ( a (#) u1 is Function of X,COMPLEX & (a (#) u1) | X is bounded ) by A16, CFUNCT_1:72;
reconsider h = a * u as Element of Funcs (X,COMPLEX) ;
A19: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def_2;
A20: dom u1 = X by FUNCT_2:def_1;
for x being set st x in dom h holds
h . x = a * (u1 . x) by A17, A16, CFUNCDOM:4;
then a * u = a (#) u1 by A20, A19, VALUED_1:def_5;
hence a * u in ComplexBoundedFunctions X by A18; ::_thesis: verum
end;
hence ComplexBoundedFunctions X is Cadditively-linearly-closed by A7, A14, Def2; ::_thesis: ComplexBoundedFunctions X is multiplicatively-closed
A21: for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v * u in ComplexBoundedFunctions X
proof
let v, u be Element of (CAlgebra X); ::_thesis: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v * u in ComplexBoundedFunctions X )
assume A22: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; ::_thesis: v * u in ComplexBoundedFunctions X
consider v1 being Function of X,COMPLEX such that
A23: ( v1 = v & v1 | X is bounded ) by A22;
consider u1 being Function of X,COMPLEX such that
A24: ( u1 = u & u1 | X is bounded ) by A22;
dom (v1 (#) u1) = X /\ X by FUNCT_2:def_1;
then A25: ( v1 (#) u1 is Function of X,COMPLEX & (v1 (#) u1) | X is bounded ) by A23, A24, CFUNCT_1:76;
reconsider h = v * u as Element of Funcs (X,COMPLEX) ;
A26: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def_2;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def_1;
then A27: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def_1;
for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A23, A24, CFUNCDOM:2;
then v * u = v1 (#) u1 by A27, A26, VALUED_1:def_4;
hence v * u in ComplexBoundedFunctions X by A25; ::_thesis: verum
end;
reconsider g = ComplexFuncUnit X as Function of X,COMPLEX ;
g | X is bounded ;
then 1. (CAlgebra X) in ComplexBoundedFunctions X ;
hence ComplexBoundedFunctions X is multiplicatively-closed by A21, C0SP1:def_4; ::_thesis: verum
end;
end;
registration
let V be ComplexAlgebra;
cluster non empty multiplicatively-closed Cadditively-linearly-closed for Element of bool the carrier of V;
existence
ex b1 being non empty Subset of V st
( b1 is Cadditively-linearly-closed & b1 is multiplicatively-closed )
proof
reconsider W = [#] V as non empty Subset of V ;
( W is add-closed & W is having-inverse & ( for a being Complex
for v being Element of V st v in W holds
a * v in W ) ) ;
then A1: W is Cadditively-linearly-closed by Def2;
( 1. V in W & ( for v, u being Element of V st v in W & u in W holds
v * u in W ) ) ;
then W is multiplicatively-closed by C0SP1:def_4;
hence ex b1 being non empty Subset of V st
( b1 is Cadditively-linearly-closed & b1 is multiplicatively-closed ) by A1; ::_thesis: verum
end;
end;
definition
let V be non empty CLSStruct ;
attrV is scalar-mult-cancelable means :: CC0SP1:def 5
for a being Complex
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );
end;
:: deftheorem defines scalar-mult-cancelable CC0SP1:def_5_:_
for V being non empty CLSStruct holds
( V is scalar-mult-cancelable iff for a being Complex
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V ) );
theorem Th2: :: CC0SP1:2
for V being ComplexAlgebra
for V1 being non empty multiplicatively-closed Cadditively-linearly-closed Subset of V holds ComplexAlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is ComplexSubAlgebra of V
proof
let V be ComplexAlgebra; ::_thesis: for V1 being non empty multiplicatively-closed Cadditively-linearly-closed Subset of V holds ComplexAlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is ComplexSubAlgebra of V
let V1 be non empty multiplicatively-closed Cadditively-linearly-closed Subset of V; ::_thesis: ComplexAlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is ComplexSubAlgebra of V
A1: Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:] by Def3;
A2: ( V1 is add-closed & V1 is having-inverse & not V1 is empty ) by Def2;
A3: ( One_ (V1,V) = 1_ V & mult_ (V1,V) = the multF of V || V1 ) by C0SP1:def_6, C0SP1:def_8;
( Zero_ (V1,V) = 0. V & Add_ (V1,V) = the addF of V || V1 ) by A2, C0SP1:def_5, C0SP1:def_7;
hence ComplexAlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is ComplexSubAlgebra of V by A1, A2, A3, Th1; ::_thesis: verum
end;
theorem Th3: :: CC0SP1:3
for V being ComplexAlgebra
for V1 being ComplexSubAlgebra 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 Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
proof
let V be ComplexAlgebra; ::_thesis: for V1 being ComplexSubAlgebra 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 Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let V1 be ComplexSubAlgebra 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 Complex 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 Complex 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 Def1;
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 Complex 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 Def1;
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 Complex st v1 = v holds
a * v1 = a * v
let v be Element of V; ::_thesis: for a being Complex st v1 = v holds
a * v1 = a * v
let a be Complex; ::_thesis: ( v1 = v implies a * v1 = a * v )
assume A3: v1 = v ; ::_thesis: a * v1 = a * v
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2;
a1 * v1 = ( the Mult of V | [:COMPLEX, the carrier of V1:]) . [a1,v1] by Def1;
then a1 * v1 = a1 * v by A3, FUNCT_1:49;
hence a * v1 = a * v ; ::_thesis: verum
end;
thus ( 1_ V1 = 1_ V & 0. V1 = 0. V ) by Def1; ::_thesis: verum
end;
definition
let X be non empty set ;
func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals :: CC0SP1:def 6
ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);
coherence
ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #) is ComplexAlgebra by Th2;
end;
:: deftheorem defines C_Algebra_of_BoundedFunctions CC0SP1:def_6_:_
for X being non empty set holds C_Algebra_of_BoundedFunctions X = ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);
theorem :: CC0SP1:4
for X being non empty set holds C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
registration
let X be non empty set ;
cluster C_Algebra_of_BoundedFunctions X -> scalar-unital ;
coherence
( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital )
proof
now__::_thesis:_for_v_being_VECTOR_of_(C_Algebra_of_BoundedFunctions_X)_holds_1r_*_v_=_v
let v be VECTOR of (C_Algebra_of_BoundedFunctions X); ::_thesis: 1r * v = v
reconsider v1 = v as VECTOR of (CAlgebra X) by TARSKI:def_3;
C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
then 1r * v = 1r * v1 by Th3;
hence 1r * v = v by CFUNCDOM:12; ::_thesis: verum
end;
hence ( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital ) by CLVECT_1:def_5; ::_thesis: verum
end;
end;
theorem Th5: :: CC0SP1:5
for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX 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 (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX 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 (C_Algebra_of_BoundedFunctions X); ::_thesis: for f, g, h being Function of X,COMPLEX 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,COMPLEX; ::_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: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (CAlgebra X) by TARSKI:def_3;
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, Th3;
hence h . x = (f . x) + (g . x) by A1, CFUNCDOM: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, CFUNCDOM:1;
hence H = F + G by A2, Th3; ::_thesis: verum
end;
theorem Th6: :: CC0SP1:6
for X being non empty set
for a being Complex
for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g being Function of X,COMPLEX 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 Complex
for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g being Function of X,COMPLEX 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 Complex; ::_thesis: for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g being Function of X,COMPLEX 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 (C_Algebra_of_BoundedFunctions X); ::_thesis: for f, g being Function of X,COMPLEX 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,COMPLEX; ::_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) )
A2: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
reconsider f1 = F, g1 = G as VECTOR of (CAlgebra X) by TARSKI:def_3;
A3: a in COMPLEX by XCMPLX_0:def_2;
hereby ::_thesis: ( ( for x being Element of X holds g . x = a * (f . x) ) implies G = a * F )
assume A4: 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, A4, Th3;
hence g . x = a * (f . x) by A1, A3, CFUNCDOM: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, A3, CFUNCDOM:4;
hence G = a * F by A2, Th3; ::_thesis: verum
end;
theorem Th7: :: CC0SP1:7
for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX 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 (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX 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 (C_Algebra_of_BoundedFunctions X); ::_thesis: for f, g, h being Function of X,COMPLEX 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,COMPLEX; ::_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: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (CAlgebra X) by TARSKI:def_3;
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, Th3;
hence h . x = (f . x) * (g . x) by A1, CFUNCDOM: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, CFUNCDOM:2;
hence H = F * G by A2, Th3; ::_thesis: verum
end;
theorem Th8: :: CC0SP1:8
for X being non empty set holds 0. (C_Algebra_of_BoundedFunctions X) = X --> 0
proof
let X be non empty set ; ::_thesis: 0. (C_Algebra_of_BoundedFunctions X) = X --> 0
A1: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
0. (CAlgebra X) = X --> 0 ;
hence 0. (C_Algebra_of_BoundedFunctions X) = X --> 0 by A1, Th3; ::_thesis: verum
end;
theorem Th9: :: CC0SP1:9
for X being non empty set holds 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r
proof
let X be non empty set ; ::_thesis: 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r
A1: C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
1_ (CAlgebra X) = X --> 1r ;
hence 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r by A1, Th3; ::_thesis: verum
end;
definition
let X be non empty set ;
let F be set ;
assume A1: F in ComplexBoundedFunctions X ;
func modetrans (F,X) -> Function of X,COMPLEX means :Def7: :: CC0SP1:def 7
( it = F & it | X is bounded );
correctness
existence
ex b1 being Function of X,COMPLEX st
( b1 = F & b1 | X is bounded );
uniqueness
for b1, b2 being Function of X,COMPLEX st b1 = F & b1 | X is bounded & b2 = F & b2 | X is bounded holds
b1 = b2;
by A1;
end;
:: deftheorem Def7 defines modetrans CC0SP1:def_7_:_
for X being non empty set
for F being set st F in ComplexBoundedFunctions X holds
for b3 being Function of X,COMPLEX 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,COMPLEX;
func PreNorms f -> non empty Subset of REAL equals :: CC0SP1:def 8
{ |.(f . x).| where x is Element of X : verum } ;
coherence
{ |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL
proof
A1: now__::_thesis:_for_z_being_set_st_z_in__{__|.(f_._x).|_where_x_is_Element_of_X_:_verum__}__holds_
z_in_REAL
let z be set ; ::_thesis: ( z in { |.(f . x).| where x is Element of X : verum } implies z in REAL )
now__::_thesis:_(_z_in__{__|.(f_._x).|_where_x_is_Element_of_X_:_verum__}__implies_z_in_REAL_)
assume z in { |.(f . x).| where x is Element of X : verum } ; ::_thesis: z in REAL
then ex x being Element of X st z = |.(f . x).| ;
hence z in REAL ; ::_thesis: verum
end;
hence ( z in { |.(f . x).| where x is Element of X : verum } implies z in REAL ) ; ::_thesis: verum
end;
set z = the Element of X;
|.(f . the Element of X).| in { |.(f . x).| where x is Element of X : verum } ;
hence { |.(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 CC0SP1:def_8_:_
for X being non empty set
for f being Function of X,COMPLEX holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;
Lm2: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
let f be PartFunc of C,COMPLEX; ::_thesis: ( |.f.| is bounded iff f is bounded )
A1: dom f = dom |.f.| by VALUED_1:def_11;
thus ( |.f.| is bounded implies f is bounded ) ::_thesis: ( f is bounded implies |.f.| is bounded )
proof
assume |.f.| is bounded ; ::_thesis: f is bounded
then consider r1 being real number such that
A2: for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < r1 by COMSEQ_2:def_3;
now__::_thesis:_for_y_being_set_st_y_in_dom_f_holds_
not_r1_<=_|.(f_._y).|
let y be set ; ::_thesis: ( y in dom f implies not r1 <= |.(f . y).| )
assume A3: y in dom f ; ::_thesis: not r1 <= |.(f . y).|
then |.(|.f.| . y).| < r1 by A1, A2;
then |.|.(f . y).|.| < r1 by A1, A3, VALUED_1:def_11;
hence not r1 <= |.(f . y).| ; ::_thesis: verum
end;
hence f is bounded by COMSEQ_2:def_3; ::_thesis: verum
end;
assume f is bounded ; ::_thesis: |.f.| is bounded
then consider r2 being real number such that
A4: for y being set st y in dom f holds
|.(f . y).| < r2 by COMSEQ_2:def_3;
now__::_thesis:_ex_r2_being_real_number_st_
for_y_being_set_st_y_in_dom_|.f.|_holds_
|.(|.f.|_._y).|_<_r2
take r2 = r2; ::_thesis: for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < r2
let y be set ; ::_thesis: ( y in dom |.f.| implies |.(|.f.| . y).| < r2 )
assume A5: y in dom |.f.| ; ::_thesis: |.(|.f.| . y).| < r2
then |.|.(f . y).|.| < r2 by A1, A4;
hence |.(|.f.| . y).| < r2 by A5, VALUED_1:def_11; ::_thesis: verum
end;
hence |.f.| is bounded by COMSEQ_2:def_3; ::_thesis: verum
end;
theorem Th10: :: CC0SP1:10
for X being non empty set
for f being Function of X,COMPLEX 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,COMPLEX st f | X is bounded holds
PreNorms f is bounded_above
let f be Function of X,COMPLEX; ::_thesis: ( f | X is bounded implies PreNorms f is bounded_above )
A1: dom |.f.| = dom f by VALUED_1:def_11;
A2: dom (|.f.| | X) = X /\ (dom |.f.|) by RELAT_1:61;
A3: |.f.| | X = |.(f | X).| by RFUNCT_1:46;
assume f | X is bounded ; ::_thesis: PreNorms f is bounded_above
then |.f.| | X is bounded by A3, Lm2;
then consider p being real number such that
A4: for c being set st c in dom (|.f.| | X) holds
|.((|.f.| | X) . c).| <= p by RFUNCT_1:72;
A5: now__::_thesis:_for_c_being_Element_of_X_st_c_in_X_/\_(dom_f)_holds_
|.(f_._c).|_<=_p
let c be Element of X; ::_thesis: ( c in X /\ (dom f) implies |.(f . c).| <= p )
assume A6: c in X /\ (dom f) ; ::_thesis: |.(f . c).| <= p
|.((|.f.| | X) . c).| = |.(|.f.| . c).| by A1, A2, A6, FUNCT_1:47
.= |.|.(f . c).|.| by VALUED_1:18 ;
hence |.(f . c).| <= p by A1, A2, A4, A6; ::_thesis: verum
end;
A7: X /\ (dom f) = X /\ X by FUNCT_2:def_1;
A8: now__::_thesis:_for_r_being_ext-real_number_st_r_in_PreNorms_f_holds_
r_<=_p
let r be ext-real number ; ::_thesis: ( r in PreNorms f implies r <= p )
assume r in PreNorms f ; ::_thesis: r <= p
then consider t being Element of X such that
A9: r = |.(f . t).| ;
thus r <= p by A7, A9, A5; ::_thesis: verum
end;
p is UpperBound of PreNorms f by A8, XXREAL_2:def_1;
hence PreNorms f is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
theorem Th11: :: CC0SP1:11
for X being non empty set
for f being Function of X,COMPLEX 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,COMPLEX holds
( f | X is bounded iff PreNorms f is bounded_above )
let f be Function of X,COMPLEX; ::_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_)
assume A1: PreNorms f is bounded_above ; ::_thesis: ex K being Real st f | X is bounded
reconsider K = upper_bound (PreNorms f) as Real ;
A2: now__::_thesis:_for_t_being_Element_of_X_st_t_in_X_/\_(dom_f)_holds_
|.(f_/._t).|_<=_K
let t be Element of X; ::_thesis: ( t in X /\ (dom f) implies |.(f /. t).| <= K )
assume t in X /\ (dom f) ; ::_thesis: |.(f /. t).| <= K
|.(f . t).| in PreNorms f ;
hence |.(f /. t).| <= K by A1, SEQ_4:def_1; ::_thesis: verum
end;
take K = K; ::_thesis: f | X is bounded
thus f | X is bounded by A2, CFUNCT_1:69; ::_thesis: verum
end;
hence ( f | X is bounded iff PreNorms f is bounded_above ) by Th10; ::_thesis: verum
end;
definition
let X be non empty set ;
func ComplexBoundedFunctionsNorm X -> Function of (ComplexBoundedFunctions X),REAL means :Def9: :: CC0SP1:def 9
for x being set st x in ComplexBoundedFunctions X holds
it . x = upper_bound (PreNorms (modetrans (x,X)));
existence
ex b1 being Function of (ComplexBoundedFunctions X),REAL st
for x being set st x in ComplexBoundedFunctions 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 ComplexBoundedFunctions X holds
H1(z) in REAL ;
ex f being Function of (ComplexBoundedFunctions X),REAL st
for x being set st x in ComplexBoundedFunctions X holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of (ComplexBoundedFunctions X),REAL st
for x being set st x in ComplexBoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (ComplexBoundedFunctions X),REAL st ( for x being set st x in ComplexBoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in ComplexBoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (ComplexBoundedFunctions X),REAL; ::_thesis: ( ( for x being set st x in ComplexBoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in ComplexBoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in ComplexBoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) and
A3: for x being set st x in ComplexBoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ; ::_thesis: NORM1 = NORM2
A4: ( dom NORM1 = ComplexBoundedFunctions X & dom NORM2 = ComplexBoundedFunctions X ) by FUNCT_2:def_1;
for z being set st z in ComplexBoundedFunctions X holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in ComplexBoundedFunctions X implies NORM1 . z = NORM2 . z )
assume A5: z in ComplexBoundedFunctions 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;
hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CC0SP1:def_9_:_
for X being non empty set
for b2 being Function of (ComplexBoundedFunctions X),REAL holds
( b2 = ComplexBoundedFunctionsNorm X iff for x being set st x in ComplexBoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) );
theorem Th12: :: CC0SP1:12
for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
modetrans (f,X) = f
proof
let X be non empty set ; ::_thesis: for f being Function of X,COMPLEX st f | X is bounded holds
modetrans (f,X) = f
let f be Function of X,COMPLEX; ::_thesis: ( f | X is bounded implies modetrans (f,X) = f )
assume f | X is bounded ; ::_thesis: modetrans (f,X) = f
then f in ComplexBoundedFunctions X ;
hence modetrans (f,X) = f by Def7; ::_thesis: verum
end;
theorem Th13: :: CC0SP1:13
for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
proof
let X be non empty set ; ::_thesis: for f being Function of X,COMPLEX st f | X is bounded holds
(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
let f be Function of X,COMPLEX; ::_thesis: ( f | X is bounded implies (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f) )
assume A1: f | X is bounded ; ::_thesis: (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
then f in ComplexBoundedFunctions X ;
then (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms (modetrans (f,X))) by Def9;
hence (ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f) by Th12, A1; ::_thesis: verum
end;
definition
let X be non empty set ;
func C_Normed_Algebra_of_BoundedFunctions X -> Normed_Complex_AlgebraStr equals :: CC0SP1:def 10
Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #);
correctness
coherence
Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #) is Normed_Complex_AlgebraStr ;
;
end;
:: deftheorem defines C_Normed_Algebra_of_BoundedFunctions CC0SP1:def_10_:_
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X = Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #);
registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> non empty ;
correctness
coherence
not C_Normed_Algebra_of_BoundedFunctions X is empty ;
;
end;
Lm3: now__::_thesis:_for_X_being_non_empty_set_
for_x,_e_being_Element_of_(C_Normed_Algebra_of_BoundedFunctions_X)_st_e_=_One__((ComplexBoundedFunctions_X),(CAlgebra_X))_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be non empty set ; ::_thesis: for x, e being Element of (C_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) holds
( x * e = x & e * x = x )
set F = C_Normed_Algebra_of_BoundedFunctions X;
let x, e be Element of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) implies ( x * e = x & e * x = x ) )
set X1 = ComplexBoundedFunctions X;
reconsider f = x as Element of ComplexBoundedFunctions X ;
assume A1: e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) ; ::_thesis: ( x * e = x & e * x = x )
then x * e = (mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (f,(1_ (CAlgebra X))) by C0SP1:def_8;
then A2: x * e = ( the multF of (CAlgebra X) || (ComplexBoundedFunctions X)) . (f,(1_ (CAlgebra X))) by C0SP1:def_6;
e * x = (mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . ((1_ (CAlgebra X)),f) by A1, C0SP1:def_8;
then A3: e * x = ( the multF of (CAlgebra X) || (ComplexBoundedFunctions X)) . ((1_ (CAlgebra X)),f) by C0SP1:def_6;
A4: 1_ (CAlgebra X) = 1_ (C_Algebra_of_BoundedFunctions X) by Th9;
then [f,(1_ (CAlgebra X))] in [:(ComplexBoundedFunctions X),(ComplexBoundedFunctions X):] by ZFMISC_1:87;
then x * e = f * (1_ (CAlgebra X)) by A2, FUNCT_1:49;
hence x * e = x by VECTSP_1:def_4; ::_thesis: e * x = x
[(1_ (CAlgebra X)),f] in [:(ComplexBoundedFunctions X),(ComplexBoundedFunctions X):] by A4, ZFMISC_1:87;
then e * x = (1_ (CAlgebra 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 C_Normed_Algebra_of_BoundedFunctions X -> unital ;
correctness
coherence
C_Normed_Algebra_of_BoundedFunctions X is unital ;
proof
reconsider e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) as Element of (C_Normed_Algebra_of_BoundedFunctions X) ;
take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions X) holds
( b1 * e = b1 & e * b1 = b1 )
thus for b1 being Element of the carrier of (C_Normed_Algebra_of_BoundedFunctions X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm3; ::_thesis: verum
end;
end;
theorem Th14: :: CC0SP1:14
for W being Normed_Complex_AlgebraStr
for V being ComplexAlgebra st ComplexAlgebraStr(# 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 ComplexAlgebra
proof
let W be Normed_Complex_AlgebraStr ; ::_thesis: for V being ComplexAlgebra st ComplexAlgebraStr(# 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 ComplexAlgebra
let V be ComplexAlgebra; ::_thesis: ( ComplexAlgebraStr(# 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 ComplexAlgebra )
assume A1: ComplexAlgebraStr(# 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 ComplexAlgebra
reconsider W = W as non empty ComplexAlgebraStr 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 Complex; :: according to CLVECT_1:def_2 ::_thesis: for b1, b2 being Element of the carrier of W holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be VECTOR 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 CLVECT_1:def_2;
hence a * (x + y) = (a * x) + (a * y) by A1; ::_thesis: verum
end;
A11: W is scalar-distributive
proof
let a, b be Complex; :: according to CLVECT_1:def_3 ::_thesis: for b1 being Element of the carrier of W holds K36(a,b) * b1 = (a * b1) + (b * b1)
let x be VECTOR of W; ::_thesis: K36(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 CLVECT_1:def_3;
hence (a + b) * x = (a * x) + (b * x) by A1; ::_thesis: verum
end;
A12: W is scalar-associative
proof
let a, b be Complex; :: according to CLVECT_1:def_4 ::_thesis: for b1 being Element of the carrier of W holds K37(a,b) * b1 = a * (b * b1)
let x be VECTOR of W; ::_thesis: K37(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 CLVECT_1:def_4;
hence (a * b) * x = a * (b * x) by A1; ::_thesis: verum
end;
A13: W is vector-associative
proof
let x, y be VECTOR of W; :: according to CFUNCDOM:def_9 ::_thesis: for b1 being Element of COMPLEX holds b1 * (x * y) = (b1 * x) * y
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Element of COMPLEX ; ::_thesis: a * (x * y) = (a * x) * y
a * (x * y) = a * (x1 * y1) by A1;
then a * (x * y) = (a * x1) * y1 by CFUNCDOM: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, z = 0. W 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 ComplexAlgebra 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 Th15: :: CC0SP1:15
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra
proof
let X be non empty set ; ::_thesis: C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra
set W = C_Normed_Algebra_of_BoundedFunctions X;
set V = C_Algebra_of_BoundedFunctions X;
C_Algebra_of_BoundedFunctions X is ComplexAlgebra ;
hence C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra by Th14; ::_thesis: verum
end;
theorem :: CC0SP1:16
for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F
proof
let X be non empty set ; ::_thesis: for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F
let F be Point of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F
set X1 = ComplexBoundedFunctions X;
reconsider f1 = F as Element of ComplexBoundedFunctions X ;
A1: [1r,f1] in [:COMPLEX,(ComplexBoundedFunctions X):] ;
(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = ( the Mult of (CAlgebra X) | [:COMPLEX,(ComplexBoundedFunctions X):]) . (1r,f1) by Def3
.= the Mult of (CAlgebra X) . (1r,f1) by A1, FUNCT_1:49
.= F by CFUNCDOM:12 ;
hence (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F ; ::_thesis: verum
end;
theorem Th17: :: CC0SP1:17
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace
proof
let X be non empty set ; ::_thesis: C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace
for v being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 1r * v = v
proof
let v be Point of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: 1r * v = v
reconsider v1 = v as Element of ComplexBoundedFunctions X ;
A1: 1r * v = ( the Mult of (CAlgebra X) | [:COMPLEX,(ComplexBoundedFunctions X):]) . [1r,v1] by Def3
.= the Mult of (CAlgebra X) . (1r,v1) by FUNCT_1:49
.= v1 by CFUNCDOM:12 ;
thus 1r * v = v by A1; ::_thesis: verum
end;
hence C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace by Th15, CLVECT_1:def_5; ::_thesis: verum
end;
theorem Th18: :: CC0SP1:18
for X being non empty set holds X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X)
proof
let X be non empty set ; ::_thesis: X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X)
X --> 0 = 0. (C_Algebra_of_BoundedFunctions X) by Th8;
hence X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: verum
end;
theorem Th19: :: CC0SP1:19
for X being non empty set
for x being Element of X
for f being Function of X,COMPLEX
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
proof
let X be non empty set ; ::_thesis: for x being Element of X
for f being Function of X,COMPLEX
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
let x be Element of X; ::_thesis: for f being Function of X,COMPLEX
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
let f be Function of X,COMPLEX; ::_thesis: for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
let F be Point of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & f | X is bounded implies |.(f . x).| <= ||.F.|| )
assume that
A1: f = F and
A2: f | X is bounded ; ::_thesis: |.(f . x).| <= ||.F.||
reconsider r = |.(f . x).| as ext-real number ;
A3: r in PreNorms f ;
( not PreNorms f is empty & PreNorms f is bounded_above ) by Th11, A2;
then r <= upper_bound (PreNorms f) by A3, SEQ_4:def_1;
hence |.(f . x).| <= ||.F.|| by A1, A2, Th13; ::_thesis: verum
end;
theorem :: CC0SP1:20
for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
proof
let X be non empty set ; ::_thesis: for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
let F be Point of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: 0 <= ||.F.||
F in ComplexBoundedFunctions X ;
then consider g being Function of X,COMPLEX such that
A1: F = g and
A2: g | X is bounded ;
consider r0 being set such that
A3: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r1 = r0 as Real by A3;
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 = |.(g . t).| ;
hence 0 <= r ; ::_thesis: verum
end;
then A4: 0 <= r1 by A3;
( not PreNorms g is empty & PreNorms g is bounded_above ) by Th11, A2;
then 0 <= upper_bound (PreNorms g) by A3, A4, SEQ_4:def_1;
hence 0 <= ||.F.|| by A1, A2, Th13; ::_thesis: verum
end;
theorem Th21: :: CC0SP1:21
for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st F = 0. (C_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
proof
let X be non empty set ; ::_thesis: for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st F = 0. (C_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
let F be Point of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies 0 = ||.F.|| )
set z = X --> 0;
reconsider z = X --> 0c as Function of X,COMPLEX ;
F in ComplexBoundedFunctions X ;
then consider g being Function of X,COMPLEX such that
A1: g = F and
A2: g | X is bounded ;
A3: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A2, Th11;
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. (C_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 = |.(g . t).| ;
z = g by A6, A1, Th18;
then |.(g . t).| = |.0.| by FUNCOP_1:7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A8; ::_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, Th13; ::_thesis: verum
end;
theorem Th22: :: CC0SP1:22
for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_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,COMPLEX
for F, G, H being Point of (C_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,COMPLEX; ::_thesis: for F, G, H being Point of (C_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 (C_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 (C_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, Th5; ::_thesis: verum
end;
theorem Th23: :: CC0SP1:23
for X being non empty set
for a being Complex
for f, g being Function of X,COMPLEX
for F, G being Point of (C_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 Complex
for f, g being Function of X,COMPLEX
for F, G being Point of (C_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 Complex; ::_thesis: for f, g being Function of X,COMPLEX
for F, G being Point of (C_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,COMPLEX; ::_thesis: for F, G being Point of (C_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 (C_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 (C_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, Th6; ::_thesis: verum
end;
theorem Th24: :: CC0SP1:24
for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_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,COMPLEX
for F, G, H being Point of (C_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,COMPLEX; ::_thesis: for F, G, H being Point of (C_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 (C_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 (C_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, Th7; ::_thesis: verum
end;
theorem Th25: :: CC0SP1:25
for X being non empty set
for a being Complex
for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proof
let X be non empty set ; ::_thesis: for a being Complex
for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let a be Complex; ::_thesis: for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1: now__::_thesis:_(_F_=_0._(C_Normed_Algebra_of_BoundedFunctions_X)_implies_||.F.||_=_0_)
set z = X --> 0c;
reconsider z = X --> 0c as Function of X,COMPLEX ;
F in ComplexBoundedFunctions X ;
then consider g being Function of X,COMPLEX such that
A2: F = g and
A3: g | X is bounded ;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A3, Th11;
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. (C_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: ||.F.|| = 0
then A7: z = g by A2, Th18;
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 = |.(g . t).| ;
|.(g . t).| = |.0.| by A7, FUNCOP_1:7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A9; ::_thesis: verum
end;
then 0 <= r0 by A5;
then upper_bound (PreNorms g) = 0 by A8, A4, A6, A5, SEQ_4:def_1;
hence ||.F.|| = 0 by A2, A3, Th13; ::_thesis: verum
end;
A10: ||.(F + G).|| <= ||.F.|| + ||.G.||
proof
F + G in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A11: h1 = F + G and
A12: h1 | X is bounded ;
G in ComplexBoundedFunctions X ;
then consider g1 being Function of X,COMPLEX such that
A13: g1 = G and
A14: g1 | X is bounded ;
F in ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A15: f1 = F and
A16: f1 | X is bounded ;
A17: now__::_thesis:_for_t_being_Element_of_X_holds_|.(h1_._t).|_<=_||.F.||_+_||.G.||
let t be Element of X; ::_thesis: |.(h1 . t).| <= ||.F.|| + ||.G.||
( |.(f1 . t).| <= ||.F.|| & |.(g1 . t).| <= ||.G.|| ) by A15, A16, A13, A14, Th19;
then A18: |.(f1 . t).| + |.(g1 . t).| <= ||.F.|| + ||.G.|| by XREAL_1:7;
( |.(h1 . t).| = |.((f1 . t) + (g1 . t)).| & |.((f1 . t) + (g1 . t)).| <= |.(f1 . t).| + |.(g1 . t).| ) by A15, A13, A11, Th22, COMPLEX1:56;
hence |.(h1 . t).| <= ||.F.|| + ||.G.|| by A18, XXREAL_0:2; ::_thesis: verum
end;
A19: now__::_thesis:_for_r_being_real_number_st_r_in_PreNorms_h1_holds_
r_<=_||.F.||_+_||.G.||
let r be real number ; ::_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 = |.(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, Th13; ::_thesis: verum
end;
A20: ||.(a * F).|| = |.a.| * ||.F.||
proof
F in ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A21: f1 = F and
A22: f1 | X is bounded ;
a * F in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A23: h1 = a * F and
A24: h1 | X is bounded ;
A25: now__::_thesis:_for_t_being_Element_of_X_holds_|.(h1_._t).|_<=_|.a.|_*_||.F.||
let t be Element of X; ::_thesis: |.(h1 . t).| <= |.a.| * ||.F.||
|.(h1 . t).| = |.(a * (f1 . t)).| by A21, A23, Th23;
then |.(h1 . t).| = |.a.| * |.(f1 . t).| by COMPLEX1:65;
hence |.(h1 . t).| <= |.a.| * ||.F.|| by A21, A22, Th19, XREAL_1:64; ::_thesis: verum
end;
A26: now__::_thesis:_for_r_being_real_number_st_r_in_PreNorms_h1_holds_
r_<=_|.a.|_*_||.F.||
let r be real number ; ::_thesis: ( r in PreNorms h1 implies r <= |.a.| * ||.F.|| )
assume r in PreNorms h1 ; ::_thesis: r <= |.a.| * ||.F.||
then ex t being Element of X st r = |.(h1 . t).| ;
hence r <= |.a.| * ||.F.|| by A25; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms h1 holds
s <= |.a.| * ||.F.|| ) implies upper_bound (PreNorms h1) <= |.a.| * ||.F.|| ) by SEQ_4:45;
then A27: ||.(a * F).|| <= |.a.| * ||.F.|| by A23, A24, A26, Th13;
percases ( a <> 0 or a = 0 ) ;
supposeA28: a <> 0 ; ::_thesis: ||.(a * F).|| = |.a.| * ||.F.||
A29: now__::_thesis:_for_t_being_Element_of_X_holds_|.(f1_._t).|_<=_(|.a.|_")_*_||.(a_*_F).||
let t be Element of X; ::_thesis: |.(f1 . t).| <= (|.a.| ") * ||.(a * F).||
|.(a ").| = |.(1 / a).| ;
then A30: |.(a ").| = 1 / |.a.| by COMPLEX1:80;
h1 . t = a * (f1 . t) by A21, A23, Th23;
then (a ") * (h1 . t) = ((a ") * a) * (f1 . t) ;
then A31: (a ") * (h1 . t) = 1 * (f1 . t) by A28, XCMPLX_0:def_7;
( |.((a ") * (h1 . t)).| = |.(a ").| * |.(h1 . t).| & 0 <= |.(a ").| ) by COMPLEX1:65;
hence |.(f1 . t).| <= (|.a.| ") * ||.(a * F).|| by A23, A24, A31, A30, Th19, XREAL_1:64; ::_thesis: verum
end;
A32: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_
r_<=_(|.a.|_")_*_||.(a_*_F).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= (|.a.| ") * ||.(a * F).|| )
assume r in PreNorms f1 ; ::_thesis: r <= (|.a.| ") * ||.(a * F).||
then ex t being Element of X st r = |.(f1 . t).| ;
hence r <= (|.a.| ") * ||.(a * F).|| by A29; ::_thesis: verum
end;
( ( for s being real number st s in PreNorms f1 holds
s <= (|.a.| ") * ||.(a * F).|| ) implies upper_bound (PreNorms f1) <= (|.a.| ") * ||.(a * F).|| ) by SEQ_4:45;
then ||.F.|| <= (|.a.| ") * ||.(a * F).|| by A21, A22, A32, Th13;
then |.a.| * ||.F.|| <= |.a.| * ((|.a.| ") * ||.(a * F).||) by XREAL_1:64;
then |.a.| * ||.F.|| <= (|.a.| * (|.a.| ")) * ||.(a * F).|| ;
then |.a.| * ||.F.|| <= 1 * ||.(a * F).|| by A28, XCMPLX_0:def_7;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A27, XXREAL_0:1; ::_thesis: verum
end;
supposeA33: a = 0 ; ::_thesis: ||.(a * F).|| = |.a.| * ||.F.||
reconsider fz = F as VECTOR of (C_Algebra_of_BoundedFunctions X) ;
a * fz = (a + a) * fz by A33
.= (a * fz) + (a * fz) by CLVECT_1:def_3 ;
then 0. (C_Algebra_of_BoundedFunctions X) = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:16;
then 0. (C_Algebra_of_BoundedFunctions X) = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def_3;
then 0. (C_Algebra_of_BoundedFunctions X) = (0. (C_Algebra_of_BoundedFunctions X)) + (a * fz) by VECTSP_1:16;
then A34: a * F = 0. (C_Normed_Algebra_of_BoundedFunctions X) by RLVECT_1:4;
|.a.| * ||.F.|| = 0 * ||.F.|| by A33;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A34, Th21; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_||.F.||_=_0_implies_F_=_0._(C_Normed_Algebra_of_BoundedFunctions_X)_)
set z = X --> 0c;
reconsider z = X --> 0c as Function of X,COMPLEX ;
F in ComplexBoundedFunctions X ;
then consider g being Function of X,COMPLEX such that
A35: F = g and
A36: g | X is bounded ;
assume A37: ||.F.|| = 0 ; ::_thesis: F = 0. (C_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
|.(g . t).| = 0 by A35, A36, A37, Th19;
hence g . t = 0
.= z . t by FUNCOP_1:7 ;
::_thesis: verum
end;
then g = z by FUNCT_2:63;
hence F = 0. (C_Normed_Algebra_of_BoundedFunctions X) by A35, Th18; ::_thesis: verum
end;
hence ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A20, A10; ::_thesis: verum
end;
Lm4: for X being non empty set holds
( C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
proof
let X be non empty set ; ::_thesis: ( C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
thus ||.(0. (C_Normed_Algebra_of_BoundedFunctions X)).|| = 0 by Th25; :: according to NORMSP_0:def_6 ::_thesis: ( C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
for x, y being Point of (C_Normed_Algebra_of_BoundedFunctions X)
for a being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( x = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th25;
hence ( C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like ) by CLVECT_1:def_13, NORMSP_0:def_5; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
( C_Normed_Algebra_of_BoundedFunctions X is right_complementable & C_Normed_Algebra_of_BoundedFunctions X is Abelian & C_Normed_Algebra_of_BoundedFunctions X is add-associative & C_Normed_Algebra_of_BoundedFunctions X is right_zeroed & C_Normed_Algebra_of_BoundedFunctions X is vector-distributive & C_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & C_Normed_Algebra_of_BoundedFunctions X is scalar-associative & C_Normed_Algebra_of_BoundedFunctions X is scalar-unital & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like ) by Th17, Lm4;
end;
theorem Th26: :: CC0SP1:26
for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_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,COMPLEX
for F, G, H being Point of (C_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,COMPLEX; ::_thesis: for F, G, H being Point of (C_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 (C_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, Th22;
then F - G = H + (G - G) by RLVECT_1:def_3;
then F - G = H + (0. (C_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. (C_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, Th22;
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 Th27: :: CC0SP1:27
for X being non empty set
for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent
proof
let X be non empty set ; ::_thesis: for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( vseq is CCauchy implies vseq is convergent )
defpred S1[ set , set ] means ex xseq being Complex_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 CCauchy ; ::_thesis: vseq is convergent
A2: for x being Element of X ex y being Element of COMPLEX st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Element of COMPLEX st S1[x,y]
deffunc H1( Element of NAT ) -> Element of COMPLEX = (modetrans ((vseq . $1),X)) . x;
consider xseq being Complex_Sequence such that
A3: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4();
take y = lim xseq; ::_thesis: S1[x,y]
A4: for m, k being Element of NAT holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
(vseq . m) - (vseq . k) in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A5: h1 = (vseq . m) - (vseq . k) and
A6: h1 | X is bounded ;
vseq . m in ComplexBoundedFunctions X ;
then ex vseqm being Function of X,COMPLEX st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A7: modetrans ((vseq . m),X) = vseq . m by Th12;
vseq . k in ComplexBoundedFunctions X ;
then ex vseqk being Function of X,COMPLEX st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A8: modetrans ((vseq . k),X) = vseq . k by Th12;
( 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, Th26;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A5, A6, Th19; ::_thesis: verum
end;
now__::_thesis:_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_
|.((xseq_._n)_-_(xseq_._k)).|_<_e
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
|.((xseq . n) - (xseq . k)).| < e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
|.((xseq . n) - (xseq . k)).| < e
then consider k being Element of NAT such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:8;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
|.((xseq . n) - (xseq . k)).| < e
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= k implies |.((xseq . n) - (xseq . k)).| < e )
assume n >= k ; ::_thesis: |.((xseq . n) - (xseq . k)).| < e
then A10: ||.((vseq . n) - (vseq . k)).|| < e by A9;
|.((xseq . n) - (xseq . k)).| <= ||.((vseq . n) - (vseq . k)).|| by A4;
hence |.((xseq . n) - (xseq . k)).| < e by A10, XXREAL_0:2; ::_thesis: verum
end;
end;
then xseq is convergent by COMSEQ_3:46;
hence S1[x,y] by A3; ::_thesis: verum
end;
consider tseq being Function of X,COMPLEX such that
A11: 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_
|.((||.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
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )
assume A12: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A12, CSSPACE3:8;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
|.((||.vseq.||_._m)_-_(||.vseq.||_._k)).|_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )
A14: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def_4;
assume m >= k ; ::_thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
then A15: ||.((vseq . m) - (vseq . k)).|| < e by A13;
( |.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by CLVECT_1:110, NORMSP_0:def_4;
hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by A15, A14, XXREAL_0:2; ::_thesis: verum
end;
hence for m being Element of NAT st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; ::_thesis: verum
end;
then A16: ||.vseq.|| is convergent by SEQ_4:41;
now__::_thesis:_for_x_being_set_st_x_in_X_/\_(dom_tseq)_holds_
|.(tseq_._x).|_<=_lim_||.vseq.||
let x be set ; ::_thesis: ( x in X /\ (dom tseq) implies |.(tseq . x).| <= lim ||.vseq.|| )
assume A17: x in X /\ (dom tseq) ; ::_thesis: |.(tseq . x).| <= lim ||.vseq.||
then consider xseq being Complex_Sequence such that
A18: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A19: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A20: for n being Element of NAT holds |.xseq.| . n <= ||.vseq.|| . n
proof
let n be Element of NAT ; ::_thesis: |.xseq.| . n <= ||.vseq.|| . n
A21: xseq . n = (modetrans ((vseq . n),X)) . x by A18;
vseq . n in ComplexBoundedFunctions X ;
then A22: ex h1 being Function of X,COMPLEX st
( vseq . n = h1 & h1 | X is bounded ) ;
then modetrans ((vseq . n),X) = vseq . n by Th12;
then |.(xseq . n).| <= ||.(vseq . n).|| by A17, A22, A21, Th19;
then |.xseq.| . n <= ||.(vseq . n).|| by VALUED_1:18;
hence |.xseq.| . n <= ||.vseq.|| . n by NORMSP_0:def_4; ::_thesis: verum
end;
( |.xseq.| is convergent & |.(tseq . x).| = lim |.xseq.| ) by A19, SEQ_2:27;
hence |.(tseq . x).| <= lim ||.vseq.|| by A16, A20, SEQ_2:18; ::_thesis: verum
end;
then for x being Element of X st x in X /\ (dom tseq) holds
|.(tseq /. x).| <= lim ||.vseq.|| ;
then tseq | X is bounded by CFUNCT_1:69;
then tseq in ComplexBoundedFunctions X ;
then reconsider tv = tseq as Point of (C_Normed_Algebra_of_BoundedFunctions X) ;
A23: 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 |.(((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 |.(((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 |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
then consider k being Element of NAT such that
A24: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:8;
take k ; ::_thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds |.(((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_|.(((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 |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )
assume A25: n >= k ; ::_thesis: for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
now__::_thesis:_for_x_being_Element_of_X_holds_|.(((modetrans_((vseq_._n),X))_._x)_-_(tseq_._x)).|_<=_e
let x be Element of X; ::_thesis: |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
consider xseq being Complex_Sequence such that
A26: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A27: xseq is convergent and
A28: tseq . x = lim xseq by A11;
reconsider fseq = NAT --> (xseq . n) as Complex_Sequence ;
set wseq = xseq - fseq;
deffunc H1( Element of NAT ) -> Element of REAL = |.((xseq . $1) - (xseq . n)).|;
consider rseq being Real_Sequence such that
A29: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A30: for m, k being Element of NAT holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
(vseq . m) - (vseq . k) in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A31: h1 = (vseq . m) - (vseq . k) and
A32: h1 | X is bounded ;
vseq . m in ComplexBoundedFunctions X ;
then ex vseqm being Function of X,COMPLEX st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A33: modetrans ((vseq . m),X) = vseq . m by Th12;
vseq . k in ComplexBoundedFunctions X ;
then ex vseqk being Function of X,COMPLEX st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A34: modetrans ((vseq . k),X) = vseq . k by Th12;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A26;
then (xseq . m) - (xseq . k) = h1 . x by A33, A34, A31, Th26;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A31, A32, Th19; ::_thesis: verum
end;
A35: 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 A36: ||.((vseq . n) - (vseq . m)).|| < e by A24, A25;
rseq . m = |.((xseq . m) - (xseq . n)).| by A29;
then rseq . m = |.((xseq . n) - (xseq . m)).| by COMPLEX1:60;
then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A30;
hence rseq . m <= e by A36, XXREAL_0:2; ::_thesis: verum
end;
A37: 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 VALUED_1:1
.= (xseq . m) - (fseq . m) by VALUED_1:8 ;
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_=_|.(xseq_-_fseq).|_._x
let x be set ; ::_thesis: ( x in NAT implies rseq . x = |.(xseq - fseq).| . x )
assume x in NAT ; ::_thesis: rseq . x = |.(xseq - fseq).| . x
then reconsider k = x as Element of NAT ;
rseq . x = |.((xseq . k) - (xseq . n)).| by A29;
then rseq . x = |.((xseq - fseq) . k).| by A37;
hence rseq . x = |.(xseq - fseq).| . x by VALUED_1:18; ::_thesis: verum
end;
then A38: rseq = |.(xseq - fseq).| by FUNCT_2:12;
A39: fseq is convergent by CFCONT_1:26;
A40: lim rseq <= e by A39, A35, A38, A27, RSSPACE2:5;
lim fseq = fseq . 0 by CFCONT_1:28;
then lim fseq = xseq . n by FUNCOP_1:7;
then lim (xseq - fseq) = (tseq . x) - (xseq . n) by A27, A28, A39, COMSEQ_2:26;
then lim rseq = |.((tseq . x) - (xseq . n)).| by A39, A27, A38, SEQ_2:27;
then |.((xseq . n) - (tseq . x)).| <= e by A40, COMPLEX1:60;
hence |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A26; ::_thesis: verum
end;
hence for x being Element of X holds |.(((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 |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e ; ::_thesis: verum
end;
A41: 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
A42: for n being Element of NAT st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A23;
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 A43: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e
vseq . n in ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A44: f1 = vseq . n and
f1 | X is bounded ;
(vseq . n) - tv in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A45: h1 = (vseq . n) - tv and
A46: h1 | X is bounded ;
A47: now__::_thesis:_for_t_being_Element_of_X_holds_|.(h1_._t).|_<=_e
let t be Element of X; ::_thesis: |.(h1 . t).| <= e
( modetrans ((vseq . n),X) = f1 & h1 . t = (f1 . t) - (tseq . t) ) by A44, A45, Def7, Th26;
hence |.(h1 . t).| <= e by A42, A43; ::_thesis: verum
end;
A48: 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 = |.(h1 . t).| ;
hence r <= e by A47; ::_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 A45, A46, A48, Th13; ::_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 A49: 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
A50: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A41, A49;
take m ; ::_thesis: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
A51: e / 2 < e by A49, 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 A50;
hence ||.((vseq . n) - tv).|| < e by A51, XXREAL_0:2; ::_thesis: verum
end;
end;
hence vseq is convergent by CLVECT_1:def_15; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X -> complete ;
coherence
C_Normed_Algebra_of_BoundedFunctions X is complete
proof
for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent by Th27;
hence C_Normed_Algebra_of_BoundedFunctions X is complete by CLOPBAN1:def_13; ::_thesis: verum
end;
end;
theorem :: CC0SP1:28
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra
proof
let X be non empty set ; ::_thesis: C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra
set B = C_Normed_Algebra_of_BoundedFunctions X;
reconsider B = C_Normed_Algebra_of_BoundedFunctions X as Normed_Complex_Algebra by Th15;
set X1 = ComplexBoundedFunctions X;
1. B in ComplexBoundedFunctions X ;
then consider ONE being Function of X,COMPLEX such that
A1: ONE = 1. B and
A2: ONE | X is bounded ;
1. B = 1_ (C_Algebra_of_BoundedFunctions X) ;
then A3: 1. B = X --> 1r by Th9;
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 = |.((X --> 1) . t).| by A1, A3;
thus s = 1 by A5, COMPLEX1:48, FUNCOP_1:7; ::_thesis: verum
end;
assume s = 1 ; ::_thesis: s in PreNorms ONE
hence s in PreNorms ONE by A1, A3, A4, COMPLEX1:48; ::_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, Th13;
A7: now__::_thesis:_for_a_being_Complex
for_f,_g_being_Element_of_B_holds_a_*_(f_*_g)_=_f_*_(a_*_g)
let a be Complex; ::_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 ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A8: f1 = f and
f1 | X is bounded ;
g in ComplexBoundedFunctions X ;
then consider g1 being Function of X,COMPLEX such that
A9: g1 = g and
g1 | X is bounded ;
a * (f * g) in ComplexBoundedFunctions X ;
then consider h3 being Function of X,COMPLEX such that
A10: h3 = a * (f * g) and
h3 | X is bounded ;
f * g in ComplexBoundedFunctions X ;
then consider h2 being Function of X,COMPLEX such that
A11: h2 = f * g and
h2 | X is bounded ;
a * g in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX 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, Th23;
then h3 . x = a * ((f1 . x) * (g1 . x)) by A8, A9, A11, Th24;
then h3 . x = (f1 . x) * (a * (g1 . x)) ;
hence h3 . x = (f1 . x) * (h1 . x) by A9, A12, Th23; ::_thesis: verum
end;
hence a * (f * g) = f * (a * g) by A8, A12, A10, Th24; ::_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 ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A14: f1 = f and
A15: f1 | X is bounded ;
g in ComplexBoundedFunctions X ;
then consider g1 being Function of X,COMPLEX such that
A16: g1 = g and
A17: g1 | X is bounded ;
A18: ( not PreNorms g1 is empty & PreNorms g1 is bounded_above ) by A17, Th10;
f * g in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX 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, Th10;
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 = |.(h1 . t).| ;
|.(g1 . t).| in PreNorms g1 ;
then A23: |.(g1 . t).| <= upper_bound (PreNorms g1) by A18, SEQ_4:def_1;
|.(f1 . t).| in PreNorms f1 ;
then A24: |.(f1 . t).| <= upper_bound (PreNorms f1) by A21, SEQ_4:def_1;
then A25: (upper_bound (PreNorms f1)) * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A23, XREAL_1:64;
A26: |.(f1 . t).| * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * |.(g1 . t).| by A24, XREAL_1:64;
|.(h1 . t).| = |.((f1 . t) * (g1 . t)).| by A14, A16, A19, Th24;
then abs (h1 . t) = |.(f1 . t).| * |.(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, Th13;
||.f.|| = upper_bound (PreNorms f1) by A14, A15, Th13;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A19, A20, A28, A27, Th13; ::_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 ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A30: f1 = f and
f1 | X is bounded ;
h in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A31: h1 = h and
h1 | X is bounded ;
g in ComplexBoundedFunctions X ;
then consider g1 being Function of X,COMPLEX such that
A32: g1 = g and
g1 | X is bounded ;
(g + h) * f in ComplexBoundedFunctions X ;
then consider F1 being Function of X,COMPLEX such that
A33: F1 = (g + h) * f and
F1 | X is bounded ;
h * f in ComplexBoundedFunctions X ;
then consider hf1 being Function of X,COMPLEX such that
A34: hf1 = h * f and
hf1 | X is bounded ;
g * f in ComplexBoundedFunctions X ;
then consider gf1 being Function of X,COMPLEX such that
A35: gf1 = g * f and
gf1 | X is bounded ;
g + h in ComplexBoundedFunctions X ;
then consider gPh1 being Function of X,COMPLEX 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, Th24;
then F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by A32, A31, A36, Th22;
then F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by A30, A32, A35, Th24;
hence F1 . x = (gf1 . x) + (hf1 . x) by A30, A31, A34, Th24; ::_thesis: verum
end;
hence (g + h) * f = (g * f) + (h * f) by A35, A34, A33, Th22; ::_thesis: verum
end;
for f being Element of B holds (1. B) * f = f by Lm3;
then A37: B is left_unital by VECTSP_1:def_8;
A38: B is Banach_Algebra-like_1 by A13, CLOPBAN2:def_9;
A39: B is Banach_Algebra-like_2 by A6, CLOPBAN2:def_10;
A40: B is Banach_Algebra-like_3 by A7, CLOPBAN2:def_11;
B is left-distributive by A29, VECTSP_1:def_3;
hence C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra by A37, A38, A39, A40; ::_thesis: verum
end;