:: 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)
proofend;

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
proofend;

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
proofend;
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
proofend;
end;

:: deftheorem  defines i_FC HAHNBAN1:def_2_:_
 i_FC = <i> ;

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

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

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) &amp; 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)) &amp; 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;
funcf + 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)
proofend;
uniqueness
 for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = (f . x) + (g . x) ) &amp; ( for x being Element of V holds b2 . x = (f . x) + (g . x) ) holds
b1 = b2
proofend;
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)
proofend;
uniqueness
 for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = - (f . x) ) &amp; ( for x being Element of V holds b2 . x = - (f . x) ) holds
b1 = b2
proofend;
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;
funcf - 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;
funcv * 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)
proofend;
uniqueness
 for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = v * (f . x) ) &amp; ( for x being Element of V holds b2 . x = v * (f . x) ) holds
b1 = b2
proofend;
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;
attrF 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;
attrF 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
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
clusterV16() 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 &amp; b1 is homogeneous &amp; b1 is 0-preserving )
proofend;
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
proofend;

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)
proofend;

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
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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;
clusterf + g ->  additive ;
coherence
 f + g is additive
proofend;
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
proofend;
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;
clusterv * f ->  additive ;
coherence
 v * f is additive
proofend;
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;
clusterf + g ->  homogeneous ;
coherence
 f + g is homogeneous
proofend;
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
proofend;
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;
clusterv * f ->  homogeneous ;
coherence
 v * f is homogeneous
proofend;
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;
funcV *'  ->  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 ) ) &amp; ( for f, g being linear-Functional of V holds the addF of it . (f,g) = f + g ) &amp; 0. it = 0Functional V &amp; ( 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 ) ) &amp; ( for f, g being linear-Functional of V holds the addF of b1 . (f,g) = f + g ) &amp; 0. b1 = 0Functional V &amp; ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . (x,f) = x * f ) )
proofend;
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 ) ) &amp; ( for f, g being linear-Functional of V holds the addF of b1 . (f,g) = f + g ) &amp; 0. b1 = 0Functional V &amp; ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . (x,f) = x * f ) &amp; ( for x being set holds
( x in the carrier of b2 iff x is linear-Functional of V ) ) &amp; ( for f, g being linear-Functional of V holds the addF of b2 . (f,g) = f + g ) &amp; 0. b2 = 0Functional V &amp; ( 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
proofend;
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 ) ) &amp; ( for f, g being linear-Functional of V holds the addF of b3 . (f,g) = f + g ) &amp; 0. b3 = 0Functional V &amp; ( 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;
clusterV *'  ->  non empty Abelian strict ;
coherence
 V *' is Abelian
proofend;
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;
clusterV *'  ->  non empty add-associative strict ;
coherence
 V *' is add-associative
proofend;
clusterV *'  ->  non empty right_zeroed strict ;
coherence
 V *' is right_zeroed
proofend;
clusterV *'  ->  non empty right_complementable strict ;
coherence
 V *' is right_complementable
proofend;
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;
clusterV *'  ->  non empty strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( V *' is vector-distributive &amp; V *' is scalar-distributive &amp; V *' is scalar-associative &amp; V *' is scalar-unital )
proofend;
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;
attrF 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;
attrF 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;
attrF 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))
proofend;

definition
let V be non empty VectSpStr over F_Complex ;
let F be RFunctional of V;
attrF 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;
attrF 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
proofend;
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
proofend;
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
proofend;
cluster 0RFunctional V ->  0-preserving ;
coherence
 0RFunctional V is 0-preserving
proofend;
end;

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

registration
let K be 1-sorted ;
let V be non empty VectSpStr over K;
clusterV16() 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 &amp; b1 is 0-preserving )
proofend;
end;

registration
let V be non empty VectSpStr over F_Complex ;
clusterV16() 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 &amp; b1 is Real_homogeneous &amp; b1 is homogeneous )
proofend;
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 #) &amp; ( 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 #) &amp; ( for r being Real
for v being Vector of V holds the Mult of b1 . (r,v) = [**r,0**] * v ) )
proofend;
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 #) &amp; ( for r being Real
for v being Vector of V holds the Mult of b1 . (r,v) = [**r,0**] * v ) &amp; 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 #) &amp; ( for r being Real
for v being Vector of V holds the Mult of b2 . (r,v) = [**r,0**] * v ) holds
b1 = b2
proofend;
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 #) &amp; ( 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
proofend;
end;

registration
let V be non empty Abelian VectSpStr over F_Complex ;
cluster RealVS V ->  strict Abelian ;
coherence
 RealVS V is Abelian
proofend;
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
proofend;
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
proofend;
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
proofend;
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 &amp; RealVS V is scalar-distributive &amp; RealVS V is scalar-associative &amp; RealVS V is scalar-unital )
proofend;
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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;
uniqueness
 for b1, b2 being Functional of (RealVS V) st ( for i being Element of V holds b1 . i = Re (l . i) ) &amp; ( for i being Element of V holds b2 . i = Re (l . i) ) holds
b1 = b2
proofend;
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)
proofend;
uniqueness
 for b1, b2 being Functional of (RealVS V) st ( for i being Element of V holds b1 . i = Im (l . i) ) &amp; ( for i being Element of V holds b2 . i = Im (l . i) ) holds
b1 = b2
proofend;
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
proofend;
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)
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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)
proofend;
uniqueness
 for b1, b2 being RFunctional of V st ( for v being Element of V holds b1 . v = l . (i_FC * v) ) &amp; ( for v being Element of V holds b2 . v = l . (i_FC * v) ) holds
b1 = b2
proofend;
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))**]
proofend;
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))**] ) &amp; ( for v being Element of V holds b2 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) holds
b1 = b2
proofend;
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)
proofend;

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)
proofend;

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
proofend;

:: 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 &amp; ( for e being Vector of V holds |.(L . e).| <= p . e ) )
proofend;

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**]
proofend;