:: Hermitan Functionals. {C}anonical Construction of Scalar Product in
:: Quotient Vector Space
:: by Jaros{\l}aw Kotowicz
::
:: Received November 12, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, ARYTM_3, RELAT_1, XCMPLX_0, ARYTM_1, SUBSET_1,
COMPLEX1, SQUARE_1, XXREAL_0, COMPLFLD, HAHNBAN1, GROUP_1, SUPINF_2,
MESFUNC1, XBOOLE_0, VECTSP_1, HAHNBAN, FUNCT_1, RLVECT_1, ALGSTR_0,
MSSUBFAM, STRUCT_0, UNIALG_1, ZFMISC_1, VECTSP10, TARSKI, RLSUB_1,
GROUP_6, BILINEAR, REAL_1, HERMITAN, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, FUNCT_2, MEMBERED,
STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, SQUARE_1,
COMPLEX1, VECTSP_4, COMSEQ_2, COMPLFLD, HAHNBAN1, VECTSP10, BILINEAR;
constructors REAL_1, SQUARE_1, BINOP_2, BORSUK_1, BILINEAR, FUNCOP_1,
SUPINF_1, BINOP_1, COMSEQ_2;
registrations RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1,
STRUCT_0, VECTSP_1, COMPLFLD, HAHNBAN1, VECTSP10, BILINEAR, ORDINAL1,
VALUED_0, MEMBERED, ALGSTR_0, GRCAT_1;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
definitions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_4, VECTSP10, BILINEAR, FUNCT_1,
VECTSP_1;
equalities HAHNBAN1, XBOOLE_0, VECTSP10, BILINEAR, SQUARE_1, BINOP_1,
COMPLEX1, VECTSP_1, ALGSTR_0;
expansions HAHNBAN1, VECTSP10, BILINEAR, FUNCT_1, BINOP_1, VECTSP_1;
theorems COMPLEX1, SQUARE_1, ABSVALUE, COMPLFLD, XREAL_0, FUNCT_2, HAHNBAN1,
VECTSP_1, RLVECT_1, VECTSP_4, VECTSP_6, TARSKI, VECTSP10, BILINEAR,
DOMAIN_1, ZFMISC_1, FUNCT_1, XCMPLX_1, XREAL_1, XXREAL_0, FUNCOP_1,
STRUCT_0, COMSEQ_2;
schemes FUNCT_2, BINOP_1;
begin :: Auxiliary Facts about Complex Numbers
Lm1: 0 = 0 +0*<i>;
theorem Th1:
for a be Complex st a = a*' holds Im a = 0
proof
let z be Complex;
assume z = z*';
then Im z = 0+ -(Im z) by COMPLEX1:27;
hence thesis;
end;
theorem Th2:
for a be Complex st a <> 0c holds |.(Re a)/|.a.|+ (-Im
a)/|.a.|*<i>.| = 1 & Re (((Re a)/|.a.|+ (-Im a)/|.a.|*<i>) * a) = |.a.| & Im ((
(Re a)/|.a.|+ (-Im a)/|.a.|*<i>) * a)= 0
proof
let z be Complex;
set r = |.z.|, a = (Re z)/r+ (-Im z)/r*<i>;
assume z <> 0c;
then
A1: 0 < r by COMPLEX1:47;
|.z*z.| = (Re z)^2 + (Im z)^2 by COMPLEX1:68;
then 0 <= (Re z)^2 + (Im z)^2 by COMPLEX1:46;
then
A2: r^2 = (Re z)^2 + (Im z)^2 by SQUARE_1:def 2;
A3: Re a = (Re z)/r & Im a = (-Im z)/r by COMPLEX1:12;
then (Re a)^2 + (Im a)^2 = (Re z)^2/r^2 + ((-Im z)/r)^2 by XCMPLX_1:76
.= (Re z)^2/r^2 + (-Im z)^2/r^2 by XCMPLX_1:76
.= ((Re z)^2 + (Im z)^2)/r^2 by XCMPLX_1:62
.= 1^2 by A1,A2,XCMPLX_1:60;
hence |.a.| = 1;
thus Re (a*z) = (Re z)/r * Re z - (-Im z)/r * Im z by A3,COMPLEX1:9
.= ((Re z)*(Re z))/r - (-Im z)/r * Im z by XCMPLX_1:74
.= (Re z)^2/r - ((-Im z)* Im z )/r by XCMPLX_1:74
.= ((Re z)^2 - -(Im z * Im z) )/r by XCMPLX_1:120
.= r by A1,A2,XCMPLX_1:89;
thus Im(a*z) = (Re z)/r * Im z + Re z * ((-Im z)/r) by A3,COMPLEX1:9
.= (Re z) * (Im z) /r + Re z * ((-Im z)/r) by XCMPLX_1:74
.= (Re z) * (Im z) /r + (-Im z)* (Re z) /r by XCMPLX_1:74
.= ((Re z) * (Im z) + -(Im z)* (Re z)) /r by XCMPLX_1:62
.=0;
end;
theorem
for a be Complex ex b be Complex st |.b.| = 1 &
Re (b * a) = |.a.| & Im (b * a)= 0
proof
let z be Complex;
set r = |.z.|;
A1: r = 0 implies ex a be Element of COMPLEX st |.a.| =1 & Re (a * z) = r &
Im (a * z)= 0
proof
assume
A2: r = 0;
take 1r;
thus thesis by A2,COMPLEX1:4,45,48;
end;
0 < r implies ex a be Complex st |.a.| =1 & Re (a * z) = r &
Im (a * z)= 0
proof
assume
A3: 0 < r;
take (Re z)/r+ (-Im z)/r*<i>;
thus thesis by A3,Th2,COMPLEX1:44;
end;
hence thesis by A1,COMPLEX1:46;
end;
theorem Th4:
for a be Element of COMPLEX holds a*a*' = |.a.|^2+0*<i>
proof
let z be Element of COMPLEX;
0<= (Re z)^2 & 0<= (Im z)^2 by XREAL_1:63;
then (Re z)^2 + (Im z)^2 = |.z.|^2 by SQUARE_1:def 2;
then
A1: Re (z*z*')=|.z.|^2 by COMPLEX1:40;
Im (z*z*')=0 by COMPLEX1:40;
hence thesis by A1,COMPLEX1:13;
end;
theorem
for a be Element of F_Complex st a = a*' holds Im a = 0 by Th1;
theorem
i_FC * i_FC*' = 1_F_Complex by COMPLEX1:7,COMPLFLD:8;
theorem Th7:
for a be Element of F_Complex st a <> 0.F_Complex holds |.[**(Re
a)/|.a.|, (-Im a)/|.a.|**].| = 1 & Re ([**(Re a)/|.a.|, (-Im a)/|.a.|**] * a) =
|.a.| & Im ([**(Re a)/|.a.|, (-Im a)/|.a.|**] * a) = 0
by Th2,COMPLFLD:7;
theorem Th8:
for a be Element of F_Complex ex b be Element of F_Complex st |.b
.| = 1 & Re (b * a) = |.a.| & Im (b * a)= 0
proof
let z be Element of F_Complex;
set r = |.z.|;
A1: r = 0 implies ex a be Element of F_Complex st |.a.| = 1 & Re (a * z) = r
& Im (a * z) = 0
proof
assume
A2: r = 0;
take a=1.F_Complex;
thus |.a.| = 1 by COMPLFLD:60;
z = 0.F_Complex by A2,COMPLFLD:58
.= 0 by COMPLFLD:def 1;
hence thesis by A2,Lm1,COMPLEX1:12;
end;
0 < r implies ex a be Element of F_Complex st |.a.| =1 & Re (a * z) = r
& Im (a * z)= 0
proof
assume
A3: 0 < r;
take [**(Re z)/r, (-Im z)/r**];
thus thesis by A3,Th7,COMPLFLD:57;
end;
hence thesis by A1,COMPLEX1:46;
end;
theorem Th9:
for a,b be Element of F_Complex holds Re (a - b) = Re a - Re b &
Im (a - b) = Im a - Im b
proof
let a,b be Element of F_Complex;
reconsider x = a, y =b as Element of COMPLEX by COMPLFLD:def 1;
thus Re (a-b) = Re (x-y)
.= Re a - Re b by COMPLEX1:19;
thus Im (a-b) = Im (x-y)
.= Im a - Im b by COMPLEX1:19;
end;
theorem Th10:
for a,b be Element of F_Complex st Im a = 0 holds
Re (a*b) = Re a * Re b & Im (a*b) = Re a * Im b
proof
let a,b be Element of F_Complex;
assume
A1: Im a = 0;
hence Re (a*b) =Re a * Re b - 0 * Im b by HAHNBAN1:11
.= Re a * Re b;
thus Im (a*b) = Re a* Im b+ Re b * 0 by A1,HAHNBAN1:11
.= Re a * Im b;
end;
theorem
for a,b be Element of F_Complex st Im a = 0 & Im b = 0 holds Im (a*b) = 0
proof
let a,b be Element of F_Complex;
assume Im a = 0 & Im b = 0;
hence Im (a*b) = Re b * 0 by Th10
.= 0;
end;
theorem Th12:
for a be Element of F_Complex st Im a = 0 holds a = a*'
proof
let x be Element of F_Complex;
reconsider d = x as Element of COMPLEX by COMPLFLD:def 1;
assume Im x = 0;
hence x = Re d+(-Im d)*<i> by COMPLEX1:13
.= x*';
end;
theorem Th13:
for a be Element of F_Complex holds a*a*' = |.a.|^2
proof
let z be Element of F_Complex;
reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;
thus z*z*' = |.a.|^2+0*<i> by Th4
.= |.z.|^2;
end;
theorem Th14:
for a be Element of F_Complex st 0 <= Re a & Im a = 0 holds |.a .| = Re a
proof
let z be Element of F_Complex;
assume that
A1: 0 <= Re z and
A2: Im z = 0;
reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;
|. a .| = |.Re a.| by A2,COMPLEX1:50;
hence thesis by A1,ABSVALUE:def 1;
end;
theorem Th15:
for a be Element of F_Complex holds Re a + Re (a*') = 2 * Re a
proof
let z be Element of F_Complex;
thus Re z + Re (z*') = Re z + Re z by COMPLEX1:27
.= 2* (Re z);
end;
begin :: Antilinear Functionals in Complex Vector Spaces
definition
let V be non empty ModuleStr over F_Complex;
let f be Functional of V;
attr f is cmplxhomogeneous means
:Def1:
for v be Vector of V, a be Scalar of V holds f.(a*v) = (a*')*f.v;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster 0Functional(V) -> cmplxhomogeneous;
coherence
proof
let x be Vector of V, r be Scalar of V;
(0Functional(V)).x = 0.F_Complex by HAHNBAN1:14;
hence thesis by HAHNBAN1:14;
end;
end;
registration
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over F_Complex;
cluster cmplxhomogeneous -> 0-preserving for Functional of V;
coherence
proof
let F be Functional of V;
assume
A1: F is cmplxhomogeneous;
thus F.(0.V) = F.((0.F_Complex) * 0.V) by VECTSP10:1
.= (0.F_Complex)*' * F.(0.V) by A1
.= 0.F_Complex by COMPLFLD:47;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster additive cmplxhomogeneous 0-preserving for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
definition
let V be non empty ModuleStr over F_Complex;
mode antilinear-Functional of V is additive cmplxhomogeneous Functional of V;
end;
registration
let V be non empty ModuleStr over F_Complex;
let f,g be cmplxhomogeneous Functional of V;
cluster f+g -> cmplxhomogeneous;
coherence
proof
let v be Vector of V, a be Scalar of V;
thus (f+g).(a*v) = f.(a*v) + g.(a*v) by HAHNBAN1:def 3
.= a*'*f.v + g.(a*v) by Def1
.= a*'*f.v + a*'*g.v by Def1
.= a*'*(f.v + g.v)
.= a*'*(f + g).v by HAHNBAN1:def 3;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
let f be cmplxhomogeneous Functional of V;
cluster -f -> cmplxhomogeneous;
coherence
proof
let v be Vector of V, a be Scalar of V;
thus (-f).(a*v) = - f.(a*v) by HAHNBAN1:def 4
.= -(a*'*f.v) by Def1
.= a*'*(-f.v)
.= a*'*(-f).v by HAHNBAN1:def 4;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
let a be Scalar of V;
let f be cmplxhomogeneous Functional of V;
cluster a*f -> cmplxhomogeneous;
coherence
proof
let v be Vector of V, b be Scalar of V;
thus (a*f).(b*v) = a* f.(b*v) by HAHNBAN1:def 6
.= a*(b*'*f.v) by Def1
.= b*'*(a*f.v)
.= b*'*(a*f).v by HAHNBAN1:def 6;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
let f,g be cmplxhomogeneous Functional of V;
cluster f-g -> cmplxhomogeneous;
coherence;
end;
definition
let V be non empty ModuleStr over F_Complex;
let f be Functional of V;
redefine func f*' -> Functional of V means :Def2: :: redefines *' (COMSEQ_2, definition)
for v being Vector of V holds it.v = (f.v)*';
coherence
proof
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f as Function of V,COMPLEX;
f*' is Function of V,COMPLEX;
hence thesis by A1;
end;
compatibility
proof
let g be Functional of V;
A2: dom g = the carrier of V by FUNCT_2:def 1;
hence g = f*' implies for v being Vector of V holds g.v = (f.v)*'
by COMSEQ_2:def 1;
assume for v being Vector of V holds g.v = (f.v)*';
then
A3: for c being set st c in dom g holds g.c = (f.c)*';
dom f = the carrier of V by FUNCT_2:def 1;
hence g = f*' by A2,A3,COMSEQ_2:def 1;
end;
end;
registration
let A be non empty addMagma;
let f be additive Function of A,F_Complex;
cluster f*' -> additive for Function of A,F_Complex;
coherence
proof
let g be Function of A,F_Complex such that
A1: g = f*';
A2: dom g = the carrier of A by FUNCT_2:def 1;
let x,y be Element of A;
A3: g.x = (f.x)*' & g.y = (f.y)*' by A1,A2,COMSEQ_2:def 1;
f.(x+y) = f.x+f.y by VECTSP_1:def 20;
hence g.x+g.y = (f.(x+y))*' by A3,COMPLEX1:32
.= g.(x+y) by A1,A2,COMSEQ_2:def 1;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
let f be homogeneous Functional of V;
cluster f*' -> cmplxhomogeneous for Functional of V;
coherence
proof
let g be Functional of V such that
A1: g = f*';
let v be Vector of V,r be Scalar of V;
thus g.(r*v) = (f.(r*v))*' by A1,Def2
.= (r*f.v)*' by HAHNBAN1:def 8
.= r*'*(f.v)*' by COMPLFLD:54
.= r*'*g.v by A1,Def2;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
let f be cmplxhomogeneous Functional of V;
cluster f*' -> homogeneous for Functional of V;
coherence
proof
let g be Functional of V such that
A1: g = f*';
let v be Vector of V,r be Scalar of V;
thus g.(r*v) = (f.(r*v))*' by A1,Def2
.= (r*'*f.v)*' by Def1
.= (r*')*'*(f.v)*' by COMPLFLD:54
.= r*g.v by A1,Def2;
end;
end;
registration
let V be non trivial VectSp of F_Complex;
let f be non constant Functional of V;
cluster f*' -> non constant;
coherence
proof
consider x,y be object such that
A1: x in dom f and
A2: y in dom f and
A3: f.x <> f.y by FUNCT_1:def 10;
reconsider v=x,w=y as Vector of V by A1,A2;
take x,y;
now
assume (f.v)*' = (f.w)*';
then f.v = (f.w)*'*';
hence contradiction by A3;
end;
then dom (f*') = the carrier of V & (f*').x <> (f.w)*'
by Def2,FUNCT_2:def 1;
hence thesis by A1,Def2;
end;
end;
registration
let V be non trivial VectSp of F_Complex;
cluster additive cmplxhomogeneous non constant non trivial
for Functional of V;
existence
proof
take (the additive homogeneous non constant non trivial Functional of V)*';
thus thesis;
end;
end;
theorem
for V be non empty ModuleStr over F_Complex, f be Functional of V
holds (f*')*' = f;
theorem
for V be non empty ModuleStr over F_Complex holds
(0Functional(V))*' = 0Functional(V)
proof
let V be non empty ModuleStr over F_Complex;
set f= 0Functional(V);
now
let v be Vector of V;
thus f*'.v = (f.v)*' by Def2
.= 0.F_Complex by COMPLFLD:47,HAHNBAN1:14
.= f.v by HAHNBAN1:14;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th18:
for V be non empty ModuleStr over F_Complex, f,g be Functional
of V holds (f+g)*'=f*'+ g*'
proof
let V be non empty ModuleStr over F_Complex, f,g be Functional of V;
now
let v be Vector of V;
thus (f+g)*'.v = ((f+g).v)*' by Def2
.= (f.v +g.v)*' by HAHNBAN1:def 3
.= (f.v)*'+(g.v)*' by COMPLFLD:51
.= f*'.v + (g.v)*' by Def2
.= f*'.v + g*'.v by Def2
.= (f*'+ g*').v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th19:
for V be non empty ModuleStr over F_Complex, f be Functional of
V holds (-f)*'=-(f*')
proof
let V be non empty ModuleStr over F_Complex, f be Functional of V;
now
let v be Vector of V;
thus (-f)*'.v = ((-f).v)*' by Def2
.= (-f.v)*' by HAHNBAN1:def 4
.= -(f.v)*' by COMPLFLD:52
.= -(f*'.v) by Def2
.= (-(f*')).v by HAHNBAN1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V be non empty ModuleStr over F_Complex for f be Functional of V,
a be Scalar of V holds (a*f)*' = a*' * (f*')
proof
let V be non empty ModuleStr over F_Complex, f be Functional of V, a be
Scalar of V;
now
let v be Vector of V;
thus (a*f)*'.v = ((a*f).v)*' by Def2
.= (a* (f.v))*' by HAHNBAN1:def 6
.= a*' * (f.v)*' by COMPLFLD:54
.= a*' *(f*'.v) by Def2
.= (a*'* (f*')).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V be non empty ModuleStr over F_Complex, f,g be Functional of V
holds (f-g)*'=f*'- g*'
proof
let V be non empty ModuleStr over F_Complex, f,g be Functional of V;
thus (f-g)*' = f*' +(-g)*' by Th18
.= f*'- g*' by Th19;
end;
theorem Th22:
for V be non empty ModuleStr over F_Complex, f be Functional of
V for v be Vector of V holds f.v = 0.F_Complex iff f*'.v = 0.F_Complex
proof
let V be non empty ModuleStr over F_Complex, f be Functional of V;
let v be Vector of V;
thus f.v = 0.F_Complex implies f*'.v = 0.F_Complex by Def2,COMPLFLD:47;
assume f*'.v = 0.F_Complex;
then (f.v)*'*' = 0.F_Complex by Def2,COMPLFLD:47;
hence thesis;
end;
theorem Th23:
for V be non empty ModuleStr over F_Complex, f be Functional of
V holds ker f = ker f*'
proof
let V be non empty ModuleStr over F_Complex, f be Functional of V;
thus ker f c= ker f*'
proof
let x be object;
assume x in ker f;
then consider v be Vector of V such that
A1: x=v and
A2: f.v = 0.F_Complex;
(f*').v = 0.F_Complex by A2,Th22;
hence thesis by A1;
end;
let x be object;
assume x in ker f*';
then consider v be Vector of V such that
A3: x=v and
A4: (f*').v = 0.F_Complex;
f.v = 0.F_Complex by A4,Th22;
hence thesis by A3;
end;
theorem
for V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F_Complex for f be antilinear-Functional of V holds
ker f is linearly-closed
proof
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over F_Complex, f be antilinear-Functional of V;
ker f = ker f*' by Th23;
hence thesis by VECTSP10:33;
end;
theorem Th25:
for V be VectSp of F_Complex, W be Subspace of V
for f be antilinear-Functional of V st the carrier of W c= ker f*' holds
QFunctional(f,W) is cmplxhomogeneous
proof
let V be VectSp of F_Complex, W be Subspace of V, f be antilinear-Functional
of V;
assume
A1: the carrier of W c= ker f*';
set vq = VectQuot(V,W);
set qf = QFunctional(f,W);
A2: ker f*' = ker f by Th23;
now
set C = CosetSet(V,W);
let A be Vector of vq;
let r be Scalar of vq;
A3: C = the carrier of vq by VECTSP10:def 6;
then A in C;
then consider aa be Coset of W such that
A4: A = aa;
consider a be Vector of V such that
A5: aa = a+W by VECTSP_4:def 6;
r*A = (lmultCoset(V,W)).(r,A) by VECTSP10:def 6
.= r*a+ W by A3,A4,A5,VECTSP10:def 5;
hence qf.(r*A) = f.(r*a) by A1,A2,VECTSP10:def 12
.= r*'*f.a by Def1
.= r*'*(qf.A) by A1,A2,A4,A5,VECTSP10:def 12;
end;
hence thesis;
end;
definition
let V be VectSp of F_Complex;
let f be antilinear-Functional of V;
func QcFunctional(f) -> antilinear-Functional of VectQuot(V,Ker(f*')) equals
QFunctional(f,Ker(f*'));
correctness
proof
the carrier of Ker (f*') = ker f*' by VECTSP10:def 11;
hence thesis by Th25;
end;
end;
theorem Th26:
for V be VectSp of F_Complex, f be antilinear-Functional of V
for A be Vector of VectQuot(V,Ker (f*')), v be Vector of V st A = v+Ker (f*')
holds (QcFunctional(f)).A = f.v
proof
let V be VectSp of F_Complex, f be antilinear-Functional of V;
let A be Vector of VectQuot(V,Ker (f*')), v be Vector of V;
assume
A1: A = v+Ker (f*');
the carrier of (Ker (f*')) = ker (f*') by VECTSP10:def 11
.= ker f by Th23;
hence thesis by A1,VECTSP10:def 12;
end;
registration
let V be non trivial VectSp of F_Complex;
let f be non constant antilinear-Functional of V;
cluster QcFunctional(f) -> non constant;
coherence
proof
set W = Ker (f*'), qf = QcFunctional(f), qv = VectQuot(V,W);
consider v be Vector of V such that
v <> 0.V and
A1: f.v <> 0.F_Complex by VECTSP10:28;
reconsider cv = v+W as Vector of qv by VECTSP10:23;
assume qf is constant;
then qf = 0Functional(qv);
then 0.F_Complex = qf.cv by HAHNBAN1:14
.= f.v by Th26;
hence contradiction by A1;
end;
end;
registration
let V be VectSp of F_Complex;
let f be antilinear-Functional of V;
cluster QcFunctional(f) -> non degenerated;
coherence
proof
set qf = QcFunctional(f), W = Ker (f*'), qV = VectQuot(V,W), K = F_Complex;
A1: the carrier of W = ker f*' by VECTSP10:def 11
.= ker f by Th23;
A2: the carrier of qV = CosetSet(V,W) by VECTSP10:def 6;
thus ker qf c= {0.qV}
proof
let x be object;
assume x in ker qf;
then consider w be Vector of qV such that
A3: x= w and
A4: qf.w=0.K;
w in CosetSet(V,W) by A2;
then consider A be Coset of W such that
A5: w = A;
consider v be Vector of V such that
A6: A = v + W by VECTSP_4:def 6;
f.v = 0.K by A1,A4,A5,A6,VECTSP10:def 12;
then v in ker f;
then v in W by A1,STRUCT_0:def 5;
then w = zeroCoset(V,W) by A5,A6,VECTSP_4:49
.= 0.qV by VECTSP10:21;
hence thesis by A3,TARSKI:def 1;
end;
thus {0.qV} c= ker qf
proof
let x be object;
assume x in {0.qV};
then
A7: x = 0.qV by TARSKI:def 1;
qf.(0.qV) = 0.K by HAHNBAN1:def 9;
hence thesis by A7;
end;
end;
end;
begin
::Sesquilinear Forms in Complex Vector Spaces
definition
let V,W be non empty ModuleStr over F_Complex;
let f be Form of V,W;
attr f is cmplxhomogeneousFAF means
:Def4:
for v be Vector of V holds FunctionalFAF(f,v) is cmplxhomogeneous;
end;
theorem Th27:
for V,W be non empty ModuleStr over F_Complex for v be Vector of
V,w be Vector of W, a be Element of F_Complex for f be Form of V,W st f is
cmplxhomogeneousFAF holds f.(v,a*w) = (a*')*f.(v,w)
proof
let V,W be non empty ModuleStr over F_Complex, v1 be Vector of V, w be
Vector of W, r be Element of F_Complex, f be Form of V,W;
set F=FunctionalFAF(f,v1);
assume f is cmplxhomogeneousFAF;
then
A1: F is cmplxhomogeneous;
thus f.(v1,r*w) = F.(r*w) by BILINEAR:8
.= (r*')*F.w by A1
.= (r*')*f.(v1,w) by BILINEAR:8;
end;
definition
let V be non empty ModuleStr over F_Complex;
let f be Form of V,V;
attr f is hermitan means
:Def5:
for v,u be Vector of V holds f.(v,u) = (f.(u ,v))*';
attr f is diagRvalued means
:Def6:
for v be Vector of V holds Im (f.(v,v)) = 0;
attr f is diagReR+0valued means
:Def7:
for v be Vector of V holds 0 <= Re (f .(v,v));
end;
Lm2: now
let V be non empty ModuleStr over F_Complex, f be Functional of V;
set 0F = 0Functional(V);
let v1,w be Vector of V;
thus (FormFunctional(f,0F)).(v1,w)= f.v1 * 0F.w by BILINEAR:def 10
.= f.v1 * 0.F_Complex by HAHNBAN1:14
.= 0.F_Complex;
end;
Lm3: for V be non empty ModuleStr over F_Complex for f be Functional of V
holds FormFunctional(f,0Functional(V)) is hermitan
proof
let V be non empty ModuleStr over F_Complex, f be Functional of V, v1,w be
Vector of V;
set 0F = 0Functional(V), F= FormFunctional(f,0F);
thus F.(v1,w) = 0.F_Complex by Lm2
.= (F.(w,v1))*' by Lm2,COMPLFLD:47;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
cluster NulForm(V,W) -> cmplxhomogeneousFAF;
coherence
proof
let v be Vector of V;
FunctionalFAF(NulForm(V,W),v) = 0Functional(W) by BILINEAR:10;
hence thesis;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster NulForm(V,V) -> hermitan;
coherence
proof
NulForm(V,V) = FormFunctional(0Functional(V),0Functional(V)) by BILINEAR:22
;
hence thesis by Lm3;
end;
cluster NulForm(V,V) -> diagReR+0valued;
coherence
proof
let v be Vector of V;
Re (0.F_Complex) = In(0,REAL) by COMPLEX1:def 1,COMPLFLD:7;
hence thesis by FUNCOP_1:70;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster hermitan -> diagRvalued for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is hermitan;
let v be Vector of V;
f.(v,v) =(f.(v,v))*' by A1;
hence thesis by Th1;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster diagReR+0valued hermitan diagRvalued additiveSAF homogeneousSAF
additiveFAF cmplxhomogeneousFAF for Form of V,V;
existence
proof
take NulForm(V,V);
thus thesis;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF
for Form of V,W;
existence
proof
take NulForm(V,W);
thus thesis;
end;
end;
definition
let V,W be non empty ModuleStr over F_Complex;
mode sesquilinear-Form of V,W is additiveSAF homogeneousSAF additiveFAF
cmplxhomogeneousFAF Form of V,W;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster hermitan additiveFAF -> additiveSAF for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is hermitan additiveFAF;
let w be Vector of V;
set F = FunctionalSAF(f,w), F1 = FunctionalFAF(f,w);
now
let x,y be Vector of V;
thus F.(x+y) = f.(x+y,w) by BILINEAR:9
.= (f.(w,x+y))*' by A1
.= (F1.(x+y))*' by BILINEAR:8
.= (F1.x+ F1.y)*' by A1,VECTSP_1:def 20
.= (f.(w,x)+ F1.y)*' by BILINEAR:8
.= (f.(w,x)+ f.(w,y))*' by BILINEAR:8
.= (f.(w,x))*' + (f.(w,y))*' by COMPLFLD:51
.= f.(x,w)+ (f.(w,y))*' by A1
.= f.(x,w)+ f.(y,w) by A1
.= F.x+f.(y,w) by BILINEAR:9
.= F.x+F.y by BILINEAR:9;
end;
hence thesis;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster hermitan additiveSAF -> additiveFAF for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is hermitan additiveSAF;
let v1 be Vector of V;
set F = FunctionalFAF(f,v1), F2 = FunctionalSAF(f,v1);
now
let x,y be Vector of V;
thus F.(x+y) = f.(v1,x+y) by BILINEAR:8
.= (f.(x+y,v1))*' by A1
.= (F2.(x+y))*' by BILINEAR:9
.= (F2.x+ F2.y)*' by A1,VECTSP_1:def 20
.= (f.(x,v1)+ F2.y)*' by BILINEAR:9
.= (f.(x,v1)+ f.(y,v1))*' by BILINEAR:9
.= (f.(x,v1))*' + (f.(y,v1))*' by COMPLFLD:51
.= f.(v1,x)+ (f.(y,v1))*' by A1
.= f.(v1,x)+ f.(v1,y) by A1
.= F.x+f.(v1,y) by BILINEAR:8
.= F.x+F.y by BILINEAR:8;
end;
hence thesis;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster hermitan homogeneousSAF -> cmplxhomogeneousFAF for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is hermitan homogeneousSAF;
let v1 be Vector of V;
set F = FunctionalFAF(f,v1), F2 = FunctionalSAF(f,v1);
now
let x be Vector of V, r be Scalar of V;
thus F.(r*x) = f.(v1,r*x) by BILINEAR:8
.= (f.(r*x,v1))*' by A1
.= (F2.(r*x))*' by BILINEAR:9
.= (r*F2.x)*' by A1,HAHNBAN1:def 8
.= r*' *(F2.x)*' by COMPLFLD:54
.= r*' *(f.(x,v1))*' by BILINEAR:9
.= r*' * f.(v1,x) by A1
.= r*' * F.x by BILINEAR:8;
end;
hence thesis;
end;
end;
registration
let V be non empty ModuleStr over F_Complex;
cluster hermitan cmplxhomogeneousFAF -> homogeneousSAF for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is hermitan cmplxhomogeneousFAF;
let w be Vector of V;
set F = FunctionalSAF(f,w), F2 = FunctionalFAF(f,w);
A2: F2 is cmplxhomogeneous by A1;
now
let x be Vector of V, r be Scalar of V;
thus F.(r*x) = f.(r*x,w) by BILINEAR:9
.= (f.(w,r*x))*' by A1
.= (F2.(r*x))*' by BILINEAR:8
.= (r*' * F2.x)*' by A2
.= (r*')*' *(F2.x)*' by COMPLFLD:54
.= r *(f.(w,x))*' by BILINEAR:8
.= r * f.(x,w) by A1
.= r * F.x by BILINEAR:9;
end;
hence thesis;
end;
end;
definition
let V be non empty ModuleStr over F_Complex;
mode hermitan-Form of V is hermitan additiveSAF homogeneousSAF Form of V,V;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be Functional of V, g be cmplxhomogeneous Functional of W;
cluster FormFunctional(f,g) -> cmplxhomogeneousFAF;
coherence
proof
let v be Vector of V;
set fg= FormFunctional(f,g), F = FunctionalFAF(fg,v);
let y be Vector of W,r be Scalar of W;
A1: F= f.v * g by BILINEAR:24;
hence F.(r* y) = f.v * g.(r*y) by HAHNBAN1:def 6
.= f.v *(r*'*g.y) by Def1
.= r*'*(f.v * g.y)
.= r*' *F.y by A1,HAHNBAN1:def 6;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be cmplxhomogeneousFAF Form of V,W;
let v be Vector of V;
cluster FunctionalFAF(f,v) -> cmplxhomogeneous;
coherence
proof
let y be Vector of W,r be Scalar of W;
set F = FunctionalFAF(f,v);
thus F.(r* y) = f.(v,r*y) by BILINEAR:8
.= r*'*f.(v,y) by Th27
.= r*' *F.y by BILINEAR:8;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f,g be cmplxhomogeneousFAF Form of V,W;
cluster f+g -> cmplxhomogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(f+g,w), Ff = FunctionalFAF(f,w);
set Fg = FunctionalFAF(g,w);
let v be Vector of W, a be Scalar of V;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by BILINEAR:13
.= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 3
.= a*'*Ff.v + Fg.(a*v) by Def1
.= a*'*Ff.v + a*'*Fg.v by Def1
.= a*'*(Ff.v + Fg.v)
.= a*'*(Ff + Fg).v by HAHNBAN1:def 3
.= a*'* Ffg.v by BILINEAR:13;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be cmplxhomogeneousFAF Form of V,W;
let a be Scalar of V;
cluster a*f -> cmplxhomogeneousFAF;
coherence
proof
let w be Vector of V;
set Ffg = FunctionalFAF(a*f,w), Ff = FunctionalFAF(f,w);
let v be Vector of W, b be Scalar of V;
thus Ffg.(b*v) = (a*Ff).(b*v) by BILINEAR:15
.= a*Ff.(b*v) by HAHNBAN1:def 6
.= a*(b*'*Ff.v) by Def1
.= b*'*(a*Ff.v)
.= b*'*(a*Ff).v by HAHNBAN1:def 6
.= b*'* Ffg.v by BILINEAR:15;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be cmplxhomogeneousFAF Form of V,W;
cluster -f -> cmplxhomogeneousFAF;
coherence;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f,g be cmplxhomogeneousFAF Form of V,W;
cluster f-g -> cmplxhomogeneousFAF;
coherence;
end;
registration
let V,W be non trivial VectSp of F_Complex;
cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF non
constant non trivial for Form of V,W;
existence
proof
set g = the additive cmplxhomogeneous non constant non trivial
Functional of W;
set f = the additive homogeneous non constant non trivial Functional of V;
take FormFunctional(f,g);
thus thesis;
end;
end;
definition
let V,W be non empty ModuleStr over F_Complex;
let f be Form of V,W;
func f*' -> Form of V,W means
:Def8:
for v be Vector of V, w be Vector of W holds it.(v,w) = (f.(v,w))*';
existence
proof
set K = F_Complex, X = the carrier of V, Y = the carrier of W, Z = the
carrier of K;
deffunc F(Element of X, Element of Y) = (f.($1,$2))*';
consider ff be Function of [:X,Y:],Z such that
A1: for x be Element of X for y be Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v be Vector of V, w be Vector of W holds F.(v,w) = (f.(v,w))*' and
A3: for v be Vector of V, w be Vector of W holds G.(v,w) = (f.(v,w))*';
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = (f.(v,w))*' by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be additiveFAF Form of V,W;
cluster f*' -> additiveFAF;
coherence
proof
let v be Vector of V;
let w,t be Vector of W;
set fg = FunctionalFAF(f*',v);
thus fg.(w+t) = (f*').(v,w+t) by BILINEAR:8
.= (f.(v,w+t))*' by Def8
.= (f.(v,w)+ f.(v,t))*' by BILINEAR:27
.= (f.(v,w))*'+ (f.(v,t))*' by COMPLFLD:51
.= (f*').(v,w)+ (f.(v,t))*' by Def8
.= (f*').(v,w)+ (f*').(v,t) by Def8
.= fg.w+ (f*').(v,t) by BILINEAR:8
.= fg.w+ fg.t by BILINEAR:8;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be additiveSAF Form of V,W;
cluster f*' -> additiveSAF;
coherence
proof
let w be Vector of W;
let v,t be Vector of V;
set fg = FunctionalSAF(f*',w);
thus fg.(v+t) = (f*').(v+t,w) by BILINEAR:9
.= (f.(v+t,w))*' by Def8
.= (f.(v,w)+ f.(t,w))*' by BILINEAR:26
.= (f.(v,w))*'+ (f.(t,w))*' by COMPLFLD:51
.= (f*').(v,w)+ (f.(t,w))*' by Def8
.= (f*').(v,w)+ (f*').(t,w) by Def8
.= fg.v+ (f*').(t,w) by BILINEAR:9
.= fg.v+ fg.t by BILINEAR:9;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be homogeneousFAF Form of V,W;
cluster f*' -> cmplxhomogeneousFAF;
coherence
proof
let v be Vector of V;
let w be Vector of W, r be Scalar of W;
set fg = FunctionalFAF(f*',v);
thus fg.(r*w) = (f*').(v,r*w) by BILINEAR:8
.= (f.(v,r*w))*' by Def8
.= (r*f.(v,w))*' by BILINEAR:32
.= r*'*(f.(v,w))*' by COMPLFLD:54
.= r*'*(f*').(v,w) by Def8
.= r*'*fg.w by BILINEAR:8;
end;
end;
registration
let V,W be non empty ModuleStr over F_Complex;
let f be cmplxhomogeneousFAF Form of V,W;
cluster f*' -> homogeneousFAF;
coherence
proof
let v be Vector of V;
let w be Vector of W, r be Scalar of W;
set fg = FunctionalFAF(f*',v);
thus fg.(r*w) = (f*').(v,r*w) by BILINEAR:8
.= (f.(v,r*w))*' by Def8
.= (r*'*f.(v,w))*' by Th27
.= r*'*'* (f.(v,w))*' by COMPLFLD:54
.= r*(f*').(v,w) by Def8
.= r* fg.w by BILINEAR:8;
end;
end;
registration
let V,W be non trivial VectSp of F_Complex;
let f be non constant Form of V,W;
cluster f*' -> non constant;
coherence
proof
A1: dom f = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
consider x,y be object such that
A2: x in dom f and
A3: y in dom f and
A4: f.x <> f.y by FUNCT_1:def 10;
consider vy be Vector of V,wy be Vector of W such that
A5: y = [vy,wy] by A3,DOMAIN_1:1;
take x,y;
consider vx be Vector of V,wx be Vector of W such that
A6: x = [vx,wx] by A2,DOMAIN_1:1;
now
assume (f*').(vx,wx) = f*'.(vy,wy);
then (f.(vx,wx))*'*' = (f*'.(vy,wy))*' by Def8;
then f.(vx,wx) = (f.(vy,wy))*'*' by Def8;
hence contradiction by A4,A6,A5;
end;
hence thesis by A2,A3,A1,A6,A5,FUNCT_2:def 1;
end;
end;
theorem Th28:
for V be non empty ModuleStr over F_Complex, f be Functional of
V, v be Vector of V holds (FormFunctional(f,f*')).(v,v) = |. f.v .|^2
proof
let V be non empty ModuleStr over F_Complex, f be Functional of V, v be
Vector of V;
set g = FormFunctional(f,f*');
thus g.(v,v) = f.v * (f*').v by BILINEAR:def 10
.= f.v * (f.v)*' by Def2
.= |. f.v .|^2 by Th13;
end;
registration
let V be non empty ModuleStr over F_Complex;
let f be Functional of V;
cluster FormFunctional(f,f*') -> diagReR+0valued hermitan diagRvalued;
coherence
proof
set g = FormFunctional(f,f*');
thus g is diagReR+0valued
proof
let v be Vector of V;
g.(v,v) = |. f.v .|^2 + 0 *<i> & g.(v,v) = Re (g.(v,v)) + Im (g.(v,v
)) *<i> by Th28,COMPLEX1:13;
then Re (g.(v,v)) = |. f.v .|^2 by COMPLEX1:77;
hence thesis by XREAL_1:63;
end;
thus g is hermitan
proof
let v,w be Vector of V;
thus g.(v,w) = (f.v * (f*').w)*'*' by BILINEAR:def 10
.= (f.v * (f.w)*')*'*' by Def2
.= ((f.v)*' * (f.w)*'*')*' by COMPLFLD:54
.= (f.w * (f*').v)*' by Def2
.= (g.(w,v))*' by BILINEAR:def 10;
end;
let v be Vector of V;
g.(v,v) = [** |. f.v .|^2, 0 **] & g.(v,v) = Re (g.(v,v)) + Im (g.(v,v
)) * <i> by Th28,COMPLEX1:13;
hence thesis by COMPLEX1:77;
end;
end;
registration
let V be non trivial VectSp of F_Complex;
cluster diagReR+0valued hermitan diagRvalued additiveSAF homogeneousSAF
additiveFAF cmplxhomogeneousFAF non constant non trivial for Form of V,V;
existence
proof
set f = the additive homogeneous non constant non trivial Functional of V;
take FormFunctional(f,f*');
thus thesis;
end;
end;
theorem
for V,W be non empty ModuleStr over F_Complex, f be Form of V,W holds
(f*')*' = f
proof
let V,W be non empty ModuleStr over F_Complex;
let f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f*'*').(v,w) = ((f*').(v,w))*' by Def8
.= (f.(v,w))*'*' by Def8
.= f.(v,w);
end;
hence thesis;
end;
theorem
for V,W be non empty ModuleStr over F_Complex holds (NulForm(V,W))*' =
NulForm(V,W)
proof
let V,W be non empty ModuleStr over F_Complex;
set f= NulForm(V,W);
now
let v be Vector of V,w be Vector of W;
thus f*'.(v,w) = (f.(v,w))*' by Def8
.= 0.F_Complex by COMPLFLD:47,FUNCOP_1:70
.= f.(v,w) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem Th31:
for V,W be non empty ModuleStr over F_Complex, f,g be Form of V,
W holds (f+g)*'=f*'+ g*'
proof
let V,W be non empty ModuleStr over F_Complex, f,g be Form of V,W;
now
let v be Vector of V,w be Vector of W;
thus (f+g)*'.(v,w) = ((f+g).(v,w))*' by Def8
.= (f.(v,w) +g.(v,w))*' by BILINEAR:def 2
.= (f.(v,w))*'+(g.(v,w))*' by COMPLFLD:51
.= f*'.(v,w) + (g.(v,w))*' by Def8
.= f*'.(v,w) + g*'.(v,w) by Def8
.= (f*'+ g*').(v,w) by BILINEAR:def 2;
end;
hence thesis;
end;
theorem Th32:
for V,W be non empty ModuleStr over F_Complex, f be Form of V,W
holds (-f)*'=-(f*')
proof
let V,W be non empty ModuleStr over F_Complex, f be Form of V,W;
now
let v be Vector of V,w be Vector of W;
thus (-f)*'.(v,w) = ((-f).(v,w))*' by Def8
.= (-f.(v,w))*' by BILINEAR:def 4
.= -(f.(v,w))*' by COMPLFLD:52
.= -(f*'.(v,w)) by Def8
.= (-(f*')).(v,w) by BILINEAR:def 4;
end;
hence thesis;
end;
theorem
for V,W be non empty ModuleStr over F_Complex for f be Form of V,W, a
be Element of F_Complex holds (a*f)*' = a*' * (f*')
proof
let V,W be non empty ModuleStr over F_Complex, f be Form of V,W, a be
Element of F_Complex;
now
let v be Vector of V,w be Vector of W;
thus (a*f)*'.(v,w) = ((a*f).(v,w))*' by Def8
.= (a* (f.(v,w)))*' by BILINEAR:def 3
.= a*' * (f.(v,w))*' by COMPLFLD:54
.= a*' *(f*'.(v,w)) by Def8
.= (a*'* (f*')).(v,w) by BILINEAR:def 3;
end;
hence thesis;
end;
theorem
for V,W be non empty ModuleStr over F_Complex, f,g be Form of V,W
holds (f-g)*'=f*'- g*'
proof
let V,W be non empty ModuleStr over F_Complex, f,g be Form of V,W;
thus (f-g)*' = f*' +(-g)*' by Th31
.= f*'- g*' by Th32;
end;
theorem Th35:
for V,W be VectSp of F_Complex, v be Vector of V, w,t be Vector
of W for f be additiveFAF cmplxhomogeneousFAF Form of V,W holds f.(v,w-t) = f.(
v,w) - f.(v,t)
proof
set K = F_Complex;
let V,W be VectSp of K, v1 be Vector of V, w,w2 be Vector of W, f be
additiveFAF cmplxhomogeneousFAF Form of V,W;
thus f.(v1,w-w2) = f.(v1,w) + f.(v1,-w2) by BILINEAR:27
.= f.(v1,w) + f.(v1,(-1_K)* w2) by VECTSP_1:14
.= f.(v1,w) + (-(1.F_Complex))*' *f.(v1,w2) by Th27
.= f.(v1,w) + (-1_K) *f.(v1,w2) by COMPLFLD:49,52
.= f.(v1,w) - f.(v1,w2) by VECTSP_6:48;
end;
theorem Th36:
for V,W be VectSp of F_Complex, v,u be Vector of V, w,t be
Vector of W for f be sesquilinear-Form of V,W holds f.(v-u,w-t) = f.(v,w) - f.(
v,t) -(f.(u,w) - f.(u,t))
proof
let V,W be VectSp of F_Complex, v1,w1 be Vector of V, w,w2 be Vector of W;
let f be sesquilinear-Form of V,W;
set v3 = f.(v1,w) , v4 = f.(v1,w2), v5 = f.(w1,w), v6 = f.(w1,w2);
thus f.(v1-w1,w-w2) = f.(v1,w-w2) - f.(w1,w-w2) by BILINEAR:35
.= v3 - v4 - f.(w1,w-w2) by Th35
.= v3 - v4 - (v5 - v6) by Th35;
end;
theorem Th37:
for V,W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F_Complex for v,u be Vector of V, w,t be
Vector of W for a,b be Element of F_Complex for f be sesquilinear-Form of V,W
holds f.(v+a*u,w+b*t) = f.(v,w) + b*' * f.(v,t) + (a*f.(u,w) + a*(b*' *f.(u,t))
)
proof
let V,W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F_Complex;
let v1,w1 be Vector of V, w,w2 be Vector of W, r,s be Element of F_Complex,
f be sesquilinear-Form of V,W;
set v3 = f.(v1,w), v4 = f.(v1,w2), v5 = f.(w1,w), v6 = f.(w1,w2);
thus f.(v1+r*w1,w+s*w2) = v3 +f.(v1,s*w2) + (f.(r*w1,w) +f.(r*w1,s*w2)) by
BILINEAR:28
.= v3 +s*'*v4 + (f.(r*w1,w) +f.(r*w1,s*w2)) by Th27
.= v3 + s*'*v4 + (r*v5 + f.(r*w1,s*w2)) by BILINEAR:31
.= v3 + s*'*v4 + (r*v5 + r*f.(w1,s*w2)) by BILINEAR:31
.= v3 + s*'*v4 + (r*v5 + r*(s*'*v6)) by Th27;
end;
theorem Th38:
for V,W be VectSp of F_Complex, v,u be Vector of V, w,t be
Vector of W for a,b be Element of F_Complex for f be sesquilinear-Form of V,W
holds f.(v-a*u,w-b*t) = f.(v,w) - b*'*f.(v,t) - (a*f.(u,w) - a*(b*'*f.(u,t)))
proof
let V,W be VectSp of F_Complex, v1,w1 be Vector of V, w,w2 be Vector of W, r
,s be Element of F_Complex, f be sesquilinear-Form of V,W;
set v3 = f.(v1,w), v4 = f.(v1,w2), v5 = f.(w1,w), v6 = f.(w1,w2);
thus f.(v1-r*w1,w-s*w2) = v3 -f.(v1,s*w2) - (f.(r*w1,w) -f.(r*w1,s*w2)) by
Th36
.= v3 -s*'*v4 - (f.(r*w1,w) -f.(r*w1,s*w2)) by Th27
.= v3 - s*'*v4 - (r*v5 - f.(r*w1,s*w2)) by BILINEAR:31
.= v3 - s*'*v4 - (r*v5 - r*f.(w1,s*w2)) by BILINEAR:31
.= v3 - s*'*v4 - (r*v5 - r*(s*'*v6)) by Th27;
end;
theorem Th39:
for V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F_Complex for f be cmplxhomogeneousFAF
Form of V,V for v be Vector of V holds f.(v,0.V) = 0.F_Complex
proof
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over F_Complex;
let f be cmplxhomogeneousFAF Form of V,V, v be Vector of V;
set F=FunctionalFAF(f,v);
thus f.(v,0.V) = f.(v,0.F_Complex *0.V) by VECTSP10:1
.= F.(0.F_Complex *0.V) by BILINEAR:8
.= (0.F_Complex)*' * F.(0.V) by Def1
.= 0.F_Complex by COMPLFLD:47;
end;
theorem
:: Polarization Formulae
for V be VectSp of F_Complex, v,w be Vector of V, f be hermitan-Form
of V holds f.(v,w) + f.(v,w) + f.(v,w) + f.(v,w) = f.(v+w,v+w) - f.(v-w,v-w) +
i_FC *f.(v+i_FC*w,v+i_FC*w) -i_FC *f.(v-i_FC*w,v-i_FC*w)
proof
let V be VectSp of F_Complex, v1,w be Vector of V, f be hermitan-Form of V;
set v3 = f.(v1,v1), v4 = f.(v1,w), w2 = f.(w,w), w1 = f.(w,v1);
f.(v1+w,v1+w) = v3 +v4 + (w1 + w2) & f.(v1-w,v1-w) = v3 - v4 - (w1 - w2)
by Th36,BILINEAR:28;
then
A1: f.(v1+w,v1+w) - f.(v1-w,v1-w) = v3 + v4 - (v3 - v4 - (w1 - w2)) + (w1 + w2)
.= (v3 + v4 - (v3 - v4)) + (w1 - w2) + (w1 + w2)
.= (v3 - (v3 - v4) + v4) + (w1 - w2) + (w1 + w2)
.= (v3 - v3 + v4 + v4) + (w1 - w2) + (w1 + w2)
.= ((0.F_Complex) + v4 + v4) + (w1 - w2) + (w1 + w2) by RLVECT_1:15
.= (v4 + v4) + (w1 - w2) + (w1 + w2) by RLVECT_1:def 4
.= (v4 + v4) + (w1 - w2 + w2 + w1)
.= (v4 + v4) + (w1 - (w2 - w2) + w1)
.= (v4 + v4) + (w1 - (0.F_Complex) + w1) by RLVECT_1:15
.= (v4 + v4) + (w1 + w1) by RLVECT_1:13;
f.(v1+i_FC * w,v1 + i_FC * w) = v3 + i_FC*' * v4 + (i_FC* w1 + i_FC*(
i_FC*' * w2)) by Th37
.= v3 + i_FC*' * v4 + i_FC*(w1 + i_FC*' * w2);
then
A2: i_FC *f.(v1+i_FC*w,v1+i_FC*w) = i_FC * (v3 + i_FC*' * v4)+ i_FC*i_FC*(w1
+ i_FC*' * w2)
.= i_FC * v3 + v4 -(w1 + i_FC*' * w2) by COMPLEX1:7;
f.(v1-i_FC * w,v1 - i_FC * w) = f.(v1,v1-i_FC*w) - f.(i_FC*w,v1-i_FC*w)
by BILINEAR:35
.= v3 - f.(v1,i_FC*w) - f.(i_FC*w,v1-i_FC*w) by Th35
.= v3 - i_FC*' * v4 - f.(i_FC*w,v1-i_FC*w) by Th27
.= v3 - i_FC*' * v4 - i_FC*f.(w,v1-i_FC*w) by BILINEAR:31
.= v3 - i_FC*' * v4 - i_FC*(w1 - f.(w,i_FC*w)) by Th35
.= v3 - i_FC*' * v4 - i_FC*(w1 - i_FC*' * w2) by Th27;
then
i_FC *f.(v1-i_FC*w,v1-i_FC*w) = i_FC * (v3 - i_FC*' * v4)- i_FC*(i_FC*(
w1 - i_FC*' * w2))
.= i_FC * (v3 - i_FC*' * v4)- i_FC*i_FC*(w1 - i_FC*' * w2)
.= i_FC * (v3 - i_FC*' * v4)- -(w1 - i_FC*' * w2)
.= i_FC * (v3 - i_FC*' * v4) +(w1 - i_FC*' * w2)
.= i_FC * v3 - i_FC *(i_FC*' * v4) +(w1 - i_FC*' * w2)
.= i_FC * v3 - v4 +(w1 - i_FC*' * w2) by COMPLEX1:7;
then i_FC *f.(v1+i_FC*w,v1+i_FC*w) - i_FC *f.(v1-i_FC*w,v1-i_FC*w) = i_FC *
v3 + v4 -(w1 + i_FC*' * w2) - (i_FC * v3 - v4) - (w1 - i_FC*' * w2) by A2
.= i_FC * v3 + v4 - (i_FC * v3 - v4) -(w1 + i_FC*' * w2) - (w1 - i_FC*'
* w2)
.= v4 + i_FC * v3 - i_FC * v3 + v4 -(w1 + i_FC*' * w2) - (w1 - i_FC*' *
w2)
.= v4 + (i_FC * v3 - i_FC * v3) + v4 -(w1 + i_FC*' * w2) - (w1 - i_FC*'
* w2)
.= v4 + (0.F_Complex) + v4 -(w1 + i_FC*' * w2) - (w1 - i_FC*' * w2) by
RLVECT_1:15
.= v4 + v4 -(w1 + i_FC*' * w2) - (w1 - i_FC*' * w2) by RLVECT_1:def 4
.= v4 + v4 -(w1 + i_FC*' * w2 + (w1 - i_FC*' * w2))
.= v4 + v4 -(w1 + w1 + (i_FC*' * w2 - i_FC*' * w2))
.= v4 + v4 -(w1 + w1 + 0.F_Complex) by RLVECT_1:15
.= v4 + v4 -(w1 + w1) by RLVECT_1:def 4;
then
f.(v1+w,v1+w) - f.(v1-w,v1-w) +i_FC *f.(v1+i_FC*w,v1+i_FC*w) -i_FC *f.(
v1-i_FC*w,v1-i_FC*w) = v4 + v4 + (w1 + w1 + (v4 + v4) -(w1 + w1)) by A1
.= v4 + v4 + (v4 + v4)
.= v4 + v4 + v4 + v4;
hence thesis;
end;
definition
let V be non empty ModuleStr over F_Complex;
let f be Form of V,V;
let v be Vector of V;
func signnorm(f,v) -> Real equals
Re (f.(v,v));
coherence;
end;
theorem Th41:
for V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F_Complex for f be diagReR+0valued
diagRvalued Form of V,V for v be Vector of V holds |. f.(v,v) .| = Re (f.(v,v))
& signnorm (f,v) = |. f.(v,v) .|
proof
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over F_Complex, f be diagReR+0valued diagRvalued Form of V,V,
v be Vector of V;
set v1 = f.(v,v);
0 <= Re v1 & Im v1 = 0 by Def6,Def7;
hence thesis by Th14;
end;
::
:: Lemmas for Schwarz inequality
::
theorem Th42:
for V be VectSp of F_Complex, v,w be Vector of V for f be
sesquilinear-Form of V,V, r be Real, a be Element of F_Complex st |.a.|
=1 holds f.(v-[**r,0**]*a*w, v-[**r,0**]*a*w) = f.(v,v) - [**r,0**]*(a* f.(w,v)
) - [**r,0**]*(a*'*f.(v,w)) + [**r^2,0**]*f.(w,w)
proof
let V be VectSp of F_Complex, v1,w be Vector of V, f be sesquilinear-Form of
V,V, r be Real, a be Element of F_Complex such that
A1: |.a.| =1;
set r1 = [**r,0**]*a;
set v3 = f.(v1,v1), v4 = f.(v1,w), w1 = f.(w,v1), w2 = f.(w,w);
A2: [**r,0**]*a*([**r,0**]*a*'*w2) = [**r^2,0**]*(a*a*')*w2
.= [**r^2*1^2,0**]*w2 by A1,Th13;
f.(v1-r1*w,v1-r1*w) = v3 - r1*'*v4 -(r1*w1 - r1*(r1*'*w2)) by Th38
.= v3 - (([**r,0**])*'*a*')*v4 - ([**r,0**]*a*w1 - [**r,0**]*a*(([**r,0
**]*a)*'*w2)) by COMPLFLD:54
.= v3 - ([**r,0**]*a*')*v4 - ([**r,0**]*a*w1 - [**r,0**]*a*(([**r,0**]*a
)*'*w2)) by Th12,COMPLEX1:12
.= v3 - ([**r,0**]*a*')*v4 - ([**r,0**]*a*w1 - [**r,0**]*a*((([**r,0**])
*'*a*')*w2)) by COMPLFLD:54
.= v3 - [**r,0**]*(a*'*v4) - ([**r,0**]*a*w1 - [**r,0**]*a*(([**r,0**]*a
*')*w2)) by Th12,COMPLEX1:12
.= v3 - [**r,0**]*(a*'*v4) - [**r,0**]*(a*w1)+[**r,0**]*a*(([**r,0**]*a
*')*w2)
.= v3 - [**r,0**]*(a*w1) - [**r,0**]*(a*'*v4)+[**r,0**]*a*(([**r,0**]*a
*')*w2);
hence thesis by A2;
end;
theorem Th43:
for V be VectSp of F_Complex, v,w be Vector of V for f be
diagReR+0valued hermitan-Form of V, r be Real, a be Element of F_Complex
st |.a.| =1 & Re (a * f.(w,v)) = |.f.(w,v).| holds Re( f.(v-[**r,0**]*a*w, v-
[**r,0**]*a*w)) = signnorm(f,v) - 2*|.f.(w,v).|*r + signnorm(f,w) * r^2 & 0 <=
signnorm(f,v) - 2*|.f.(w,v).|*r + signnorm(f,w) * r^2
proof
let V be VectSp of F_Complex, v1,w be Vector of V, f be diagReR+0valued
hermitan-Form of V, r be Real, a be Element of F_Complex such that
A1: |.a.| =1 and
A2: Re (a * f.(w,v1)) = |.f.(w,v1).|;
set v3=f.(v1,v1), v4=f.(v1,w), w1=f.(w,v1), w2=f.(w,w), A = signnorm(f,v1),
B = |.w1.|, C = signnorm(f,w);
A3: Re [**r,0**] =r & Im [**r,0**] = 0 by COMPLEX1:12;
then
A4: Re ([**r,0**]*(a* w1)) = r * B by A2,Th10;
a*'*v4 = (a*'*v4)*'*' .= (a*'*' * v4*')*' by COMPLFLD:54
.= (a*w1)*' by Def5;
then
A5: Re ([**r,0**]*(a*'*v4)) = r * Re ((a*w1)*') by A3,Th10
.= r * B by A2,COMPLEX1:27;
Re [**r^2,0**] =r^2 & Im [**r^2,0**] = 0 by COMPLEX1:12;
then
A6: Re ([**r^2,0**]*w2) = r^2 * C by Th10;
f.(v1-[**r,0**]*a*w,v1-[**r,0**]*a*w) = v3 - [**r,0**]*(a* w1) - [**r,0
**]*(a*'*v4) + [**r^2,0**]*w2 by A1,Th42;
then Re (f.(v1-[**r,0**]*a*w,v1-[**r,0**]*a*w)) = Re(v3 - [**r,0**]*(a* w1)
- [**r,0**]*(a*'*v4)) + C * r^2 by A6,HAHNBAN1:10
.= Re(v3 - [**r,0**]*(a* w1)) - r*B + C * r^2 by A5,Th9
.= A - r*B - r*B + C * r^2 by A4,Th9
.= A -2*B*r + C * r^2;
hence thesis by Def7;
end;
theorem Th44:
for V be VectSp of F_Complex, v,w be Vector of V for f be
diagReR+0valued hermitan-Form of V st signnorm(f,w)= 0 holds |.f.(w,v).| = 0
proof
let V be VectSp of F_Complex, v1,w be Vector of V, f be diagReR+0valued
hermitan-Form of V;
set w1 = f.(w,v1), A = signnorm(f,v1), B = |.w1.|, C = signnorm(f,w);
reconsider A as Real;
assume that
A1: C = 0 and
A2: B <> 0;
A3: ex a be Element of F_Complex st |.a.| =1 & Re (a * w1) = |.w1.| & Im (a *
w1)= 0 by Th8;
A4: now
A5: now
assume
A6: A >0;
A - 2*B * (A/B) + C*(A/B)^2 = A - (A*(2*B))/B by A1,XCMPLX_1:74
.= A - (A*2)*B/B
.= A - (A+A) by A2,XCMPLX_1:89
.= - A;
hence contradiction by A3,A6,Th43;
end;
A7: now
assume
A8: A <0;
0 <= A - 2*B*0 + C * 0^2 by A3,Th43;
hence contradiction by A8;
end;
assume A<>0;
hence contradiction by A7,A5;
end;
now
assume
A9: A= 0;
A10: now
assume
A11: 0 < B;
0 <= A - 2*B*1 + C * 1^2 by A3,Th43;
hence contradiction by A1,A9,A11;
end;
now
assume
A12: B < 0;
0 <= A - 2*B*(-1) + C * (-1)^2 by A3,Th43;
hence contradiction by A1,A9,A12;
end;
hence contradiction by A2,A10;
end;
hence contradiction by A4;
end;
::$N Cauchy-Schwarz inequality
::$L https://en.wikipedia.org/wiki/CauchyâSchwarz_inequality Cauchy-Schwarz inequality
theorem Th45:
for V be VectSp of F_Complex, v,w be Vector of V for f be
diagReR+0valued hermitan-Form of V holds |. f.(v,w) .|^2 <= signnorm(f,v) *
signnorm(f,w)
proof
let V be VectSp of F_Complex, v1,w be Vector of V, f be diagReR+0valued
hermitan-Form of V;
set v4=f.(v1,w), w1=f.(w,v1), A = signnorm(f,v1), B = |.w1.|, C = signnorm(f
,w);
reconsider A,B,C as Real;
A1: C = 0^2 implies B^2 <=A*C by Th44;
A2: ex a be Element of F_Complex st |.a.| =1 & Re (a * w1) = |.w1.| & Im (a *
w1)= 0 by Th8;
A3: C > 0 implies B^2 <=A*C
proof
assume
A4: C > 0;
A - 2*B *(B/C) + C*(B/C)^2 = A - (B*(2*B)/C) + C*(B/C)^2 by XCMPLX_1:74
.= A - (B^2*2)/C + C*(B/C)^2
.= A - 2 *(B^2/C) + C*(B/C)^2 by XCMPLX_1:74
.= A - 2 *(B^2/C) + C*(B^2/(C*C)) by XCMPLX_1:76
.= A - 2 *(B^2/C) + (C*B^2)/(C*C) by XCMPLX_1:74
.= A - 2 *(B^2/C) + B^2/C by A4,XCMPLX_1:91
.= A - B^2/C
.= (A*C - B^2)/C by A4,XCMPLX_1:127;
then 0 <= A*C - B^2 by A2,A4,Th43;
then 0+ B^2 <= A*C - B^2 + B^2 by XREAL_1:6;
hence thesis;
end;
B= |.v4*'.| by Def5
.= |.v4.| by COMPLEX1:53;
hence thesis by A1,A3,Def7;
end;
::$N Schwarz inequality - second version
::$L https://en.wikipedia.org/wiki/CauchyâSchwarz_inequality Cauchy-Schwarz inequality
theorem Th46:
for V be VectSp of F_Complex for f be diagReR+0valued
hermitan-Form of V for v,w be Vector of V holds |. f.(v,w) .|^2 <= |. f.(v,v).|
* |. f.(w,w) .|
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V, v1,w
be Vector of V;
set v3 = f.(v1,v1), s1 = signnorm(f,v1), s2 = signnorm(f,w);
|. f.(v1,w) .|^2 <= s1 * s2 & s1 = |.v3.| by Th41,Th45;
hence thesis by Th41;
end;
::$N Minkowski inequality
::$L https://en.wikipedia.org/wiki/Minkowski_inequality Minkowski inequality
theorem Th47:
for V be VectSp of F_Complex for f be diagReR+0valued
hermitan-Form of V for v,w be Vector of V holds signnorm(f,v+w) <= (sqrt(
signnorm(f,v)) + sqrt(signnorm(f,w)))^2
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V, v,w
be Vector of V;
set v3 = f.(v,v), v4 = f.(v,w), w1 = f.(w,v), w2 = f.(w,w), sv = signnorm(f,
v), sw = signnorm(f,w), svw = signnorm(f,v+w);
A1: 0 <= sv by Def7;
A2: svw = Re (v3 + v4 +(w1+w2)) by BILINEAR:28
.= Re (v3 + v4)+ Re(w1+w2) by HAHNBAN1:10
.= Re v3 + Re v4 + Re(w1+w2) by HAHNBAN1:10
.= Re v3 + Re v4 + (Re w1 + Re w2) by HAHNBAN1:10
.= sv + (Re v4 + Re w1) + sw
.= sv + (Re v4 + Re (v4*')) + sw by Def5
.= sv + 2*(Re v4) + sw by Th15
.= sv + sw+ 2*(Re v4);
A3: 0 <= sw by Def7;
0 <= |.v4.| by COMPLEX1:46;
then sqrt(|.v4.|^2) <= sqrt(sv * sw) by Th45,SQUARE_1:26;
then |.v4.| <= sqrt(sv * sw) by COMPLEX1:46,SQUARE_1:22;
then Re v4 <= |.v4.| & |.v4.| <= sqrt(sv) * sqrt(sw) by A1,A3,COMPLEX1:54
,SQUARE_1:29;
then Re v4 <= sqrt(sv) * sqrt(sw) by XXREAL_0:2;
then 2* (Re v4) <= 2*(sqrt(sv) * sqrt(sw)) by XREAL_1:64;
then svw <= sv + sw + 2*(sqrt(sv) * sqrt(sw)) by A2,XREAL_1:6;
then svw <= (sqrt sv)^2 + sw + 2*(sqrt(sv) * sqrt(sw)) by A1,SQUARE_1:def 2;
then svw <= (sqrt sv)^2 + (sqrt sw)^2 + 2*(sqrt(sv) * sqrt(sw)) by A3,
SQUARE_1:def 2;
hence thesis;
end;
theorem
::Minkowski inequality - second version
for V be VectSp of F_Complex for f be diagReR+0valued hermitan-Form of
V for v,w be Vector of V holds |. f.(v+w,v+w) .| <= (sqrt(|. f.(v,v) .|) + sqrt
(|. f.(w,w) .|))^2
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V, v1,w
be Vector of V;
set v3 = f.(v1,v1), v4 = f.(v1+w,v1+w), s1 = signnorm(f,v1), s2 = signnorm(f
,w), s12 = signnorm(f,v1+w);
A1: |.v4.| =s12 by Th41;
s12 <= (sqrt(s1) + sqrt(s2))^2 & |.v3.| = s1 by Th41,Th47;
hence thesis by A1,Th41;
end;
theorem Th49:
:: Parallerogram equality
for V be VectSp of F_Complex for f be hermitan-Form of V for v,w
be Element of V holds signnorm(f,v+w) + signnorm(f,v-w) =2* signnorm(f,v)+ 2*
signnorm(f,w)
proof
let V be VectSp of F_Complex, f be hermitan-Form of V, v1,w be Element of V;
set v3 = f.(v1,v1), v4 = f.(v1,w), w1 = f.(w,v1), w2 = f.(w,w), vp = f.(v1+w
,v1+w), vm = f.(v1-w,v1-w), s1 = signnorm(f,v1), s2 = signnorm(f,w), sp =
signnorm(f,v1+w), sm = signnorm(f,v1-w);
vp = v3 + v4 +(w1+w2) by BILINEAR:28;
then
A1: vp + vm = v3 + v4 +(w1+w2) + (v3 - v4 - (w1 -w2)) by Th36
.= v3 + (v4 + v3 - v4) + (w1+w2) - (w1 -w2)
.= v3 + v3 + (w1+w2) - (w1 -w2)
.= v3 + v3 + (w1+w2 - (w1 -w2))
.= v3 + v3 + (w1+w2 - w1 +w2)
.= v3 + v3 + (w2 + w2);
thus sp + sm = Re (vp+ vm) by HAHNBAN1:10
.= Re (v3 + v3) + Re (w2 + w2) by A1,HAHNBAN1:10
.= Re v3 + Re v3 + Re (w2 + w2) by HAHNBAN1:10
.= 2 * (Re v3) + (Re w2 + Re w2) by HAHNBAN1:10
.= 2 * s1 + 2 *s2;
end;
theorem
:: Parallerogram equality - second version (stronger assumption)
for V be VectSp of F_Complex for f be diagReR+0valued hermitan-Form of
V for v,w be Element of V holds |. f.(v+w,v+w) .| + |. f.(v-w,v-w) .| = 2*|. f.
(v,v) .| + 2*|. f.(w,w) .|
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V, v1,w
be Element of V;
set s1 = signnorm(f,v1), s2 = signnorm(f,w), sp = signnorm(f,v1+w), sm =
signnorm(f,v1-w);
A1: sm = |. f.(v1-w,v1-w) .| & s1 = |. f.(v1,v1) .| by Th41;
sp + sm = 2*s1 + 2*s2 & sp = |. f.(v1+w,v1+w) .| by Th41,Th49;
hence thesis by A1,Th41;
end;
definition
let V be non empty ModuleStr over F_Complex;
let f be Form of V,V;
func quasinorm(f) -> RFunctional of V means
:Def10:
for v be Element of V holds it.v = sqrt (signnorm(f,v));
existence
proof
set C = the carrier of V;
defpred P[Element of C,set] means $2 = sqrt (signnorm(f,$1));
A1: now
let x be Element of C;
reconsider y = sqrt (signnorm(f,x)) as Element of REAL by XREAL_0:def 1;
take y;
thus P[x,y];
end;
consider F be Function of the carrier of V, REAL such that
A2: for v be Element of V holds P[v,F.v] from FUNCT_2:sch 3(A1);
reconsider F as RFunctional of V;
take F;
thus thesis by A2;
end;
uniqueness
proof
let h,g be RFunctional of V such that
A3: for v be Element of V holds h.v = sqrt (signnorm(f,v)) and
A4: for v be Element of V holds g.v = sqrt (signnorm(f,v));
now
let v be Element of V;
thus h.v = sqrt (signnorm(f,v)) by A3
.= g.v by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
let V be VectSp of F_Complex;
let f be diagReR+0valued hermitan-Form of V;
cluster quasinorm(f) -> subadditive homogeneous;
coherence
proof
set q = quasinorm(f);
thus quasinorm(f) is subadditive
proof
let v,w be Vector of V;
set fvw = signnorm(f,v+w), fv = signnorm(f,v), fw = signnorm(f,w);
A1: q.v = sqrt fv by Def10;
0 <= Re (f.(v,v)) by Def7;
then
A2: 0<= q.v by A1,SQUARE_1:def 2;
A3: q.w = sqrt fw by Def10;
0 <= Re (f.(w,w)) by Def7;
then
A4: 0<= q.w by A3,SQUARE_1:def 2;
0 <= Re (f.(v+w,v+w)) & q.(v+w) = sqrt fvw by Def7,Def10;
then q.(v+w) <= sqrt ((q.v + q.w)^2) by A1,A3,Th47,SQUARE_1:26;
hence q.(v+w) <= q.v + q.w by A2,A4,SQUARE_1:22;
end;
let v be Vector of V, r be Scalar of V;
A5: 0 <= |.r.|^2 & 0 <= Re(f.(v,v)) by Def7,XREAL_1:63;
A6: f.(r*v,r*v) = r*f.(v,r*v) by BILINEAR:31
.= r*(r*' * f.(v,v)) by Th27
.= r*r*' * f.(v,v)
.= [**|.r.|^2,0**] * f.(v,v) by Th13
.= [**|.r.|^2,0**] * [**Re(f.(v,v)),Im (f.(v,v))**] by COMPLEX1:13
.= [**|.r.|^2,0**] * [**Re(f.(v,v)),0**] by Def6
.= [**|.r.|^2 * Re(f.(v,v)),0**];
thus q.(r*v) = sqrt (signnorm(f,r*v)) by Def10
.= sqrt (|.r.|^2 * Re(f.(v,v))) by A6,COMPLEX1:12
.= sqrt (|.r.|^2) * sqrt (Re(f.(v,v))) by A5,SQUARE_1:29
.= |.r.| * sqrt (signnorm(f,v)) by COMPLEX1:46,SQUARE_1:22
.= |.r.|*q.v by Def10;
end;
end;
begin
:: Kernel of Hermitan Forms and Hermitan Forms in Quotinet Vector Spaces
registration
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over F_Complex;
let f be cmplxhomogeneousFAF Form of V,V;
cluster diagker f -> non empty;
coherence
proof
set F = F_Complex;
f.(0.V,0.V) = 0.F by Th39;
then 0.V in diagker f;
hence thesis;
end;
end;
theorem
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
holds diagker f is linearly-closed
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V;
set V1 = diagker f;
thus for v,u be Element of V st v in V1 & u in V1 holds v + u in V1
proof
let v,u being Element of V;
assume that
A1: v in V1 and
A2: u in V1;
A3: ex b be Vector of V st b = u & f.(b,b)= 0.F_Complex by A2;
then |.f.(v,u).|^2 <= |. f.(v,v).| * 0 by Th46,COMPLFLD:57;
then
A4: |.f.(v,u).| = 0 by XREAL_1:63;
then 0 = |.(f.(v,u))*'.| by COMPLEX1:53
.= |.f.(u,v).| by Def5;
then
A5: f.(u,v) = 0.F_Complex by COMPLFLD:58;
ex a be Vector of V st a = v & f.(a,a)= 0.F_Complex by A1;
then
A6: f.(v+u,v+u) = 0.F_Complex + f.(v,u) +(f.(u,v)+0.F_Complex) by A3,
BILINEAR:28
.= f.(v,u) +(f.(u,v)+0.F_Complex) by RLVECT_1:4
.= f.(v,u) +f.(u,v) by RLVECT_1:4;
f.(v,u) = 0.F_Complex by A4,COMPLFLD:58;
then f.(v+u,v+u) = 0.F_Complex by A6,A5,RLVECT_1:4;
hence thesis;
end;
let a be Element of F_Complex;
let v be Element of V;
assume v in V1;
then
A7: ex w be Vector of V st w=v & f.(w,w)=0.F_Complex;
f.(a*v,a*v) = a *f.(v,a*v) by BILINEAR:31
.= a*(a*'* 0.F_Complex) by A7,Th27
.=0.F_Complex;
hence thesis;
end;
theorem Th52:
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form
of V holds diagker f = leftker f
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V;
thus diagker f c= leftker f
proof
let x be object;
assume x in diagker f;
then consider a be Vector of V such that
A1: a=x and
A2: f.(a,a) = 0. F_Complex;
now
let w be Vector of V;
|.f.(a,w).|^2 <= 0*|. f.(w,w).| by A2,Th46,COMPLFLD:57;
then |.f.(a,w).| = 0 by XREAL_1:63;
hence f.(a,w)=0.F_Complex by COMPLFLD:58;
end;
hence thesis by A1;
end;
let x be object;
assume x in leftker f;
then consider a be Vector of V such that
A3: a=x and
A4: for w be Vector of V holds f.(a,w) = 0.F_Complex;
f.(a,a) = 0.F_Complex by A4;
hence thesis by A3;
end;
theorem Th53:
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form
of V holds diagker f = rightker f
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V;
thus diagker f c= rightker f
proof
let x be object;
assume x in diagker f;
then consider a be Vector of V such that
A1: a=x and
A2: f.(a,a) = 0. F_Complex;
now
let w be Vector of V;
|.f.(w,a).|^2 <= |. f.(w,w).|*0 by A2,Th46,COMPLFLD:57;
then |.f.(w,a).| = 0 by XREAL_1:63;
hence f.(w,a)=0.F_Complex by COMPLFLD:58;
end;
hence thesis by A1;
end;
thus thesis by BILINEAR:41;
end;
theorem
for V be non empty ModuleStr over F_Complex, f be Form of V,V holds
diagker f = diagker f*'
proof
let V be non empty ModuleStr over F_Complex, f be Form of V,V;
set K = F_Complex;
thus diagker f c= diagker f*'
proof
let x be object;
assume x in diagker f;
then consider v be Vector of V such that
A1: x=v and
A2: f.(v,v)= 0.K;
(f*').(v,v) = 0.K by A2,Def8,COMPLFLD:47;
hence thesis by A1;
end;
let x be object;
assume x in diagker f*';
then consider v be Vector of V such that
A3: x=v and
A4: f*'.(v,v)= 0.K;
(f.(v,v))*'*' = 0.K by A4,Def8,COMPLFLD:47;
hence thesis by A3;
end;
theorem Th55:
for V,W be non empty ModuleStr over F_Complex, f be Form of V,W
holds leftker f = leftker f*' & rightker f = rightker f*'
proof
let V,W be non empty ModuleStr over F_Complex, f be Form of V,W;
set K = F_Complex;
thus leftker f c= leftker f*'
proof
let x be object;
assume x in leftker f;
then consider v be Vector of V such that
A1: x=v and
A2: for w be Vector of W holds f.(v,w)= 0.K;
now
let w be Vector of W;
(f.(v,w))*' = 0.K by A2,COMPLFLD:47;
hence (f*').(v,w) = 0.K by Def8;
end;
hence thesis by A1;
end;
thus leftker f*' c= leftker f
proof
let x be object;
assume x in leftker f*';
then consider v be Vector of V such that
A3: x=v and
A4: for w be Vector of W holds f*'.(v,w)= 0.K;
now
let w be Vector of W;
(f*'.(v,w))*' = 0.K by A4,COMPLFLD:47;
then (f.(v,w))*'*' = 0.K by Def8;
hence f.(v,w) = 0.K;
end;
hence thesis by A3;
end;
thus rightker f c= rightker f*'
proof
let x be object;
assume x in rightker f;
then consider w be Vector of W such that
A5: x=w and
A6: for v be Vector of V holds f.(v,w)= 0.K;
now
let v be Vector of V;
(f.(v,w))*' = 0.K by A6,COMPLFLD:47;
hence (f*').(v,w) = 0.K by Def8;
end;
hence thesis by A5;
end;
let x be object;
assume x in rightker f*';
then consider w be Vector of W such that
A7: x=w and
A8: for v be Vector of V holds f*'.(v,w)= 0.K;
now
let v be Vector of V;
(f*'.(v,w))*' = 0.K by A8,COMPLFLD:47;
then (f.(v,w))*'*' = 0.K by Def8;
hence f.(v,w) = 0.K;
end;
hence thesis by A7;
end;
theorem Th56:
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form
of V holds LKer f = RKer (f*')
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V;
the carrier of LKer(f) = leftker f by BILINEAR:def 18
.= diagker f by Th52
.= rightker f by Th53
.= rightker (f*') by Th55
.= the carrier of RKer (f*') by BILINEAR:def 19;
hence thesis by VECTSP_4:29;
end;
theorem Th57:
for V be VectSp of F_Complex, f be diagReR+0valued diagRvalued
Form of V,V for v be Vector of V st Re (f.(v,v))= 0 holds f.(v,v)= 0.F_Complex
proof
let V be VectSp of F_Complex, f be diagReR+0valued diagRvalued Form of V,V,
v be Vector of V;
assume
A1: Re (f.(v,v)) = 0;
Im (f.(v,v)) = 0 by Def6;
then f.(v,v) = 0 + 0*<i> by A1,COMPLEX1:13;
hence thesis by COMPLFLD:7;
end;
theorem Th58:
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form
of V, v be Vector of V st Re (f.(v,v))= 0 & (f is non degenerated-on-left or f
is non degenerated-on-right) holds v=0.V
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V, v be
Vector of V;
assume that
A1: Re (f.(v,v))= 0 and
A2: f is non degenerated-on-left or f is non degenerated-on-right;
f.(v,v) = 0.F_Complex by A1,Th57;
then
A3: v in {w where w is Vector of V: f.(w,w)=0.F_Complex};
per cases by A2;
suppose
f is non degenerated-on-left;
then {0.V} = diagker f by Th52;
hence thesis by A3,TARSKI:def 1;
end;
suppose
f is non degenerated-on-right;
then {0.V} = diagker f by Th53;
hence thesis by A3,TARSKI:def 1;
end;
end;
definition
let V be non empty ModuleStr over F_Complex, W be VectSp of F_Complex;
let f be additiveFAF cmplxhomogeneousFAF Form of V,W;
func RQ*Form(f) -> additiveFAF cmplxhomogeneousFAF Form of V,VectQuot(W,RKer
(f*')) equals
(RQForm(f*'))*';
correctness;
end;
theorem Th59:
for V be non empty ModuleStr over F_Complex, W be VectSp of
F_Complex for f be additiveFAF cmplxhomogeneousFAF Form of V,W for v be Vector
of V, w be Vector of W holds (RQ*Form(f)).(v,w+RKer (f*')) = f.(v,w)
proof
let V be non empty ModuleStr over F_Complex, W be VectSp of F_Complex, f be
additiveFAF cmplxhomogeneousFAF Form of V,W, v be Vector of V, w be Vector of W
;
reconsider A=w+RKer(f*') as Vector of VectQuot(W,RKer (f*')) by VECTSP10:23;
thus (RQ*Form(f)).(v,w+RKer (f*')) = ((RQForm(f*')).(v,A))*' by Def8
.= (f*'.(v,w))*' by BILINEAR:def 21
.= (f.(v,w))*'*' by Def8
.= f.(v,w);
end;
registration
let V,W be VectSp of F_Complex;
let f be sesquilinear-Form of V,W;
cluster LQForm(f) -> additiveFAF cmplxhomogeneousFAF;
coherence
proof
set lf = LQForm(f);
thus LQForm(f) is additiveFAF
proof
let A be Vector of VectQuot(V,LKer(f));
set flf = FunctionalFAF(lf,A);
consider v be Vector of V such that
A1: A = v + LKer(f) by VECTSP10:22;
let w,t be Vector of W;
thus flf.(w+t) = lf.(A,w+t) by BILINEAR:8
.= f.(v,w+t) by A1,BILINEAR:def 20
.= f.(v,w)+f.(v,t) by BILINEAR:27
.= lf.(A,w)+ f.(v,t) by A1,BILINEAR:def 20
.= lf.(A,w)+ lf.(A,t) by A1,BILINEAR:def 20
.= flf.w+ lf.(A,t) by BILINEAR:8
.= flf.w + flf.t by BILINEAR:8;
end;
let A be Vector of VectQuot(V,LKer(f));
set flf = FunctionalFAF(lf,A);
consider v be Vector of V such that
A2: A = v + LKer(f) by VECTSP10:22;
let w be Vector of W, r be Scalar of W;
thus flf.(r*w) = lf.(A,r*w) by BILINEAR:8
.= f.(v,r*w) by A2,BILINEAR:def 20
.= r*'*f.(v,w) by Th27
.= r*'*lf.(A,w) by A2,BILINEAR:def 20
.= r*'*flf.w by BILINEAR:8;
end;
cluster RQ*Form(f) -> additiveSAF homogeneousSAF;
coherence
proof
set lf = RQ*Form(f);
thus RQ*Form(f) is additiveSAF
proof
let A be Vector of VectQuot(W,RKer(f*'));
set flf = FunctionalSAF(lf,A);
consider w be Vector of W such that
A3: A = w + RKer(f*') by VECTSP10:22;
let v,t be Vector of V;
thus flf.(v+t) = lf.(v+t,A) by BILINEAR:9
.= f.(v+t,w) by A3,Th59
.= f.(v,w)+f.(t,w) by BILINEAR:26
.= lf.(v,A)+ f.(t,w) by A3,Th59
.= lf.(v,A)+ lf.(t,A) by A3,Th59
.= flf.v+ lf.(t,A) by BILINEAR:9
.= flf.v + flf.t by BILINEAR:9;
end;
let A be Vector of VectQuot(W,RKer(f*'));
set flf = FunctionalSAF(lf,A);
consider w be Vector of W such that
A4: A = w + RKer(f*') by VECTSP10:22;
let v be Vector of V, r be Scalar of V;
thus flf.(r*v) = lf.(r*v,A) by BILINEAR:9
.= f.(r*v,w) by A4,Th59
.= r*f.(v,w) by BILINEAR:31
.= r*lf.(v,A) by A4,Th59
.= r*flf.v by BILINEAR:9;
end;
end;
definition
let V,W be VectSp of F_Complex;
let f be sesquilinear-Form of V,W;
func Q*Form(f) -> sesquilinear-Form of VectQuot(V,LKer(f)),VectQuot(W,RKer(f
*')) means
:Def12:
for A be Vector of VectQuot(V,LKer f), B be Vector of
VectQuot(W, RKer(f*')) for v be Vector of V, w be Vector of W st A = v + LKer f
& B = w + RKer (f*') holds it.(A,B)= f.(v,w);
existence
proof
set K = F_Complex, L = LKer(f), vq = VectQuot(V,L), Cv = CosetSet(V,L),
aCv = addCoset(V,L), mCv = lmultCoset(V,L), R = RKer(f*'), wq = VectQuot(W,R),
Cw = CosetSet(W,R), aCw = addCoset(W,R), mCw = lmultCoset(W,R);
defpred P[set,set,set] means for v be Vector of V, w be Vector of W st $1
= v+L & $2 = w+R holds $3 = f.(v,w);
A1: rightker f = rightker f*' by Th55;
A2: now
let A be Vector of vq, B be Vector of wq;
consider a be Vector of V such that
A3: A = a+L by VECTSP10:22;
consider b be Vector of W such that
A4: B = b+R by VECTSP10:22;
take y = f.(a,b);
now
let a1 be Vector of V;
let b1 be Vector of W;
assume A = a1+L;
then a in a1+L by A3,VECTSP_4:44;
then consider vv be Vector of V such that
A5: vv in L and
A6: a = a1 + vv by VECTSP_4:42;
vv in the carrier of L by A5,STRUCT_0:def 5;
then vv in leftker f by BILINEAR:def 18;
then
A7: ex aa be Vector of V st aa=vv & for w0 be Vector of W holds f.(aa,
w0) =0.K;
assume B = b1+R;
then b in b1+R by A4,VECTSP_4:44;
then consider ww be Vector of W such that
A8: ww in R and
A9: b = b1 + ww by VECTSP_4:42;
ww in the carrier of R by A8,STRUCT_0:def 5;
then ww in rightker (f*') by BILINEAR:def 19;
then
A10: ex bb be Vector of W st bb=ww & for v0 be Vector of V holds f.(v0,
bb) =0.K by A1;
thus y = f.(a1,b1)+f.(a1,ww) + (f.(vv,b1)+f.(vv,ww)) by A6,A9,
BILINEAR:28
.=f.(a1,b1)+0.K + (f.(vv,b1)+f.(vv,ww)) by A10
.= f.(a1,b1) +0.K + (0.K+f.(vv,ww)) by A7
.= f.(a1,b1) + (0.K+f.(vv,ww)) by RLVECT_1:def 4
.= f.(a1,b1) + f.(vv,ww) by RLVECT_1:4
.= f.(a1,b1) + 0.K by A7
.= f.(a1,b1) by RLVECT_1:def 4;
end;
hence P[A,B,y];
end;
consider ff be Function of [:the carrier of vq,the carrier of wq:], the
carrier of K such that
A11: for A be Vector of vq, B be Vector of wq holds P[A, B, ff.(A,B)]
from BINOP_1:sch 3(A2);
reconsider ff as Form of vq,wq;
A12: Cv = the carrier of vq by VECTSP10:def 6;
A13: now
let ww be Vector of wq;
consider w be Vector of W such that
A14: ww= w+R by VECTSP10:22;
set ffw = FunctionalSAF(ff,ww);
now
let A be Vector of vq, r be Element of K;
consider a be Vector of V such that
A15: A = a+L by VECTSP10:22;
A16: the lmult of vq = mCv & mCv.(r,A) =r*a+L by A12,A15,VECTSP10:def 5
,def 6;
thus ffw.(r*A) = ff.((the lmult of vq).(r,A),ww) by BILINEAR:9
.= f.(r*a,w) by A11,A14,A16
.= r*f.(a,w) by BILINEAR:31
.= r*ff.(A,ww) by A11,A14,A15
.= r*ffw.A by BILINEAR:9;
end;
hence ffw is homogeneous;
end;
A17: Cw = the carrier of wq by VECTSP10:def 6;
A18: now
let vv be Vector of vq;
consider v be Vector of V such that
A19: vv= v+L by VECTSP10:22;
set ffv = FunctionalFAF(ff,vv);
now
let A be Vector of wq, r be Element of K;
consider a be Vector of W such that
A20: A = a+R by VECTSP10:22;
A21: the lmult of wq = mCw & mCw.(r,A) =r*a+R by A17,A20,VECTSP10:def 5
,def 6;
thus ffv.(r*A) = ff.(vv,(the lmult of wq).(r,A)) by BILINEAR:8
.= f.(v,r*a) by A11,A19,A21
.= r*'*f.(v,a) by Th27
.= r*'*ff.(vv,A) by A11,A19,A20
.= r*'*ffv.A by BILINEAR:8;
end;
hence ffv is cmplxhomogeneous;
end;
A22: now
let ww be Vector of wq;
consider w be Vector of W such that
A23: ww= w+R by VECTSP10:22;
set ffw = FunctionalSAF(ff,ww);
now
let A,B be Vector of vq;
consider a be Vector of V such that
A24: A = a+L by VECTSP10:22;
consider b be Vector of V such that
A25: B = b+L by VECTSP10:22;
A26: the addF of vq = aCv & aCv.(A,B) =a+b+L by A12,A24,A25,VECTSP10:def 3
,def 6;
thus ffw.(A+B) = ff.((the addF of vq).(A,B),ww) by BILINEAR:9
.= f.(a+b,w) by A11,A23,A26
.= f.(a,w) + f.(b,w) by BILINEAR:26
.= ff.(A,ww) + f.(b,w) by A11,A23,A24
.= ff.(A,ww) + ff.(B,ww) by A11,A23,A25
.= ffw.A + ff.(B,ww) by BILINEAR:9
.= ffw.A + ffw.B by BILINEAR:9;
end;
hence ffw is additive;
end;
now
let vv be Vector of vq;
consider v be Vector of V such that
A27: vv= v+L by VECTSP10:22;
set ffv = FunctionalFAF(ff,vv);
now
let A,B be Vector of wq;
consider a be Vector of W such that
A28: A = a+R by VECTSP10:22;
consider b be Vector of W such that
A29: B = b+R by VECTSP10:22;
A30: the addF of wq = aCw & aCw.(A,B) =a+b+R by A17,A28,A29,VECTSP10:def 3
,def 6;
thus ffv.(A+B) = ff.(vv,(the addF of wq).(A,B)) by BILINEAR:8
.= f.(v,a+b) by A11,A27,A30
.= f.(v,a) + f.(v,b) by BILINEAR:27
.= ff.(vv,A) + f.(v,b) by A11,A27,A28
.= ff.(vv,A) + ff.(vv,B) by A11,A27,A29
.= ffv.A + ff.(vv,B) by BILINEAR:8
.= ffv.A + ffv.B by BILINEAR:8;
end;
hence ffv is additive;
end;
then reconsider ff as sesquilinear-Form of vq,wq by A22,A13,A18,Def4,
BILINEAR:def 11,def 12,def 14;
take ff;
thus thesis by A11;
end;
uniqueness
proof
set L = LKer(f), vq = VectQuot(V,L), R = RKer(f*'), wq = VectQuot(W,R);
let f1,f2 be sesquilinear-Form of vq,wq;
assume that
A31: for A be Vector of vq, B be Vector of wq for v be Vector of V, w
be Vector of W st A = v + L & B = w + R holds f1.(A,B)= f.(v,w) and
A32: for A be Vector of vq, B be Vector of wq for v be Vector of V, w
be Vector of W st A = v + L & B = w + R holds f2.(A,B)= f.(v,w);
now
let A be Vector of vq, B be Vector of wq;
consider a be Vector of V such that
A33: A = a + L by VECTSP10:22;
consider b be Vector of W such that
A34: B = b + R by VECTSP10:22;
thus f1.(A,B) = f.(a,b) by A31,A33,A34
.= f2.(A,B) by A32,A33,A34;
end;
hence thesis;
end;
end;
registration
let V,W be non trivial VectSp of F_Complex;
let f be non constant sesquilinear-Form of V,W;
cluster Q*Form(f) -> non constant;
coherence
proof
set K = F_Complex;
consider v be Vector of V, w be Vector of W such that
A1: f.(v,w) <> 0.K by BILINEAR:40;
reconsider B=w + RKer(f*') as Vector of VectQuot(W,RKer(f*')) by
VECTSP10:23;
reconsider A = v +LKer f as Vector of VectQuot(V,LKer(f)) by VECTSP10:23;
(Q*Form(f)).(A,B) = f.(v,w) by Def12;
hence thesis by A1,BILINEAR:40;
end;
end;
registration
let V be right_zeroed non empty ModuleStr over F_Complex, W be VectSp of
F_Complex;
let f be additiveFAF cmplxhomogeneousFAF Form of V,W;
cluster RQ*Form(f) -> non degenerated-on-right;
coherence
proof
set K= F_Complex, qf = RQ*Form(f), R = RKer(f*'), qW = VectQuot(W,R);
A1: rightker f = rightker f*' by Th55;
thus rightker qf c= {0.qW}
proof
let x be object;
assume x in rightker qf;
then consider ww be Vector of qW such that
A2: x= ww and
A3: for v be Vector of V holds qf.(v,ww)=0.K;
consider w be Vector of W such that
A4: ww = w + R by VECTSP10:22;
now
let v be Vector of V;
thus f.(v,w) = qf.(v,ww) by A4,Th59
.= 0.K by A3;
end;
then w in rightker f;
then w in the carrier of R by A1,BILINEAR:def 19;
then w in R by STRUCT_0:def 5;
then w+R = zeroCoset(W,R) by VECTSP_4:49
.= 0.qW by VECTSP10:21;
hence thesis by A2,A4,TARSKI:def 1;
end;
let x be object;
assume x in {0.qW};
then
A5: x = 0.qW by TARSKI:def 1;
for v be Vector of V holds qf.(v,0.qW) = 0.K by BILINEAR:29;
hence thesis by A5;
end;
end;
theorem Th60:
for V be non empty ModuleStr over F_Complex, W be VectSp of
F_Complex for f be additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f
= leftker (RQ*Form f)
proof
set K = F_Complex;
let V be non empty ModuleStr over K, W be VectSp of K;
let f be additiveFAF cmplxhomogeneousFAF Form of V,W;
set rf = RQ*Form(f), qw = VectQuot(W,RKer f*');
thus leftker f c= leftker (RQ*Form f)
proof
let x be object;
assume x in leftker f;
then consider v be Vector of V such that
A1: x=v and
A2: for w be Vector of W holds f.(v,w) = 0.K;
now
let A be Vector of qw;
consider w be Vector of W such that
A3: A = w+RKer (f*') by VECTSP10:22;
thus rf.(v,A) = f.(v,w) by A3,Th59
.= 0.K by A2;
end;
hence thesis by A1;
end;
let x be object;
assume x in leftker rf;
then consider v be Vector of V such that
A4: x=v and
A5: for A be Vector of qw holds rf.(v,A) = 0.K;
now
let w be Vector of W;
reconsider A = w + RKer f*' as Vector of qw by VECTSP10:23;
thus f.(v,w) = rf.(v,A) by Th59
.= 0.K by A5;
end;
hence thesis by A4;
end;
theorem Th61:
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W
holds RKer f*' = RKer (LQForm f)*'
proof
set K = F_Complex;
let V,W be VectSp of K, f be sesquilinear-Form of V,W;
the carrier of (RKer f*') = rightker f*' by BILINEAR:def 19
.= rightker f by Th55
.= rightker (LQForm f) by BILINEAR:44
.= rightker ((LQForm f)*') by Th55
.= the carrier of (RKer (LQForm f)*') by BILINEAR:def 19;
hence thesis by VECTSP_4:29;
end;
theorem Th62:
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W
holds LKer f = LKer (RQ*Form f)
proof
set K = F_Complex;
let V,W be VectSp of K, f be sesquilinear-Form of V,W;
the carrier of (LKer f) = leftker f by BILINEAR:def 18
.= leftker (RQ*Form f) by Th60
.= the carrier of (LKer (RQ*Form f)) by BILINEAR:def 18;
hence thesis by VECTSP_4:29;
end;
theorem Th63:
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W
holds Q*Form(f) = RQ*Form(LQForm(f)) & Q*Form(f) = LQForm(RQ*Form(f))
proof
set K = F_Complex;
let V,W be VectSp of K, f be sesquilinear-Form of V,W;
set L = LKer(f), vq = VectQuot(V,L), R = RKer(f*'), wq = VectQuot(W,R), RL =
RKer(LQForm(f))*', wqr = VectQuot(W,RL), LR = LKer(RQ*Form(f)), vql = VectQuot(
V,LR);
A1: dom Q*Form(f) =[:the carrier of vq, the carrier of wq:] by FUNCT_2:def 1;
A2: now
A3: R = RL by Th61;
let x be object;
assume x in dom Q*Form(f);
then consider A,B be object such that
A4: A in the carrier of vq and
A5: B in the carrier of wq and
A6: x=[A,B] by ZFMISC_1:def 2;
reconsider A as Vector of vq by A4;
consider v be Vector of V such that
A7: A = v + L by VECTSP10:22;
reconsider B as Vector of wq by A5;
consider w be Vector of W such that
A8: B = w + R by VECTSP10:22;
thus (Q*Form(f)).x = (Q*Form(f)).(A,B) by A6
.= f.(v,w) by A7,A8,Def12
.= (LQForm(f)).(A,w) by A7,BILINEAR:def 20
.=(RQ*Form(LQForm(f))).(A,B) by A8,A3,Th59
.=(RQ*Form(LQForm(f))).x by A6;
end;
dom RQ*Form (LQForm(f))= [:the carrier of vq, the carrier of wqr:] & the
carrier of wqr = the carrier of wq by Th61,FUNCT_2:def 1;
hence Q*Form(f) = RQ*Form(LQForm(f)) by A1,A2;
A9: now
A10: L = LR by Th62;
let x be object;
assume x in dom Q*Form(f);
then consider A,B be object such that
A11: A in the carrier of vq and
A12: B in the carrier of wq and
A13: x=[A,B] by ZFMISC_1:def 2;
reconsider A as Vector of vq by A11;
consider v be Vector of V such that
A14: A = v + L by VECTSP10:22;
reconsider B as Vector of wq by A12;
consider w be Vector of W such that
A15: B = w + R by VECTSP10:22;
thus (Q*Form(f)).x = (Q*Form(f)).(A,B) by A13
.= f.(v,w) by A14,A15,Def12
.= (RQ*Form(f)).(v,B) by A15,Th59
.=(LQForm(RQ*Form(f))).(A,B) by A14,A10,BILINEAR:def 20
.=(LQForm(RQ*Form(f))).x by A13;
end;
dom LQForm (RQ*Form(f))= [:the carrier of vql, the carrier of wq:] & the
carrier of vql = the carrier of vq by Th62,FUNCT_2:def 1;
hence thesis by A1,A9;
end;
theorem Th64:
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W
holds leftker Q*Form(f) = leftker (RQ*Form(LQForm(f))) & rightker Q*Form(f) =
rightker (RQ*Form(LQForm(f))) & leftker Q*Form(f) = leftker (LQForm(RQ*Form(f))
) & rightker Q*Form(f) = rightker (LQForm(RQ*Form(f)))
proof
set K =F_Complex;
let V,W be VectSp of K, f be sesquilinear-Form of V,W;
set vq = VectQuot(V,LKer(f)), wq = VectQuot(W,RKer(f*')), wqr = VectQuot(W,
RKer(LQForm(f))*'), vql = VectQuot(V,LKer(RQ*Form(f)));
set rlf = RQ*Form (LQForm(f)) , qf = Q*Form(f), lrf = LQForm (RQ*Form(f));
thus leftker qf c= leftker rlf
proof
let x be object;
assume x in leftker qf;
then consider vv be Vector of vq such that
A1: x=vv and
A2: for ww be Vector of wq holds qf.(vv,ww)=0.K;
now
let ww be Vector of wqr;
reconsider w = ww as Vector of wq by Th61;
thus rlf.(vv,ww) = qf.(vv,w) by Th63
.= 0.K by A2;
end;
hence thesis by A1;
end;
thus leftker rlf c= leftker qf
proof
let x be object;
assume x in leftker rlf;
then consider vv be Vector of vq such that
A3: x=vv and
A4: for ww be Vector of wqr holds rlf.(vv,ww)=0.K;
now
let ww be Vector of wq;
reconsider w = ww as Vector of wqr by Th61;
thus qf.(vv,ww) = rlf.(vv,w) by Th63
.= 0.K by A4;
end;
hence thesis by A3;
end;
thus rightker qf c= rightker rlf
proof
let x be object;
assume x in rightker qf;
then consider ww be Vector of wq such that
A5: x=ww and
A6: for vv be Vector of vq holds qf.(vv,ww)=0.K;
reconsider w = ww as Vector of wqr by Th61;
now
let vv be Vector of vq;
thus rlf.(vv,w) = qf.(vv,ww) by Th63
.= 0.K by A6;
end;
hence thesis by A5;
end;
thus rightker rlf c= rightker qf
proof
let x be object;
assume x in rightker rlf;
then consider ww be Vector of wqr such that
A7: x=ww and
A8: for vv be Vector of vq holds rlf.(vv,ww)=0.K;
reconsider w = ww as Vector of wq by Th61;
now
let vv be Vector of vq;
thus qf.(vv,w) = rlf.(vv,ww) by Th63
.= 0.K by A8;
end;
hence thesis by A7;
end;
thus leftker qf c= leftker lrf
proof
let x be object;
assume x in leftker qf;
then consider vv be Vector of vq such that
A9: x=vv and
A10: for ww be Vector of wq holds qf.(vv,ww)=0.K;
reconsider v=vv as Vector of vql by Th62;
now
let ww be Vector of wq;
thus lrf.(v,ww) = qf.(vv,ww) by Th63
.= 0.K by A10;
end;
hence thesis by A9;
end;
thus leftker lrf c= leftker qf
proof
let x be object;
assume x in leftker lrf;
then consider vv be Vector of vql such that
A11: x=vv and
A12: for ww be Vector of wq holds lrf.(vv,ww)=0.K;
reconsider v=vv as Vector of vq by Th62;
now
let ww be Vector of wq;
thus qf.(v,ww) = lrf.(vv,ww) by Th63
.= 0.K by A12;
end;
hence thesis by A11;
end;
thus rightker qf c= rightker lrf
proof
let x be object;
assume x in rightker qf;
then consider ww be Vector of wq such that
A13: x=ww and
A14: for vv be Vector of vq holds qf.(vv,ww)=0.K;
now
let vv be Vector of vql;
reconsider v = vv as Vector of vq by Th62;
thus lrf.(vv,ww) = qf.(v,ww) by Th63
.= 0.K by A14;
end;
hence thesis by A13;
end;
let x be object;
assume x in rightker lrf;
then consider ww be Vector of wq such that
A15: x=ww and
A16: for vv be Vector of vql holds lrf.(vv,ww)=0.K;
now
let vv be Vector of vq;
reconsider v = vv as Vector of vql by Th62;
thus qf.(vv,ww) = lrf.(v,ww) by Th63
.= 0.K by A16;
end;
hence thesis by A15;
end;
registration
let V,W be VectSp of F_Complex;
let f be sesquilinear-Form of V,W;
cluster RQ*Form(LQForm(f)) -> non degenerated-on-left non
degenerated-on-right;
coherence
proof
leftker LQForm(f) = {0.(VectQuot(V,LKer f))} by BILINEAR:def 23;
then leftker RQ*Form(LQForm(f)) = {0.(VectQuot(V,LKer f))} by Th60;
hence thesis;
end;
cluster LQForm(RQ*Form(f)) -> non degenerated-on-left non
degenerated-on-right;
coherence
proof
rightker RQ*Form(f) = {0.(VectQuot(W,RKer f*'))} by BILINEAR:def 24;
then rightker LQForm(RQ*Form(f)) = {0.(VectQuot(W,RKer f*'))} by
BILINEAR:44;
hence thesis;
end;
end;
registration
let V,W be VectSp of F_Complex;
let f be sesquilinear-Form of V,W;
cluster Q*Form(f) -> non degenerated-on-left non degenerated-on-right;
coherence
proof
A1: leftker RQ*Form(LQForm(f))= {0.(VectQuot(V,LKer f))} & rightker LQForm
( RQ*Form(f)) = {0.(VectQuot(W,RKer f*'))} by BILINEAR:def 23,def 24;
leftker RQ*Form(LQForm(f)) = leftker Q*Form(f) & rightker LQForm(
RQ*Form(f)) = rightker Q*Form(f) by Th64;
hence thesis by A1;
end;
end;
begin
:: Scalar Product in Quotient Vector Space Generated by Nonnegative Hermitan Form
definition
let V be non empty ModuleStr over F_Complex;
let f be Form of V,V;
attr f is positivediagvalued means
for v be Vector of V st v <> 0.V holds 0 < Re (f.(v,v));
end;
registration
let V be right_zeroed non empty ModuleStr over F_Complex;
cluster positivediagvalued additiveSAF -> diagReR+0valued for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is positivediagvalued additiveSAF;
let v be Vector of V;
per cases;
suppose
A2: v = 0.V;
A3: [**Re (0.F_Complex), Im(0.F_Complex)**] = [**0,0**] by COMPLEX1:13
,COMPLFLD:7;
f.(v,v) = 0.F_Complex by A1,A2,BILINEAR:30;
hence thesis by A3,COMPLEX1:77;
end;
suppose
v <> 0.V;
hence thesis by A1;
end;
end;
end;
registration
let V be right_zeroed non empty ModuleStr over F_Complex;
cluster positivediagvalued additiveFAF -> diagReR+0valued for Form of V,V;
coherence
proof
let f be Form of V,V;
assume
A1: f is positivediagvalued additiveFAF;
let v be Vector of V;
per cases;
suppose
A2: v = 0.V;
A3: [**Re (0.F_Complex), Im(0.F_Complex)**] = [**0,0**] by COMPLEX1:13
,COMPLFLD:7;
f.(v,v) = 0.F_Complex by A1,A2,BILINEAR:29;
hence thesis by A3,COMPLEX1:77;
end;
suppose
v <> 0.V;
hence thesis by A1;
end;
end;
end;
definition
let V be VectSp of F_Complex;
let f be diagReR+0valued hermitan-Form of V;
func ScalarForm(f) -> diagReR+0valued hermitan-Form of VectQuot(V,LKer(f))
equals
Q*Form(f);
coherence
proof
set vq = VectQuot(V,LKer(f)), vr = VectQuot(V,RKer(f*'));
vr = vq by Th56;
then reconsider sc = Q*Form(f) as Form of vq,vq;
A1: sc is homogeneousSAF
proof
let w be Vector of vq;
set fg =FunctionalSAF(sc,w);
let v be Vector of vq, r be Scalar of vq;
consider va be Vector of V such that
A2: v = va + LKer f by VECTSP10:22;
A3: r*v = r*va + LKer f by A2,VECTSP10:25;
reconsider A=w as Vector of vr by Th56;
consider wa be Vector of V such that
A4: A = wa + RKer(f*') by VECTSP10:22;
thus fg.(r*v) = (Q*Form(f)).(r*v,w) by BILINEAR:9
.= f.(r*va,wa) by A4,A3,Def12
.= r*f.(va,wa) by BILINEAR:31
.= r* sc.(v,w) by A4,A2,Def12
.= r* fg.v by BILINEAR:9;
end;
A5: sc is additiveSAF
proof
let w be Vector of vq;
set fg =FunctionalSAF(sc,w);
let v1,v2 be Vector of vq;
consider va be Vector of V such that
A6: v1 = va + LKer f by VECTSP10:22;
consider vb be Vector of V such that
A7: v2 = vb + LKer f by VECTSP10:22;
reconsider A=w as Vector of vr by Th56;
consider wa be Vector of V such that
A8: A = wa + RKer(f*') by VECTSP10:22;
A9: v1+v2 = va+vb + LKer f by A6,A7,VECTSP10:26;
thus fg.(v1+v2) = (Q*Form(f)).(v1+v2,w) by BILINEAR:9
.= f.(va+vb,wa) by A8,A9,Def12
.= f.(va,wa) + f.(vb,wa) by BILINEAR:26
.= sc.(v1,w) + f.(vb,wa) by A8,A6,Def12
.= sc.(v1,w) +sc.(v2,w) by A8,A7,Def12
.= fg.v1 +sc.(v2,w) by BILINEAR:9
.= fg.v1 + fg.v2 by BILINEAR:9;
end;
A10: sc is hermitan
proof
let v,w be Vector of vq;
reconsider A=w as Vector of vr by Th56;
consider wa be Vector of V such that
A11: A = wa + RKer(f*') by VECTSP10:22;
A12: w = wa + LKer f by A11,Th56;
reconsider B=v as Vector of vr by Th56;
consider va be Vector of V such that
A13: v = va + LKer f by VECTSP10:22;
A14: B = va + RKer(f*') by A13,Th56;
thus sc.(v,w) = f.(va,wa) by A11,A13,Def12
.= (f.(wa,va))*' by Def5
.= (sc.(w,v))*' by A14,A12,Def12;
end;
sc is diagReR+0valued
proof
let v be Vector of vq;
reconsider A = v as Vector of vr by Th56;
consider va be Vector of V such that
A15: v = va + LKer f by VECTSP10:22;
A = va + RKer (f*') by A15,Th56;
then sc.(v,v) = f.(va,va) by A15,Def12;
hence thesis by Def7;
end;
hence thesis by A1,A5,A10;
end;
end;
theorem
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
for A,B be Vector of VectQuot(V,LKer(f)), v,w be Vector of V st A = v + LKer f
& B = w + LKer f holds (ScalarForm(f)).(A,B) = f.(v,w)
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V;
set vq = VectQuot(V,LKer(f)), vr = VectQuot(V,RKer(f*'));
let A,B be Vector of vq, v,w be Vector of V;
reconsider W = B as Vector of vr by Th56;
assume that
A1: A = v + LKer f and
A2: B = w + LKer f;
W = w + RKer(f*') by A2,Th56;
hence thesis by A1,Def12;
end;
theorem Th66:
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form
of V holds leftker ScalarForm(f) = leftker Q*Form(f)
proof
let V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V;
set vq = VectQuot(V,LKer(f)), vr = VectQuot(V,RKer(f*')), qf=Q*Form(f), qhf=
ScalarForm(f), K = F_Complex;
thus leftker qhf c= leftker qf
proof
let x be object;
assume x in leftker qhf;
then consider A be Vector of vq such that
A1: x= A and
A2: for B be Vector of vq holds qhf.(A,B)=0.K;
now
let B be Vector of vr;
reconsider w=B as Vector of vq by Th56;
thus qf.(A,B) = qhf.(A,w) .= 0.K by A2;
end;
hence thesis by A1;
end;
let x be object;
assume x in leftker qf;
then consider A be Vector of vq such that
A3: x= A and
A4: for B be Vector of vr holds qf.(A,B)=0.K;
now
let B be Vector of vq;
reconsider w=B as Vector of vr by Th56;
thus qhf.(A,B) = qf.(A,w) .= 0.K by A4;
end;
hence thesis by A3;
end;
theorem
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
holds rightker ScalarForm(f) = rightker Q*Form(f) by Th56;
::
:: The From in Quotient Space Generated by Non negative Hermitan Form is the Scalar Product
::
registration
let V be VectSp of F_Complex;
let f be diagReR+0valued hermitan-Form of V;
cluster ScalarForm(f) -> non degenerated-on-left non degenerated-on-right
positivediagvalued;
coherence
proof
set vq = VectQuot(V,LKer(f)), vr = VectQuot(V,RKer(f*')), qh = ScalarForm(
f);
A1: leftker qh = leftker Q*Form(f) by Th66
.= {0.vq} by BILINEAR:def 23;
rightker qh = rightker Q*Form(f) by Th56
.= {0.vr} by BILINEAR:def 24
.= {0.vq} by Th56;
hence
A2: qh is non degenerated-on-left & qh is non degenerated-on-right by A1;
let A be Vector of vq;
assume A <> 0.vq;
then Re (qh.(A,A)) <> 0 by A2,Th58;
hence thesis by Def7;
end;
end;
registration
let V be non trivial VectSp of F_Complex;
let f be diagReR+0valued non constant hermitan-Form of V;
cluster ScalarForm(f) -> non constant;
coherence;
end;