:: Hahn Banach Theorem in the Vector Space over the Field of Complex Numbers
:: by Anna Justyna Milewska
::
:: Received May 23, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

Lm1: for F being non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr
for x, y being Element of F holds x * (- y) = - (x * y)
proof end;

theorem :: HAHNBAN1:1
canceled;

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

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

begin

definition
let x, y be real number ;
func [**x,y**] -> Element of F_Complex equals :: HAHNBAN1:def 1
x + (y * <i>);
coherence
x + (y * <i>) is Element of F_Complex
proof end;
end;

:: deftheorem defines [** HAHNBAN1:def 1 :
for x, y being real number holds [**x,y**] = x + (y * <i>);

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

:: deftheorem defines i_FC HAHNBAN1:def 2 :
i_FC = <i> ;

theorem Th4: :: HAHNBAN1:4
i_FC * i_FC = - (1_ F_Complex)
proof end;

theorem Th5: :: HAHNBAN1:5
(- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex
proof end;

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

theorem :: HAHNBAN1:7
for x1, y1, x2, y2 being real number holds [**x1,y1**] * [**x2,y2**] = [**((x1 * x2) - (y1 * y2)),((x1 * y2) + (x2 * y1))**] ;

theorem :: HAHNBAN1:8
canceled;

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

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

theorem :: HAHNBAN1:11
for x, y being 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)) ) by COMPLEX1:9;

begin

definition
let K be 1-sorted ;
let V be VectSpStr 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 VectSpStr over K;
let f, g be Functional of V;
func f + g -> Functional of V means :Def3: :: HAHNBAN1:def 3
 for x being Element of V holds it . x = (f . x) + (g . x);
existence
ex b1 being Functional of V st
for x being Element of V holds b1 . x = (f . x) + (g . x)
proof end;
uniqueness
for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = (f . x) + (g . x) ) & ( for x being Element of V holds b2 . x = (f . x) + (g . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines + HAHNBAN1:def 3 :
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, g, b5 being Functional of V holds
( b5 = f + g iff for x being Element of V holds b5 . x = (f . x) + (g . x) );

definition
let K be non empty addLoopStr ;
let V be non empty VectSpStr over K;
let f be Functional of V;
func - f -> Functional of V means :Def4: :: HAHNBAN1:def 4
 for x being Element of V holds it . x = - (f . x);
existence
ex b1 being Functional of V st
for x being Element of V holds b1 . x = - (f . x)
proof end;
uniqueness
for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = - (f . x) ) & ( for x being Element of V holds b2 . x = - (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines - HAHNBAN1:def 4 :
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, b4 being Functional of V holds
( b4 = - f iff for x being Element of V holds b4 . x = - (f . x) );

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

:: deftheorem defines - HAHNBAN1:def 5 :
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, g being Functional of V holds f - g = f + (- g);

definition
let K be non empty multMagma ;
let V be non empty VectSpStr over K;
let v be Element of K;
let f be Functional of V;
func v * f -> Functional of V means :Def6: :: HAHNBAN1:def 6
 for x being Element of V holds it . x = v * (f . x);
existence
ex b1 being Functional of V st
for x being Element of V holds b1 . x = v * (f . x)
proof end;
uniqueness
for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = v * (f . x) ) & ( for x being Element of V holds b2 . x = v * (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines * HAHNBAN1:def 6 :
for K being non empty multMagma
for V being non empty VectSpStr over K
for v being Element of K
for f, b5 being Functional of V holds
( b5 = v * f iff for x being Element of V holds b5 . x = v * (f . x) );

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

:: deftheorem defines 0Functional HAHNBAN1:def 7 :
for K being non empty ZeroStr
for V being VectSpStr over K holds 0Functional V = ([#] V) --> (0. K);

definition
let K be non empty multMagma ;
let V be non empty VectSpStr over K;
let F be Functional of V;
attr F is homogeneous means :Def8: :: HAHNBAN1:def 8
 for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x);
end;

:: deftheorem Def8 defines homogeneous HAHNBAN1:def 8 :
for K being non empty multMagma
for V being non empty VectSpStr over K
for F being Functional of V holds
( F is homogeneous iff for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x) );

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

:: deftheorem defines 0-preserving HAHNBAN1:def 9 :
for K being non empty ZeroStr
for V being non empty VectSpStr over K
for F being Functional of V holds
( F is 0-preserving iff F . (0. V) = 0. K );

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
cluster Function-like V30( the carrier of V, the carrier of K) homogeneous -> 0-preserving for Element of bool [: the carrier of V, the carrier of K:];
coherence
for b1 being Functional of V st b1 is homogeneous holds
b1 is 0-preserving
proof end;
end;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V -> additive ;
coherence
0Functional V is additive
proof end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V -> homogeneous ;
coherence
0Functional V is homogeneous
proof end;
end;

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V -> 0-preserving ;
coherence
0Functional V is 0-preserving
proof end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
cluster V16() V19( the carrier of V) V20( the carrier of K) Function-like V30( the carrier of V, the carrier of K) additive homogeneous 0-preserving for Element of bool [: the carrier of V, the carrier of K:];
existence
ex b1 being Functional of V st
( b1 is additive & b1 is homogeneous & b1 is 0-preserving )
proof end;
end;

theorem Th12: :: HAHNBAN1:12
for K being non empty Abelian addLoopStr
for V being non empty VectSpStr over K
for f, g being Functional of V holds f + g = g + f
proof end;

theorem Th13: :: HAHNBAN1:13
for K being non empty add-associative addLoopStr
for V being non empty VectSpStr over K
for f, g, h being Functional of V holds (f + g) + h = f + (g + h)
proof end;

theorem :: HAHNBAN1:14
for K being non empty ZeroStr
for V being non empty VectSpStr over K
for x being Element of V holds (0Functional V) . x = 0. K by FUNCOP_1:7;

theorem Th15: :: HAHNBAN1:15
for K being non empty right_zeroed addLoopStr
for V being non empty VectSpStr over K
for f being Functional of V holds f + (0Functional V) = f
proof end;

theorem Th16: :: HAHNBAN1:16
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V being non empty VectSpStr over K
for f being Functional of V holds f - f = 0Functional V
proof end;

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

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

theorem Th19: :: HAHNBAN1:19
for K being non empty associative multMagma
for V being non empty VectSpStr over K
for r, s being Element of K
for f being Functional of V holds (r * s) * f = r * (s * f)
proof end;

theorem Th20: :: HAHNBAN1:20
for K being non empty left_unital doubleLoopStr
for V being non empty VectSpStr over K
for f being Functional of V holds (1. K) * f = f
proof end;

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

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

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

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

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

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

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

begin

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
func V *' -> non empty strict VectSpStr over K means :Def10: :: HAHNBAN1:def 10
( ( for x being set holds
( x in the carrier of it iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of it . (f,g) = f + g ) & 0. it = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of it . (x,f) = x * f ) );
existence
ex b1 being non empty strict VectSpStr over K st
( ( for x being set holds
( x in the carrier of b1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b1 . (f,g) = f + g ) & 0. b1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . (x,f) = x * f ) )
proof end;
uniqueness
for b1, b2 being non empty strict VectSpStr over K st ( for x being set holds
( x in the carrier of b1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b1 . (f,g) = f + g ) & 0. b1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . (x,f) = x * f ) & ( for x being set holds
( x in the carrier of b2 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b2 . (f,g) = f + g ) & 0. b2 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b2 . (x,f) = x * f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines *' HAHNBAN1:def 10 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr
for V being non empty VectSpStr over K
for b3 being non empty strict VectSpStr over K holds
( b3 = V *' iff ( ( for x being set holds
( x in the carrier of b3 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b3 . (f,g) = f + g ) & 0. b3 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b3 . (x,f) = x * f ) ) );

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

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

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ;
let V be non empty VectSpStr over K;
cluster V *' -> non empty strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( V *' is vector-distributive & V *' is scalar-distributive & V *' is scalar-associative & V *' is scalar-unital )
proof end;
end;

begin

definition
let K be 1-sorted ;
let V be VectSpStr 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 VectSpStr over K;
let F be RFunctional of V;
attr F is subadditive means :Def11: :: HAHNBAN1:def 11
 for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y);
end;

:: deftheorem Def11 defines subadditive HAHNBAN1:def 11 :
for K being 1-sorted
for V being non empty VectSpStr over K
for F being RFunctional of V holds
( F is subadditive iff for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y) );

definition
let K be 1-sorted ;
let V be non empty VectSpStr over K;
let F be RFunctional of V;
attr F is additive means :Def12: :: HAHNBAN1:def 12
 for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y);
end;

:: deftheorem Def12 defines additive HAHNBAN1:def 12 :
for K being 1-sorted
for V being non empty VectSpStr over K
for F being RFunctional of V holds
( F is additive iff for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y) );

definition
let V be non empty VectSpStr over F_Complex ;
let F be RFunctional of V;
attr F is Real_homogeneous means :Def13: :: HAHNBAN1:def 13
 for v being Vector of V
for r being Real holds F . ([**r,0**] * v) = r * (F . v);
end;

:: deftheorem Def13 defines Real_homogeneous HAHNBAN1:def 13 :
for V being non empty VectSpStr over F_Complex
for F being RFunctional of V holds
( F is Real_homogeneous iff for v being Vector of V
for r being Real holds F . ([**r,0**] * v) = r * (F . v) );

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

definition
let V be non empty VectSpStr over F_Complex ;
let F be RFunctional of V;
attr F is homogeneous means :Def14: :: HAHNBAN1:def 14
 for v being Vector of V
for r being Scalar of holds F . (r * v) = |.r.| * (F . v);
end;

:: deftheorem Def14 defines homogeneous HAHNBAN1:def 14 :
for V being non empty VectSpStr over F_Complex
for F being RFunctional of V holds
( F is homogeneous iff for v being Vector of V
for r being Scalar of holds F . (r * v) = |.r.| * (F . v) );

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

:: deftheorem defines 0-preserving HAHNBAN1:def 15 :
for K being 1-sorted
for V being VectSpStr over K
for F being RFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0 );

registration
let K be 1-sorted ;
let V be non empty VectSpStr over K;
cluster Function-like V30( the carrier of V, REAL ) additive -> subadditive for Element of bool [: the carrier of V,REAL:];
coherence
for b1 being RFunctional of V st b1 is additive holds
b1 is subadditive
proof end;
end;

registration
let V be VectSp of F_Complex ;
cluster Function-like V30( the carrier of V, REAL ) Real_homogeneous -> 0-preserving for Element of bool [: the carrier of V,REAL:];
coherence
for b1 being RFunctional of V st b1 is Real_homogeneous holds
b1 is 0-preserving
proof end;
end;

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

:: deftheorem defines 0RFunctional HAHNBAN1:def 16 :
for K being 1-sorted
for V being VectSpStr over K holds 0RFunctional V = ([#] V) --> 0;

registration
let K be 1-sorted ;
let V be non empty VectSpStr over K;
cluster 0RFunctional V -> additive ;
coherence
0RFunctional V is additive
proof end;
cluster 0RFunctional V -> 0-preserving ;
coherence
0RFunctional V is 0-preserving
proof end;
end;

registration
let V be non empty VectSpStr over F_Complex ;
cluster 0RFunctional V -> Real_homogeneous ;
coherence
0RFunctional V is Real_homogeneous
proof end;
cluster 0RFunctional V -> homogeneous ;
coherence
0RFunctional V is homogeneous
proof end;
end;

registration
let K be 1-sorted ;
let V be non empty VectSpStr over K;
cluster V16() V19( the carrier of V) V20( REAL ) Function-like V30( the carrier of V, REAL ) additive 0-preserving for Element of bool [: the carrier of V,REAL:];
existence
ex b1 being RFunctional of V st
( b1 is additive & b1 is 0-preserving )
proof end;
end;

registration
let V be non empty VectSpStr over F_Complex ;
cluster V16() V19( the carrier of V) V20( REAL ) Function-like V30( the carrier of V, REAL ) additive Real_homogeneous homogeneous for Element of bool [: the carrier of V,REAL:];
existence
ex b1 being RFunctional of V st
( b1 is additive & b1 is Real_homogeneous & b1 is homogeneous )
proof end;
end;

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

begin

definition
let V be non empty VectSpStr over F_Complex ;
func RealVS V -> strict RLSStruct means :Def17: :: HAHNBAN1:def 17
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of it . (r,v) = [**r,0**] * v ) );
existence
ex b1 being strict RLSStruct st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b1 . (r,v) = [**r,0**] * v ) )
proof end;
uniqueness
for b1, b2 being strict RLSStruct st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b1 . (r,v) = [**r,0**] * v ) & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b2 . (r,v) = [**r,0**] * v ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines RealVS HAHNBAN1:def 17 :
for V being non empty VectSpStr over F_Complex
for b2 being strict RLSStruct holds
( b2 = RealVS V iff ( addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b2 . (r,v) = [**r,0**] * v ) ) );

registration
let V be non empty VectSpStr over F_Complex ;
cluster RealVS V -> non empty strict ;
coherence
not RealVS V is empty
proof end;
end;

registration
let V be non empty Abelian VectSpStr over F_Complex ;
cluster RealVS V -> strict Abelian ;
coherence
RealVS V is Abelian
proof end;
end;

registration
let V be non empty add-associative VectSpStr over F_Complex ;
cluster RealVS V -> strict add-associative ;
coherence
RealVS V is add-associative
proof end;
end;

registration
let V be non empty right_zeroed VectSpStr over F_Complex ;
cluster RealVS V -> strict right_zeroed ;
coherence
RealVS V is right_zeroed
proof end;
end;

registration
let V be non empty right_complementable VectSpStr over F_Complex ;
cluster RealVS V -> right_complementable strict ;
coherence
RealVS V is right_complementable
proof end;
end;

registration
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ;
cluster RealVS V -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RealVS V is vector-distributive & RealVS V is scalar-distributive & RealVS V is scalar-associative & RealVS V is scalar-unital )
proof end;
end;

theorem Th22: :: HAHNBAN1:22
for V being VectSp of F_Complex
for M being Subspace of V holds RealVS M is Subspace of RealVS V
proof end;

theorem Th23: :: HAHNBAN1:23
for V being non empty VectSpStr over F_Complex
for p being RFunctional of V holds p is Functional of (RealVS V)
proof end;

theorem Th24: :: HAHNBAN1:24
for V being VectSp of F_Complex
for p being Semi-Norm of V holds p is Banach-Functional of (RealVS V)
proof end;

definition
let V be non empty VectSpStr over F_Complex ;
let l be Functional of V;
func projRe l -> Functional of (RealVS V) means :Def18: :: HAHNBAN1:def 18
 for i being Element of V holds it . i = Re (l . i);
existence
ex b1 being Functional of (RealVS V) st
for i being Element of V holds b1 . i = Re (l . i)
proof end;
uniqueness
for b1, b2 being Functional of (RealVS V) st ( for i being Element of V holds b1 . i = Re (l . i) ) & ( for i being Element of V holds b2 . i = Re (l . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines projRe HAHNBAN1:def 18 :
for V being non empty VectSpStr over F_Complex
for l being Functional of V
for b3 being Functional of (RealVS V) holds
( b3 = projRe l iff for i being Element of V holds b3 . i = Re (l . i) );

definition
let V be non empty VectSpStr over F_Complex ;
let l be Functional of V;
func projIm l -> Functional of (RealVS V) means :Def19: :: HAHNBAN1:def 19
 for i being Element of V holds it . i = Im (l . i);
existence
ex b1 being Functional of (RealVS V) st
for i being Element of V holds b1 . i = Im (l . i)
proof end;
uniqueness
for b1, b2 being Functional of (RealVS V) st ( for i being Element of V holds b1 . i = Im (l . i) ) & ( for i being Element of V holds b2 . i = Im (l . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines projIm HAHNBAN1:def 19 :
for V being non empty VectSpStr over F_Complex
for l being Functional of V
for b3 being Functional of (RealVS V) holds
( b3 = projIm l iff for i being Element of V holds b3 . i = Im (l . i) );

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

:: deftheorem defines RtoC HAHNBAN1:def 20 :
for V being non empty VectSpStr over F_Complex
for l being Functional of (RealVS V) holds RtoC l = l;

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

:: deftheorem defines CtoR HAHNBAN1:def 21 :
for V being non empty VectSpStr over F_Complex
for l being RFunctional of V holds CtoR l = l;

registration
let V be VectSp of F_Complex ;
let l be additive Functional of (RealVS V);
cluster RtoC l -> additive ;
coherence
RtoC l is additive
proof end;
end;

registration
let V be VectSp of F_Complex ;
let l be additive RFunctional of V;
cluster CtoR l -> additive ;
coherence
CtoR l is additive
proof end;
end;

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

registration
let V be VectSp of F_Complex ;
let l be Real_homogeneous RFunctional of V;
cluster CtoR l -> homogeneous ;
coherence
CtoR l is homogeneous
proof end;
end;

definition
let V be non empty VectSpStr over F_Complex ;
let l be RFunctional of V;
func i-shift l -> RFunctional of V means :Def22: :: HAHNBAN1:def 22
 for v being Element of V holds it . v = l . (i_FC * v);
existence
ex b1 being RFunctional of V st
for v being Element of V holds b1 . v = l . (i_FC * v)
proof end;
uniqueness
for b1, b2 being RFunctional of V st ( for v being Element of V holds b1 . v = l . (i_FC * v) ) & ( for v being Element of V holds b2 . v = l . (i_FC * v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines i-shift HAHNBAN1:def 22 :
for V being non empty VectSpStr over F_Complex
for l, b3 being RFunctional of V holds
( b3 = i-shift l iff for v being Element of V holds b3 . v = l . (i_FC * v) );

definition
let V be non empty VectSpStr over F_Complex ;
let l be Functional of (RealVS V);
func prodReIm l -> Functional of V means :Def23: :: HAHNBAN1:def 23
 for v being Element of V holds it . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**];
existence
ex b1 being Functional of V st
for v being Element of V holds b1 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**]
proof end;
uniqueness
for b1, b2 being Functional of V st ( for v being Element of V holds b1 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) & ( for v being Element of V holds b2 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines prodReIm HAHNBAN1:def 23 :
for V being non empty VectSpStr over F_Complex
for l being Functional of (RealVS V)
for b3 being Functional of V holds
( b3 = prodReIm l iff for v being Element of V holds b3 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] );

theorem Th25: :: HAHNBAN1:25
for V being VectSp of F_Complex
for l being linear-Functional of V holds projRe l is linear-Functional of (RealVS V)
proof end;

theorem :: HAHNBAN1:26
for V being VectSp of F_Complex
for l being linear-Functional of V holds projIm l is linear-Functional of (RealVS V)
proof end;

theorem Th27: :: HAHNBAN1:27
for V being VectSp of F_Complex
for l being linear-Functional of (RealVS V) holds prodReIm l is linear-Functional of V
proof end;

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

begin

:: from COMPTRIG, 2006.08.12, A.T.
theorem :: HAHNBAN1:29
for x being Real st x > 0 holds
for n being Element of NAT holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]
proof end;