:: Hahn Banach Theorem in the Vector Space over the Field of :: Complex Numbers :: by Anna Justyna Milewska :: :: Received May 23, 2000 :: Copyright (c) 2000-2018 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*) * (x2+y2*) = x1 *x2-y1*y2 + (x1*y2+x2*y1)*; theorem Th2: for z be Element of COMPLEX holds |.z.|+0* = (z*'/(|.z.|+0* ))*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*; 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*; coherence proof x+y* in COMPLEX by XCMPLX_0:def 2; hence thesis by COMPLFLD:def 1; end; end; definition func i_FC -> Element of F_Complex equals ; coherence proof 0+1* = [**0,1**]; hence thesis; end; end; theorem Th3: i_FC * i_FC = -1_F_Complex proof thus i_FC * i_FC = -1r .= -1_F_Complex by COMPLFLD:2,8; end; theorem Th4: (-1_F_Complex) * (-1_F_Complex) = 1_F_Complex proof -1r = -1_F_Complex by COMPLFLD:2,8; hence thesis by COMPLFLD:8; end; 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; A1: (0Functional(V)).x = 0.K by FUNCOP_1:7; thus (0Functional(V)).(r*x) = 0.K by FUNCOP_1:7 .= r*(0Functional(V)).x by A1; 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* by COMPLEX1:13; A3: -1_F_Complex = [**-1,0**] by COMPLFLD:2,8; x = i_FC*(i_FC*(-1_F_Complex))*x by Th3,Th4,VECTSP_1:def 17 .= 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)* 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)* by COMPLEX1:13; then A7: i_FC*l.x = 0*Re lx-1*Im lx + (0*Im lx+1*Re lx)*; 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*) 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* = 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))*; 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)*.|; then (RtoC L1).e+(-(i-shift(RtoC L1)).e)* = 0+0* 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* 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;