The abstract of the Mizar article:

Real Functions Spaces

by

Henryk Oryszczyszyn, and

Krzysztof Prazmowski

Received March 23, 1990

MML identifier: FUNCSDOM

[ Mizar article, MML identifier index ]

environ

 vocabulary BINOP_1, FUNCT_2, FUNCT_1, QC_LANG1, RELAT_1, FUNCOP_1, VECTSP_1,
      RLVECT_1, ARYTM_1, LATTICES, FUNCSDOM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, STRUCT_0, RLVECT_1, REAL_1,
      VECTSP_1, FRAENKEL;
 constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, VECTSP_1, FRAENKEL,
      MEMBERED, XBOOLE_0;
 clusters SUBSET_1, RLVECT_1, VECTSP_1, FUNCOP_1, RELSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve x1,x2,z for set;
reserve A,B for non empty set;

definition let A,B; let F be BinOp of Funcs(A,B);
           let f,g be Element of Funcs(A,B);
 redefine func F.(f,g) -> Element of Funcs(A,B);
end;

definition let A,B,C,D be non empty set;
 let F be Function of [:C,D:],Funcs(A,B);
           let cd be Element of [:C,D:];
 redefine func F.cd -> Element of Funcs(A,B);
end;

definition let A,B be non empty set; let f be Function of A,B;
 func @f -> Element of Funcs(A,B) equals
:: FUNCSDOM:def 1
  f;
end;

reserve f,g,h for Element of Funcs(A,REAL);

definition let X,Z be non empty set;
 let F be (BinOp of X), f,g be Function of Z,X;
 redefine func F.:(f,g) -> Element of Funcs(Z,X);
end;

definition let X,Z be non empty set;
 let F be (BinOp of X),a be Element of X,f be Function of Z,X;
 redefine func F[;](a,f) -> Element of Funcs(Z,X);
end;

definition let A; func RealFuncAdd(A) -> BinOp of Funcs(A,REAL)
 means
:: FUNCSDOM:def 2
for f,g being Element of Funcs(A,REAL) holds
 it.(f,g) = addreal.:(f,g);
end;

definition let A; func RealFuncMult(A) -> BinOp of Funcs(A,REAL)
 means
:: FUNCSDOM:def 3
for f,g being Element of Funcs(A,REAL) holds
 it.(f,g) = multreal.:(f,g);
end;

definition let A;
 func RealFuncExtMult(A) ->
             Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL)
  means
:: FUNCSDOM:def 4
for a being Real,
    f being (Element of Funcs(A,REAL)), x being (Element of A) holds
                                            (it.[a,f]).x = a*(f.x);
end;

definition let A;
  func RealFuncZero(A) -> Element of Funcs(A,REAL) equals
:: FUNCSDOM:def 5
   A --> 0;
end;

definition let A;
  func RealFuncUnit(A) -> Element of Funcs(A,REAL) equals
:: FUNCSDOM:def 6
   A --> 1;
end;

canceled 9;

theorem :: FUNCSDOM:10
    h = (RealFuncAdd(A)).(f,g) iff
           for x being Element of A holds h.x = f.x + g.x;

theorem :: FUNCSDOM:11
    h = (RealFuncMult(A)).(f,g) iff
            for x being Element of A holds h.x = f.x * g.x;

theorem :: FUNCSDOM:12
    for x being Element of A holds (RealFuncUnit(A)).x = 1;

theorem :: FUNCSDOM:13
    for x being Element of A holds (RealFuncZero(A)).x = 0;

theorem :: FUNCSDOM:14
    RealFuncZero(A) <> RealFuncUnit(A);

reserve a,b for Real;

theorem :: FUNCSDOM:15
  h = (RealFuncExtMult(A)).[a,f] iff
  for x being Element of A holds h.x = a*(f.x);

reserve u,v,w for VECTOR of RLSStruct(#Funcs(A,REAL),
            (RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#);

theorem :: FUNCSDOM:16
 (RealFuncAdd(A)).(f,g) = (RealFuncAdd(A)).(g,f);

theorem :: FUNCSDOM:17
 (RealFuncAdd(A)).(f,(RealFuncAdd(A)).(g,h)) =
                    (RealFuncAdd(A)).((RealFuncAdd(A)).(f,g),h);

theorem :: FUNCSDOM:18
 (RealFuncMult(A)).(f,g) = (RealFuncMult(A)).(g,f);

theorem :: FUNCSDOM:19
 (RealFuncMult(A)).(f,(RealFuncMult(A)).(g,h)) =
                    (RealFuncMult(A)).((RealFuncMult(A)).(f,g),h);

theorem :: FUNCSDOM:20
 (RealFuncMult(A)).(RealFuncUnit(A),f) = f;

theorem :: FUNCSDOM:21
 (RealFuncAdd(A)).(RealFuncZero(A),f) = f;

theorem :: FUNCSDOM:22
 (RealFuncAdd(A)).(f,(RealFuncExtMult(A)).[-1,f]) = RealFuncZero(A);

theorem :: FUNCSDOM:23
 (RealFuncExtMult(A)).[1,f] = f;

theorem :: FUNCSDOM:24
 (RealFuncExtMult(A)).[a,(RealFuncExtMult(A)).[b,f]] =
  (RealFuncExtMult(A)).[a*b,f];

theorem :: FUNCSDOM:25
 (RealFuncAdd(A)).
      ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,f])
                                = (RealFuncExtMult(A)).[a+b,f];

theorem :: FUNCSDOM:26
 (RealFuncMult(A)).(f,(RealFuncAdd(A)).(g,h)) =
  (RealFuncAdd(A)).((RealFuncMult(A)).(f,g),(RealFuncMult(A)).(f,h));

theorem :: FUNCSDOM:27
 (RealFuncMult(A)).((RealFuncExtMult(A)).[a,f],g) =
   (RealFuncExtMult(A)).[a,(RealFuncMult(A)).(f,g)];

theorem :: FUNCSDOM:28
 ex f,g st
      (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
      (for z st z in A holds
      (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1));

theorem :: FUNCSDOM:29
 (x1 in A & x2 in A & x1<>x2) &
      (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
      (for z st z in A holds
      (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1)) implies
   (for a,b st (RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]) = RealFuncZero(A)
   holds a=0 & b=0);

theorem :: FUNCSDOM:30
   x1 in A & x2 in A & x1<>x2 implies
 (ex f,g st
 for a,b st (RealFuncAdd(A)).
  ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]) = RealFuncZero(A)
   holds a=0 & b=0);

theorem :: FUNCSDOM:31
 A = {x1,x2} & x1<>x2 &
     (for z st z in A holds
       (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
     (for z st z in A holds
      (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1))
     implies for h holds
     (ex a,b st h = (RealFuncAdd(A)).
      ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]));

theorem :: FUNCSDOM:32
   A = {x1,x2} & x1<>x2 implies ex f,g st
   (for h holds
     (ex a,b st h =
     (RealFuncAdd(A)).
      ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g])));

theorem :: FUNCSDOM:33
  (A = {x1,x2} & x1<>x2) implies (ex f,g st
   (for a,b st
    (RealFuncAdd(A)).((RealFuncExtMult(A)).[a,f],
         (RealFuncExtMult(A)).[b,g]) = RealFuncZero(A)
                                        holds a=0 & b=0) &
    (for h holds
     (ex a,b st h = (RealFuncAdd(A)).
      ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]))));

theorem :: FUNCSDOM:34
 RLSStruct(#Funcs(A,REAL),
     (RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#)
       is RealLinearSpace;

definition let A;
  func RealVectSpace(A) -> strict RealLinearSpace equals
:: FUNCSDOM:def 7

   RLSStruct(#Funcs(A,REAL),
              (RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#);
end;

canceled 2;

 theorem :: FUNCSDOM:37
ex V being strict RealLinearSpace st
    (ex u,v being VECTOR of V st
     (for a,b st a*u + b*v = 0.V holds a=0 & b=0) &
     (for w being VECTOR of V ex a,b st w = a*u + b*v));





definition
 let A;
 canceled 4;

 func RRing(A) -> strict doubleLoopStr equals
:: FUNCSDOM:def 12
    doubleLoopStr(#Funcs(A,REAL),RealFuncAdd(A),RealFuncMult(A),
                    (RealFuncUnit(A)),(RealFuncZero(A))#);
end;

definition
 let A;
 cluster RRing A -> non empty;
end;

canceled 4;

theorem :: FUNCSDOM:42
   for x,y,z being Element of RRing(A) holds
         x+y = y+x &
         (x+y)+z = x+(y+z) &
         x+(0.RRing(A)) = x &
         (ex t being Element of RRing(A) st
                                            x+t=(0.RRing(A))) &
         x*y = y*x &
         (x*y)*z = x*(y*z) &
         x*(1_ RRing(A)) = x &
         (1_ RRing(A))*x = x &
         x*(y+z) = x*y + x*z &
         (y+z)*x = y*x + z*x;

definition
 cluster strict Abelian add-associative right_zeroed right_complementable
   associative commutative right_unital right-distributive
   (non empty doubleLoopStr);
end;

definition
  mode Ring is Abelian add-associative right_zeroed right_complementable
    associative left_unital right_unital
    distributive (non empty doubleLoopStr);
end;

theorem :: FUNCSDOM:43
RRing(A) is commutative Ring;

definition
  struct(doubleLoopStr,RLSStruct) AlgebraStr (# carrier -> set,
                 mult,add -> (BinOp of the carrier),
                 Mult -> (Function of [:REAL,the carrier:],the carrier),
                 unity,Zero -> Element of the carrier #);
end;

definition
 cluster non empty AlgebraStr;
end;

definition let A;
 canceled 6;

 func RAlgebra(A) -> strict AlgebraStr equals
:: FUNCSDOM:def 19
    AlgebraStr(#Funcs(A,REAL),RealFuncMult(A),RealFuncAdd(A),
            RealFuncExtMult(A),(RealFuncUnit(A)),(RealFuncZero(A))#);
end;

definition let A;
 cluster RAlgebra(A) -> non empty;
end;

canceled 5;

theorem :: FUNCSDOM:49
   for x,y,z being Element of RAlgebra(A)
    for a,b holds
         x+y = y+x &
         (x+y)+z = x+(y+z) &
         x+(0.RAlgebra(A)) = x &
         (ex t being Element of RAlgebra(A) st
                                            x+t=(0.RAlgebra(A))) &
         x*y = y*x &
         (x*y)*z = x*(y*z) &
         x*(1_ RAlgebra(A)) = x &
         x*(y+z) = x*y + x*z &
         a*(x*y) = (a*x)*y &
         a*(x+y) = a*x + a*y &
         (a+b)*x = a*x + b*x &
         (a*b)*x = a*(b*x);

 definition let IT be non empty AlgebraStr;
  attr IT is Algebra-like means
:: FUNCSDOM:def 20
    for x,y,z being Element of IT
           for a,b holds
         x*(1_ IT) = x &
         x*(y+z) = x*y + x*z &
         a*(x*y) = (a*x)*y &
         a*(x+y) = a*x + a*y &
         (a+b)*x = a*x + b*x &
         (a*b)*x = a*(b*x);
end;

definition
 cluster strict Abelian add-associative right_zeroed right_complementable
    commutative associative Algebra-like (non empty AlgebraStr);
end;

definition
  mode Algebra is Abelian add-associative right_zeroed right_complementable
    commutative associative Algebra-like (non empty AlgebraStr);
end;

theorem :: FUNCSDOM:50
    RAlgebra(A) is Algebra;