:: Complex Valued Function's Space
::  by Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-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 XBOOLE_0, SUBSET_1, FUNCT_2, NUMBERS, BINOP_1, FUNCT_1, BINOP_2,
      RELAT_1, ZFMISC_1, XCMPLX_0, FUNCOP_1, CARD_1, COMPLEX1, ARYTM_3,
      RLVECT_1, CLVECT_1, ARYTM_1, ALGSTR_0, SUPINF_2, CLOPBAN1, STRUCT_0,
      GROUP_1, MESFUNC1, FUNCSDOM, VECTSP_1, CFUNCDOM, VALUED_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
      FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, XCMPLX_0, VALUED_0,
      VALUED_2, BINOP_2, STRUCT_0, ALGSTR_0, RLVECT_1, COMPLEX1, GROUP_1,
      VECTSP_1, FUNCSDOM, CLVECT_1;
 constructors DOMAIN_1, BINOP_2, COMPLEX1, FUNCSDOM, CLVECT_1, VECTSP_1,
      RELSET_1, VALUED_2, VALUED_0, MEMBERED, NUMBERS, GROUP_1;
 registrations XBOOLE_0, RELSET_1, NUMBERS, VECTSP_1, CLVECT_1, XCMPLX_0,
      VALUED_2, MEMBERED;
 requirements SUBSET, BOOLE, ARITHM, NUMERALS;


begin  :: Operation of complex functions

reserve x1,x2,z for set;
reserve A,B for non empty set;
reserve f,g,h for Element of Funcs(A,COMPLEX);

definition
  let A be set;
  func ComplexFuncAdd(A) -> BinOp of Funcs(A,COMPLEX) means
:: CFUNCDOM:def 1

  for f,g being Element of Funcs(A,COMPLEX) holds it.(f,g) = addcomplex.:(f,g);
end;

registration let A be set;
 cluster ComplexFuncAdd A -> complex-functions-valued;
end;

definition
  let A be set;
  func ComplexFuncMult(A) -> BinOp of Funcs(A,COMPLEX) means
:: CFUNCDOM:def 2

  for f,g
  being Element of Funcs(A,COMPLEX) holds it.(f,g) = multcomplex.:(f,g);
end;

registration let A be set;
 cluster ComplexFuncMult A -> complex-functions-valued;
end;

definition
  let A be non empty set;
  func ComplexFuncExtMult(A) ->
   Function of [:COMPLEX,Funcs(A,COMPLEX):], Funcs(A,COMPLEX) means
:: CFUNCDOM:def 3

  for z being Complex, f being Element of Funcs(A, COMPLEX),
      x being Element of A
     holds (it.[z,f]).x = z*(f.x);
end;

registration let A be non empty set;
 cluster ComplexFuncExtMult A -> complex-functions-valued;
end;

definition
  let A;
  func ComplexFuncZero(A) -> Element of Funcs(A,COMPLEX) equals
:: CFUNCDOM:def 4
  A --> 0;
end;

definition
  let A;
  func ComplexFuncUnit(A) -> Element of Funcs(A,COMPLEX) equals
:: CFUNCDOM:def 5
  A --> 1r;
end;

theorem :: CFUNCDOM:1
  h = (ComplexFuncAdd(A)).(f,g) iff for x being Element of A holds
  h.x = f.x + g.x;

theorem :: CFUNCDOM:2
  h = (ComplexFuncMult(A)).(f,g) iff for x being Element of A holds
  h.x = f.x * g.x;

theorem :: CFUNCDOM:3
  ComplexFuncZero(A) <> ComplexFuncUnit(A);

reserve a,b for Complex;

theorem :: CFUNCDOM:4
  h = (ComplexFuncExtMult(A)).[a,f] iff for x being Element of A
  holds h.x = a*(f.x);

theorem :: CFUNCDOM:5
  (ComplexFuncAdd(A)).(f,g) = (ComplexFuncAdd(A)).(g,f);

theorem :: CFUNCDOM:6
  (ComplexFuncAdd(A)).(f,(ComplexFuncAdd(A)).(g,h)) = (
  ComplexFuncAdd(A)).((ComplexFuncAdd(A)).(f,g),h);

theorem :: CFUNCDOM:7
  (ComplexFuncMult(A)).(f,g) = (ComplexFuncMult(A)).(g,f);

theorem :: CFUNCDOM:8
  (ComplexFuncMult(A)).(f,(ComplexFuncMult(A)).(g,h)) = (
  ComplexFuncMult(A)).((ComplexFuncMult(A)).(f,g),h);

theorem :: CFUNCDOM:9
  (ComplexFuncMult(A)).(ComplexFuncUnit(A),f) = f;

theorem :: CFUNCDOM:10
  (ComplexFuncAdd(A)).(ComplexFuncZero(A),f) = f;

theorem :: CFUNCDOM:11
  (ComplexFuncAdd(A)).(f,(ComplexFuncExtMult(A)).[-1r,f]) = ComplexFuncZero(A);

theorem :: CFUNCDOM:12
  (ComplexFuncExtMult(A)).[1r,f] = f;

theorem :: CFUNCDOM:13
  for a, b be Complex holds
  (ComplexFuncExtMult(A)).[a,(ComplexFuncExtMult(A)).[b,f]] = (
  ComplexFuncExtMult(A)).[a*b,f];

theorem :: CFUNCDOM:14
  for a, b be Complex holds
  (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
  ComplexFuncExtMult(A)).[b,f]) = (ComplexFuncExtMult(A)).[a+b,f];

theorem :: CFUNCDOM:15
  (ComplexFuncMult(A)).(f,(ComplexFuncAdd(A)).(g,h)) = (
  ComplexFuncAdd(A)).((ComplexFuncMult(A)).(f,g),(ComplexFuncMult(A)).(f,h));

theorem :: CFUNCDOM:16
  (ComplexFuncMult(A)).((ComplexFuncExtMult(A)).[a,f],g) = (
  ComplexFuncExtMult(A)).[a,(ComplexFuncMult(A)).(f,g)];

begin  :: Complex linear space of complex valued functions

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

theorem :: CFUNCDOM:18
  x1 in A & x2 in A & x1<>x2 & (for z st z in A holds (z=x1
  implies f.z = 1r) & (z<>x1 implies f.z = 0)) & (for z st z in A holds (z=x1
implies g.z = 0) & (z<>x1 implies g.z = 1r)) implies for a,b st (ComplexFuncAdd
  (A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g]) =
  ComplexFuncZero(A) holds a=0c & b=0c;

theorem :: CFUNCDOM:19
  x1 in A & x2 in A & x1<>x2 implies ex f,g st for a,b st (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ]) = ComplexFuncZero(A) holds a=0 & b=0;

theorem :: CFUNCDOM:20
  A = {x1,x2} & x1<>x2 & ( for z st z in A holds (z=x1 implies f.z
= 1r) & (z<>x1 implies f.z = 0) ) & ( for z st z in A holds (z=x1 implies g.z =
  0) & (z<>x1 implies g.z = 1r) ) implies for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ]);

theorem :: CFUNCDOM:21
  A = {x1,x2} & x1<>x2 implies ex f,g st for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ]);

theorem :: CFUNCDOM:22
  A = {x1,x2} & x1<>x2 implies ex f,g st (for a,b st (
ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (ComplexFuncExtMult(A)).[b,g
  ]) = ComplexFuncZero(A) holds a=0 & b=0) & for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
  ]);

definition
  let A;
  func ComplexVectSpace(A) -> strict non empty CLSStruct equals
:: CFUNCDOM:def 6
  CLSStruct(# Funcs(A,COMPLEX), ComplexFuncZero A,
              ComplexFuncAdd A, ComplexFuncExtMult A #);
end;

reserve C for strict non empty CLSStruct,
        u,v,w for Element of C;

registration
  let A;
  cluster ComplexVectSpace A -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital for strict non empty CLSStruct;
end;

theorem :: CFUNCDOM:23
  ex V being strict ComplexLinearSpace 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;
  func CRing(A) -> doubleLoopStr equals
:: CFUNCDOM:def 7
  doubleLoopStr(# Funcs(A,COMPLEX), ComplexFuncAdd A, ComplexFuncMult A,
       ComplexFuncUnit A, ComplexFuncZero A #);
end;

registration
  let A;
  cluster CRing A -> non empty strict;
end;

registration
  let A;
  cluster CRing(A) -> unital;
end;

theorem :: CFUNCDOM:24
  for x,y,z being Element of CRing(A) holds x+y = y+x & (x+y)+z =
x+(y+z) & x+(0.CRing(A)) = x & x is right_complementable & x*y = y*x & (x*y)*z
= x*(y*z) & x*(1.CRing(A)) = x & (1.CRing(A))*x = x & x*(y+z) = x*y + x*z & (y+
  z)*x = y*x + z*x;

theorem :: CFUNCDOM:25
  CRing(A) is commutative Ring;

definition
  struct(doubleLoopStr,CLSStruct) ComplexAlgebraStr (# carrier -> set, multF,
addF -> (BinOp of the carrier), Mult -> (Function of [:COMPLEX,the carrier:],
    the carrier), OneF,ZeroF -> Element of the carrier #);
end;

registration
  cluster non empty for ComplexAlgebraStr;
end;

definition
  let A;
  func CAlgebra(A) -> strict ComplexAlgebraStr equals
:: CFUNCDOM:def 8
  ComplexAlgebraStr(#Funcs
    (A,COMPLEX),ComplexFuncMult(A),ComplexFuncAdd(A), ComplexFuncExtMult(A),(
    ComplexFuncUnit(A)),(ComplexFuncZero(A))#);
end;

registration
  let A;
  cluster CAlgebra(A) -> non empty;
end;

registration
  let A;
  cluster CAlgebra(A) -> unital;
end;

theorem :: CFUNCDOM:26
  for x,y,z being Element of CAlgebra(A), a,b holds x + y = y + x
  & (x + y) + z = x + (y + z) & x + (0.CAlgebra(A)) = x & x is
  right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1.
CAlgebra(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 ComplexAlgebraStr;
  attr IT is vector-associative means
:: CFUNCDOM:def 9
 for x,y being Element of IT, a holds a * (x * y) = (a * x) * y;
end;

registration let A;
 cluster CAlgebra A -> strict Abelian add-associative right_zeroed
      right_complementable commutative associative right_unital
      right-distributive vector-distributive scalar-distributive
      scalar-associative vector-associative;
end;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
    commutative associative right_unital right-distributive vector-distributive
    scalar-distributive scalar-associative vector-associative
     for non empty ComplexAlgebraStr;
end;

definition
  mode ComplexAlgebra is Abelian add-associative right_zeroed
    right_complementable commutative associative right_unital
    right-distributive vector-distributive scalar-distributive
    scalar-associative vector-associative non empty ComplexAlgebraStr;
end;

theorem :: CFUNCDOM:27
  CAlgebra(A) is ComplexAlgebra;

theorem :: CFUNCDOM:28
  1.CRing(A) = ComplexFuncUnit(A);

theorem :: CFUNCDOM:29
  1.CAlgebra(A) = ComplexFuncUnit(A);