:: 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;