:: Hahn Banach Theorem in the Vector Space over the Field of
:: Complex Numbers
:: by Anna Justyna Milewska
::
:: Received May 23, 2000
:: Copyright (c) 2000-2026 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;
definitions TARSKI, RLSUB_1, HAHNBAN, RLVECT_1, VECTSP_1, ALGSTR_0;
equalities SQUARE_1, BINOP_1, RLVECT_1, VECTSP_1, COMPLEX1, STRUCT_0,
ALGSTR_0;
expansions TARSKI, VECTSP_1;
theorems TARSKI, ZFMISC_1, ABSVALUE, FUNCT_1, FUNCT_2, COMPLEX1, COMPLFLD,
VECTSP_1, FUNCOP_1, RLVECT_1, BINOP_1, HAHNBAN, VECTSP_4, XBOOLE_0,
RELAT_1, XCMPLX_1, GROUP_1, XXREAL_0, XCMPLX_0, POWER, ALGSTR_0, XREAL_0;
schemes FUNCT_2, BINOP_1, NAT_1;
begin :: Preliminaries
Lm1: for F be add-associative right_zeroed right_complementable Abelian
right-distributive non empty doubleLoopStr for x,y be Element of F holds x*(-
y) = -x*y
proof
let F be add-associative right_zeroed right_complementable Abelian
right-distributive non empty doubleLoopStr;
let x,y be Element of F;
x*y +x*(-y) = x*(y+(-y)) by VECTSP_1:def 2
.= x*(0.F) by RLVECT_1:def 10
.= 0.F;
hence thesis by RLVECT_1:def 10;
end;
::$CT
theorem
for x1,y1,x2,y2 being Real holds (x1+y1*<i>) * (x2+y2*<i>) = x1
*x2-y1*y2 + (x1*y2+x2*y1)*<i>;
theorem Th2:
for z be Element of COMPLEX holds |.z.|+0*<i> = (z*'/(|.z.|+0*<i> ))*z
proof
let z be Element of COMPLEX;
per cases;
suppose
A1: |.z.| = 0;
then z = 0 by COMPLEX1:45;
hence thesis by A1;
end;
suppose
A2: |.z.| <> 0;
A3: Im(z*z*') = 0 by COMPLEX1:40;
|.z.| = |.z.|+0*<i>;
then
A4: Re |.z.| = |.z.| & Im |.z.| = 0 by COMPLEX1:12;
A5: (z*'/|.z.|)*z = z*z*'/|.z.| & Re(z*z*') = (Re z)^2 + (Im z)^2 by
COMPLEX1:40,XCMPLX_1:74;
then
A6: Im((z*'/|.z.|)*z) = (|.z.|*0 - ((Re z)^2+(Im z)^2)*0) / (|.z.| ^2 +0^2
) by A3,A4,COMPLEX1:24;
Re((z*'/|.z.|)*z) = (((Re z)^2+(Im z)^2)*|.z.| + 0*0) / (|.z .|^2 +0^2
) by A5,A3,A4,COMPLEX1:24
.= |.z*z.|*|.z.| / (|.z.|*|.z.|) by COMPLEX1:68
.= |.z*z.| / |.z.| by A2,XCMPLX_1:91
.= |.z.|*|.z.| / |.z.| by COMPLEX1:65
.= |.z.| by A2,XCMPLX_1:89;
hence thesis by A6,COMPLEX1:13;
end;
end;
begin :: Some Facts on the Field of Complex Numbers
definition
let x,y be Real;
func [**x,y**] -> Element of F_Complex equals
x+y*<i>;
coherence
proof
x+y*<i> in COMPLEX by XCMPLX_0:def 2;
hence thesis by COMPLFLD:def 1;
end;
end;
definition
func i_FC -> Element of F_Complex equals
<i>;
coherence
proof
0+1*<i> = [**0,1**];
hence thesis;
end;
end;
theorem
i_FC * i_FC = -1_F_Complex by COMPLFLD:8;
theorem
(-1_F_Complex) * (-1_F_Complex) = 1_F_Complex by COMPLFLD:8;
theorem
for x1,y1,x2,y2 be Real holds
[**x1,y1**] + [**x2,y2**] = [**x1 + x2, y1 + y2**];
theorem
for x1,y1,x2,y2 be Real holds
[**x1,y1**] * [**x2,y2**] = [**x1*x2 - y1*y2, x1*y2+x2*y1**];
::$CT
theorem
for r be Real holds |.[**r,0**].| = |.r.|;
theorem
for x,y be Element of F_Complex holds
Re (x+y) = Re x + Re y & Im (x+y) = Im x + Im y by COMPLEX1:8;
theorem
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
by COMPLEX1:9;
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
:Def3:
for x be Element of V holds it.x = f.x + g.x;
existence
proof
deffunc G(Element of V) = f.$1 + g.$1;
consider F be Function of the carrier of V,the carrier of K such that
A1: for x be Element of V holds F.x = G(x)from FUNCT_2:sch 4;
reconsider F as Functional of V;
take F;
thus thesis by A1;
end;
uniqueness
proof
let a,b be Functional of V such that
A2: for x be Element of V holds a.x = f.x + g.x and
A3: for x be Element of V holds b.x = f.x + g.x;
now
let x be Element of V;
thus a.x = f.x + g.x by A2
.= b.x by A3;
end;
hence a = b by FUNCT_2:63;
end;
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
:Def4:
for x be Element of V holds it.x = - (f.x);
existence
proof
deffunc G(Element of V) = -(f.$1);
consider F be Function of the carrier of V,the carrier of K such that
A1: for x be Element of V holds F.x = G(x) from FUNCT_2:sch 4;
reconsider F as Functional of V;
take F;
thus thesis by A1;
end;
uniqueness
proof
let a,b be Functional of V such that
A2: for x be Element of V holds a.x = -(f.x) and
A3: for x be Element of V holds b.x = -(f.x);
now
let x be Element of V;
thus a.x = -(f.x) by A2
.= b.x by A3;
end;
hence a = b by FUNCT_2:63;
end;
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
f+-g;
coherence;
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
:Def6:
for x be Element of V holds it.x = v*(f.x);
existence
proof
deffunc G(Element of V) = v *(f.$1);
consider F be Function of the carrier of V,the carrier of K such that
A1: for x be Element of V holds F.x = G(x) from FUNCT_2:sch 4;
reconsider F as Functional of V;
take F;
thus thesis by A1;
end;
uniqueness
proof
let a,b be Functional of V such that
A2: for x be Element of V holds a.x = v*(f.x) and
A3: for x be Element of V holds b.x = v*(f.x);
now
let x be Element of V;
thus a.x = v*(f.x) by A2
.= b.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let K be non empty ZeroStr;
let V be ModuleStr over K;
func 0Functional(V) -> Functional of V equals
[#]V --> 0.K;
coherence;
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
:Def8:
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
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;
coherence
proof
let F be Functional of V;
assume
A1: F is homogeneous;
thus F.(0.V) = F.(0.K * 0.V) by VECTSP_1:14
.= 0.K * F.(0.V) by A1
.= 0.K;
end;
end;
registration
let K be right_zeroed non empty addLoopStr;
let V be non empty ModuleStr over K;
cluster 0Functional(V) -> additive;
coherence
proof
let x,y be Vector of V;
A1: (0Functional(V)).x = 0.K & (0Functional(V)).y = 0.K by FUNCOP_1:7;
thus (0Functional(V)).(x+y) = 0.K by FUNCOP_1:7
.= (0Functional(V)).x + (0Functional(V)).y by A1,RLVECT_1:def 4;
end;
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;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
(0Functional(V)).x = 0.K by FUNCOP_1:7;
hence (0Functional(V)).(r*x) = r*(0Functional(V)).x by FUNCOP_1:7;
end;
end;
registration
let K be non empty ZeroStr;
let V be non empty ModuleStr over K;
cluster 0Functional(V) -> 0-preserving;
coherence by FUNCOP_1:7;
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;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
theorem Th10:
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
proof
let K be Abelian non empty addLoopStr;
let V be non empty ModuleStr over K;
let f,g be Functional of V;
now
let x be Element of V;
thus (f+g).x = f.x + g.x by Def3
.= (g+f).x by Def3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th11:
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)
proof
let K be add-associative non empty addLoopStr;
let V be non empty ModuleStr over K;
let f,g,h be Functional of V;
now
let x be Element of V;
thus (f+g+h).x = (f+g).x + h.x by Def3
.= f.x + g.x + h.x by Def3
.= f.x + (g.x + h.x) by RLVECT_1:def 3
.= f.x + ((g+h).x) by Def3
.= (f+(g+h)).x by Def3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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 by FUNCOP_1:7;
theorem Th13:
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
proof
let K be right_zeroed non empty addLoopStr;
let V be non empty ModuleStr over K;
let f be Functional of V;
now
let x be Element of V;
thus (f+0Functional(V)).x = f.x+(0Functional(V)).x by Def3
.= f.x+0.K by FUNCOP_1:7
.= f.x by RLVECT_1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th14:
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)
proof
let K be add-associative right_zeroed right_complementable non empty
addLoopStr;
let V be non empty ModuleStr over K;
let f be Functional of V;
now
let x be Element of V;
thus (f-f).x = f.x+(-f).x by Def3
.= f.x+-f.x by Def4
.= 0.K by RLVECT_1:5
.= (0Functional(V)).x by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th15:
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
proof
let K be right-distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let r be Element of K;
let f,g be Functional of V;
now
let x be Element of V;
thus (r*(f+g)).x = r*(f+g).x by Def6
.= r*(f.x+g.x) by Def3
.= r*f.x+r*g.x by VECTSP_1:def 2
.= (r*f).x+r*g.x by Def6
.= (r*f).x+(r*g).x by Def6
.= (r*f+r*g).x by Def3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
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
proof
let K be left-distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let r,s be Element of K;
let f be Functional of V;
now
let x be Element of V;
thus ((r+s)*f).x = (r+s)*f.x by Def6
.= r*f.x+s*f.x by VECTSP_1:def 3
.= (r*f).x+s*f.x by Def6
.= (r*f).x+(s*f).x by Def6
.= (r*f+s*f).x by Def3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th17:
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)
proof
let K be associative non empty multMagma;
let V be non empty ModuleStr over K;
let r,s be Element of K;
let f be Functional of V;
now
let x be Element of V;
thus ((r*s)*f).x = (r*s)*f.x by Def6
.= r*(s*f.x) by GROUP_1:def 3
.= r*(s*f).x by Def6
.= (r*(s*f)).x by Def6;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th18:
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
proof
let K be left_unital non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let f be Functional of V;
now
let x be Element of V;
thus ((1.K)*f).x = (1.K)*f.x by Def6
.= f.x;
end;
hence thesis by FUNCT_2:63;
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,g be additive Functional of V;
cluster f+g -> additive;
coherence
proof
let x,y be Vector of V;
thus (f+g).(x+y) = f.(x+y)+g.(x+y) by Def3
.= f.x+f.y+g.(x+y) by VECTSP_1:def 20
.= f.x+f.y+(g.x+g.y) by VECTSP_1:def 20
.= f.x+(f.y+(g.x+g.y)) by RLVECT_1:def 3
.= f.x+(g.x+(f.y+g.y)) by RLVECT_1:def 3
.= f.x+g.x+(f.y+g.y) by RLVECT_1:def 3
.= (f+g).x+(f.y+g.y) by Def3
.= (f+g).x+(f+g).y by Def3;
end;
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;
coherence
proof
let x,y be Vector of V;
thus (-f).(x+y) = -f.(x+y) by Def4
.= -(f.x + f.y) by VECTSP_1:def 20
.= -f.x+-f.y by RLVECT_1:31
.= (-f).x+-f.y by Def4
.= (-f).x+(-f).y by Def4;
end;
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;
coherence
proof
let x,y be Vector of V;
thus (v*f).(x+y) = v*f.(x+y) by Def6
.= v*(f.x + f.y) by VECTSP_1:def 20
.= v*f.x+v*f.y by VECTSP_1:def 2
.= (v*f).x+v*f.y by Def6
.= (v*f).x+(v*f).y by Def6;
end;
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;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
thus (f+g).(r*x) = f.(r*x) + g.(r*x) by Def3
.= r*f.x + g.(r*x) by Def8
.= r*f.x + r*g.x by Def8
.= r*(f.x + g.x) by VECTSP_1:def 2
.= r*(f+g).x by Def3;
end;
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;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
thus (-f).(r*x) = -f.(r*x) by Def4
.= -r*f.x by Def8
.= r*-f.x by Lm1
.= r*(-f).x by Def4;
end;
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;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
thus (v*f).(r*x) = v*f.(r*x) by Def6
.= v*(r*f.x) by Def8
.= r*(v*f.x) by GROUP_1:def 3
.= r*(v*f).x by Def6;
end;
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
:Def10:
(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;
existence
proof
defpred P[set,set,set] means ex f,g be Functional of V st $1=f & $2=g & $3
=f+g;
0Functional(V) in the set of all x where x is linear-Functional of V;
then reconsider
ca = the set of all x where x is linear-Functional of V
as non empty set;
A1: now
let x be set;
thus x in ca implies x is linear-Functional of V
proof
assume x in ca;
then ex y be linear-Functional of V st x=y;
hence thesis;
end;
thus x is linear-Functional of V implies x in ca;
end;
then reconsider 0F=0Functional(V) as Element of ca;
A2: for x,y be Element of ca ex u be Element of ca st P[x,y,u]
proof
let x,y be Element of ca;
reconsider f=x,g=y as linear-Functional of V by A1;
reconsider u=f+g as Element of ca by A1;
take u,f,g;
thus thesis;
end;
consider ad be Function of [:ca,ca:],ca such that
A3: for x,y be Element of ca holds P[x,y,ad.(x,y)] from BINOP_1:sch 3(
A2);
defpred P[Element of K,set,set] means ex f be Functional of V st $2=f & $3
=$1*f;
A4: for x be Element of K,y be Element of ca ex u be Element of ca st P[x, y,u]
proof
let x be Element of K,y be Element of ca;
reconsider f=y as linear-Functional of V by A1;
reconsider u=x*f as Element of ca by A1;
take u,f;
thus thesis;
end;
consider lm be Function of [:the carrier of K,ca:],ca such that
A5: for x be Element of K,y be Element of ca holds P[x,y,lm.(x,y)]
from BINOP_1:sch 3(A4);
A6: now
let f be linear-Functional of V;
reconsider y=f as Element of ca by A1;
let x be Element of K;
ex f1 be Functional of V st y=f1 & lm.(x,y)=x*f1 by A5;
hence lm.(x,f) = x*f;
end;
reconsider V1 = ModuleStr(# ca,ad,0F,lm #) as non empty strict ModuleStr
over K;
take V1;
now
let f,g be linear-Functional of V;
reconsider x=f,y=g as Element of ca by A1;
ex f1,g1 be Functional of V st x=f1 & y=g1 & ad.(x,y)=f1 +g1 by A3;
hence ad.(f,g) = f+g;
end;
hence thesis by A1,A6;
end;
uniqueness
proof
let V1,V2 be non empty strict ModuleStr over K;
assume that
A7: for x be set holds x in the carrier of V1 iff x is
linear-Functional of V and
A8: for f,g be linear-Functional of V holds (the addF of V1).(f,g)=f+ g and
A9: 0.V1 = 0Functional(V) and
A10: for f be linear-Functional of V for x be Element of K holds (the
lmult of V1).(x,f) = x*f and
A11: for x be set holds x in the carrier of V2 iff x is
linear-Functional of V and
A12: for f,g be linear-Functional of V holds (the addF of V2).(f,g)=f+ g and
A13: 0.V2 = 0Functional(V) and
A14: for f be linear-Functional of V for x be Element of K holds (the
lmult of V2).(x,f) = x*f;
A15: now
let r be Element of K;
let x be Element of V1;
reconsider f=x as linear-Functional of V by A7;
thus (the lmult of V1).(r,x) = r*f by A10
.= (the lmult of V2).(r,x) by A14;
end;
now
let x be object;
thus x in the carrier of V1 implies x in the carrier of V2
proof
assume x in the carrier of V1;
then x is linear-Functional of V by A7;
hence thesis by A11;
end;
assume x in the carrier of V2;
then x is linear-Functional of V by A11;
hence x in the carrier of V1 by A7;
end;
then
A16: the carrier of V1 = the carrier of V2 by TARSKI:2;
now
let x,y be Element of V1;
reconsider f=x, g=y as linear-Functional of V by A7;
thus (the addF of V1).(x,y) = f+g by A8
.= (the addF of V2).(x,y) by A12;
end;
then the addF of V1 = the addF of V2 by A16,BINOP_1:2;
hence thesis by A9,A13,A16,A15,BINOP_1:2;
end;
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;
coherence
proof
let v,w be Element of V*';
reconsider f=v,g=w as linear-Functional of V by Def10;
thus v+w = f+g by Def10
.= g+f by Th10
.= w+v by Def10;
end;
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;
coherence
proof
let u,v,w be Element of V*';
reconsider f=u,g=v,h=w as linear-Functional of V by Def10;
thus u+v+w = (the addF of V*').(f+g,w) by Def10
.= f+g+h by Def10
.= f+(g+h) by Th11
.= (the addF of V*').(u,g+h) by Def10
.= u+(v+w) by Def10;
end;
cluster V*' -> right_zeroed;
coherence
proof
let x be Element of V*';
reconsider f=x as linear-Functional of V by Def10;
thus x + 0.(V*') = (the addF of V*').(x,0Functional(V)) by Def10
.= f+0Functional(V) by Def10
.= x by Th13;
end;
cluster V*' -> right_complementable;
coherence
proof
let x be Element of V*';
reconsider f=x as linear-Functional of V by Def10;
reconsider b = -f as Element of V*' by Def10;
take b;
thus x+b = f-f by Def10
.= 0Functional(V) by Th14
.= 0.(V*') by Def10;
end;
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;
coherence
proof
now let x,y be Element of K;
let v,w be Element of V*';
reconsider f=v,g=w as linear-Functional of V by Def10;
thus x*(v+w) = (the lmult of V*').(x,f+g) by Def10
.= x*(f+g) by Def10
.= x*f+x*g by Th15
.= (the addF of V*').(x*f,x*g) by Def10
.= (the addF of V*').((the lmult of V*').(x,f),x*g) by Def10
.= x*v+x*w by Def10;
thus (x+y)*v = (x+y)*f by Def10
.= x*f+y*f by Th16
.= (the addF of V*').(x*f,y*f) by Def10
.= (the addF of V*').((the lmult of V*').(x,f),y*f) by Def10
.= x*v+y*v by Def10;
thus (x*y)*v = (x*y)*f by Def10
.= x*(y*f) by Th17
.= (the lmult of V*').(x,y*f) by Def10
.= x*(y*v) by Def10;
thus (1.K)*v = (1.K)*f by Def10
.= v by Th18;
end;
hence thesis;
end;
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
:Def11:
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
:Def12:
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
:Def13:
for v be Vector of V for r be Real holds F.([**r,0**]*v) = r*F.v;
end;
theorem Th19:
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)
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty ModuleStr over F_Complex;
let F be RFunctional of V;
assume
A1: F is Real_homogeneous;
let v be Vector of V;
let r be Real;
thus F.([**0,r**]*v) = F.([**r,0**]*i_FC*v)
.= F.([**r,0**]*(i_FC*v)) by VECTSP_1:def 16
.= r*F.(i_FC*v) by A1;
end;
definition
let V be non empty ModuleStr over F_Complex;
let F be RFunctional of V;
attr F is homogeneous means
:Def14:
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
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;
coherence;
end;
registration
let V be VectSp of F_Complex;
cluster Real_homogeneous -> 0-preserving for RFunctional of V;
coherence
proof
let F be RFunctional of V;
assume
A1: F is Real_homogeneous;
A2: 0.F_Complex = [**0,0**] by COMPLFLD:7;
thus F.(0.V) = F.(0.F_Complex*0.V) by VECTSP_1:14
.= 0*F.(0.V) by A1,A2
.= 0;
end;
end;
definition
let K be 1-sorted;
let V be ModuleStr over K;
func 0RFunctional(V) -> RFunctional of V equals
[#]V --> 0;
coherence
proof
[#]V --> In(0,REAL) is RFunctional of V;
hence thesis;
end;
end;
registration
let K be 1-sorted;
let V be non empty ModuleStr over K;
cluster 0RFunctional(V) -> additive;
coherence
proof
let x,y be Vector of V;
(0RFunctional(V)).x = 0 & (0RFunctional(V)).y = 0 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
cluster 0RFunctional(V) -> 0-preserving;
coherence
by FUNCOP_1:7;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster 0RFunctional(V) -> Real_homogeneous;
coherence
proof
let x be Vector of V;
let r be Real;
(0RFunctional(V)).x = 0 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
cluster 0RFunctional(V) -> homogeneous;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
(0RFunctional(V)).x = 0 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let K be 1-sorted;
let V be non empty ModuleStr over K;
cluster additive 0-preserving for RFunctional of V;
existence
proof
take 0RFunctional(V);
thus thesis;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster additive Real_homogeneous homogeneous for RFunctional of V;
existence
proof
take 0RFunctional(V);
thus thesis;
end;
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
:Def17:
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;
existence
proof
deffunc F(Element of REAL, Element of V) = [**$1,0**]*$2;
consider f be Function of [:REAL, the carrier of V:], the carrier of V
such that
A1: for r be Element of REAL,
v be Vector of V holds f.(r,v)=F(r,v) from BINOP_1:
sch 4;
take R = RLSStruct (#the carrier of V, 0.V, the addF of V, f#);
thus the addLoopStr of R = the addLoopStr of V;
let r be Real;
let v be Vector of V;
reconsider r as Element of REAL by XREAL_0:def 1;
f.(r,v)=F(r,v) by A1;
hence thesis;
end;
uniqueness
proof
let a,b be strict RLSStruct such that
A2: the addLoopStr of a = the addLoopStr of V and
A3: for r be Real, v be Vector of V
holds (the Mult of a).(r,v)=[**r,0**]*v and
A4: the addLoopStr of b = the addLoopStr of V and
A5: for r be Real, v be Vector of V
holds (the Mult of b).(r,v)=[**r,0 **]*v;
now
let r be Element of REAL, v be Vector of V;
thus (the Mult of a).(r,v) = [**r,0**]*v by A3
.= (the Mult of b).(r,v) by A5;
end;
hence thesis by A2,A4,BINOP_1:2;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster RealVS(V) -> non empty;
coherence
proof
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
hence thesis;
end;
end;
registration
let V be Abelian non empty ModuleStr over F_Complex;
cluster RealVS(V) -> Abelian;
coherence
proof
let v,w be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v,w1=w as Element of V;
thus v + w = v1 + w1 by A1
.= w1 + v1
.= w + v by A1;
end;
end;
registration
let V be add-associative non empty ModuleStr over F_Complex;
cluster RealVS(V) -> add-associative;
coherence
proof
let u,v,w be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider u1=u,v1=v,w1=w as Element of V;
thus (u + v) + w = (u1 + v1) + w1 by A1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) by A1;
end;
end;
registration
let V be right_zeroed non empty ModuleStr over F_Complex;
cluster RealVS(V) -> right_zeroed;
coherence
proof
let v be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v as Element of V;
thus v + 0.RealVS(V) = v1 + 0.V by A1
.= v by RLVECT_1:def 4;
end;
end;
registration
let V be right_complementable non empty ModuleStr over F_Complex;
cluster RealVS(V) -> right_complementable;
coherence
proof
let v be Element of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v as Element of V;
consider w1 be Element of V such that
A2: v1 + w1 = 0.V by ALGSTR_0:def 11;
reconsider w=w1 as Element of RealVS(V) by A1;
take w;
thus thesis by A1,A2;
end;
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;
coherence
proof
thus for a be Real for v,w be Element of RealVS(V) holds a * (v + w
) = a * v + a * w
proof
let a be Real;
reconsider a as Real;
let v,w be Element of RealVS(V);
set a1=[**a,0**];
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v,w1=w as Element of V;
a * (v + w) = [**a,0**] * (v1 + w1) by A1,Def17
.= a1 * v1 + a1 * w1 by VECTSP_1:def 14
.= (the addF of V).[((the Mult of RealVS(V)).(a,v1)),[**a,0**]*w1]
by Def17
.= a * v + a * w by A1,Def17;
hence thesis;
end;
thus for a,b be Real for v be Element of RealVS(V) holds (a + b) *
v = a * v + b * v
proof
let a,b be Real;
reconsider a,b as Real;
let v be Element of RealVS(V);
set a1=[**a,0**];
set b1=[**b,0**];
A2: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v as Element of V;
[**a,0**] + [**b,0**] = [**a+b,0**];
then (a + b) * v = ([**a,0**] + [**b,0**]) * v1 by Def17
.= a1 * v1 + b1 * v1 by VECTSP_1:def 15
.= (the addF of RealVS(V)).[((the Mult of RealVS(V)).(a,v)), ([**b,0
**]*v1)] by A2,Def17
.= a * v + b * v by Def17;
hence thesis;
end;
thus for a,b be Real for v be Element of RealVS(V) holds (a * b) *
v = a * (b * v)
proof
let a,b be Real;
reconsider a,b as Real;
let v be Element of RealVS(V);
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v as Element of V;
[**a*b,0**] = [**a,0**]*[**b,0**];
then (a * b) * v = ([**a,0**] * [**b,0**]) * v1 by Def17
.= [**a,0**] * ([**b,0**] * v1) by VECTSP_1:def 16
.= (the Mult of RealVS(V)).(a,([**b,0**] * v1)) by Def17
.= a * (b * v) by Def17;
hence thesis;
end;
let v be Element of RealVS(V);
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider v1=v as Element of V;
thus 1 * v = [**1,0**] * v1 by Def17
.= v by COMPLFLD:8,VECTSP_1:def 17;
end;
end;
theorem Th20:
for V be non empty VectSp of F_Complex for M be Subspace of V
holds RealVS(M) is Subspace of RealVS(V)
proof
let V be non empty VectSp of F_Complex;
let M be Subspace of V;
A1: the carrier of M c= the carrier of V by VECTSP_4:def 2;
A2: the lmult of M = (the lmult of V) | [:the carrier of F_Complex, the
carrier of M:] by VECTSP_4:def 2;
A3: the addLoopStr of M = the addLoopStr of RealVS(M) by Def17;
A4: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
hence
A5: the carrier of RealVS(M) c= the carrier of RealVS(V) by A3,VECTSP_4:def 2;
then
[:REAL,the carrier of RealVS(M):] c= [:REAL,the carrier of RealVS(V) :]
by ZFMISC_1:95;
then [:REAL,the carrier of RealVS(M):] c= dom (the Mult of RealVS(V)) by
FUNCT_2:def 1;
then
A6: dom((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):])= [:REAL
,the carrier of RealVS(M):] by RELAT_1:62;
rng ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):]) c= the
carrier of RealVS(M)
proof
let y be object;
assume
y in rng ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS( M):]);
then consider x be object such that
A7: x in dom ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS( M):]) and
A8: y = ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):])
.x by FUNCT_1:def 3;
consider a,b be object such that
A9: x = [a,b] by A7,RELAT_1:def 1;
reconsider a as Element of REAL by A7,A9,ZFMISC_1:87;
reconsider b as Element of RealVS(M) by A6,A7,A9,ZFMISC_1:87;
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1;
[[**a,0**],b2] in [:the carrier of F_Complex, the carrier of V:] by
ZFMISC_1:87;
then [[**a,0**],b1] in [:the carrier of F_Complex, the carrier of M:] & [
[**a,0 **],b2] in dom (the lmult of V) by FUNCT_2:def 1,ZFMISC_1:87;
then [[**a,0**],b2] in (dom (the lmult of V)) /\ [:the carrier of
F_Complex, the carrier of M:] by XBOOLE_0:def 4;
then
A10: [[**a,0**],b2] in dom ((the lmult of V) | [:the carrier of F_Complex,
the carrier of M:]) by RELAT_1:61;
y = (the Mult of RealVS(V)).(a,b) by A7,A8,A9,FUNCT_1:47
.= [**a,0**]*b2 by Def17
.= [**a,0**]*b1 by A2,A10,FUNCT_1:47
.= (the Mult of RealVS(M)).(a,b) by Def17;
hence thesis;
end;
then reconsider
RM = (the Mult of RealVS(V)) | [: REAL,the carrier of RealVS(M)
:] as Function of [:REAL,the carrier of RealVS(M):],the carrier of RealVS(M)
by A6,FUNCT_2:2;
thus 0.RealVS(M) = 0.M by A3
.= 0.V by VECTSP_4:def 2
.= 0.RealVS(V) by A4;
thus the addF of RealVS(M) = (the addF of RealVS(V))||the carrier of RealVS(
M) by A3,A4,VECTSP_4:def 2;
now
let a be Element of REAL, b be Element of RealVS(M);
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1;
[[**a,0**],b2] in [:the carrier of F_Complex, the carrier of V:] by
ZFMISC_1:87;
then [[**a,0**],b1] in [:the carrier of F_Complex, the carrier of M:] & [
[**a,0 **],b2] in dom (the lmult of V) by FUNCT_2:def 1,ZFMISC_1:87;
then [[**a,0**],b2] in (dom (the lmult of V)) /\ [:the carrier of
F_Complex, the carrier of M:] by XBOOLE_0:def 4;
then
A11: [[**a,0**],b2] in dom ((the lmult of V) | [:the carrier of F_Complex,
the carrier of M:]) by RELAT_1:61;
a in REAL & b in the carrier of RealVS(V)
by A5;
then [a,b] in [: REAL,the carrier of RealVS(V) :] by ZFMISC_1:87;
then
[a,b] in [: REAL,the carrier of RealVS(M) :] & [a,b] in dom (the Mult
of RealVS(V)) by FUNCT_2:def 1,ZFMISC_1:87;
then [a,b] in (dom (the Mult of RealVS(V))) /\ [: REAL,the carrier of
RealVS(M) :] by XBOOLE_0:def 4;
then
A12: [a,b] in dom RM by RELAT_1:61;
thus (the Mult of RealVS(M)).(a,b) = [**a,0**]*b1 by Def17
.= [**a,0**]*b2 by A2,A11,FUNCT_1:47
.= (the Mult of RealVS(V)).(a,b) by Def17
.= RM.(a,b) by A12,FUNCT_1:47;
end;
hence
the Mult of RealVS(M) = (the Mult of RealVS(V)) | [:REAL,the carrier of
RealVS(M):] by BINOP_1:2;
end;
theorem Th21:
for V be non empty ModuleStr over F_Complex for p be RFunctional
of V holds p is Functional of RealVS(V)
proof
let V be non empty ModuleStr over F_Complex;
let p be RFunctional of V;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
hence thesis;
end;
theorem Th22:
for V be non empty VectSp of F_Complex for p be Semi-Norm of V
holds p is Banach-Functional of RealVS(V)
proof
let V be non empty VectSp of F_Complex;
let p be Semi-Norm of V;
reconsider p1=p as Functional of RealVS(V) by Th21;
A1: p1 is positively_homogeneous
proof
let x be VECTOR of RealVS(V);
let r be Real;
assume
A2: r > 0;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x as Vector of V;
r*x = [**r,0**]*x1 by Def17;
hence p1.(r*x) = |.r.|*p1.x by Def14
.= r*p1.x by A2,ABSVALUE:def 1;
end;
p1 is subadditive
proof
let x,y be VECTOR of RealVS(V);
A3: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x, y1=y as Vector of V;
x+y = x1+y1 by A3;
hence thesis by Def11;
end;
hence thesis by A1;
end;
definition
let V be non empty ModuleStr over F_Complex;
let l be Functional of V;
func projRe(l) -> Functional of RealVS(V) means
:Def18:
for i be Element of V holds it.i = Re(l.i);
existence
proof
deffunc F(Element of V) = Re(l.$1);
consider f be Function of the carrier of V,REAL such that
A1: for i be Element of V holds f.i = F(i) from FUNCT_2:sch 4;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider f as Functional of RealVS(V);
take f;
thus thesis by A1;
end;
uniqueness
proof
let a,b be Functional of RealVS(V);
assume
A2: for i be Element of V holds a.i = Re(l.i);
assume
A3: for i be Element of V holds b.i = Re(l.i);
now
let i be Element of RealVS(V);
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider j=i as Element of V;
thus a.i = Re(l.j) by A2
.= b.i by A3;
end;
hence a = b by FUNCT_2:63;
end;
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
:Def19:
for i be Element of V holds it.i = Im(l.i);
existence
proof
deffunc F(Element of V) = Im(l.$1);
consider f be Function of the carrier of V,REAL such that
A1: for i be Element of V holds f.i = F(i) from FUNCT_2:sch 4;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider f as Functional of RealVS(V);
take f;
thus thesis by A1;
end;
uniqueness
proof
let a,b be Functional of RealVS(V);
assume
A2: for i be Element of V holds a.i = Im(l.i);
assume
A3: for i be Element of V holds b.i = Im(l.i);
now
let i be Element of RealVS(V);
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider j=i as Element of V;
thus a.i = Im(l.j) by A2
.= b.i by A3;
end;
hence a = b by FUNCT_2:63;
end;
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
l;
coherence
proof
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
hence thesis;
end;
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
l;
coherence
proof
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
hence thesis;
end;
end;
registration
let V be non empty VectSp of F_Complex;
let l be additive Functional of RealVS(V);
cluster RtoC(l) -> additive;
coherence
proof
let x,y be Vector of V;
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x,y1=y as VECTOR of RealVS(V);
x+y = x1+y1 by A1;
hence (RtoC l).(x+y) = (RtoC l).x+(RtoC l).y by HAHNBAN:def 2;
end;
end;
registration
let V be non empty VectSp of F_Complex;
let l be additive RFunctional of V;
cluster CtoR(l) -> additive;
coherence
proof
let x,y be VECTOR of RealVS(V);
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x,y1=y as Vector of V;
x+y = x1+y1 by A1;
hence thesis by Def12;
end;
end;
registration
let V be non empty VectSp of F_Complex;
let l be homogeneous Functional of RealVS(V);
cluster RtoC(l) -> Real_homogeneous;
coherence
proof
let x be Vector of V;
let r be Real;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x as VECTOR of RealVS(V);
[**r,0**]*x = r*x1 by Def17;
hence thesis by HAHNBAN:def 3;
end;
end;
registration
let V be non empty VectSp of F_Complex;
let l be Real_homogeneous RFunctional of V;
cluster CtoR(l) -> homogeneous;
coherence
proof
let x be VECTOR of RealVS(V);
let r be Real;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x as Vector of V;
reconsider r as Real;
[**r,0**]*x1 = r*x by Def17;
hence thesis by Def13;
end;
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
:Def22:
for v be Element of V holds it.v = l.(i_FC*v);
existence
proof
deffunc F(Element of V) = l.(i_FC*$1);
consider f be Function of the carrier of V,REAL such that
A1: for v be Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as RFunctional of V;
take f;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be RFunctional of V such that
A2: for v be Element of V holds F1.v = l.(i_FC*v) and
A3: for v be Element of V holds F2.v = l.(i_FC*v);
now
let v be Element of V;
thus F1.v = l.(i_FC*v) by A2
.= F2.v by A3;
end;
hence F1 = F2 by FUNCT_2:63;
end;
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
:Def23:
for v be Element of V holds it.v = [**(RtoC l).v,-(i-shift(RtoC l)).v**];
existence
proof
deffunc F(Element of V) = [**(RtoC l).$1,-(i-shift(RtoC l)).$1**];
consider f be Function of the carrier of V,the carrier of F_Complex such
that
A1: for v be Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Functional of V;
take f;
thus thesis by A1;
end;
uniqueness
proof
let a,b be Functional of V;
assume
A2: for v be Element of V holds a.v = [**(RtoC l).v,-(i-shift(RtoC l)) .v**];
assume
A3: for v be Element of V holds b.v = [**(RtoC l).v,-(i-shift(RtoC l)) .v**];
now
let v be Element of V;
thus a.v = [**(RtoC l).v,-(i-shift(RtoC l)).v**] by A2
.= b.v by A3;
end;
hence a = b by FUNCT_2:63;
end;
end;
theorem Th23:
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)
proof
let V be non empty VectSp of F_Complex;
let l be linear-Functional of V;
A1: projRe(l) is homogeneous
proof
let x be VECTOR of RealVS(V);
let r be Real;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x as Vector of V;
r*x = [**r,0**]*x1 by Def17;
hence (projRe(l)).(r*x) = Re(l.([**r,0**]*x1)) by Def18
.= Re([**r,0**]*l.x1) by Def8
.= Re [**r,0**] * Re (l.x1) - Im [**r,0**] * Im (l.x1) by COMPLEX1:9
.= Re [**r,0**] * Re (l.x1) - 0 * Im (l.x1) by COMPLEX1:12
.= r * Re (l.x1) by COMPLEX1:12
.= r*(projRe(l)).x by Def18;
end;
projRe(l) is additive
proof
let x,y be VECTOR of RealVS(V);
A2: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x, y1=y as Vector of V;
thus (projRe(l)).(x+y) = Re(l.(x1+y1)) by A2,Def18
.= Re(l.x1+l.y1) by VECTSP_1:def 20
.= Re(l.x1)+Re(l.y1) by COMPLEX1:8
.= Re(l.x1)+(projRe(l)).y by Def18
.= (projRe(l)).x+(projRe(l)).y by Def18;
end;
hence thesis by A1;
end;
theorem
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)
proof
let V be non empty VectSp of F_Complex;
let l be linear-Functional of V;
A1: projIm(l) is homogeneous
proof
let x be VECTOR of RealVS(V);
let r be Real;
the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x as Vector of V;
r*x = [**r,0**]*x1 by Def17;
hence (projIm(l)).(r*x) = Im(l.([**r,0**]*x1)) by Def19
.= Im([**r,0**]*l.x1) by Def8
.= Re [**r,0**] * Im (l.x1) + Re (l.x1) * Im [**r,0**] by COMPLEX1:9
.= Re [**r,0**] * Im (l.x1) + Re (l.x1) * 0 by COMPLEX1:12
.= r * Im (l.x1) by COMPLEX1:12
.= r*(projIm(l)).x by Def19;
end;
projIm(l) is additive
proof
let x,y be VECTOR of RealVS(V);
A2: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
then reconsider x1=x, y1=y as Vector of V;
thus (projIm(l)).(x+y) = Im(l.(x1+y1)) by A2,Def19
.= Im(l.x1+l.y1) by VECTSP_1:def 20
.= Im(l.x1)+Im(l.y1) by COMPLEX1:8
.= Im(l.x1)+(projIm(l)).y by Def19
.= (projIm(l)).x+(projIm(l)).y by Def19;
end;
hence thesis by A1;
end;
theorem Th25:
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
proof
let V be non empty VectSp of F_Complex;
let l be linear-Functional of RealVS(V);
A1: prodReIm(l) is homogeneous
proof
let x be Vector of V;
let r be Scalar of V;
reconsider r1=r as Element of COMPLEX by COMPLFLD:def 1;
set a=Re r1,b=Im r1;
A2: r1 = a+b*<i> by COMPLEX1:13;
A3: -1_F_Complex = [**-1,0**] by COMPLFLD:8;
x = i_FC*(i_FC*(-1_F_Complex))*x
.= i_FC*((-1_F_Complex)*i_FC*x) by VECTSP_1:def 16;
then
A4: a*(-(RtoC l).(i_FC*x))+((RtoC l).x)*b = -a*(RtoC l).(i_FC*x)+b*(RtoC l
).(i_FC*((-1_F_Complex)*i_FC*x))
.= -(RtoC l).([**a,0**]*(i_FC*x))+ -(-b)*(RtoC l).(i_FC*((-1_F_Complex
)*i_FC*x)) by Def13
.= -(RtoC l).([**a,0**]*(i_FC*x))+ -(RtoC l).([**0,-b**]*((-
1_F_Complex)*i_FC*x)) by Th19
.= -(RtoC l).([**a,0**]*(i_FC*x))+ -(RtoC l).([**0,-b**]*((-
1_F_Complex)*(i_FC*x))) by VECTSP_1:def 16
.= -(RtoC l).([**a,0**]*(i_FC*x))+ -(RtoC l).([**0,-b**]*(-1_F_Complex
)*(i_FC*x)) by VECTSP_1:def 16
.= -((RtoC l).([**a,0**]*(i_FC*x))+(RtoC l).([**0,b**]*(i_FC*x))) by A3
.= -(RtoC l).([**a,0**]*(i_FC*x)+[**0,b**]*(i_FC*x)) by Def12
.= -(RtoC l).(([**a,0**]+[**0,b**])*(i_FC*x)) by VECTSP_1:def 15
.= -(RtoC l).(i_FC*r*x) by A2,VECTSP_1:def 16;
A5: a*((RtoC l).x)-b*(-(RtoC l).(i_FC*x)) = a*((RtoC l).x)+b*(RtoC l).( i_FC*x)
.= (RtoC l).([**a,0**]*x)+b*(RtoC l).(i_FC*x) by Def13
.= (RtoC l).([**a,0**]*x)+(RtoC l).([**0,b**]*x) by Th19
.= (RtoC l).([**a,0**]*x+[**0,b**]*x) by Def12
.= (RtoC l).(([**a,0**]+[**0,b**])*x) by VECTSP_1:def 15
.= (RtoC l).(r*x) by COMPLEX1:13;
thus (prodReIm(l)).(r*x) = [**(RtoC l).(r*x),-(i-shift(RtoC l)).(r*x)**]
by Def23
.= [**(RtoC l).(r*x),-(RtoC l).(i_FC*(r*x))**] by Def22
.= (RtoC l).(r*x)+(a*(-(RtoC l).(i_FC*x))+((RtoC l).x)*b)*<i> by A4,
VECTSP_1:def 16
.= r*[**(RtoC l).x,-(RtoC l).(i_FC*x)**] by A2,A5
.= r*[**(RtoC l).x,-(i-shift(RtoC l)).x**] by Def22
.= r*(prodReIm(l)).x by Def23;
end;
prodReIm(l) is additive
proof
let x,y be Vector of V;
thus (prodReIm(l)).(x+y) = [**(RtoC l).(x+y),-(i-shift(RtoC l)).(x+y)**]
by Def23
.= [**(RtoC l).(x+y),-(RtoC l).(i_FC*(x+y))**] by Def22
.= [**(RtoC l).x+(RtoC l).y,-(RtoC l).(i_FC*(x+y))**] by Def12
.= [**(RtoC l).x+(RtoC l).y, -(RtoC l).(i_FC*x+i_FC*y)**] by
VECTSP_1:def 14
.= [**(RtoC l).x+(RtoC l).y, -((RtoC l).(i_FC*x)+(RtoC l).(i_FC*y))**]
by Def12
.= [**(RtoC l).x,-(RtoC l).(i_FC*x)**] + [**(RtoC l).y,-(RtoC l).(i_FC
*y)**]
.= [**(RtoC l).x,-(i-shift(RtoC l)).x**] + [**(RtoC l).y,-(RtoC l).(
i_FC*y)**] by Def22
.= [**(RtoC l).x,-(i-shift(RtoC l)).x**] + [**(RtoC l).y,-(i-shift(
RtoC l)).y**] by Def22
.= (prodReIm(l)).x + [**(RtoC l).y,-(i-shift(RtoC l)).y**] by Def23
.= (prodReIm(l)).x + (prodReIm(l)).y by Def23;
end;
hence thesis by A1;
end;
:: Hahn Banach Theorem
::$N Hahn-Banach Theorem (complex spaces)
theorem
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
proof
let V be non empty VectSp of F_Complex;
let p be Semi-Norm of V;
reconsider p1=p as Banach-Functional of RealVS(V) by Th22;
let M be Subspace of V;
reconsider tcM = the carrier of M as Subset of V by VECTSP_4:def 2;
reconsider RVSM = RealVS(M) as Subspace of RealVS(V) by Th20;
let l be linear-Functional of M;
reconsider prRl = projRe(l) as linear-Functional of RVSM by Th23;
A1: the addLoopStr of V = the addLoopStr of RealVS(V) by Def17;
A2: the addLoopStr of M = the addLoopStr of RealVS(M) by Def17;
assume
A3: for e be Vector of M for v be Vector of V st v=e holds |.l.e.| <= p. v;
for x be VECTOR of RVSM for v be VECTOR of RealVS(V) st x=v holds prRl.x
<= p1.v
proof
let x be VECTOR of RVSM;
reconsider x1=x as Vector of M by A2;
let v be VECTOR of RealVS(V);
reconsider v1=v as Vector of V by A1;
prRl.x = Re(l.x1) by Def18;
then
A4: prRl.x <= |.l.x1.| by COMPLEX1:54;
assume x=v;
then |.l.x1.| <= p.v1 by A3;
hence thesis by A4,XXREAL_0:2;
end;
then consider L1 be linear-Functional of RealVS(V) such that
A5: L1|the carrier of RVSM=prRl and
A6: for e be VECTOR of RealVS(V) holds L1.e <= p1.e by HAHNBAN:22;
reconsider L=prodReIm(L1) as linear-Functional of V by Th25;
take L;
now
let x be Element of M;
the carrier of M c= the carrier of V by VECTSP_4:def 2;
then reconsider x2=x as Element of V;
reconsider x1=x2,ix1=i_FC*x2 as Element of RealVS(V) by A1;
reconsider lx=l.x as Element of COMPLEX by COMPLFLD:def 1;
lx = Re lx+(Im lx)*<i> by COMPLEX1:13;
then
A7: i_FC*l.x = 0*Re lx-1*Im lx + (0*Im lx+1*Re lx)*<i>;
A8: i_FC*x = i_FC*x2 by VECTSP_4:14;
then
A9: L1.ix1 = (projRe(l)).ix1 by A2,A5,FUNCT_1:49
.= Re(l.(i_FC*x)) by A8,Def18
.= Re((-Im lx)+Re lx*<i>) by A7,Def8
.= -Im(l.x) by COMPLEX1:12;
A10: L1.x1 = (projRe(l)).x1 by A2,A5,FUNCT_1:49
.= Re(l.x) by Def18;
thus (L|tcM).x = L.x by FUNCT_1:49
.= [**(RtoC L1).x2,-(i-shift(RtoC L1)).x2**] by Def23
.= [**Re(l.x),-(RtoC L1).(i_FC*x2)**] by A10,Def22
.= l.x by A9,COMPLEX1:13;
end;
hence L|the carrier of M = l by FUNCT_2:63;
let e be Vector of V;
reconsider Le = L.e as Element of COMPLEX by COMPLFLD:def 1;
Le*'/|.Le.| in COMPLEX by XCMPLX_0:def 2;
then reconsider Ledz = Le*'/|.Le.| as Element of F_Complex
by COMPLFLD:def 1;
reconsider e1=e,Ledze=Ledz*e as VECTOR of RealVS(V) by A1;
per cases;
suppose
A11: |.Le.| <> 0;
A12: |.Ledz.| = |.Le*'.|/|.|.Le.|.| by COMPLEX1:67
.= |.Le.|/|.Le.| by COMPLEX1:53
.= 1 by A11,XCMPLX_1:60;
|.Le.|+0*<i> = Ledz*L.e by Th2
.= L.(Ledz*e) by Def8
.= [**(RtoC L1).(Ledz*e),-(i-shift(RtoC L1)).(Ledz*e)**] by Def23
.= L1.Ledze+(-(i-shift(RtoC L1)).(Ledz*e))*<i>;
then
A13: L1.Ledze = |.L.e.| by COMPLEX1:77;
p1.Ledze = |.Ledz.|*p.e by Def14
.= p.e by A12;
hence thesis by A6,A13;
end;
suppose
A14: |.Le.| = 0;
|.L.e.| = |.[**(RtoC L1).e,-(i-shift(RtoC L1)).e**].| by Def23
.= |.(RtoC L1).e+(-(i-shift(RtoC L1)).e)*<i>.|;
then (RtoC L1).e+(-(i-shift(RtoC L1)).e)*<i> = 0+0*<i> by A14,COMPLEX1:45;
then L1.e1 = 0 by COMPLEX1:77;
hence thesis by A6,A14;
end;
end;
begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.
theorem
for x be Real st x > 0 for n be Nat holds (power F_Complex)
.([**x,0**],n) = [**x to_power n,0**]
proof
let x be Real;
defpred P[Nat] means
(power F_Complex).([**x,0**],$1) = [**x to_power $1,0**];
assume
A1: x > 0;
A2: now
let n be Nat;
assume P[n];
then
(power F_Complex).([**x,0**],n+1) = [**x to_power n,0**]*[**x,0**] by
GROUP_1:def 7
.= [**(x to_power n)*(x to_power 1),0**] by POWER:25
.= [**x to_power (n+1),0**] by A1,POWER:27;
hence P[n+1];
end;
(power F_Complex).([**x,0**],0) = 1r+0*<i> by COMPLFLD:8,GROUP_1:def 7
.= [**x to_power 0,0**] by POWER:24;
then
A3: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A3,A2);
end;