:: Hahn Banach Theorem in the Vector Space over the Field of
:: Complex Numbers
::  by Anna Justyna Milewska
::
:: Received May 23, 2000
:: Copyright (c) 2000-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 RLVECT_1, ALGSTR_0, VECTSP_1, XBOOLE_0, SUBSET_1, RELAT_1,
      ARYTM_1, ARYTM_3, SUPINF_2, XCMPLX_0, COMPLEX1, NUMBERS, CARD_1,
      SQUARE_1, COMPLFLD, GROUP_1, REAL_1, STRUCT_0, HAHNBAN, FUNCT_1,
      FUNCOP_1, MSSUBFAM, UNIALG_1, BINOP_1, LATTICES, MESFUNC1, ZFMISC_1,
      XXREAL_0, RLSUB_1, TARSKI, REALSET1, POWER, HAHNBAN1, FUNCT_7, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, REALSET1, NUMBERS,
      XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, SQUARE_1, POWER, STRUCT_0,
      ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, RLSUB_1, VECTSP_4, FUNCT_1,
      FUNCT_2, BINOP_1, RELSET_1, NATTRA_1, FUNCOP_1, FUNCT_3, HAHNBAN,
      COMPLFLD, XXREAL_0, GRCAT_1;
 constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, POWER, REALSET1, RLSUB_1,
      COMPLFLD, VECTSP_4, NATTRA_1, BORSUK_1, HAHNBAN, SUPINF_1, FUNCOP_1,
      GRCAT_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      MEMBERED, STRUCT_0, RLVECT_1, VECTSP_1, COMPLFLD, HAHNBAN, ALGSTR_0,
      SQUARE_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

::$CT

theorem :: HAHNBAN1:2
  for x1,y1,x2,y2 being Real holds (x1+y1*<i>) * (x2+y2*<i>) = x1
  *x2-y1*y2 + (x1*y2+x2*y1)*<i>;

theorem :: HAHNBAN1:3
  for z be Element of COMPLEX holds |.z.|+0*<i> = (z*'/(|.z.|+0*<i> ))*z;

begin :: Some Facts on the Field of Complex Numbers

definition
  let x,y be Real;
  func [**x,y**] -> Element of F_Complex equals
:: HAHNBAN1:def 1
  x+y*<i>;
end;

definition
  func i_FC -> Element of F_Complex equals
:: HAHNBAN1:def 2
  <i>;
end;

theorem :: HAHNBAN1:4
  i_FC * i_FC = -1_F_Complex;

theorem :: HAHNBAN1:5
  (-1_F_Complex) * (-1_F_Complex) = 1_F_Complex;

theorem :: HAHNBAN1:6
  for x1,y1,x2,y2 be Real holds [**x1,y1**] + [**x2,y2**] = [**x1 + x2,
  y1 + y2**];

theorem :: HAHNBAN1:7
  for x1,y1,x2,y2 be Real holds [**x1,y1**] * [**x2,y2**] = [**x1
  *x2 - y1*y2,x1*y2+x2*y1**];

::$CT

theorem :: HAHNBAN1:9
  for r be Real holds |.[**r,0**].| = |.r.|;

theorem :: HAHNBAN1:10
  for x,y be Element of F_Complex holds Re (x+y) = Re x + Re y & Im (x+y
  ) = Im x + Im y;

theorem :: HAHNBAN1:11
  for x,y be Element of F_Complex holds Re (x*y) = Re x * Re y - Im x *
  Im y & Im (x*y) = Re x * Im y + Re y * Im x;

begin :: Functionals of Vector Space

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  mode Functional of V is Function of the carrier of V, the carrier of K;
end;

definition
  let K be non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be Functional of V;

  func f+g -> Functional of V means
:: HAHNBAN1:def 3

  for x be Element of V holds it.x = f.x + g.x;
end;

definition
  let K be non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f be Functional of V;
  func -f -> Functional of V means
:: HAHNBAN1:def 4

  for x be Element of V holds it.x = - (f.x);
end;

definition
  let K be non empty addLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be Functional of V;
  func f-g -> Functional of V equals
:: HAHNBAN1:def 5
  f+-g;
end;

definition
  let K be non empty multMagma;
  let V be non empty ModuleStr over K;
  let v be Element of K;
  let f be Functional of V;
  func v*f -> Functional of V means
:: HAHNBAN1:def 6

  for x be Element of V holds it.x = v*(f.x);
end;

definition
  let K be non empty ZeroStr;
  let V be ModuleStr over K;
  func 0Functional(V) -> Functional of V equals
:: HAHNBAN1:def 7
  [#]V --> 0.K;
end;

definition
  let K be non empty multMagma;
  let V be non empty ModuleStr over K;
  let F be Functional of V;

  attr F is homogeneous means
:: HAHNBAN1:def 8

  for x be Vector of V, r be Scalar of V holds F.(r*x) = r*F.x;
end;

definition
  let K be non empty ZeroStr;
  let V be non empty ModuleStr over K;
  let F be Functional of V;
  attr F is 0-preserving means
:: HAHNBAN1:def 9
  F.(0.V) = 0.K;
end;

registration
  let K be add-associative right_zeroed right_complementable Abelian
  associative well-unital distributive non empty doubleLoopStr;
  let V be VectSp of K;
  cluster homogeneous -> 0-preserving for Functional of V;
end;

registration
  let K be right_zeroed non empty addLoopStr;
  let V be non empty ModuleStr over K;
  cluster 0Functional(V) -> additive;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster 0Functional(V) -> homogeneous;
end;

registration
  let K be non empty ZeroStr;
  let V be non empty ModuleStr over K;
  cluster 0Functional(V) -> 0-preserving;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster additive homogeneous 0-preserving for Functional of V;
end;

theorem :: HAHNBAN1:12
  for K be Abelian non empty addLoopStr for V be non empty
  ModuleStr over K for f,g be Functional of V holds f+g = g+f;

theorem :: HAHNBAN1:13
  for K be add-associative non empty addLoopStr for V be non
  empty ModuleStr over K for f,g,h be Functional of V holds f+g+h = f+(g+h);

theorem :: HAHNBAN1:14
  for K be non empty ZeroStr for V be non empty ModuleStr over K for x
  be Element of V holds (0Functional(V)).x = 0.K;

theorem :: HAHNBAN1:15
  for K be right_zeroed non empty addLoopStr for V be non empty
  ModuleStr over K for f be Functional of V holds f + 0Functional(V) = f;

theorem :: HAHNBAN1:16
  for K be add-associative right_zeroed right_complementable non
empty addLoopStr for V be non empty ModuleStr over K for f be Functional of V
  holds f-f = 0Functional(V);

theorem :: HAHNBAN1:17
  for K be right-distributive non empty doubleLoopStr for V be
  non empty ModuleStr over K for r be Element of K for f,g be Functional of V
  holds r*(f+g) = r*f+r*g;

theorem :: HAHNBAN1:18
  for K be left-distributive non empty doubleLoopStr for V be
  non empty ModuleStr over K for r,s be Element of K for f be Functional of V
  holds (r+s)*f = r*f+s*f;

theorem :: HAHNBAN1:19
  for K be associative non empty multMagma for V be non empty
ModuleStr over K for r,s be Element of K for f be Functional of V holds (r*s)*f
  = r*(s*f);

theorem :: HAHNBAN1:20
  for K be left_unital non empty doubleLoopStr for V be non
  empty ModuleStr over K for f be Functional of V holds (1.K)*f = f;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be additive Functional of V;
  cluster f+g -> additive;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f be additive Functional of V;
  cluster -f -> additive;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let v be Element of K;
  let f be additive Functional of V;
  cluster v*f -> additive;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f,g be homogeneous Functional of V;
  cluster f+g -> homogeneous;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let f be homogeneous Functional of V;
  cluster -f -> homogeneous;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  let v be Element of K;
  let f be homogeneous Functional of V;
  cluster v*f -> homogeneous;
end;

definition
  let K be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  mode linear-Functional of V is additive homogeneous Functional of V;
end;

begin :: The Vector Space of linear Functionals

definition
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  func V*' -> non empty strict ModuleStr over K means
:: HAHNBAN1:def 10

  (for x be set
  holds x in the carrier of it iff x is linear-Functional of V) & (for f,g be
linear-Functional of V holds (the addF of it).(f,g) = f+g) & 0.it = 0Functional
(V) & for f be linear-Functional of V for x be Element of K holds (the lmult of
  it).(x,f) = x*f;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster V*' -> Abelian;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  right-distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster V*' -> add-associative;
  cluster V*' -> right_zeroed;
  cluster V*' -> right_complementable;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  left_unital distributive associative commutative non empty doubleLoopStr;
  let V be non empty ModuleStr over K;
  cluster V*' -> vector-distributive scalar-distributive
  scalar-associative scalar-unital;
end;

begin :: Semi Norm of Vector Space

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  mode RFunctional of V is Function of the carrier of V,REAL;
end;

definition
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  let F be RFunctional of V;

  attr F is subadditive means
:: HAHNBAN1:def 11

  for x,y be Vector of V holds F.(x+y) <= F.x+F.y;
end;

definition
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  let F be RFunctional of V;
  attr F is additive means
:: HAHNBAN1:def 12

  for x,y be Vector of V holds F.(x+y) = F.x+ F.y;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let F be RFunctional of V;
  attr F is Real_homogeneous means
:: HAHNBAN1:def 13

  for v be Vector of V for r be Real holds F.([**r,0**]*v) = r*F.v;
end;

theorem :: HAHNBAN1:21
  for V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty ModuleStr over F_Complex for F
be RFunctional of V st F is Real_homogeneous for v be Vector of V for r be Real
  holds F.([**0,r**]*v) = r*F.(i_FC*v);

definition
  let V be non empty ModuleStr over F_Complex;
  let F be RFunctional of V;
  attr F is homogeneous means
:: HAHNBAN1:def 14

  for v be Vector of V for r be Scalar of V holds F.(r*v) = |.r.|*F.v;
end;

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  let F be RFunctional of V;
  attr F is 0-preserving means
:: HAHNBAN1:def 15
  F.(0.V) = 0;
end;

registration
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  cluster additive -> subadditive for RFunctional of V;
end;

registration
  let V be VectSp of F_Complex;
  cluster Real_homogeneous -> 0-preserving for RFunctional of V;
end;

definition
  let K be 1-sorted;
  let V be ModuleStr over K;
  func 0RFunctional(V) -> RFunctional of V equals
:: HAHNBAN1:def 16
  [#]V --> 0;
end;

registration
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  cluster 0RFunctional(V) -> additive;
  cluster 0RFunctional(V) -> 0-preserving;
end;

registration
  let V be non empty ModuleStr over F_Complex;
  cluster 0RFunctional(V) -> Real_homogeneous;
  cluster 0RFunctional(V) -> homogeneous;
end;

registration
  let K be 1-sorted;
  let V be non empty ModuleStr over K;
  cluster additive 0-preserving for RFunctional of V;
end;

registration
  let V be non empty ModuleStr over F_Complex;
  cluster additive Real_homogeneous homogeneous for RFunctional of V;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  mode Semi-Norm of V is subadditive homogeneous RFunctional of V;
end;

begin :: Hahn Banach Theorem

definition
  let V be non empty ModuleStr over F_Complex;
  func RealVS(V) -> strict RLSStruct means
:: HAHNBAN1:def 17

  the addLoopStr of it = the addLoopStr of V &
  for r be Real, v be Vector of V holds (the Mult of it).(r,v)=
  [**r,0**]*v;
end;

registration
  let V be non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> non empty;
end;

registration
  let V be Abelian non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> Abelian;
end;

registration
  let V be add-associative non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> add-associative;
end;

registration
  let V be right_zeroed non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> right_zeroed;
end;

registration
  let V be right_complementable non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> right_complementable;
end;

registration
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty ModuleStr over F_Complex;
  cluster RealVS(V) -> vector-distributive scalar-distributive
  scalar-associative scalar-unital;
end;

theorem :: HAHNBAN1:22
  for V be non empty VectSp of F_Complex for M be Subspace of V
  holds RealVS(M) is Subspace of RealVS(V);

theorem :: HAHNBAN1:23
  for V be non empty ModuleStr over F_Complex for p be RFunctional
  of V holds p is Functional of RealVS(V);

theorem :: HAHNBAN1:24
  for V be non empty VectSp of F_Complex for p be Semi-Norm of V
  holds p is Banach-Functional of RealVS(V);

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of V;
  func projRe(l) -> Functional of RealVS(V) means
:: HAHNBAN1:def 18

  for i be Element of V holds it.i = Re(l.i);
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of V;
  func projIm(l) -> Functional of RealVS(V) means
:: HAHNBAN1:def 19

  for i be Element of V holds it.i = Im(l.i);
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of RealVS(V);
  func RtoC(l) -> RFunctional of V equals
:: HAHNBAN1:def 20
  l;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be RFunctional of V;
  func CtoR(l) -> Functional of RealVS(V) equals
:: HAHNBAN1:def 21
  l;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be additive Functional of RealVS(V);
  cluster RtoC(l) -> additive;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be additive RFunctional of V;
  cluster CtoR(l) -> additive;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be homogeneous Functional of RealVS(V);
  cluster RtoC(l) -> Real_homogeneous;
end;

registration
  let V be non empty VectSp of F_Complex;
  let l be Real_homogeneous RFunctional of V;
  cluster CtoR(l) -> homogeneous;
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be RFunctional of V;
  func i-shift(l) -> RFunctional of V means
:: HAHNBAN1:def 22

  for v be Element of V holds it.v = l.(i_FC*v);
end;

definition
  let V be non empty ModuleStr over F_Complex;
  let l be Functional of RealVS(V);
  func prodReIm(l) -> Functional of V means
:: HAHNBAN1:def 23

  for v be Element of V holds it.v = [**(RtoC l).v,-(i-shift(RtoC l)).v**];
end;

theorem :: HAHNBAN1:25
  for V be non empty VectSp of F_Complex for l be
  linear-Functional of V holds projRe(l) is linear-Functional of RealVS(V);

theorem :: HAHNBAN1:26
  for V be non empty VectSp of F_Complex for l be linear-Functional of V
  holds projIm(l) is linear-Functional of RealVS(V);

theorem :: HAHNBAN1:27
  for V be non empty VectSp of F_Complex for l be
  linear-Functional of RealVS(V) holds prodReIm(l) is linear-Functional of V;

:: Hahn Banach Theorem

::$N Hahn-Banach Theorem  (complex spaces)
theorem :: HAHNBAN1:28
  for V be non empty VectSp of F_Complex for p be Semi-Norm of V for M
be Subspace of V for l be linear-Functional of M st for e be Vector of M for v
be Vector of V st v=e holds |.l.e.| <= p.v ex L be linear-Functional of V st L|
  the carrier of M = l & for e be Vector of V holds |.L.e.| <= p.e;

begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.

theorem :: HAHNBAN1:29
  for x be Real st x > 0 for n be Nat holds (power F_Complex)
  .([**x,0**],n) = [**x to_power n,0**];