:: Banach Algebra of Bounded Functionals
::  by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_1, IDEAL_1, ARYTM_3,
      FUNCSDOM, STRUCT_0, TARSKI, REALSET1, MESFUNC1, SUPINF_2, BINOP_1,
      FUNCT_1, ZFMISC_1, RELAT_1, RLVECT_1, VECTSP_1, LATTICES, RSSPACE,
      GROUP_1, REAL_1, POLYALG1, CARD_1, RSSPACE4, XXREAL_2, FUNCOP_1, FUNCT_2,
      VALUED_1, LOPBAN_1, COMPLEX1, XXREAL_0, SEQ_4, ORDINAL2, LOPBAN_2,
      PRE_TOPC, NORMSP_1, NAT_1, RSSPACE3, SEQ_2, SEQ_1, REWRITE1, C0SP1,
      METRIC_1, RELAT_2, FUNCT_7, ASYMPT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
      XCMPLX_0, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, STRUCT_0, ALGSTR_0,
      REAL_1, REALSET1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, RELSET_1,
      PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM, PARTFUN1, IDEAL_1,
      RSSPACE3, VALUED_1, SEQ_1, SEQ_2, SEQ_4, FUNCOP_1, NORMSP_0, NORMSP_1,
      LOPBAN_1, LOPBAN_2;
 constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, BINOP_2, LOPBAN_2, SEQ_2,
      IDEAL_1, SEQ_4, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0,
      NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, XXREAL_0, RLVECT_1, VECTSP_1,
      VECTSP_2, FUNCT_2, VALUED_0, VALUED_1, LOPBAN_2, FUNCOP_1, SEQ_4,
      RFUNCT_1, RELSET_1, SEQ_1, SEQ_2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin :: Some properties of Rings

definition
  let V be non empty addLoopStr;
  let V1 be Subset of V;
  attr V1 is having-inverse means
:: C0SP1:def 1

  for v be Element of V st v in V1 holds -v in V1;
end;

definition
  let V be non empty addLoopStr;
  let V1 be Subset of V;
  attr V1 is additively-closed means
:: C0SP1:def 2

  V1 is add-closed having-inverse;
end;

registration
  let V be non empty addLoopStr;
  cluster [#]V -> add-closed having-inverse;
end;

registration
  let V be non empty doubleLoopStr;
  cluster additively-closed -> add-closed having-inverse for Subset of V;
  cluster add-closed having-inverse -> additively-closed for Subset of V;
end;

registration
  let V be non empty addLoopStr;
  cluster add-closed having-inverse non empty for Subset of V;
end;

definition
  let V be Ring;
  mode Subring of V -> Ring means
:: C0SP1:def 3

    the carrier of it c= the carrier of V
  & the addF of it = (the addF of V)||the carrier of it
  & the multF of it = (the multF of V)||the carrier of it
  & 1.it=1.V & 0.it = 0.V;
end;

reserve X for non empty set;
reserve x for Element of X;
reserve d1,d2 for Element of X;
reserve A for BinOp of X;
reserve M for Function of [:X,X:],X;
reserve V for Ring;
reserve V1 for Subset of V;

theorem :: C0SP1:1
  V1 = X & A = (the addF of V)||V1 & M = (the multF of V)||V1 & d1
= 1.V & d2 = 0.V & V1 is having-inverse implies doubleLoopStr (# X,A,M,d1,d2 #)
  is Subring of V;

registration
  let V be Ring;
  cluster strict for Subring of V;
end;

definition
  let V be non empty multLoopStr_0;
  let V1 be Subset of V;
  attr V1 is multiplicatively-closed means
:: C0SP1:def 4

  1.V in V1 & for v,u be Element of V st v in V1 & u in V1 holds v * u in V1;
end;

definition
  let V be non empty addLoopStr, V1 be Subset of V such that
 V1 is add-closed non empty;
  func Add_(V1,V) -> BinOp of V1 equals
:: C0SP1:def 5

  (the addF of V)||V1;
end;

definition
  let V be non empty multLoopStr_0, V1 be Subset of V such that
 V1 is multiplicatively-closed non empty;
  func mult_(V1,V) -> BinOp of V1 equals
:: C0SP1:def 6

  (the multF of V)||V1;
end;

definition
  let V be add-associative right_zeroed right_complementable non empty
  doubleLoopStr, V1 be Subset of V such that
 V1 is add-closed having-inverse non empty;
  func Zero_(V1,V) -> Element of V1 equals
:: C0SP1:def 7

  0.V;
end;

definition
  let V be non empty multLoopStr_0, V1 be Subset of V such that
 V1 is multiplicatively-closed non empty;
  func One_(V1,V) -> Element of V1 equals
:: C0SP1:def 8

  1.V;
end;

theorem :: C0SP1:2
  V1 is additively-closed multiplicatively-closed non empty implies
  doubleLoopStr(# V1,Add_(V1,V),mult_(V1,V),One_(V1,V),Zero_(V1,V) #) is Ring;

begin :: Some properties of Algebras

reserve V for Algebra;
reserve V1 for Subset of V;

reserve MR for Function of [:REAL,X:],X;
reserve a for Real;

definition
  let V be Algebra;
  mode Subalgebra of V -> Algebra means
:: C0SP1:def 9

    the carrier of it c= the
carrier of V & the addF of it = (the addF of V)||the carrier of it & the multF
of it = (the multF of V)||the carrier of it & the Mult of it = (the Mult of V)
    | [:REAL,the carrier of it:] & 1.it = 1.V & 0.it = 0.V;
end;

theorem :: C0SP1:3
  V1 = X & d1 = 0.V & d2 = 1.V & A = (the addF of V)||V1 & M = (the
  multF of V)||V1 & MR = (the Mult of V) | [:REAL,V1:] & V1 is having-inverse
  implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V;

registration
  let V be Algebra;
  cluster strict for Subalgebra of V;
end;

definition
  let V be Algebra, V1 be Subset of V;
  attr V1 is additively-linearly-closed means
:: C0SP1:def 10

  V1 is add-closed
having-inverse & for a be Real, v be Element of V st v in V1 holds a * v in V1;
end;

registration
  let V be Algebra;
  cluster additively-linearly-closed -> additively-closed for Subset of V;
end;

definition
  let V be Algebra, V1 be Subset of V such that
 V1 is additively-linearly-closed non empty;
  func Mult_(V1,V) -> Function of [:REAL,V1:], V1 equals
:: C0SP1:def 11

  (the Mult of V) | [:REAL,V1:];
end;

definition
  let V be non empty RLSStruct;
  attr V is scalar-mult-cancelable means
:: C0SP1:def 12

  for a be Real, v be Element of V st a*v=0.V holds a=0 or v=0.V;
end;

theorem :: C0SP1:4
  for V being add-associative right_zeroed right_complementable
  vector-distributive scalar-distributive scalar-associative
  vector-associative non empty AlgebraStr, a be Real holds a*0.V = 0.V;

theorem :: C0SP1:5
  for V being Abelian add-associative right_zeroed right_complementable
  vector-distributive scalar-distributive scalar-associative
  vector-associative non empty AlgebraStr st V is scalar-mult-cancelable
  holds V is RealLinearSpace;

theorem :: C0SP1:6
  V1 is additively-linearly-closed multiplicatively-closed non
empty implies AlgebraStr(# V1,mult_(V1,V), Add_(V1,V), Mult_(V1,V), One_(V1,V),
    Zero_(V1,V) #) is Subalgebra of V;

registration
  let X be non empty set;
  cluster RAlgebra X -> Abelian add-associative right_zeroed
right_complementable commutative associative right_unital right-distributive
    vector-distributive scalar-distributive scalar-associative
    vector-associative;
end;

theorem :: C0SP1:7
  RAlgebra X is RealLinearSpace;

theorem :: C0SP1:8
  for V be Algebra, V1 be Subalgebra of V holds
  ( for v1,w1 be Element of V1, v,w be Element of V st v1=v & w1=w
   holds v1+w1=v+w ) &
   ( for v1,  w1 be Element of V1, v,w be Element of V st v1=v & w1=w
    holds v1*w1=v*w ) & (
for v1 be Element of V1, v be Element of V,
    a be Real st v1=v holds a*v1=a*v )
  & 1_V1 = 1_V & 0.V1=0.V;

begin :: Banach Algebra of Bounded Functionals

definition
  let X be non empty set;
  func BoundedFunctions X -> non empty Subset of RAlgebra X equals
:: C0SP1:def 13
  { f where f
  is Function of X,REAL : f|X is bounded };
end;

theorem :: C0SP1:9
  BoundedFunctions X is additively-linearly-closed multiplicatively-closed;

registration
  let X;
  cluster BoundedFunctions X -> additively-linearly-closed
    multiplicatively-closed;
end;

definition
  let X be non empty set;
  func R_Algebra_of_BoundedFunctions X -> Algebra equals
:: C0SP1:def 14
  AlgebraStr (#
BoundedFunctions X, mult_(BoundedFunctions X,RAlgebra X), Add_(BoundedFunctions
X,RAlgebra X), Mult_(BoundedFunctions X,RAlgebra X), One_(BoundedFunctions X,
    RAlgebra X), Zero_(BoundedFunctions X,RAlgebra X) #);
end;

theorem :: C0SP1:10
  R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X;

theorem :: C0SP1:11
  R_Algebra_of_BoundedFunctions X is RealLinearSpace;

reserve F,G,H for VECTOR of R_Algebra_of_BoundedFunctions X;
reserve f,g,h for Function of X,REAL;

theorem :: C0SP1:12
  f=F & g=G & h=H implies ( H = F+G iff for x be Element of X
  holds h.x = f.x + g.x );

theorem :: C0SP1:13
  f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x );

theorem :: C0SP1:14
  f=F & g=G & h=H implies ( H = F*G iff for x be Element of X
  holds h.x = f.x * g.x );

theorem :: C0SP1:15
  0.R_Algebra_of_BoundedFunctions X = X -->0;

theorem :: C0SP1:16
  1_R_Algebra_of_BoundedFunctions X = X -->1;

definition
  let X be non empty set, F be object such that
 F in BoundedFunctions X;
  func modetrans(F,X) -> Function of X,REAL means
:: C0SP1:def 15

  it=F & it|X is bounded;
end;

definition
  let X be non empty set, f be Function of X,REAL;
  func PreNorms f -> non empty Subset of REAL equals
:: C0SP1:def 16
  the set of all  |.f.x.| where x is Element of X ;
end;

theorem :: C0SP1:17
  f|X is bounded implies PreNorms f is bounded_above;

theorem :: C0SP1:18
  f|X is bounded iff PreNorms f is bounded_above;

definition
  let X be non empty set;
  func BoundedFunctionsNorm X -> Function of BoundedFunctions X,REAL means
:: C0SP1:def 17

   for x be object st x in BoundedFunctions X
  holds it.x = upper_bound PreNorms(modetrans(x,X));
end;

theorem :: C0SP1:19
  f|X is bounded implies modetrans(f,X) = f;

theorem :: C0SP1:20
  f|X is bounded implies (BoundedFunctionsNorm X).f = upper_bound PreNorms f;

definition
  let X be non empty set;
  func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals
:: C0SP1:def 18
Normed_AlgebraStr (# BoundedFunctions X, mult_(BoundedFunctions X,RAlgebra X),
Add_(BoundedFunctions X,RAlgebra X), Mult_(BoundedFunctions X,RAlgebra X), One_
    (BoundedFunctions X,RAlgebra X), Zero_(BoundedFunctions X,RAlgebra X),
    BoundedFunctionsNorm X #);
end;

registration
  let X be non empty set;
  cluster R_Normed_Algebra_of_BoundedFunctions X -> non empty;
end;

registration
  let X be non empty set;
  cluster R_Normed_Algebra_of_BoundedFunctions X -> unital;
end;

theorem :: C0SP1:21
  for W be Normed_AlgebraStr, V be Algebra st the AlgebraStr of W
  = V holds W is Algebra;

reserve F,G,H for Point of R_Normed_Algebra_of_BoundedFunctions X;

theorem :: C0SP1:22
  R_Normed_Algebra_of_BoundedFunctions X is Algebra;

theorem :: C0SP1:23
  (Mult_(BoundedFunctions X,RAlgebra X)).(1,F) = F;

theorem :: C0SP1:24
  R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace;

theorem :: C0SP1:25
  X-->0 = 0.R_Normed_Algebra_of_BoundedFunctions X;

theorem :: C0SP1:26
  f=F & f|X is bounded implies |.f.x.| <= ||.F.||;

theorem :: C0SP1:27
  0 <= ||.F.||;

theorem :: C0SP1:28
  F = 0.R_Normed_Algebra_of_BoundedFunctions X implies 0 = ||.F.||;

theorem :: C0SP1:29
  f=F & g=G & h=H implies (H = F+G iff for x be Element of X holds
  h.x = f.x + g.x);

theorem :: C0SP1:30
  f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x );

theorem :: C0SP1:31
  f=F & g=G & h=H implies (H = F*G iff for x be Element of X holds
  h.x = f.x * g.x);

theorem :: C0SP1:32
  ( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_BoundedFunctions X )
  & ||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||;

theorem :: C0SP1:33
  R_Normed_Algebra_of_BoundedFunctions X is
   reflexive discerning RealNormSpace-like;

registration
  let X be non empty set;
  cluster R_Normed_Algebra_of_BoundedFunctions X ->
   reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
 Abelian add-associative right_zeroed right_complementable;
end;

theorem :: C0SP1:34
  f=F & g=G & h=H implies (H = F-G iff for x be Element of X holds
  h.x = f.x - g.x );

theorem :: C0SP1:35
  for X be non empty set for seq be sequence of
R_Normed_Algebra_of_BoundedFunctions X st seq is Cauchy_sequence_by_Norm holds
  seq is convergent;

theorem :: C0SP1:36
  R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace;

registration
  let X be non empty set;
  cluster R_Normed_Algebra_of_BoundedFunctions X -> complete;
end;

registration let X;
 cluster R_Normed_Algebra_of_BoundedFunctions X
    -> Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
  left-distributive left_unital;
end;

theorem :: C0SP1:37
  R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra;