Copyright (c) 2000 Association of Mizar Users
environ
vocabulary RLVECT_1, VECTSP_1, ARYTM_1, COMPLEX1, ABSVALUE, ARYTM_3, SQUARE_1,
COMPLFLD, HAHNBAN, FUNCT_1, SUBSET_1, FUNCOP_1, GRCAT_1, UNIALG_1,
BINOP_1, LATTICES, ALGSTR_2, RLSUB_1, RELAT_1, BOOLE, HAHNBAN1, XCMPLX_0;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, ARYTM_0, XREAL_0,
STRUCT_0, REAL_1, ABSVALUE, SQUARE_1, PRE_TOPC, RLVECT_1, VECTSP_1,
RLSUB_1, VECTSP_4, FUNCT_1, FUNCT_2, BINOP_1, RELSET_1, NATTRA_1,
BORSUK_1, COMPLEX1, HAHNBAN, COMPLFLD;
constructors REAL_1, SQUARE_1, RLSUB_1, VECTSP_4, NATTRA_1, BORSUK_1, HAHNBAN,
COMPLFLD, DOMAIN_1, COMPLSP1, MONOID_0, COMPLEX1, MEMBERED, ARYTM_0,
ARYTM_3, FUNCT_4;
clusters STRUCT_0, VECTSP_1, RELSET_1, FUNCT_1, SUBSET_1, COMPLFLD, RLVECT_1,
HAHNBAN, MEMBERED;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RLVECT_1, VECTSP_1, RLSUB_1, HAHNBAN;
theorems TARSKI, AXIOMS, ZFMISC_1, SQUARE_1, ABSVALUE, FUNCT_1, FUNCT_2,
COMPLEX1, COMPLFLD, STRUCT_0, PRE_TOPC, VECTSP_1, FUNCOP_1, RLVECT_1,
BINOP_1, HAHNBAN, VECTSP_4, XBOOLE_0, RELAT_1, XCMPLX_0, XCMPLX_1,
ARYTM_0;
schemes FUNCT_2;
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 11
.= x*(0.F) by RLVECT_1:def 10
.= 0.F by VECTSP_1:36;
hence x*(-y) = -x*y by RLVECT_1:def 10;
end;
theorem Th1:
for z be Element of COMPLEX holds
abs |.z.| = |.z.|
proof
let z be Element of COMPLEX;
|.z.| >= 0 by COMPLEX1:132;
hence thesis by ABSVALUE:def 1;
end;
theorem Th2:
for x1,y1,x2,y2 be Real holds
[*x1,y1*] * [*x2,y2*] = [*x1*x2 - y1*y2,x1*y2+x2*y1*]
proof
let x1,y1,x2,y2 be Real;
set z1 = [*x1,y1*];
set z2 = [*x2,y2*];
Re z1 = x1 & Re z2 = x2 & Im z1 = y1 & Im z2 = y2 by COMPLEX1:7;
hence thesis by COMPLEX1:def 10;
end;
theorem Th3:
for r be Real holds [*r,0*]*<i> = [*0,r*]
proof
let r be Real;
A1: Re [*0,1*] = 0 & Im [*0,1*] = 1 by COMPLEX1:7;
[*0,r*] = [*0,r*]*--1r by COMPLEX1:29
.= [*0,r*]*((-<i>)*<i>) by COMPLEX1:37,XCMPLX_1:175
.= [*0,r*]*(-[*0,1*])*<i> by COMPLEX1:def 8,XCMPLX_1:4
.= [*0,r*]*[*-0,-1*]*<i> by A1,COMPLEX1:def 11
.= [*0*0-r*-1,0*(-1)+r*0*]*<i> by Th2
.= [*0+(-r*-1),0*]*<i> by XCMPLX_0:def 8
.= [*r*1,0*]*<i> by XCMPLX_1:179;
hence thesis;
end;
theorem Th4:
for r be Real holds |.[*r,0*].| = abs r
proof
let r be Real;
Re [*r,0*] = r & Im [*r,0*] = 0 by COMPLEX1:7;
hence thesis by COMPLEX1:136;
end;
theorem Th5:
for z be Element of COMPLEX st |.z.| <> 0 holds
[*|.z.|,0*] = (z*'/[*|.z.|,0*])*z
proof
let z be Element of COMPLEX;
assume A1: |.z.| <> 0;
A2: (z*'/[*|.z.|,0*])*z = z*z*'/[*|.z.|,0*] by XCMPLX_1:75;
A3: Re(z*z*') = (Re z)^2 + (Im z)^2 & Im(z*z*') = 0 by COMPLEX1:126;
A4: Re [*|.z.|,0*] = |.z.| & Im [*|.z.|,0*] = 0 by COMPLEX1:7;
then A5: Re((z*'/[*|.z.|,0*])*z) = (((Re z)^2+(Im z)^2)*|.z.| + 0*0) / (|.z
.|^2 +0)
by A2,A3,COMPLEX1:82,SQUARE_1:60
.= |.z*z.|*|.z.| / |.z.|^2 by COMPLEX1:154
.= |.z*z.|*|.z.| / (|.z.|*|.z.|) by SQUARE_1:def 3
.= |.z*z.| / |.z.| by A1,XCMPLX_1:92
.= |.z.|*|.z.| / |.z.| by COMPLEX1:151
.= |.z.| by A1,XCMPLX_1:90;
Im((z*'/[*|.z.|,0*])*z) = (|.z.|*0 - ((Re z)^2+(Im z)^2)*0) / (|.z.|^2 +
0
)
by A2,A3,A4,COMPLEX1:82,SQUARE_1:60;
hence thesis by A5,COMPLEX1:8;
end;
begin :: Some Facts on the Field of Complex Numbers
definition
let x,y be Real;
func [**x,y**] -> Element of F_Complex equals :Def1:
[*x,y*];
coherence by COMPLFLD:def 1;
end;
definition
func i_FC -> Element of F_Complex equals :Def2:
<i>;
coherence
proof
<i> = [**0,1**] by Def1,COMPLEX1:def 8;
hence thesis;
end;
end;
theorem
i_FC = [*0,1*] & i_FC = [**0,1**] by Def1,Def2,COMPLEX1:def 8;
theorem
|.i_FC.| = 1 by Def2,COMPLEX1:135,COMPLFLD:def 3;
theorem Th8:
i_FC * i_FC = -1_ F_Complex
proof
thus i_FC * i_FC = -1r by Def2,COMPLEX1:37,COMPLFLD:6
.= -1_ F_Complex by COMPLFLD:4,10;
end;
theorem Th9:
(-1_ F_Complex) * (-1_ F_Complex) = 1_ F_Complex
proof
-1r = -1_ F_Complex by COMPLFLD:4,10;
hence (-1_ F_Complex) * (-1_ F_Complex) = (-1r) * -1r by COMPLFLD:6
.= --1r by COMPLEX1:46
.= 1_ F_Complex by COMPLFLD:10;
end;
theorem Th10:
for x1,y1,x2,y2 be Real holds
[**x1,y1**] + [**x2,y2**] = [**x1 + x2,y1 + y2**]
proof
let x1,y1,x2,y2 be Real;
[**x1,y1**] = [*x1,y1*] & [**x2,y2**] = [*x2,y2*] by Def1;
hence [**x1,y1**] + [**x2,y2**] = [*x1,y1*] + [*x2,y2*] by COMPLFLD:3
.= [*x1 + x2,y1 + y2*] by COMPLFLD:2
.= [**x1 + x2,y1 + y2**] by Def1;
end;
theorem Th11:
for x1,y1,x2,y2 be Real holds
[**x1,y1**] * [**x2,y2**] = [**x1*x2 - y1*y2,x1*y2+x2*y1**]
proof
let x1,y1,x2,y2 be Real;
[**x1,y1**] = [*x1,y1*] & [**x2,y2**] = [*x2,y2*] by Def1;
hence [**x1,y1**] * [**x2,y2**] = [*x1,y1*] * [*x2,y2*] by COMPLFLD:6
.= [*x1*x2 - y1*y2,x1*y2+x2*y1*] by Th2
.= [**x1*x2 - y1*y2,x1*y2+x2*y1**] by Def1;
end;
theorem
for z be Element of F_Complex holds
abs(|.z.|) = |.z.|
proof
let z be Element of F_Complex;
|.z.| >= 0 by COMPLFLD:95;
hence thesis by ABSVALUE:def 1;
end;
theorem Th13:
for r be Real holds |.[**r,0**].| = abs r
proof
let r be Real;
consider r1 be Element of COMPLEX such that
A1: [**r,0**] = r1 and
A2: |.[**r,0**].| = |.r1.| by COMPLFLD:def 3;
A3: r1 = [*r,0*] by A1,Def1;
then Im r1 = 0 by COMPLEX1:7;
then |.r1.| = abs Re r1 by COMPLEX1:136;
hence thesis by A2,A3,COMPLEX1:7;
end;
theorem Th14:
for r be Real holds [**r,0**]*i_FC = [**0,r**]
proof
let r be Real;
[**r,0**] = [*r,0*] by Def1;
hence [**r,0**]*i_FC = [*r,0*]*<i> by Def2,COMPLFLD:6
.= [*0,r*] by Th3
.= [**0,r**] by Def1;
end;
definition
let z be Element of F_Complex;
func Re z -> Real means :Def3:
ex z' be Element of COMPLEX st z = z' & it = Re z';
existence
proof
reconsider z'=z as Element of COMPLEX by COMPLFLD:def 1;
take z1=Re z';
take z';
thus z = z' & z1 = Re z';
end;
uniqueness;
end;
definition
let z be Element of F_Complex;
func Im z -> Real means :Def4:
ex z' be Element of COMPLEX st z = z' & it = Im z';
existence
proof
reconsider z'=z as Element of COMPLEX by COMPLFLD:def 1;
take z1 = Im z';
take z';
thus z = z' & z1 = Im z';
end;
uniqueness;
end;
theorem Th15:
for x,y be Real holds
Re [**x,y**] = x & Im [**x,y**] = y
proof
let x,y be Real;
consider z be Element of COMPLEX such that
A1: [**x,y**] = z and
A2: Re [**x,y**] = Re z by Def3;
z = [*x,y*] by A1,Def1;
hence Re [**x,y**] = x by A2,COMPLEX1:7;
consider z be Element of COMPLEX such that
A3: [**x,y**] = z and
A4: Im [**x,y**] = Im z by Def4;
z = [*x,y*] by A3,Def1;
hence thesis by A4,COMPLEX1:7;
end;
theorem Th16:
for x,y be Element of F_Complex holds
Re (x+y) = Re x + Re y &
Im (x+y) = Im x + Im y
proof
let x,y be Element of F_Complex;
consider x1 be Element of COMPLEX such that
A1: x = x1 and
A2: Re x = Re x1 by Def3;
consider y1 be Element of COMPLEX such that
A3: y = y1 and
A4: Re y = Re y1 by Def3;
consider xy1 be Element of COMPLEX such that
A5: x+y = xy1 and
A6: Re (x+y) = Re xy1 by Def3;
x+y = x1+y1 by A1,A3,COMPLFLD:3;
hence Re (x+y) = Re x + Re y by A2,A4,A5,A6,COMPLEX1:19;
consider x1 be Element of COMPLEX such that
A7: x = x1 and
A8: Im x = Im x1 by Def4;
consider y1 be Element of COMPLEX such that
A9: y = y1 and
A10: Im y = Im y1 by Def4;
consider xy1 be Element of COMPLEX such that
A11: x+y = xy1 and
A12: Im (x+y) = Im xy1 by Def4;
x+y = x1+y1 by A7,A9,COMPLFLD:3;
hence thesis by A8,A10,A11,A12,COMPLEX1:19;
end;
theorem Th17:
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
proof
let x,y be Element of F_Complex;
consider x1 be Element of COMPLEX such that
A1: x = x1 and
A2: Re x = Re x1 by Def3;
consider y1 be Element of COMPLEX such that
A3: y = y1 and
A4: Re y = Re y1 by Def3;
consider xy1 be Element of COMPLEX such that
A5: x*y = xy1 and
A6: Re (x*y) = Re xy1 by Def3;
consider x2 be Element of COMPLEX such that
A7: x = x2 and
A8: Im x = Im x2 by Def4;
consider y2 be Element of COMPLEX such that
A9: y = y2 and
A10: Im y = Im y2 by Def4;
consider xy2 be Element of COMPLEX such that
A11: x*y = xy2 and
A12: Im (x*y) = Im xy2 by Def4;
thus Re (x*y) = Re (x1*y1) by A1,A3,A5,A6,COMPLFLD:6
.= Re x * Re y - Im x * Im y by A1,A2,A3,A4,A7,A8,A9,A10,COMPLEX1:24;
thus Im (x*y) = Im (x1*y1) by A1,A3,A11,A12,COMPLFLD:6
.= Re x * Im y + Re y * Im x by A1,A2,A3,A4,A7,A8,A9,A10,COMPLEX1:24;
end;
theorem Th18:
for z be Element of F_Complex holds
Re z <= |.z.|
proof
let z be Element of F_Complex;
consider z1 be Element of COMPLEX such that
A1: z = z1 and
A2: Re z = Re z1 by Def3;
consider z2 be Element of COMPLEX such that
A3: z = z2 and
A4: |.z.| = |.z2.| by COMPLFLD:def 3;
thus thesis by A1,A2,A3,A4,COMPLEX1:140;
end;
theorem
for z be Element of F_Complex holds
Im z <= |.z.|
proof
let z be Element of F_Complex;
consider z1 be Element of COMPLEX such that
A1: z = z1 and
A2: Im z = Im z1 by Def4;
consider z2 be Element of COMPLEX such that
A3: z = z2 and
A4: |.z.| = |.z2.| by COMPLFLD:def 3;
thus thesis by A1,A2,A3,A4,COMPLEX1:141;
end;
begin :: Functionals of Vector Space
definition
let K be 1-sorted;
let V be VectSpStr over K;
mode Functional of V is Function of the carrier of V, the carrier of K;
canceled;
end;
definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let f,g be Functional of V;
func f+g -> Functional of V means :Def6:
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 LambdaD;
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:113;
end;
end;
definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let f be Functional of V;
func -f -> Functional of V means :Def7:
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 LambdaD;
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:113;
end;
end;
definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let f,g be Functional of V;
func f-g -> Functional of V equals :Def8:
f+-g;
coherence;
end;
definition
let K be non empty HGrStr;
let V be non empty VectSpStr over K;
let v be Element of K;
let f be Functional of V;
func v*f -> Functional of V means :Def9:
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 LambdaD;
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:113;
end;
end;
definition
let K be non empty ZeroStr;
let V be VectSpStr over K;
func 0Functional(V) -> Functional of V equals :Def10:
[#]V --> 0.K;
coherence
proof
[#]V = the carrier of V by PRE_TOPC:12;
hence [#]V --> 0.K is Functional of V;
end;
end;
definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let F be Functional of V;
attr F is additive means :Def11:
for x,y be Vector of V holds F.(x+y) = F.x+F.y;
end;
definition
let K be non empty HGrStr;
let V be non empty VectSpStr over K;
let F be Functional of V;
attr F is homogeneous means :Def12:
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 VectSpStr over K;
let F be Functional of V;
attr F is 0-preserving means
F.(0.V) = 0.K;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative left_unital distributive (non empty doubleLoopStr);
let V be VectSp of K;
cluster homogeneous -> 0-preserving 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:59
.= 0.K * F.(0.V) by A1,Def12
.= 0.K by VECTSP_1:39;
end;
end;
definition
let K be right_zeroed (non empty LoopStr);
let V be non empty VectSpStr over K;
cluster 0Functional(V) -> additive;
coherence
proof
let x,y be Vector of V;
A1: [#]V = the carrier of V by PRE_TOPC:12;
A2: (0Functional(V)).x = ([#]V --> 0.K).x by Def10
.= 0.K by A1,FUNCOP_1:13;
A3: (0Functional(V)).y = ([#]V --> 0.K).y by Def10
.= 0.K by A1,FUNCOP_1:13;
thus (0Functional(V)).(x+y) = ([#]V --> 0.K).(x+y) by Def10
.= 0.K by A1,FUNCOP_1:13
.= (0Functional(V)).x + (0Functional(V)).y
by A2,A3,RLVECT_1:def 7;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
cluster 0Functional(V) -> homogeneous;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
A1: [#]V = the carrier of V by PRE_TOPC:12;
A2: (0Functional(V)).x = ([#]V --> 0.K).x by Def10
.= 0.K by A1,FUNCOP_1:13;
thus (0Functional(V)).(r*x) = ([#]V --> 0.K).(r*x) by Def10
.= 0.K by A1,FUNCOP_1:13
.= r*(0Functional(V)).x by A2,VECTSP_1:36;
end;
end;
definition
let K be non empty ZeroStr;
let V be non empty VectSpStr over K;
cluster 0Functional(V) -> 0-preserving;
coherence
proof
A1: [#]V = the carrier of V by PRE_TOPC:12;
thus (0Functional(V)).(0.V) = ([#]V --> 0.K).(0.V) by Def10
.= 0.K by A1,FUNCOP_1:13;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
cluster additive homogeneous 0-preserving Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
theorem Th20:
for K be Abelian (non empty LoopStr)
for V be non empty VectSpStr over K
for f,g be Functional of V holds
f+g = g+f
proof
let K be Abelian (non empty LoopStr);
let V be non empty VectSpStr 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 Def6
.= (g+f).x by Def6;
end;
hence f+g = g+f by FUNCT_2:113;
end;
theorem Th21:
for K be add-associative (non empty LoopStr)
for V be non empty VectSpStr 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 LoopStr);
let V be non empty VectSpStr 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 Def6
.= f.x + g.x + h.x by Def6
.= f.x + (g.x + h.x) by RLVECT_1:def 6
.= f.x + ((g+h).x) by Def6
.= (f+(g+h)).x by Def6;
end;
hence f+g+h = f+(g+h) by FUNCT_2:113;
end;
theorem Th22:
for K be non empty ZeroStr
for V be non empty VectSpStr over K
for x be Element of V holds
(0Functional(V)).x = 0.K
proof
let K be non empty ZeroStr;
let V be non empty VectSpStr over K;
let x be Element of V;
x in the carrier of V;
then A1: x in [#]V by PRE_TOPC:12;
thus (0Functional(V)).x = ([#]V --> 0.K).x by Def10
.= 0.K by A1,FUNCOP_1:13;
end;
theorem Th23:
for K be right_zeroed (non empty LoopStr)
for V be non empty VectSpStr over K
for f be Functional of V holds
f + 0Functional(V) = f
proof
let K be right_zeroed (non empty LoopStr);
let V be non empty VectSpStr 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 Def6
.= f.x+0.K by Th22
.= f.x by RLVECT_1:def 7;
end;
hence thesis by FUNCT_2:113;
end;
theorem Th24:
for K be add-associative right_zeroed right_complementable
(non empty LoopStr)
for V be non empty VectSpStr 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 LoopStr);
let V be non empty VectSpStr over K;
let f be Functional of V;
now let x be Element of V;
thus (f-f).x = (f+-f).x by Def8
.= f.x+(-f).x by Def6
.= f.x+-f.x by Def7
.= 0.K by RLVECT_1:16
.= (0Functional(V)).x by Th22;
end;
hence thesis by FUNCT_2:113;
end;
theorem Th25:
for K be right-distributive (non empty doubleLoopStr)
for V be non empty VectSpStr 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 VectSpStr 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 Def9
.= r*(f.x+g.x) by Def6
.= r*f.x+r*g.x by VECTSP_1:def 11
.= (r*f).x+r*g.x by Def9
.= (r*f).x+(r*g).x by Def9
.= (r*f+r*g).x by Def6;
end;
hence thesis by FUNCT_2:113;
end;
theorem Th26:
for K be left-distributive (non empty doubleLoopStr)
for V be non empty VectSpStr 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 VectSpStr 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 Def9
.= r*f.x+s*f.x by VECTSP_1:def 12
.= (r*f).x+s*f.x by Def9
.= (r*f).x+(s*f).x by Def9
.= (r*f+s*f).x by Def6;
end;
hence thesis by FUNCT_2:113;
end;
theorem Th27:
for K be associative (non empty HGrStr)
for V be non empty VectSpStr 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 HGrStr);
let V be non empty VectSpStr 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 Def9
.= r*(s*f.x) by VECTSP_1:def 16
.= r*(s*f).x by Def9
.= (r*(s*f)).x by Def9;
end;
hence thesis by FUNCT_2:113;
end;
theorem Th28:
for K be left_unital (non empty doubleLoopStr)
for V be non empty VectSpStr 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 VectSpStr 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 Def9
.= f.x by VECTSP_1:def 19;
end;
hence thesis by FUNCT_2:113;
end;
definition
let K be Abelian add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr 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 Def6
.= f.x+f.y+g.(x+y) by Def11
.= f.x+f.y+(g.x+g.y) by Def11
.= f.x+(f.y+(g.x+g.y)) by RLVECT_1:def 6
.= f.x+(g.x+(f.y+g.y)) by RLVECT_1:def 6
.= f.x+g.x+(f.y+g.y) by RLVECT_1:def 6
.= (f+g).x+(f.y+g.y) by Def6
.= (f+g).x+(f+g).y by Def6;
end;
end;
definition
let K be Abelian add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr 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 Def7
.= -(f.x + f.y) by Def11
.= -f.x+-f.y by RLVECT_1:45
.= (-f).x+-f.y by Def7
.= (-f).x+(-f).y by Def7;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
let v be Element of K;
let f be additive Functional of V;
cluster v*f -> additive;
coherence
proof
let x,y be Vector of V;
thus (v*f).(x+y) = v*f.(x+y) by Def9
.= v*(f.x + f.y) by Def11
.= v*f.x+v*f.y by VECTSP_1:def 11
.= (v*f).x+v*f.y by Def9
.= (v*f).x+(v*f).y by Def9;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr 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 Def6
.= r*f.x + g.(r*x) by Def12
.= r*f.x + r*g.x by Def12
.= r*(f.x + g.x) by VECTSP_1:def 11
.= r*(f+g).x by Def6;
end;
end;
definition
let K be Abelian add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr 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 Def7
.= -r*f.x by Def12
.= r*-f.x by Lm1
.= r*(-f).x by Def7;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive associative commutative (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
let v be Element of K;
let f be homogeneous Functional of V;
cluster v*f -> homogeneous;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
thus (v*f).(r*x) = v*f.(r*x) by Def9
.= v*(r*f.x) by Def12
.= r*(v*f.x) by VECTSP_1:def 16
.= r*(v*f).x by Def9;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr 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 VectSpStr over K;
func V*' -> non empty strict VectSpStr over K means :Def14:
(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 add of it).(f,g) = f+g) &
(the Zero of 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
0Functional(V) in {x where x is linear-Functional of V: not contradiction
}
;
then reconsider ca = {x where x is linear-Functional of V :
not contradiction} 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 consider y be linear-Functional of V such that
A2: x=y;
thus x is linear-Functional of V by A2;
end;
thus x is linear-Functional of V implies x in ca;
end;
defpred P[set,set,set] means
ex f,g be Functional of V st $1=f & $2=g & $3=f+g;
A3: 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
A4: for x,y be Element of ca holds P[x,y,ad.[x,y]] from FuncEx2D(A3);
A5: now let f,g be linear-Functional of V;
reconsider x=f,y=g as Element of ca by A1;
consider f1,g1 be Functional of V such that
A6: x=f1 & y=g1 & ad.[x,y]=f1+g1 by A4;
thus ad.(f,g) = f+g by A6,BINOP_1:def 1;
end;
reconsider 0F=0Functional(V) as Element of ca by A1;
defpred P[Element of K,set,set] means
ex f be Functional of V st $2=f & $3=$1*f;
A7: 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
A8: for x be Element of K,y be Element of ca holds
P[x,y,lm.[x,y]] from FuncEx2D(A7);
A9: now let f be linear-Functional of V;
let x be Element of K;
reconsider y=f as Element of ca by A1;
consider f1 be Functional of V such that
A10: y=f1 & lm.[x,y]=x*f1 by A8;
thus lm.(x,f) = x*f by A10,BINOP_1:def 1;
end;
reconsider V1 = VectSpStr(# ca,ad,0F,lm #)
as non empty strict VectSpStr over K;
take V1;
thus thesis by A1,A5,A9;
end;
uniqueness
proof
let V1,V2 be non empty strict VectSpStr over K;
assume that
A11: for x be set holds x in the carrier of V1 iff
x is linear-Functional of V and
A12: for f,g be linear-Functional of V holds (the add of V1).(f,g)=f+g and
A13: the Zero of V1 = 0Functional(V) and
A14: for f be linear-Functional of V for x be Element of K
holds (the lmult of V1).(x,f) = x*f and
A15: for x be set holds x in the carrier of V2 iff
x is linear-Functional of V and
A16: for f,g be linear-Functional of V holds (the add of V2).(f,g)=f+g and
A17: the Zero of V2 = 0Functional(V) and
A18: for f be linear-Functional of V for x be Element of K
holds (the lmult of V2).(x,f) = x*f;
now let x be set;
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 A11;
hence x in the carrier of V2 by A15;
end;
assume x in the carrier of V2;
then x is linear-Functional of V by A15;
hence x in the carrier of V1 by A11;
end;
then A19: 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 A11;
thus (the add of V1).(x,y) = f+g by A12
.= (the add of V2).(x,y) by A16;
end;
then A20: the add of V1 = the add of V2 by A19,BINOP_1:2;
now let r be Element of K;
let x be Element of V1;
reconsider f=x as linear-Functional of V by A11;
thus (the lmult of V1).(r,x) = r*f by A14
.= (the lmult of V2).(r,x) by A18;
end;
hence V1 = V2 by A13,A17,A19,A20,BINOP_1:2;
end;
end;
definition
let K be Abelian add-associative right_zeroed right_complementable
right-distributive associative commutative (non empty doubleLoopStr);
let V be non empty VectSpStr 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 Def14;
thus v+w = (the add of V*').[v,w] by RLVECT_1:def 3
.= (the add of V*').(v,w) by BINOP_1:def 1
.= f+g by Def14
.= g+f by Th20
.= (the add of V*').(w,v) by Def14
.= (the add of V*').[w,v] by BINOP_1:def 1
.= w+v by RLVECT_1:def 3;
end;
end;
definition
let K be Abelian add-associative right_zeroed right_complementable
right-distributive associative commutative (non empty doubleLoopStr);
let V be non empty VectSpStr 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 Def14;
thus u+v+w = (the add of V*').[u+v,w] by RLVECT_1:def 3
.= (the add of V*').(u+v,w) by BINOP_1:def 1
.= (the add of V*').((the add of V*').[u,v],w) by RLVECT_1:def 3
.= (the add of V*').((the add of V*').(u,v),w) by BINOP_1:def 1
.= (the add of V*').(f+g,w) by Def14
.= f+g+h by Def14
.= f+(g+h) by Th21
.= (the add of V*').(u,g+h) by Def14
.= (the add of V*').(u,(the add of V*').(v,w)) by Def14
.= (the add of V*').(u,(the add of V*').[v,w]) by BINOP_1:def 1
.= (the add of V*').(u,v+w) by RLVECT_1:def 3
.= (the add of V*').[u,v+w] by BINOP_1:def 1
.= u+(v+w) by RLVECT_1:def 3;
end;
cluster V*' -> right_zeroed;
coherence
proof
let x be Element of V*';
reconsider f=x as linear-Functional of V by Def14;
thus x + 0.(V*') = (the add of V*').[x,0.(V*')] by RLVECT_1:def 3
.= (the add of V*').(x,0.(V*')) by BINOP_1:def 1
.= (the add of V*').(x,the Zero of V*') by RLVECT_1:def 2
.= (the add of V*').(x,0Functional(V)) by Def14
.= f+0Functional(V) by Def14
.= x by Th23;
end;
cluster V*' -> right_complementable;
coherence
proof
let x be Element of V*';
reconsider f=x as linear-Functional of V by Def14;
reconsider b = -f as Element of V*' by Def14;
take b;
thus x+b = (the add of V*').[x,b] by RLVECT_1:def 3
.= (the add of V*').(x,-f) by BINOP_1:def 1
.= f+-f by Def14
.= f-f by Def8
.= 0Functional(V) by Th24
.= the Zero of V*' by Def14
.= 0.(V*') by RLVECT_1:def 2;
end;
end;
definition
let K be Abelian add-associative right_zeroed right_complementable
left_unital distributive associative commutative (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
cluster V*' -> VectSp-like;
coherence
proof
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 Def14;
thus x*(v+w) = (the lmult of V*').(x,v+w) by VECTSP_1:def 24
.= (the lmult of V*').(x,(the add of V*').[v,w]) by RLVECT_1:def 3
.= (the lmult of V*').(x,(the add of V*').(v,w)) by BINOP_1:def 1
.= (the lmult of V*').(x,f+g) by Def14
.= x*(f+g) by Def14
.= x*f+x*g by Th25
.= (the add of V*').(x*f,x*g) by Def14
.= (the add of V*').((the lmult of V*').(x,f),x*g) by Def14
.= (the add of V*').((the lmult of V*').(x,f),(the lmult of V*').(x,g))
by Def14
.= (the add of V*').(x*v,(the lmult of V*').(x,g)) by VECTSP_1:def 24
.= (the add of V*').(x*v,x*w) by VECTSP_1:def 24
.= (the add of V*').[x*v,x*w] by BINOP_1:def 1
.= x*v+x*w by RLVECT_1:def 3;
thus (x+y)*v = (the lmult of V*').(x+y,v) by VECTSP_1:def 24
.= (x+y)*f by Def14
.= x*f+y*f by Th26
.= (the add of V*').(x*f,y*f) by Def14
.= (the add of V*').((the lmult of V*').(x,f),y*f) by Def14
.= (the add of V*').((the lmult of V*').(x,f),(the lmult of V*').(y,f))
by Def14
.= (the add of V*').(x*v,(the lmult of V*').(y,f)) by VECTSP_1:def 24
.= (the add of V*').(x*v,y*v) by VECTSP_1:def 24
.= (the add of V*').[x*v,y*v] by BINOP_1:def 1
.= x*v+y*v by RLVECT_1:def 3;
thus (x*y)*v = (the lmult of V*').(x*y,v) by VECTSP_1:def 24
.= (x*y)*f by Def14
.= x*(y*f) by Th27
.= (the lmult of V*').(x,y*f) by Def14
.= (the lmult of V*').(x,(the lmult of V*').(y,f)) by Def14
.= (the lmult of V*').(x,y*v) by VECTSP_1:def 24
.= x*(y*v) by VECTSP_1:def 24;
thus (1_ K)*v = (the lmult of V*').(1_ K,v) by VECTSP_1:def 24
.= (1_ K)*f by Def14
.= v by Th28;
end;
end;
begin :: Semi Norm of Vector Space
definition
let K be 1-sorted;
let V be VectSpStr over K;
mode RFunctional of V is Function of the carrier of V,REAL;
canceled;
end;
definition
let K be 1-sorted;
let V be non empty VectSpStr over K;
let F be RFunctional of V;
attr F is subadditive means :Def16:
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 VectSpStr over K;
let F be RFunctional of V;
attr F is additive means :Def17:
for x,y be Vector of V holds F.(x+y) = F.x+F.y;
end;
definition
let V be non empty VectSpStr over F_Complex;
let F be RFunctional of V;
attr F is Real_homogeneous means :Def18:
for v be Vector of V
for r be Real holds
F.([**r,0**]*v) = r*F.v;
end;
theorem Th29:
for V be VectSp-like (non empty VectSpStr 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 VectSp-like (non empty VectSpStr 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) by Th14
.= F.([**r,0**]*(i_FC*v)) by VECTSP_1:def 26
.= r*F.(i_FC*v) by A1,Def18;
end;
definition
let V be non empty VectSpStr over F_Complex;
let F be RFunctional of V;
attr F is homogeneous means :Def19:
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 VectSpStr over K;
let F be RFunctional of V;
attr F is 0-preserving means
F.(0.V) = 0;
end;
definition
let K be 1-sorted;
let V be non empty VectSpStr over K;
cluster additive -> subadditive RFunctional of V;
coherence
proof
let F be RFunctional of V;
assume A1: F is additive;
let x,y be Vector of V;
thus F.(x+y) <= F.x+F.y by A1,Def17;
end;
end;
L0: 0c = [*0,0*] by ARYTM_0:def 7,COMPLEX1:def 6;
L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7;
definition
let V be VectSp of F_Complex;
cluster Real_homogeneous -> 0-preserving RFunctional of V;
coherence
proof
let F be RFunctional of V;
assume A1: F is Real_homogeneous;
A2: 0.F_Complex = [**0,0**] by Def1,COMPLFLD:9,L0;
thus F.(0.V) = F.(0.F_Complex*0.V) by VECTSP_1:59
.= 0*F.(0.V) by A1,A2,Def18
.= 0;
end;
end;
definition
let K be 1-sorted;
let V be VectSpStr over K;
func 0RFunctional(V) -> RFunctional of V equals :Def21:
[#]V --> 0;
coherence
proof
[#]V = the carrier of V by PRE_TOPC:12;
hence [#]V --> 0 is RFunctional of V;
end;
end;
definition
let K be 1-sorted;
let V be non empty VectSpStr over K;
cluster 0RFunctional(V) -> additive;
coherence
proof
let x,y be Vector of V;
A1: [#]V = the carrier of V by PRE_TOPC:12;
A2: (0RFunctional(V)).x = ([#]V --> 0).x by Def21
.= 0 by A1,FUNCOP_1:13;
A3: (0RFunctional(V)).y = ([#]V --> 0).y by Def21
.= 0 by A1,FUNCOP_1:13;
thus (0RFunctional(V)).(x+y) = ([#]V --> 0).(x+y) by Def21
.= (0RFunctional(V)).x + (0RFunctional(V)).y
by A1,A2,A3,FUNCOP_1:13;
end;
cluster 0RFunctional(V) -> 0-preserving;
coherence
proof
A4: [#]V = the carrier of V by PRE_TOPC:12;
thus (0RFunctional(V)).(0.V) = ([#]V --> 0).(0.V) by Def21
.= 0 by A4,FUNCOP_1:13;
thus thesis;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
cluster 0RFunctional(V) -> Real_homogeneous;
coherence
proof
let x be Vector of V;
let r be Real;
A1: [#]V = the carrier of V by PRE_TOPC:12;
A2: (0RFunctional(V)).x = ([#]V --> 0).x by Def21
.= 0 by A1,FUNCOP_1:13;
thus (0RFunctional(V)).([**r,0**]*x) = ([#]V --> 0).([**r,0**]*x) by Def21
.= r*((0RFunctional(V)).x) by A1,A2,FUNCOP_1:13;
end;
cluster 0RFunctional(V) -> homogeneous;
coherence
proof
let x be Vector of V;
let r be Scalar of V;
A3: [#]V = the carrier of V by PRE_TOPC:12;
A4: (0RFunctional(V)).x = ([#]V --> 0).x by Def21
.= 0 by A3,FUNCOP_1:13;
thus (0RFunctional(V)).(r*x) = ([#]V --> 0).(r*x) by Def21
.= |.r.|*((0RFunctional(V)).x) by A3,A4,FUNCOP_1:13;
end;
end;
definition
let K be 1-sorted;
let V be non empty VectSpStr over K;
cluster additive 0-preserving RFunctional of V;
existence
proof
take 0RFunctional(V);
thus thesis;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
cluster additive Real_homogeneous homogeneous RFunctional of V;
existence
proof
take 0RFunctional(V);
thus thesis;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
mode Semi-Norm of V is subadditive homogeneous RFunctional of V;
end;
begin :: Hahn Banach Theorem
definition
let V be non empty VectSpStr over F_Complex;
func RealVS(V) -> strict RLSStruct means :Def22:
the LoopStr of it = the LoopStr 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 Real, v be Vector of V holds
f.[r,v]=F(r,v) from Lambda2D;
take R = RLSStruct (#the carrier of V, the Zero of V, the add of V, f#);
thus the LoopStr of R = the LoopStr of V;
let r be Real;
let v be Vector of V;
thus (the Mult of R).(r,v) = (the Mult of R).[r,v] by BINOP_1:def 1
.= [**r,0**]*v by A1;
end;
uniqueness
proof
let a,b be strict RLSStruct such that
A2: the LoopStr of a = the LoopStr 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 LoopStr of b = the LoopStr 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 Real, v be Vector of V;
thus (the Mult of a).[r,v] = (the Mult of a).(r,v) by BINOP_1:def 1
.= [**r,0**]*v by A3
.= (the Mult of b).(r,v) by A5
.= (the Mult of b).[r,v] by BINOP_1:def 1;
end;
hence a=b by A2,A4,FUNCT_2:120;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
cluster RealVS(V) -> non empty;
coherence
proof
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
hence RealVS(V) is non empty by STRUCT_0:def 1;
end;
end;
definition
let V be Abelian (non empty VectSpStr over F_Complex);
cluster RealVS(V) -> Abelian;
coherence
proof
let v,w be Element of RealVS(V);
A1: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider v1=v,w1=w as Element of V;
thus v + w = (the add of V).[v1,w1] by A1,RLVECT_1:def 3
.= v1 + w1 by RLVECT_1:def 3
.= (the add of RealVS(V)).[w,v] by A1,RLVECT_1:def 3
.= w + v by RLVECT_1:def 3;
end;
end;
definition
let V be add-associative (non empty VectSpStr over F_Complex);
cluster RealVS(V) -> add-associative;
coherence
proof
let u,v,w be Element of RealVS(V);
A1: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider u1=u,v1=v,w1=w as Element of V;
thus (u + v) + w = (the add of RealVS(V)).[u+v,w] by RLVECT_1:def 3
.= (the add of V).[((the add of V).[u1,v1]),w1] by A1,RLVECT_1
:def 3
.= (the add of V).[u1+v1,w1] by RLVECT_1:def 3
.= (u1 + v1) + w1 by RLVECT_1:def 3
.= u1 + (v1 + w1) by RLVECT_1:def 6
.= (the add of V).[u1,v1+w1] by RLVECT_1:def 3
.= (the add of RealVS(V)).[u,((the add of RealVS(V)).[v,w])]
by A1,RLVECT_1:def
3
.= (the add of RealVS(V)).[u,v+w] by RLVECT_1:def 3
.= u + (v + w) by RLVECT_1:def 3;
end;
end;
definition
let V be right_zeroed (non empty VectSpStr over F_Complex);
cluster RealVS(V) -> right_zeroed;
coherence
proof
let v be Element of RealVS(V);
A1: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider v1=v as Element of V;
thus v + 0.RealVS(V) = (the add of V).[v1,0.RealVS(V)] by A1,RLVECT_1:def 3
.= (the add of V).[v1,the Zero of RealVS(V)]
by RLVECT_1:def 2
.= (the add of V).[v1,0.V] by A1,RLVECT_1:def 2
.= v1 + 0.V by RLVECT_1:def 3
.= v by RLVECT_1:def 7;
end;
end;
definition
let V be right_complementable (non empty VectSpStr over F_Complex);
cluster RealVS(V) -> right_complementable;
coherence
proof
let v be Element of RealVS(V);
A1: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider v1=v as Element of V;
consider w1 be Element of V such that
A2: v1 + w1 = 0.V by RLVECT_1:def 8;
reconsider w=w1 as Element of RealVS(V) by A1;
take w;
thus v + w = (the add of V).[v1,w1] by A1,RLVECT_1:def 3
.= v1 + w1 by RLVECT_1:def 3
.= the Zero of RealVS(V) by A1,A2,RLVECT_1:def 2
.= 0.RealVS(V) by RLVECT_1:def 2;
end;
end;
definition
let V be VectSp-like (non empty VectSpStr over F_Complex);
cluster RealVS(V) -> RealLinearSpace-like;
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;
let v,w be Element of RealVS(V);
A1: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
set a1=[**a,0**];
reconsider v1=v,w1=w as Element of V by A1;
thus a * (v + w) = (the Mult of RealVS(V)).[a,v+w] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(a,v+w) by BINOP_1:def 1
.= (the Mult of RealVS(V)).(a,((the add of V).[v1,w1])) by A1,
RLVECT_1:def 3
.= (the Mult of RealVS(V)).(a,(v1 + w1)) by RLVECT_1:def 3
.= [**a,0**] * (v1 + w1) by Def22
.= a1 * v1 + a1 * w1 by VECTSP_1:def 26
.= (the add of V).[a1*v1,a1*w1] by RLVECT_1:def 3
.= (the add of V).[((the Mult of RealVS(V)).(a,v1)),[**a,0**]*w1]
by Def22
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).(a,v)),
((the Mult of RealVS(V)).(a,w))] by A1,
Def22
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).[a,v]),
((the Mult of RealVS(V)).(a,w))] by BINOP_1:def 1
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).[a,v]),
((the Mult of RealVS(V)).[a,w])] by BINOP_1:def 1
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).[a,v]),
(a*w)] by RLVECT_1:def 4
.= (the add of RealVS(V)).[a*v,a*w] by RLVECT_1:def 4
.= a * v + a * w by RLVECT_1:def 3;
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;
let v be Element of RealVS(V);
A2: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
set a1=[**a,0**];
set b1=[**b,0**];
[**a,0**] = [*a,0*] & [**b,0**] = [*b,0*] by Def1;
then A3: [**a,0**] + [**b,0**] = [*a,0*] + [*b,0*] by COMPLFLD:3
.= [*a+b,0+0*] by COMPLFLD:2
.= [**a+b,0**] by Def1;
reconsider v1=v as Element of V by A2;
thus (a + b) * v = (the Mult of RealVS(V)).[a+b,v] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(a+b,v) by BINOP_1:def 1
.= ([**a,0**] + [**b,0**]) * v1 by A3,Def22
.= a1 * v1 + b1 * v1 by VECTSP_1:def 26
.= (the add of RealVS(V)).[([**a,0**]*v1),([**b,0**]*v1)] by A2,
RLVECT_1:def 3
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).(a,v)),
([**b,0**]*v1)] by Def22
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).(a,v)),
((the Mult of RealVS(V)).(b,v))] by Def22
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).[a,v]),
((the Mult of RealVS(V)).(b,v))] by BINOP_1:def 1
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).[a,v]),
((the Mult of RealVS(V)).[b,v])] by BINOP_1:def 1
.= (the add of RealVS(V)).[((the Mult of RealVS(V)).[a,v]),
b*v] by RLVECT_1:def 4
.= (the add of RealVS(V)).[a*v,b*v] by RLVECT_1:def 4
.= a * v + b * v by RLVECT_1:def 3;
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;
let v be Element of RealVS(V);
A4: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
A5: [**a,0**]=[*a,0*] & [**b,0**]=[*b,0*] by Def1;
A6: [**a*b,0**] = [*a*b - 0*0,a*0+b*0*] by Def1
.= [*a,0*] * [*b,0*] by Th2
.= [**a,0**]*[**b,0**] by A5,COMPLFLD:6;
reconsider v1=v as Element of V by A4;
thus (a * b) * v = (the Mult of RealVS(V)).[a*b,v] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(a*b,v) by BINOP_1:def 1
.= ([**a,0**] * [**b,0**]) * v1 by A6,Def22
.= [**a,0**] * ([**b,0**] * v1) by VECTSP_1:def 26
.= (the Mult of RealVS(V)).(a,([**b,0**] * v1)) by Def22
.= (the Mult of RealVS(V)).(a,(the Mult of RealVS(V)).(b,v)) by Def22
.= (the Mult of RealVS(V)).[a,(the Mult of RealVS(V)).(b,v)]
by BINOP_1:def 1
.= (the Mult of RealVS(V)).[a,(the Mult of RealVS(V)).[b,v]]
by BINOP_1:def 1
.= (the Mult of RealVS(V)).[a,b*v] by RLVECT_1:def 4
.= a * (b * v) by RLVECT_1:def 4;
end;
let v be Element of RealVS(V);
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider v1=v as Element of V;
A7: [**1,0**] = 1_(F_Complex) by Def1,COMPLFLD:10,L1;
thus 1 * v = (the Mult of RealVS(V)).[1,v] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(1,v) by BINOP_1:def 1
.= [**1,0**] * v1 by Def22
.= v by A7,VECTSP_1:def 26;
end;
end;
theorem Th30:
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 LoopStr of M = the LoopStr of RealVS(M) by Def22;
A3: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
hence A4: the carrier of RealVS(M) c= the carrier of RealVS(V) by A2,
VECTSP_4:def 2;
thus the Zero of RealVS(M) = the Zero of RealVS(V) by A2,A3,VECTSP_4:def 2
;
thus the add of RealVS(M) = (the add of RealVS(V)) |
[:the carrier of RealVS(M),the carrier of RealVS(M):] by A2,A3,
VECTSP_4:def 2;
[:REAL,the carrier of RealVS(M):] c= [:REAL,the carrier of RealVS(V):]
by A4,ZFMISC_1:118;
then [:REAL,the carrier of RealVS(M):] c= dom (the Mult of RealVS(V))
by FUNCT_2:def 1;
then A5: dom((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):])=
[:REAL,the carrier of RealVS(M):] by RELAT_1:91;
A6: the lmult of M = (the lmult of V) |
[:the carrier of F_Complex, the carrier of M:] by VECTSP_4:def 2;
rng ((the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):]) c=
the carrier of RealVS(M)
proof
let y be set;
assume y in rng ((the Mult of RealVS(V)) |
[:REAL,the carrier of RealVS(M):]);
then consider x be set 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 5
;
consider a,b be set such that
A9: x = [a,b] by A7,ZFMISC_1:102;
reconsider a as Real by A7,A9,ZFMISC_1:106;
reconsider b as Element of RealVS(M)
by A5,A7,A9,ZFMISC_1:106;
reconsider b1 = b as Element of M by A2;
reconsider b2 = b1 as Element of V by A1,TARSKI:def 3;
A10: [[**a,0**],b1] in [:the carrier of F_Complex, the carrier of M:]
by ZFMISC_1:106;
[[**a,0**],b2] in [:the carrier of F_Complex, the carrier of V:]
by ZFMISC_1:106;
then [[**a,0**],b2] in dom (the lmult of V) by FUNCT_2:def 1;
then [[**a,0**],b2] in (dom (the lmult of V)) /\
[:the carrier of F_Complex, the carrier of M:] by A10,XBOOLE_0:def 3;
then A11: [[**a,0**],b2] in dom ((the lmult of V) |
[:the carrier of F_Complex, the carrier of M:]) by FUNCT_1:68;
y = (the Mult of RealVS(V)).[a,b] by A7,A8,A9,FUNCT_1:70
.= (the Mult of RealVS(V)).(a,b) by BINOP_1:def 1
.= [**a,0**]*b2 by Def22
.= (the lmult of V).([**a,0**],b2) by VECTSP_1:def 24
.= (the lmult of V).[[**a,0**],b2] by BINOP_1:def 1
.= (the lmult of M).[[**a,0**],b1] by A6,A11,FUNCT_1:70
.= (the lmult of M).([**a,0**],b1) by BINOP_1:def 1
.= [**a,0**]*b1 by VECTSP_1:def 24
.= (the Mult of RealVS(M)).(a,b) by Def22;
hence y in the carrier of RealVS(M);
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 A5,FUNCT_2:4;
now let a be Real,
b be Element of RealVS(M);
reconsider b1 = b as Element of M by A2;
reconsider b2 = b1 as Element of V by A1,TARSKI:def 3;
A12: [a,b] in [: REAL,the carrier of RealVS(M) :] by ZFMISC_1:106;
b in the carrier of RealVS(V) by A4,TARSKI:def 3;
then [a,b] in [: REAL,the carrier of RealVS(V) :] by ZFMISC_1:106;
then [a,b] in dom (the Mult of RealVS(V)) by FUNCT_2:def 1;
then [a,b] in (dom (the Mult of RealVS(V))) /\
[: REAL,the carrier of RealVS(M) :] by A12,XBOOLE_0:def 3;
then A13: [a,b] in dom RM by FUNCT_1:68;
A14: [[**a,0**],b1] in [:the carrier of F_Complex, the carrier of M:]
by ZFMISC_1:106;
[[**a,0**],b2] in [:the carrier of F_Complex, the carrier of V:]
by ZFMISC_1:106;
then [[**a,0**],b2] in dom (the lmult of V) by FUNCT_2:def 1;
then [[**a,0**],b2] in (dom (the lmult of V)) /\
[:the carrier of F_Complex, the carrier of M:] by A14,XBOOLE_0:def 3;
then A15: [[**a,0**],b2] in dom ((the lmult of V) |
[:the carrier of F_Complex, the carrier of M:]) by FUNCT_1:68;
thus (the Mult of RealVS(M)).(a,b) = [**a,0**]*b1 by Def22
.= (the lmult of M).([**a,0**],b1) by VECTSP_1:def 24
.= (the lmult of M).[[**a,0**],b1] by BINOP_1:def 1
.= (the lmult of V).[[**a,0**],b2] by A6,A15,FUNCT_1:70
.= (the lmult of V).([**a,0**],b2) by BINOP_1:def 1
.= [**a,0**]*b2 by VECTSP_1:def 24
.= (the Mult of RealVS(V)).(a,b) by Def22
.= (the Mult of RealVS(V)).[a,b] by BINOP_1:def 1
.= RM.[a,b] by A13,FUNCT_1:70
.= RM.(a,b) by BINOP_1:def 1;
end;
hence the Mult of RealVS(M) =
(the Mult of RealVS(V)) | [:REAL,the carrier of RealVS(M):] by BINOP_1:2;
end;
theorem Th31:
for V be non empty VectSpStr over F_Complex
for p be RFunctional of V holds
p is Functional of RealVS(V)
proof
let V be non empty VectSpStr over F_Complex;
let p be RFunctional of V;
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
hence p is Functional of RealVS(V);
end;
theorem Th32:
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 Th31;
A1: p1 is positively_homogeneous
proof
let x be VECTOR of RealVS(V);
let r be Real;
assume A2: r > 0;
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x as Vector of V;
r*x = (the Mult of RealVS(V)).[r,x] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(r,x) by BINOP_1:def 1
.= [**r,0**]*x1 by Def22;
hence p1.(r*x) = |.[**r,0**].|*p1.x by Def19
.= abs(r)*p1.x by Th13
.= r*p1.x by A2,ABSVALUE:def 1;
end;
p1 is subadditive
proof
let x,y be VECTOR of RealVS(V);
A3: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x, y1=y as Vector of V;
x+y = (the add of V).[x1,y1] by A3,RLVECT_1:def 3
.= x1+y1 by RLVECT_1:def 3;
hence p1.(x+y) <= p1.x + p1.y by Def16;
end;
hence thesis by A1;
end;
definition
let V be non empty VectSpStr over F_Complex;
let l be Functional of V;
func projRe(l) -> Functional of RealVS(V) means :Def23:
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 LambdaD;
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
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 LoopStr of V = the LoopStr of RealVS(V) by Def22;
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:113;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
let l be Functional of V;
func projIm(l) -> Functional of RealVS(V) means :Def24:
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 LambdaD;
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
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 LoopStr of V = the LoopStr of RealVS(V) by Def22;
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:113;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
let l be Functional of RealVS(V);
func RtoC(l) -> RFunctional of V equals :Def25:
l;
coherence
proof
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
hence thesis;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
let l be RFunctional of V;
func CtoR(l) -> Functional of RealVS(V) equals :Def26:
l;
coherence
proof
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
hence thesis;
end;
end;
definition
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 LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x,y1=y as VECTOR of RealVS(V);
x+y = (the add of RealVS(V)).[x1,y1] by A1,RLVECT_1:def 3
.= x1+y1 by RLVECT_1:def 3;
hence (RtoC l).(x+y) = l.(x1+y1) by Def25
.= l.x1+l.y1 by HAHNBAN:def 4
.= (RtoC l).x+l.y1 by Def25
.= (RtoC l).x+(RtoC l).y by Def25;
end;
end;
definition
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 LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x,y1=y as Vector of V;
x+y = (the add of V).[x1,y1] by A1,RLVECT_1:def 3
.= x1+y1 by RLVECT_1:def 3;
hence (CtoR l).(x+y) = l.(x1+y1) by Def26
.= l.x1+l.y1 by Def17
.= (CtoR l).x+l.y1 by Def26
.= (CtoR l).x+(CtoR l).y by Def26;
end;
end;
definition
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 LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x as VECTOR of RealVS(V);
[**r,0**]*x = (the Mult of RealVS(V)).(r,x) by Def22
.= (the Mult of RealVS(V)).[r,x] by BINOP_1:def 1
.= r*x1 by RLVECT_1:def 4;
hence (RtoC l).([**r,0**]*x) = l.(r*x1) by Def25
.= r*l.x1 by HAHNBAN:def 5
.= r*(RtoC l).x by Def25;
end;
end;
definition
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 LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x as Vector of V;
[**r,0**]*x1 = (the Mult of RealVS(V)).(r,x1) by Def22
.= (the Mult of RealVS(V)).[r,x1] by BINOP_1:def 1
.= r*x by RLVECT_1:def 4;
hence (CtoR l).(r*x) = l.([**r,0**]*x1) by Def26
.= r*l.x1 by Def18
.= r*(CtoR l).x by Def26;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
let l be RFunctional of V;
func i-shift(l) -> RFunctional of V means :Def27:
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 LambdaD;
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:113;
end;
end;
definition
let V be non empty VectSpStr over F_Complex;
let l be Functional of RealVS(V);
func prodReIm(l) -> Functional of V means :Def28:
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 LambdaD;
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:113;
end;
end;
theorem Th33:
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 additive
proof
let x,y be VECTOR of RealVS(V);
A2: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x, y1=y as Vector of V;
x+y = (the add of V).[x1,y1] by A2,RLVECT_1:def 3
.= x1+y1 by RLVECT_1:def 3;
hence (projRe(l)).(x+y) = Re(l.(x1+y1)) by Def23
.= Re(l.x1+l.y1) by Def11
.= Re(l.x1)+Re(l.y1) by Th16
.= Re(l.x1)+(projRe(l)).y by Def23
.= (projRe(l)).x+(projRe(l)).y by Def23;
end;
projRe(l) is homogeneous
proof
let x be VECTOR of RealVS(V);
let r be Real;
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x as Vector of V;
r*x = (the Mult of RealVS(V)).[r,x] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(r,x) by BINOP_1:def 1
.= [**r,0**]*x1 by Def22;
hence (projRe(l)).(r*x) = Re(l.([**r,0**]*x1)) by Def23
.= Re([**r,0**]*l.x1) by Def12
.= Re [**r,0**] * Re (l.x1) - Im [**r,0**] * Im (l.x1) by Th17
.= Re [**r,0**] * Re (l.x1) - 0 * Im (l.x1) by Th15
.= r * Re (l.x1) by Th15
.= r*(projRe(l)).x by Def23;
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 additive
proof
let x,y be VECTOR of RealVS(V);
A2: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x, y1=y as Vector of V;
x+y = (the add of V).[x1,y1] by A2,RLVECT_1:def 3
.= x1+y1 by RLVECT_1:def 3;
hence (projIm(l)).(x+y) = Im(l.(x1+y1)) by Def24
.= Im(l.x1+l.y1) by Def11
.= Im(l.x1)+Im(l.y1) by Th16
.= Im(l.x1)+(projIm(l)).y by Def24
.= (projIm(l)).x+(projIm(l)).y by Def24;
end;
projIm(l) is homogeneous
proof
let x be VECTOR of RealVS(V);
let r be Real;
the LoopStr of V = the LoopStr of RealVS(V) by Def22;
then reconsider x1=x as Vector of V;
r*x = (the Mult of RealVS(V)).[r,x] by RLVECT_1:def 4
.= (the Mult of RealVS(V)).(r,x) by BINOP_1:def 1
.= [**r,0**]*x1 by Def22;
hence (projIm(l)).(r*x) = Im(l.([**r,0**]*x1)) by Def24
.= Im([**r,0**]*l.x1) by Def12
.= Re [**r,0**] * Im (l.x1) + Re (l.x1) * Im [**r,0**] by Th17
.= Re [**r,0**] * Im (l.x1) + Re (l.x1) * 0 by Th15
.= r * Im (l.x1) by Th15
.= r*(projIm(l)).x by Def24;
end;
hence thesis by A1;
end;
theorem Th35:
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 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 Def28
.= [**(RtoC l).(x+y),-(RtoC l).(i_FC*(x+y))**] by Def27
.= [**(RtoC l).x+(RtoC l).y,-(RtoC l).(i_FC*(x+y))**] by Def17
.= [**(RtoC l).x+(RtoC l).y,
-(RtoC l).(i_FC*x+i_FC*y)**] by VECTSP_1:def 26
.= [**(RtoC l).x+(RtoC l).y,
-((RtoC l).(i_FC*x)+(RtoC l).(i_FC*y))**] by Def17
.= [**(RtoC l).x+(RtoC l).y,
-(RtoC l).(i_FC*x)+-(RtoC l).(i_FC*y)**] by XCMPLX_1:140
.= [**(RtoC l).x,-(RtoC l).(i_FC*x)**] +
[**(RtoC l).y,-(RtoC l).(i_FC*y)**] by Th10
.= [**(RtoC l).x,-(i-shift(RtoC l)).x**] +
[**(RtoC l).y,-(RtoC l).(i_FC*y)**] by Def27
.= [**(RtoC l).x,-(i-shift(RtoC l)).x**] +
[**(RtoC l).y,-(i-shift(RtoC l)).y**] by Def27
.= (prodReIm(l)).x + [**(RtoC l).y,-(i-shift(RtoC l)).y**] by Def28
.= (prodReIm(l)).x + (prodReIm(l)).y by Def28;
end;
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;
A2: [**(RtoC l).x,-(RtoC l).(i_FC*x)**] =
[*(RtoC l).x,-(RtoC l).(i_FC*x)*] by Def1;
set a=Re r1,b=Im r1;
A3: r1 = [*a,b*] by COMPLEX1:8;
then A4: r = [**a,b**] by Def1;
A5: a*((RtoC l).x)-b*(-(RtoC l).(i_FC*x)) =
a*((RtoC l).x)+-b*(-(RtoC l).(i_FC*x)) by XCMPLX_0:def 8
.= a*((RtoC l).x)+b*(RtoC l).(i_FC*x) by XCMPLX_1:179
.= (RtoC l).([**a,0**]*x)+b*(RtoC l).(i_FC*x) by Def18
.= (RtoC l).([**a,0**]*x)+(RtoC l).([**0,b**]*x) by Th29
.= (RtoC l).([**a,0**]*x+[**0,b**]*x) by Def17
.= (RtoC l).(([**a,0**]+[**0,b**])*x) by VECTSP_1:def 26
.= (RtoC l).([**a+0,0+b**]*x) by Th10
.= (RtoC l).(r*x) by A3,Def1;
A6: x = (-1_ F_Complex)*(-1_ F_Complex)*x by Th9,VECTSP_1:def 26
.= i_FC*(i_FC*(-1_ F_Complex))*x by Th8,VECTSP_1:def 16
.= i_FC*((-1_ F_Complex)*i_FC*x) by VECTSP_1:def 26;
-1_ F_Complex = -[*1,0*] by COMPLFLD:4,10,L1
.= [*-Re [*1,0*],-Im [*1,0*]*] by COMPLEX1:def 11
.= [*-1,-Im [*1,0*]*] by COMPLEX1:7
.= [*-1,-0*] by COMPLEX1:7
.= [**-1,0**] by Def1;
then A7: [**0,-b**]*(-1_ F_Complex) = [**0*-1-(-b)*0,0*0+(-b)*-1**] by Th11
.=[**0,b*1**] by XCMPLX_1:177;
A8: 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))
by A6,XCMPLX_1:175
.= -(RtoC l).([**a,0**]*(i_FC*x))+
b*(RtoC l).(i_FC*((-1_ F_Complex)*i_FC*x)) by Def18
.= -(RtoC l).([**a,0**]*(i_FC*x))+
-(-b)*(RtoC l).(i_FC*((-1_ F_Complex)*i_FC*x)) by XCMPLX_1:179
.= -(RtoC l).([**a,0**]*(i_FC*x))+
-(RtoC l).([**0,-b**]*((-1_ F_Complex)*i_FC*x)) by Th29
.= -(RtoC l).([**a,0**]*(i_FC*x))+
-(RtoC l).([**0,-b**]*((-1_ F_Complex)*(i_FC*x))) by VECTSP_1:def 26
.= -(RtoC l).([**a,0**]*(i_FC*x))+
-(RtoC l).([**0,-b**]*(-1_ F_Complex)*(i_FC*x)) by VECTSP_1:def 26
.= -((RtoC l).([**a,0**]*(i_FC*x))+(RtoC l).([**0,b**]*(i_FC*x)))
by A7,XCMPLX_1:
140
.= -(RtoC l).([**a,0**]*(i_FC*x)+[**0,b**]*(i_FC*x)) by Def17
.= -(RtoC l).(([**a,0**]+[**0,b**])*(i_FC*x)) by VECTSP_1:def 26
.= -(RtoC l).([**a+0,0+b**]*(i_FC*x)) by Th10
.= -(RtoC l).(i_FC*r*x) by A4,VECTSP_1:def 26;
thus (prodReIm(l)).(r*x) =
[**(RtoC l).(r*x),-(i-shift(RtoC l)).(r*x)**] by Def28
.= [**(RtoC l).(r*x),-(RtoC l).(i_FC*(r*x))**] by Def27
.= [**(RtoC l).(r*x),-(RtoC l).(i_FC*r*x)**] by VECTSP_1:def 26
.= [*(RtoC l).(r*x),-(RtoC l).(i_FC*r*x)*] by Def1
.= r1*[*(RtoC l).x,-(RtoC l).(i_FC*x)*] by A3,A5,A8,Th2
.= r*[**(RtoC l).x,-(RtoC l).(i_FC*x)**] by A2,COMPLFLD:6
.= r*[**(RtoC l).x,-(i-shift(RtoC l)).x**] by Def27
.= r*(prodReIm(l)).x by Def28;
end;
hence thesis by A1;
end;
theorem :: Hahn Banach 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;
let M be Subspace of V;
let l be linear-Functional of M;
assume A1: for e be Vector of M
for v be Vector of V st v=e holds |.l.e.| <= p.v;
reconsider RVSM = RealVS(M) as Subspace of RealVS(V) by Th30;
reconsider p1=p as Banach-Functional of RealVS(V) by Th32;
reconsider prRl = projRe(l) as linear-Functional of RVSM by Th33;
A2: the LoopStr of V = the LoopStr of RealVS(V) by Def22;
A3: the LoopStr of M = the LoopStr of RealVS(M) by Def22;
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;
let v be VECTOR of RealVS(V);
reconsider x1=x as Vector of M by A3;
reconsider v1=v as Vector of V by A2;
assume x=v;
then A4: |.l.x1.| <= p.v1 by A1;
prRl.x = Re(l.x1) by Def23;
then prRl.x <= |.l.x1.| by Th18;
hence prRl.x <= p1.v by A4,AXIOMS:22;
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:35;
reconsider L=prodReIm(L1) as linear-Functional of V by Th35;
take L;
reconsider tcM = the carrier of M as Subset of V
by VECTSP_4:def 2;
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 by TARSKI:def 3;
reconsider x1=x2,ix1=i_FC*x2 as Element of RealVS(V) by A2;
A7: L1.x1 = (projRe(l)).x1 by A3,A5,FUNCT_1:72
.= Re(l.x) by Def23;
reconsider lx=l.x as Element of COMPLEX by COMPLFLD:def 1;
lx = [*Re lx,Im lx*] by COMPLEX1:8;
then A8: i_FC*l.x = [*0,1*]*[*Re lx,Im lx*] by Def2,COMPLEX1:def 8,
COMPLFLD:6
.= [*0*Re lx-1*Im lx,0*Im lx+1*Re lx*] by Th2
.= [*-Im lx,Re lx*] by XCMPLX_1:150;
A9: i_FC*x = i_FC*x2 by VECTSP_4:22;
then A10: L1.ix1 = (projRe(l)).ix1 by A3,A5,FUNCT_1:72
.= Re(l.(i_FC*x)) by A9,Def23
.= Re(i_FC*l.x) by Def12
.= Re [*-Im lx,Re lx*] by A8,Def3
.= -Im lx by COMPLEX1:7
.= -Im(l.x) by Def4;
consider lx1 be Element of COMPLEX such that
A11: l.x = lx1 & Re(l.x) = Re lx1 by Def3;
consider lx2 be Element of COMPLEX such that
A12: l.x = lx2 & Im(l.x) = Im lx2 by Def4;
thus (L|tcM).x = L.x by FUNCT_1:72
.= [**(RtoC L1).x2,-(i-shift(RtoC L1)).x2**] by Def28
.= [**(RtoC L1).x2,-(RtoC L1).(i_FC*x2)**] by Def27
.= [**Re(l.x),-(RtoC L1).(i_FC*x2)**] by A7,Def25
.= [**Re(l.x),--Im(l.x)**] by A10,Def25
.= [*Re(l.x),Im(l.x)*] by Def1
.= l.x by A11,A12,COMPLEX1:8;
end;
hence L|the carrier of M = l by FUNCT_2:113;
let e be Vector of V;
reconsider Le = L.e as Element of COMPLEX by COMPLFLD:def 1;
reconsider Ledz = Le*'/[*|.Le.|,0*] as Element of F_Complex
by COMPLFLD:def 1;
reconsider e1=e,Ledze=Ledz*e as VECTOR of RealVS(V) by A2;
per cases;
suppose A13: |.Le.| <> 0;
A14: |.[*|.Le.|,0*].| = abs |.Le.| by Th4
.= |.Le.| by Th1;
A15: [*|.Le.|,0*] <> 0c by A13,ARYTM_0:12,L0;
A16: |.Ledz.| = |.Le*'/[*|.Le.|,0*].| by COMPLFLD:def 3
.= |.Le*'.|/|.[*|.Le.|,0*].| by A15,COMPLEX1:153
.= |.Le.|/|.Le.| by A14,COMPLEX1:139
.= 1 by A13,XCMPLX_1:60;
A17: p1.Ledze = |.Ledz.|*p.e by Def19
.= p.e by A16;
[*|.Le.|,0*] = (Le*'/[*|.Le.|,0*])*Le by A13,Th5
.= Ledz*L.e by COMPLFLD:6
.= L.(Ledz*e) by Def12
.= [**(RtoC L1).(Ledz*e),-(i-shift(RtoC L1)).(Ledz*e)**] by Def28
.= [*(RtoC L1).(Ledz*e),-(i-shift(RtoC L1)).(Ledz*e)*] by Def1
.= [*L1.Ledze,-(i-shift(RtoC L1)).(Ledz*e)*] by Def25;
then L1.Ledze = |.Le.| by ARYTM_0:12
.= |.L.e.| by COMPLFLD:def 3;
hence |.L.e.| <= p.e by A6,A17;
suppose |.Le.| = 0;
then A18: |.L.e.| = 0 by COMPLFLD:def 3;
A19: [**(RtoC L1).e,-(i-shift(RtoC L1)).e**] =
[*(RtoC L1).e,-(i-shift(RtoC L1)).e*] by Def1;
|.L.e.| = |.[**(RtoC L1).e,-(i-shift(RtoC L1)).e**].| by Def28
.= |.[*(RtoC L1).e,-(i-shift(RtoC L1)).e*].| by A19,COMPLFLD:def 3;
then [*(RtoC L1).e,-(i-shift(RtoC L1)).e*] = [*0,0*]
by A18,COMPLEX1:131,L0;
then (RtoC L1).e = 0 by ARYTM_0:12;
then L1.e1 = 0 by Def25;
hence |.L.e.| <= p.e by A6,A18;
end;