:: HERMITAN semantic presentation
begin
Lm1: 0 = 0 + (0 * *)
;
theorem Th1: :: HERMITAN:1
for a being complex number st a = a *' holds
Im a = 0
proof
let z be complex number ; ::_thesis: ( z = z *' implies Im z = 0 )
assume z = z *' ; ::_thesis: Im z = 0
then Im z = 0 + (- (Im z)) by COMPLEX1:27;
hence Im z = 0 ; ::_thesis: verum
end;
theorem Th2: :: HERMITAN:2
for a being Element of COMPLEX st a <> 0c 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 )
proof
let z be Element of COMPLEX ; ::_thesis: ( z <> 0c implies ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = 0 ) )
set r = |.z.|;
set a = ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **);
assume z <> 0c ; ::_thesis: ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = 0 )
then A1: 0 < |.z.| 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: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) by SQUARE_1:def_2;
A3: ( Re (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) = (Re z) / |.z.| & Im (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) = (- (Im z)) / |.z.| ) by COMPLEX1:12;
then ((Re (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **))) ^2) + ((Im (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **))) ^2) = (((Re z) ^2) / (|.z.| ^2)) + (((- (Im z)) / |.z.|) ^2) by XCMPLX_1:76
.= (((Re z) ^2) / (|.z.| ^2)) + (((- (Im z)) ^2) / (|.z.| ^2)) by XCMPLX_1:76
.= (((Re z) ^2) + ((Im z) ^2)) / (|.z.| ^2) by XCMPLX_1:62
.= (|.z.| / |.z.|) ^2 by A2, XCMPLX_1:76
.= 1 ^2 by A1, XCMPLX_1:60 ;
hence |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)).| = 1 by SQUARE_1:18; ::_thesis: ( Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = 0 )
thus Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = (((Re z) / |.z.|) * (Re z)) - (((- (Im z)) / |.z.|) * (Im z)) by A3, COMPLEX1:9
.= (((Re z) * (Re z)) / |.z.|) - (((- (Im z)) / |.z.|) * (Im z)) by XCMPLX_1:74
.= (((Re z) ^2) / |.z.|) - (((- (Im z)) * (Im z)) / |.z.|) by XCMPLX_1:74
.= (((Re z) ^2) - (- ((Im z) * (Im z)))) / |.z.| by XCMPLX_1:120
.= |.z.| by A1, A2, XCMPLX_1:89 ; ::_thesis: Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = 0
thus Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = (((Re z) / |.z.|) * (Im z)) + ((Re z) * ((- (Im z)) / |.z.|)) by A3, COMPLEX1:9
.= (((Re z) * (Im z)) / |.z.|) + ((Re z) * ((- (Im z)) / |.z.|)) by XCMPLX_1:74
.= (((Re z) * (Im z)) / |.z.|) + (((- (Im z)) * (Re z)) / |.z.|) by XCMPLX_1:74
.= (((Re z) * (Im z)) + (- ((Im z) * (Re z)))) / |.z.| by XCMPLX_1:62
.= 0 ; ::_thesis: verum
end;
theorem :: HERMITAN:3
for a being Element of COMPLEX ex b being Element of COMPLEX st
( |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a) = 0 )
proof
let z be Element of COMPLEX ; ::_thesis: ex b being Element of COMPLEX st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 )
set r = |.z.|;
A1: ( |.z.| = 0 implies ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A2: |.z.| = 0 ; ::_thesis: ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take 1r ; ::_thesis: ( |.1r.| = 1 & Re (1r * z) = |.z.| & Im (1r * z) = 0 )
thus ( |.1r.| = 1 & Re (1r * z) = |.z.| & Im (1r * z) = 0 ) by A2, COMPLEX1:4, COMPLEX1:45, COMPLEX1:48; ::_thesis: verum
end;
( 0 < |.z.| implies ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A3: 0 < |.z.| ; ::_thesis: ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **) ; ::_thesis: ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = 0 )
thus ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * z) = 0 ) by A3, Th2, COMPLEX1:44; ::_thesis: verum
end;
hence ex b being Element of COMPLEX st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:46; ::_thesis: verum
end;
theorem Th4: :: HERMITAN:4
for a being Element of COMPLEX holds a * (a *') = (|.a.| ^2) + (0 * **)
proof
let z be Element of COMPLEX ; ::_thesis: z * (z *') = (|.z.| ^2) + (0 * **)
( 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 z * (z *') = (|.z.| ^2) + (0 * **) by A1, COMPLEX1:13; ::_thesis: verum
end;
theorem :: HERMITAN:5
for a being Element of F_Complex st a = a *' holds
Im a = 0 by Th1;
theorem :: HERMITAN:6
i_FC * (i_FC *') = 1_ F_Complex by COMPLEX1:7, COMPLFLD:8;
theorem Th7: :: HERMITAN:7
for a being 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 )
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 ) )
reconsider b = z as Element of COMPLEX by COMPLFLD:def_1;
set a = [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**];
set a1 = ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **);
A1: [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z = (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * **)) * b ;
assume z <> 0. F_Complex ; ::_thesis: ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 )
hence ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 ) by A1, Th2, COMPLFLD:7; ::_thesis: verum
end;
theorem Th8: :: HERMITAN:8
for a being Element of F_Complex ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a) = 0 )
proof
let z be Element of F_Complex; ::_thesis: ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 )
set r = |.z.|;
A1: ( |.z.| = 0 implies ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A2: |.z.| = 0 ; ::_thesis: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take a = 1. F_Complex; ::_thesis: ( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
thus |.a.| = 1 by COMPLFLD:60; ::_thesis: ( Re (a * z) = |.z.| & Im (a * z) = 0 )
z = 0. F_Complex by A2, COMPLFLD:58
.= 0 by COMPLFLD:def_1 ;
hence ( Re (a * z) = |.z.| & Im (a * z) = 0 ) by A2, Lm1, COMPLEX1:12; ::_thesis: verum
end;
( 0 < |.z.| implies ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A3: 0 < |.z.| ; ::_thesis: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] ; ::_thesis: ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 )
thus ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 ) by A3, Th7, COMPLFLD:57; ::_thesis: verum
end;
hence ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:46; ::_thesis: verum
end;
theorem Th9: :: HERMITAN:9
for a, b being 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; ::_thesis: ( Re (a - b) = (Re a) - (Re b) & Im (a - b) = (Im a) - (Im b) )
reconsider x = a, y = b as Element of COMPLEX by COMPLFLD:def_1;
thus Re (a - b) = Re (x - y) by COMPLFLD:3
.= (Re a) - (Re b) by COMPLEX1:19 ; ::_thesis: Im (a - b) = (Im a) - (Im b)
thus Im (a - b) = Im (x - y) by COMPLFLD:3
.= (Im a) - (Im b) by COMPLEX1:19 ; ::_thesis: verum
end;
theorem Th10: :: HERMITAN:10
for a, b being 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; ::_thesis: ( Im a = 0 implies ( Re (a * b) = (Re a) * (Re b) & Im (a * b) = (Re a) * (Im b) ) )
assume A1: Im a = 0 ; ::_thesis: ( Re (a * b) = (Re a) * (Re b) & Im (a * b) = (Re a) * (Im b) )
hence Re (a * b) = ((Re a) * (Re b)) - (0 * (Im b)) by HAHNBAN1:11
.= (Re a) * (Re b) ;
::_thesis: Im (a * b) = (Re a) * (Im b)
thus Im (a * b) = ((Re a) * (Im b)) + ((Re b) * 0) by A1, HAHNBAN1:11
.= (Re a) * (Im b) ; ::_thesis: verum
end;
theorem :: HERMITAN:11
for a, b being 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; ::_thesis: ( Im a = 0 & Im b = 0 implies Im (a * b) = 0 )
assume ( Im a = 0 & Im b = 0 ) ; ::_thesis: Im (a * b) = 0
hence Im (a * b) = (Re b) * 0 by Th10
.= 0 ;
::_thesis: verum
end;
theorem Th12: :: HERMITAN:12
for a being Element of F_Complex st Im a = 0 holds
a = a *'
proof
let x be Element of F_Complex; ::_thesis: ( Im x = 0 implies x = x *' )
reconsider d = x as Element of COMPLEX by COMPLFLD:def_1;
assume Im x = 0 ; ::_thesis: x = x *'
hence x = (Re d) + ((- (Im d)) * **) by COMPLEX1:13
.= x *' ;
::_thesis: verum
end;
theorem Th13: :: HERMITAN:13
for a being Element of F_Complex holds a * (a *') = |.a.| ^2
proof
let z be Element of F_Complex; ::_thesis: z * (z *') = |.z.| ^2
reconsider a = z as Element of COMPLEX by COMPLFLD:def_1;
thus z * (z *') = (|.a.| ^2) + (0 * **) by Th4
.= |.z.| ^2 ; ::_thesis: verum
end;
theorem Th14: :: HERMITAN:14
for a being Element of F_Complex st 0 <= Re a & Im a = 0 holds
|.a.| = Re a
proof
let z be Element of F_Complex; ::_thesis: ( 0 <= Re z & Im z = 0 implies |.z.| = Re z )
assume that
A1: 0 <= Re z and
A2: Im z = 0 ; ::_thesis: |.z.| = Re z
reconsider a = z as Element of COMPLEX by COMPLFLD:def_1;
|.a.| = abs (Re a) by A2, COMPLEX1:50;
hence |.z.| = Re z by A1, ABSVALUE:def_1; ::_thesis: verum
end;
theorem Th15: :: HERMITAN:15
for a being Element of F_Complex holds (Re a) + (Re (a *')) = 2 * (Re a)
proof
let z be Element of F_Complex; ::_thesis: (Re z) + (Re (z *')) = 2 * (Re z)
thus (Re z) + (Re (z *')) = (Re z) + (Re z) by COMPLEX1:27
.= 2 * (Re z) ; ::_thesis: verum
end;
begin
definition
let V be non empty VectSpStr over F_Complex ;
let f be Functional of V;
attrf is cmplxhomogeneous means :Def1: :: HERMITAN:def 1
for v being Vector of V
for a being Scalar of holds f . (a * v) = (a *') * (f . v);
end;
:: deftheorem Def1 defines cmplxhomogeneous HERMITAN:def_1_:_
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds
( f is cmplxhomogeneous iff for v being Vector of V
for a being Scalar of holds f . (a * v) = (a *') * (f . v) );
registration
let V be non empty VectSpStr over F_Complex ;
cluster 0Functional V -> cmplxhomogeneous ;
coherence
0Functional V is cmplxhomogeneous
proof
let x be Vector of V; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (0Functional V) . (a * x) = (a *') * ((0Functional V) . x)
let r be Scalar of ; ::_thesis: (0Functional V) . (r * x) = (r *') * ((0Functional V) . x)
A1: (0Functional V) . x = 0. F_Complex by HAHNBAN1:14;
thus (0Functional V) . (r * x) = 0. F_Complex by HAHNBAN1:14
.= (r *') * ((0Functional V) . x) by A1, VECTSP_1:7 ; ::_thesis: verum
end;
end;
registration
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ;
cluster Function-like V30( the carrier of V, the carrier of F_Complex) cmplxhomogeneous -> 0-preserving for Element of bool [: the carrier of V, the carrier of F_Complex:];
coherence
for b1 being Functional of V st b1 is cmplxhomogeneous holds
b1 is 0-preserving
proof
let F be Functional of V; ::_thesis: ( F is cmplxhomogeneous implies F is 0-preserving )
assume A1: F is cmplxhomogeneous ; ::_thesis: F is 0-preserving
thus F . (0. V) = F . ((0. F_Complex) * (0. V)) by VECTSP10:1
.= ((0. F_Complex) *') * (F . (0. V)) by A1, Def1
.= 0. F_Complex by COMPLFLD:47, VECTSP_1:7 ; :: according to HAHNBAN1:def_9 ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
clusterV16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) additive 0-preserving cmplxhomogeneous for Element of bool [: the carrier of V, the carrier of F_Complex:];
existence
ex b1 being Functional of V st
( b1 is additive & b1 is cmplxhomogeneous & b1 is 0-preserving )
proof
take 0Functional V ; ::_thesis: ( 0Functional V is additive & 0Functional V is cmplxhomogeneous & 0Functional V is 0-preserving )
thus ( 0Functional V is additive & 0Functional V is cmplxhomogeneous & 0Functional V is 0-preserving ) ; ::_thesis: verum
end;
end;
definition
let V be non empty VectSpStr over F_Complex ;
mode antilinear-Functional of V is additive cmplxhomogeneous Functional of V;
end;
registration
let V be non empty VectSpStr over F_Complex ;
let f, g be cmplxhomogeneous Functional of V;
clusterf + g -> cmplxhomogeneous ;
coherence
f + g is cmplxhomogeneous
proof
let v be Vector of V; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (f + g) . (a * v) = (a *') * ((f + g) . v)
let a be Scalar of ; ::_thesis: (f + g) . (a * v) = (a *') * ((f + g) . 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 ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneous Functional of V;
cluster - f -> cmplxhomogeneous ;
coherence
- f is cmplxhomogeneous
proof
let v be Vector of V; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (- f) . (a * v) = (a *') * ((- f) . v)
let a be Scalar of ; ::_thesis: (- f) . (a * v) = (a *') * ((- f) . v)
thus (- f) . (a * v) = - (f . (a * v)) by HAHNBAN1:def_4
.= - ((a *') * (f . v)) by Def1
.= (a *') * (- (f . v)) by VECTSP_1:9
.= (a *') * ((- f) . v) by HAHNBAN1:def_4 ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
let a be Scalar of ;
let f be cmplxhomogeneous Functional of V;
clustera * f -> cmplxhomogeneous ;
coherence
a * f is cmplxhomogeneous
proof
let v be Vector of V; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (a * f) . (a * v) = (a *') * ((a * f) . v)
let b be Scalar of ; ::_thesis: (a * f) . (b * v) = (b *') * ((a * f) . 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 ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
let f, g be cmplxhomogeneous Functional of V;
clusterf - g -> cmplxhomogeneous ;
coherence
f - g is cmplxhomogeneous ;
end;
definition
let V be non empty VectSpStr over F_Complex ;
let f be Functional of V;
funcf *' -> Functional of V means :Def2: :: HERMITAN:def 2
for v being Vector of V holds it . v = (f . v) *' ;
existence
ex b1 being Functional of V st
for v being Vector of V holds b1 . v = (f . v) *'
proof
deffunc H1( Element of V) -> Element of the carrier of F_Complex = (f . $1) *' ;
consider h being Function of the carrier of V, the carrier of F_Complex such that
A1: for a being Element of V holds h . a = H1(a) from FUNCT_2:sch_4();
reconsider h = h as Functional of V ;
take h ; ::_thesis: for v being Vector of V holds h . v = (f . v) *'
thus for v being Vector of V holds h . v = (f . v) *' by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of V st ( for v being Vector of V holds b1 . v = (f . v) *' ) & ( for v being Vector of V holds b2 . v = (f . v) *' ) holds
b1 = b2
proof
let h, g be Functional of V; ::_thesis: ( ( for v being Vector of V holds h . v = (f . v) *' ) & ( for v being Vector of V holds g . v = (f . v) *' ) implies h = g )
assume that
A2: for a being Vector of V holds h . a = (f . a) *' and
A3: for a being Vector of V holds g . a = (f . a) *' ; ::_thesis: h = g
now__::_thesis:_for_a_being_Vector_of_V_holds_h_._a_=_g_._a
let a be Vector of V; ::_thesis: h . a = g . a
thus h . a = (f . a) *' by A2
.= g . a by A3 ; ::_thesis: verum
end;
hence h = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines *' HERMITAN:def_2_:_
for V being non empty VectSpStr over F_Complex
for f, b3 being Functional of V holds
( b3 = f *' iff for v being Vector of V holds b3 . v = (f . v) *' );
registration
let V be non empty VectSpStr over F_Complex ;
let f be additive Functional of V;
clusterf *' -> additive ;
coherence
f *' is additive
proof
let v, w be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (f *') . (v + w) = ((f *') . v) + ((f *') . w)
thus (f *') . (v + w) = (f . (v + w)) *' by Def2
.= ((f . v) + (f . w)) *' by VECTSP_1:def_20
.= ((f . v) *') + ((f . w) *') by COMPLFLD:51
.= ((f *') . v) + ((f . w) *') by Def2
.= ((f *') . v) + ((f *') . w) by Def2 ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
let f be homogeneous Functional of V;
clusterf *' -> cmplxhomogeneous ;
coherence
f *' is cmplxhomogeneous
proof
let v be Vector of V; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (f *') . (a * v) = (a *') * ((f *') . v)
let r be Scalar of ; ::_thesis: (f *') . (r * v) = (r *') * ((f *') . v)
thus (f *') . (r * v) = (f . (r * v)) *' by Def2
.= (r * (f . v)) *' by HAHNBAN1:def_8
.= (r *') * ((f . v) *') by COMPLFLD:54
.= (r *') * ((f *') . v) by Def2 ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneous Functional of V;
clusterf *' -> homogeneous ;
coherence
f *' is homogeneous
proof
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of F_Complex holds (f *') . (b1 * v) = b1 * ((f *') . v)
let r be Scalar of ; ::_thesis: (f *') . (r * v) = r * ((f *') . v)
thus (f *') . (r * v) = (f . (r * v)) *' by Def2
.= ((r *') * (f . v)) *' by Def1
.= ((r *') *') * ((f . v) *') by COMPLFLD:54
.= r * ((f *') . v) by Def2 ; ::_thesis: verum
end;
end;
registration
let V be non trivial VectSp of F_Complex ;
let f be non constant Functional of V;
clusterf *' -> non constant ;
coherence
not f *' is constant
proof
consider x, y being set 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 ; :: according to FUNCT_1:def_10 ::_thesis: ex b1 being set st
( x in K93((f *')) & b1 in K93((f *')) & not (f *') . x = (f *') . b1 )
take y ; ::_thesis: ( x in K93((f *')) & y in K93((f *')) & not (f *') . x = (f *') . y )
now__::_thesis:_not_(f_._v)_*'_=_(f_._w)_*'
assume (f . v) *' = (f . w) *' ; ::_thesis: contradiction
then f . v = ((f . w) *') *' ;
hence contradiction by A3; ::_thesis: verum
end;
then ( dom (f *') = the carrier of V & (f *') . x <> (f . w) *' ) by Def2, FUNCT_2:def_1;
hence ( x in K93((f *')) & y in K93((f *')) & not (f *') . x = (f *') . y ) by A1, Def2; ::_thesis: verum
end;
end;
registration
let V be non trivial VectSp of F_Complex ;
cluster non trivial V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like non constant V30( the carrier of V, the carrier of F_Complex) additive cmplxhomogeneous for Element of bool [: the carrier of V, the carrier of F_Complex:];
existence
ex b1 being Functional of V st
( b1 is additive & b1 is cmplxhomogeneous & not b1 is constant & not b1 is trivial )
proof
set f = the non trivial non constant additive homogeneous Functional of V;
take the non trivial non constant additive homogeneous Functional of V *' ; ::_thesis: ( the non trivial non constant additive homogeneous Functional of V *' is additive & the non trivial non constant additive homogeneous Functional of V *' is cmplxhomogeneous & not the non trivial non constant additive homogeneous Functional of V *' is constant & not the non trivial non constant additive homogeneous Functional of V *' is trivial )
thus ( the non trivial non constant additive homogeneous Functional of V *' is additive & the non trivial non constant additive homogeneous Functional of V *' is cmplxhomogeneous & not the non trivial non constant additive homogeneous Functional of V *' is constant & not the non trivial non constant additive homogeneous Functional of V *' is trivial ) ; ::_thesis: verum
end;
end;
theorem :: HERMITAN:16
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds (f *') *' = f
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V holds (f *') *' = f
let f be Functional of V; ::_thesis: (f *') *' = f
now__::_thesis:_for_v_being_Vector_of_V_holds_((f_*')_*')_._v_=_f_._v
let v be Vector of V; ::_thesis: ((f *') *') . v = f . v
thus ((f *') *') . v = ((f *') . v) *' by Def2
.= ((f . v) *') *' by Def2
.= f . v ; ::_thesis: verum
end;
hence (f *') *' = f by FUNCT_2:63; ::_thesis: verum
end;
theorem :: HERMITAN:17
for V being non empty VectSpStr over F_Complex holds (0Functional V) *' = 0Functional V
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: (0Functional V) *' = 0Functional V
set f = 0Functional V;
set K = F_Complex ;
now__::_thesis:_for_v_being_Vector_of_V_holds_((0Functional_V)_*')_._v_=_(0Functional_V)_._v
let v be Vector of V; ::_thesis: ((0Functional V) *') . v = (0Functional V) . v
thus ((0Functional V) *') . v = ((0Functional V) . v) *' by Def2
.= 0. F_Complex by COMPLFLD:47, HAHNBAN1:14
.= (0Functional V) . v by HAHNBAN1:14 ; ::_thesis: verum
end;
hence (0Functional V) *' = 0Functional V by FUNCT_2:63; ::_thesis: verum
end;
theorem Th18: :: HERMITAN:18
for V being non empty VectSpStr over F_Complex
for f, g being Functional of V holds (f + g) *' = (f *') + (g *')
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f, g being Functional of V holds (f + g) *' = (f *') + (g *')
let f, g be Functional of V; ::_thesis: (f + g) *' = (f *') + (g *')
now__::_thesis:_for_v_being_Vector_of_V_holds_((f_+_g)_*')_._v_=_((f_*')_+_(g_*'))_._v
let v be Vector of V; ::_thesis: ((f + g) *') . v = ((f *') + (g *')) . 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 ; ::_thesis: verum
end;
hence (f + g) *' = (f *') + (g *') by FUNCT_2:63; ::_thesis: verum
end;
theorem Th19: :: HERMITAN:19
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds (- f) *' = - (f *')
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V holds (- f) *' = - (f *')
let f be Functional of V; ::_thesis: (- f) *' = - (f *')
now__::_thesis:_for_v_being_Vector_of_V_holds_((-_f)_*')_._v_=_(-_(f_*'))_._v
let v be Vector of V; ::_thesis: ((- f) *') . v = (- (f *')) . 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 ; ::_thesis: verum
end;
hence (- f) *' = - (f *') by FUNCT_2:63; ::_thesis: verum
end;
theorem :: HERMITAN:20
for V being non empty VectSpStr over F_Complex
for f being Functional of V
for a being Scalar of holds (a * f) *' = (a *') * (f *')
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V
for a being Scalar of holds (a * f) *' = (a *') * (f *')
let f be Functional of V; ::_thesis: for a being Scalar of holds (a * f) *' = (a *') * (f *')
let a be Scalar of ; ::_thesis: (a * f) *' = (a *') * (f *')
now__::_thesis:_for_v_being_Vector_of_V_holds_((a_*_f)_*')_._v_=_((a_*')_*_(f_*'))_._v
let v be Vector of V; ::_thesis: ((a * f) *') . v = ((a *') * (f *')) . 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 ; ::_thesis: verum
end;
hence (a * f) *' = (a *') * (f *') by FUNCT_2:63; ::_thesis: verum
end;
theorem :: HERMITAN:21
for V being non empty VectSpStr over F_Complex
for f, g being Functional of V holds (f - g) *' = (f *') - (g *')
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f, g being Functional of V holds (f - g) *' = (f *') - (g *')
let f, g be Functional of V; ::_thesis: (f - g) *' = (f *') - (g *')
thus (f - g) *' = (f *') + ((- g) *') by Th18
.= (f *') - (g *') by Th19 ; ::_thesis: verum
end;
theorem Th22: :: HERMITAN:22
for V being non empty VectSpStr over F_Complex
for f being Functional of V
for v being Vector of V holds
( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V
for v being Vector of V holds
( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )
let f be Functional of V; ::_thesis: for v being Vector of V holds
( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )
let v be Vector of V; ::_thesis: ( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )
thus ( f . v = 0. F_Complex implies (f *') . v = 0. F_Complex ) by Def2, COMPLFLD:47; ::_thesis: ( (f *') . v = 0. F_Complex implies f . v = 0. F_Complex )
assume (f *') . v = 0. F_Complex ; ::_thesis: f . v = 0. F_Complex
then ((f . v) *') *' = 0. F_Complex by Def2, COMPLFLD:47;
hence f . v = 0. F_Complex ; ::_thesis: verum
end;
theorem Th23: :: HERMITAN:23
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds ker f = ker (f *')
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V holds ker f = ker (f *')
let f be Functional of V; ::_thesis: ker f = ker (f *')
thus ker f c= ker (f *') :: according to XBOOLE_0:def_10 ::_thesis: ker (f *') c= ker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ker f or x in ker (f *') )
assume x in ker f ; ::_thesis: x in ker (f *')
then consider v being Vector of V such that
A1: x = v and
A2: f . v = 0. F_Complex ;
(f *') . v = 0. F_Complex by A2, Th22;
hence x in ker (f *') by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ker (f *') or x in ker f )
assume x in ker (f *') ; ::_thesis: x in ker f
then consider v being Vector of V such that
A3: x = v and
A4: (f *') . v = 0. F_Complex ;
f . v = 0. F_Complex by A4, Th22;
hence x in ker f by A3; ::_thesis: verum
end;
theorem :: HERMITAN:24
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex
for f being antilinear-Functional of V holds ker f is linearly-closed
proof
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ; ::_thesis: for f being antilinear-Functional of V holds ker f is linearly-closed
let f be antilinear-Functional of V; ::_thesis: ker f is linearly-closed
ker f = ker (f *') by Th23;
hence ker f is linearly-closed by VECTSP10:33; ::_thesis: verum
end;
theorem Th25: :: HERMITAN:25
for V being VectSp of F_Complex
for W being Subspace of V
for f being 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 ; ::_thesis: for W being Subspace of V
for f being antilinear-Functional of V st the carrier of W c= ker (f *') holds
QFunctional (f,W) is cmplxhomogeneous
let W be Subspace of V; ::_thesis: for f being antilinear-Functional of V st the carrier of W c= ker (f *') holds
QFunctional (f,W) is cmplxhomogeneous
let f be antilinear-Functional of V; ::_thesis: ( the carrier of W c= ker (f *') implies QFunctional (f,W) is cmplxhomogeneous )
assume A1: the carrier of W c= ker (f *') ; ::_thesis: QFunctional (f,W) is cmplxhomogeneous
set vq = VectQuot (V,W);
set qf = QFunctional (f,W);
A2: ker (f *') = ker f by Th23;
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,W))
for_r_being_Scalar_of_holds_(QFunctional_(f,W))_._(r_*_A)_=_(r_*')_*_((QFunctional_(f,W))_._A)
set C = CosetSet (V,W);
let A be Vector of (VectQuot (V,W)); ::_thesis: for r being Scalar of holds (QFunctional (f,W)) . (r * A) = (r *') * ((QFunctional (f,W)) . A)
let r be Scalar of ; ::_thesis: (QFunctional (f,W)) . (r * A) = (r *') * ((QFunctional (f,W)) . A)
A3: CosetSet (V,W) = the carrier of (VectQuot (V,W)) by VECTSP10:def_6;
then A in CosetSet (V,W) ;
then consider aa being Coset of W such that
A4: A = aa ;
consider a being 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 (QFunctional (f,W)) . (r * A) = f . (r * a) by A1, A2, VECTSP10:def_12
.= (r *') * (f . a) by Def1
.= (r *') * ((QFunctional (f,W)) . A) by A1, A2, A4, A5, VECTSP10:def_12 ;
::_thesis: verum
end;
hence QFunctional (f,W) is cmplxhomogeneous by Def1; ::_thesis: verum
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 :: HERMITAN:def 3
QFunctional (f,(Ker (f *')));
correctness
coherence
QFunctional (f,(Ker (f *'))) is antilinear-Functional of (VectQuot (V,(Ker (f *'))));
proof
the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def_11;
hence QFunctional (f,(Ker (f *'))) is antilinear-Functional of (VectQuot (V,(Ker (f *')))) by Th25; ::_thesis: verum
end;
end;
:: deftheorem defines QcFunctional HERMITAN:def_3_:_
for V being VectSp of F_Complex
for f being antilinear-Functional of V holds QcFunctional f = QFunctional (f,(Ker (f *')));
theorem Th26: :: HERMITAN:26
for V being VectSp of F_Complex
for f being antilinear-Functional of V
for A being Vector of (VectQuot (V,(Ker (f *'))))
for v being Vector of V st A = v + (Ker (f *')) holds
(QcFunctional f) . A = f . v
proof
let V be VectSp of F_Complex ; ::_thesis: for f being antilinear-Functional of V
for A being Vector of (VectQuot (V,(Ker (f *'))))
for v being Vector of V st A = v + (Ker (f *')) holds
(QcFunctional f) . A = f . v
let f be antilinear-Functional of V; ::_thesis: for A being Vector of (VectQuot (V,(Ker (f *'))))
for v being Vector of V st A = v + (Ker (f *')) holds
(QcFunctional f) . A = f . v
let A be Vector of (VectQuot (V,(Ker (f *')))); ::_thesis: for v being Vector of V st A = v + (Ker (f *')) holds
(QcFunctional f) . A = f . v
let v be Vector of V; ::_thesis: ( A = v + (Ker (f *')) implies (QcFunctional f) . A = f . v )
assume A1: A = v + (Ker (f *')) ; ::_thesis: (QcFunctional f) . A = f . v
the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def_11
.= ker f by Th23 ;
hence (QcFunctional f) . A = f . v by A1, VECTSP10:def_12; ::_thesis: verum
end;
registration
let V be non trivial VectSp of F_Complex ;
let f be V23() antilinear-Functional of V;
cluster QcFunctional f -> V23() ;
coherence
not QcFunctional f is constant
proof
set W = Ker (f *');
set qf = QcFunctional f;
set qv = VectQuot (V,(Ker (f *')));
consider v being Vector of V such that
v <> 0. V and
A1: f . v <> 0. F_Complex by VECTSP10:28;
reconsider cv = v + (Ker (f *')) as Vector of (VectQuot (V,(Ker (f *')))) by VECTSP10:23;
assume QcFunctional f is V23() ; ::_thesis: contradiction
then QcFunctional f = 0Functional (VectQuot (V,(Ker (f *')))) by VECTSP10:def_7;
then 0. F_Complex = (QcFunctional f) . cv by HAHNBAN1:14
.= f . v by Th26 ;
hence contradiction by A1; ::_thesis: verum
end;
end;
registration
let V be VectSp of F_Complex ;
let f be antilinear-Functional of V;
cluster QcFunctional f -> non degenerated ;
coherence
not QcFunctional f is degenerated
proof
set qf = QcFunctional f;
set W = Ker (f *');
set qV = VectQuot (V,(Ker (f *')));
set K = F_Complex ;
A1: the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def_11
.= ker f by Th23 ;
A2: the carrier of (VectQuot (V,(Ker (f *')))) = CosetSet (V,(Ker (f *'))) by VECTSP10:def_6;
thus ker (QcFunctional f) c= {(0. (VectQuot (V,(Ker (f *')))))} :: according to XBOOLE_0:def_10,VECTSP10:def_10 ::_thesis: K203( the carrier of (VectQuot (V,(Ker (f *')))),(0. (VectQuot (V,(Ker (f *')))))) c= ker (QcFunctional f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ker (QcFunctional f) or x in {(0. (VectQuot (V,(Ker (f *')))))} )
assume x in ker (QcFunctional f) ; ::_thesis: x in {(0. (VectQuot (V,(Ker (f *')))))}
then consider w being Vector of (VectQuot (V,(Ker (f *')))) such that
A3: x = w and
A4: (QcFunctional f) . w = 0. F_Complex ;
w in CosetSet (V,(Ker (f *'))) by A2;
then consider A being Coset of Ker (f *') such that
A5: w = A ;
consider v being Vector of V such that
A6: A = v + (Ker (f *')) by VECTSP_4:def_6;
f . v = 0. F_Complex by A1, A4, A5, A6, VECTSP10:def_12;
then v in ker f ;
then v in Ker (f *') by A1, STRUCT_0:def_5;
then w = zeroCoset (V,(Ker (f *'))) by A5, A6, VECTSP_4:49
.= 0. (VectQuot (V,(Ker (f *')))) by VECTSP10:21 ;
hence x in {(0. (VectQuot (V,(Ker (f *')))))} by A3, TARSKI:def_1; ::_thesis: verum
end;
thus {(0. (VectQuot (V,(Ker (f *')))))} c= ker (QcFunctional f) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. (VectQuot (V,(Ker (f *')))))} or x in ker (QcFunctional f) )
assume x in {(0. (VectQuot (V,(Ker (f *')))))} ; ::_thesis: x in ker (QcFunctional f)
then A7: x = 0. (VectQuot (V,(Ker (f *')))) by TARSKI:def_1;
(QcFunctional f) . (0. (VectQuot (V,(Ker (f *'))))) = 0. F_Complex by HAHNBAN1:def_9;
hence x in ker (QcFunctional f) by A7; ::_thesis: verum
end;
end;
end;
begin
definition
let V, W be non empty VectSpStr over F_Complex ;
let f be Form of V,W;
attrf is cmplxhomogeneousFAF means :Def4: :: HERMITAN:def 4
for v being Vector of V holds FunctionalFAF (f,v) is cmplxhomogeneous ;
end;
:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def_4_:_
for V, W being non empty VectSpStr over F_Complex
for f being Form of V,W holds
( f is cmplxhomogeneousFAF iff for v being Vector of V holds FunctionalFAF (f,v) is cmplxhomogeneous );
theorem Th27: :: HERMITAN:27
for V, W being non empty VectSpStr over F_Complex
for v being Vector of V
for w being Vector of W
for a being Element of F_Complex
for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . (v,(a * w)) = (a *') * (f . (v,w))
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for v being Vector of V
for w being Vector of W
for a being Element of F_Complex
for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . (v,(a * w)) = (a *') * (f . (v,w))
let v1 be Vector of V; ::_thesis: for w being Vector of W
for a being Element of F_Complex
for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . (v1,(a * w)) = (a *') * (f . (v1,w))
let w be Vector of W; ::_thesis: for a being Element of F_Complex
for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . (v1,(a * w)) = (a *') * (f . (v1,w))
let r be Element of F_Complex; ::_thesis: for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . (v1,(r * w)) = (r *') * (f . (v1,w))
let f be Form of V,W; ::_thesis: ( f is cmplxhomogeneousFAF implies f . (v1,(r * w)) = (r *') * (f . (v1,w)) )
set F = FunctionalFAF (f,v1);
assume f is cmplxhomogeneousFAF ; ::_thesis: f . (v1,(r * w)) = (r *') * (f . (v1,w))
then A1: FunctionalFAF (f,v1) is cmplxhomogeneous by Def4;
thus f . (v1,(r * w)) = (FunctionalFAF (f,v1)) . (r * w) by BILINEAR:8
.= (r *') * ((FunctionalFAF (f,v1)) . w) by A1, Def1
.= (r *') * (f . (v1,w)) by BILINEAR:8 ; ::_thesis: verum
end;
definition
let V be non empty VectSpStr over F_Complex ;
let f be Form of V,V;
attrf is hermitan means :Def5: :: HERMITAN:def 5
for v, u being Vector of V holds f . (v,u) = (f . (u,v)) *' ;
attrf is diagRvalued means :Def6: :: HERMITAN:def 6
for v being Vector of V holds Im (f . (v,v)) = 0 ;
attrf is diagReR+0valued means :Def7: :: HERMITAN:def 7
for v being Vector of V holds 0 <= Re (f . (v,v));
end;
:: deftheorem Def5 defines hermitan HERMITAN:def_5_:_
for V being non empty VectSpStr over F_Complex
for f being Form of V,V holds
( f is hermitan iff for v, u being Vector of V holds f . (v,u) = (f . (u,v)) *' );
:: deftheorem Def6 defines diagRvalued HERMITAN:def_6_:_
for V being non empty VectSpStr over F_Complex
for f being Form of V,V holds
( f is diagRvalued iff for v being Vector of V holds Im (f . (v,v)) = 0 );
:: deftheorem Def7 defines diagReR+0valued HERMITAN:def_7_:_
for V being non empty VectSpStr over F_Complex
for f being Form of V,V holds
( f is diagReR+0valued iff for v being Vector of V holds 0 <= Re (f . (v,v)) );
Lm2: now__::_thesis:_for_V_being_non_empty_VectSpStr_over_F_Complex_
for_f_being_Functional_of_V
for_v1,_w_being_Vector_of_V_holds_(FormFunctional_(f,(0Functional_V)))_._(v1,w)_=_0._F_Complex
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V
for v1, w being Vector of V holds (FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complex
let f be Functional of V; ::_thesis: for v1, w being Vector of V holds (FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complex
set 0F = 0Functional V;
let v1, w be Vector of V; ::_thesis: (FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complex
thus (FormFunctional (f,(0Functional V))) . (v1,w) = (f . v1) * ((0Functional V) . w) by BILINEAR:def_10
.= (f . v1) * (0. F_Complex) by HAHNBAN1:14
.= 0. F_Complex by VECTSP_1:7 ; ::_thesis: verum
end;
Lm3: for V being non empty VectSpStr over F_Complex
for f being Functional of V holds FormFunctional (f,(0Functional V)) is hermitan
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V holds FormFunctional (f,(0Functional V)) is hermitan
let f be Functional of V; ::_thesis: FormFunctional (f,(0Functional V)) is hermitan
let v1, w be Vector of V; :: according to HERMITAN:def_5 ::_thesis: (FormFunctional (f,(0Functional V))) . (v1,w) = ((FormFunctional (f,(0Functional V))) . (w,v1)) *'
set 0F = 0Functional V;
set F = FormFunctional (f,(0Functional V));
thus (FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complex by Lm2
.= ((FormFunctional (f,(0Functional V))) . (w,v1)) *' by Lm2, COMPLFLD:47 ; ::_thesis: verum
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
cluster NulForm (V,W) -> cmplxhomogeneousFAF ;
coherence
NulForm (V,W) is cmplxhomogeneousFAF
proof
let v be Vector of V; :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF ((NulForm (V,W)),v) is cmplxhomogeneous
FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by BILINEAR:10;
hence FunctionalFAF ((NulForm (V,W)),v) is cmplxhomogeneous ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster NulForm (V,V) -> hermitan ;
coherence
NulForm (V,V) is hermitan
proof
NulForm (V,V) = FormFunctional ((0Functional V),(0Functional V)) by BILINEAR:22;
hence NulForm (V,V) is hermitan by Lm3; ::_thesis: verum
end;
cluster NulForm (V,V) -> diagReR+0valued ;
coherence
NulForm (V,V) is diagReR+0valued
proof
let v be Vector of V; :: according to HERMITAN:def_7 ::_thesis: 0 <= Re ((NulForm (V,V)) . (v,v))
Re (0. F_Complex) = 0 by COMPLEX1:def_1, COMPLFLD:7;
hence 0 <= Re ((NulForm (V,V)) . (v,v)) by FUNCOP_1:70; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) hermitan -> diagRvalued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is hermitan holds
b1 is diagRvalued
proof
let f be Form of V,V; ::_thesis: ( f is hermitan implies f is diagRvalued )
assume A1: f is hermitan ; ::_thesis: f is diagRvalued
let v be Vector of V; :: according to HERMITAN:def_6 ::_thesis: Im (f . (v,v)) = 0
f . (v,v) = (f . (v,v)) *' by A1, Def5;
hence Im (f . (v,v)) = 0 by Th1; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
clusterV16() V19([: the carrier of V, the carrier of V:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
existence
ex b1 being Form of V,V st
( b1 is diagReR+0valued & b1 is hermitan & b1 is diagRvalued & b1 is additiveSAF & b1 is homogeneousSAF & b1 is additiveFAF & b1 is cmplxhomogeneousFAF )
proof
take NulForm (V,V) ; ::_thesis: ( NulForm (V,V) is diagReR+0valued & NulForm (V,V) is hermitan & NulForm (V,V) is diagRvalued & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF & NulForm (V,V) is additiveFAF & NulForm (V,V) is cmplxhomogeneousFAF )
thus ( NulForm (V,V) is diagReR+0valued & NulForm (V,V) is hermitan & NulForm (V,V) is diagRvalued & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF & NulForm (V,V) is additiveFAF & NulForm (V,V) is cmplxhomogeneousFAF ) ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
clusterV16() V19([: the carrier of V, the carrier of W:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of V, the carrier of W:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Complex:];
existence
ex b1 being Form of V,W st
( b1 is additiveSAF & b1 is homogeneousSAF & b1 is additiveFAF & b1 is cmplxhomogeneousFAF )
proof
take NulForm (V,W) ; ::_thesis: ( NulForm (V,W) is additiveSAF & NulForm (V,W) is homogeneousSAF & NulForm (V,W) is additiveFAF & NulForm (V,W) is cmplxhomogeneousFAF )
thus ( NulForm (V,W) is additiveSAF & NulForm (V,W) is homogeneousSAF & NulForm (V,W) is additiveFAF & NulForm (V,W) is cmplxhomogeneousFAF ) ; ::_thesis: verum
end;
end;
definition
let V, W be non empty VectSpStr over F_Complex ;
mode sesquilinear-Form of V,W is additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Form of V,W;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveFAF hermitan -> additiveSAF for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is hermitan & b1 is additiveFAF holds
b1 is additiveSAF
proof
let f be Form of V,V; ::_thesis: ( f is hermitan & f is additiveFAF implies f is additiveSAF )
assume A1: ( f is hermitan & f is additiveFAF ) ; ::_thesis: f is additiveSAF
let w be Vector of V; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF (f,w) is additive
set F = FunctionalSAF (f,w);
set F1 = FunctionalFAF (f,w);
now__::_thesis:_for_x,_y_being_Vector_of_V_holds_(FunctionalSAF_(f,w))_._(x_+_y)_=_((FunctionalSAF_(f,w))_._x)_+_((FunctionalSAF_(f,w))_._y)
let x, y be Vector of V; ::_thesis: (FunctionalSAF (f,w)) . (x + y) = ((FunctionalSAF (f,w)) . x) + ((FunctionalSAF (f,w)) . y)
thus (FunctionalSAF (f,w)) . (x + y) = f . ((x + y),w) by BILINEAR:9
.= (f . (w,(x + y))) *' by A1, Def5
.= ((FunctionalFAF (f,w)) . (x + y)) *' by BILINEAR:8
.= (((FunctionalFAF (f,w)) . x) + ((FunctionalFAF (f,w)) . y)) *' by A1, VECTSP_1:def_20
.= ((f . (w,x)) + ((FunctionalFAF (f,w)) . 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, Def5
.= (f . (x,w)) + (f . (y,w)) by A1, Def5
.= ((FunctionalSAF (f,w)) . x) + (f . (y,w)) by BILINEAR:9
.= ((FunctionalSAF (f,w)) . x) + ((FunctionalSAF (f,w)) . y) by BILINEAR:9 ; ::_thesis: verum
end;
hence FunctionalSAF (f,w) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveSAF hermitan -> additiveFAF for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is hermitan & b1 is additiveSAF holds
b1 is additiveFAF
proof
let f be Form of V,V; ::_thesis: ( f is hermitan & f is additiveSAF implies f is additiveFAF )
assume A1: ( f is hermitan & f is additiveSAF ) ; ::_thesis: f is additiveFAF
let v1 be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF (f,v1) is additive
set F = FunctionalFAF (f,v1);
set F2 = FunctionalSAF (f,v1);
now__::_thesis:_for_x,_y_being_Vector_of_V_holds_(FunctionalFAF_(f,v1))_._(x_+_y)_=_((FunctionalFAF_(f,v1))_._x)_+_((FunctionalFAF_(f,v1))_._y)
let x, y be Vector of V; ::_thesis: (FunctionalFAF (f,v1)) . (x + y) = ((FunctionalFAF (f,v1)) . x) + ((FunctionalFAF (f,v1)) . y)
thus (FunctionalFAF (f,v1)) . (x + y) = f . (v1,(x + y)) by BILINEAR:8
.= (f . ((x + y),v1)) *' by A1, Def5
.= ((FunctionalSAF (f,v1)) . (x + y)) *' by BILINEAR:9
.= (((FunctionalSAF (f,v1)) . x) + ((FunctionalSAF (f,v1)) . y)) *' by A1, VECTSP_1:def_20
.= ((f . (x,v1)) + ((FunctionalSAF (f,v1)) . 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, Def5
.= (f . (v1,x)) + (f . (v1,y)) by A1, Def5
.= ((FunctionalFAF (f,v1)) . x) + (f . (v1,y)) by BILINEAR:8
.= ((FunctionalFAF (f,v1)) . x) + ((FunctionalFAF (f,v1)) . y) by BILINEAR:8 ; ::_thesis: verum
end;
hence FunctionalFAF (f,v1) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) homogeneousSAF hermitan -> cmplxhomogeneousFAF for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is hermitan & b1 is homogeneousSAF holds
b1 is cmplxhomogeneousFAF
proof
let f be Form of V,V; ::_thesis: ( f is hermitan & f is homogeneousSAF implies f is cmplxhomogeneousFAF )
assume A1: ( f is hermitan & f is homogeneousSAF ) ; ::_thesis: f is cmplxhomogeneousFAF
let v1 be Vector of V; :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF (f,v1) is cmplxhomogeneous
set F = FunctionalFAF (f,v1);
set F2 = FunctionalSAF (f,v1);
now__::_thesis:_for_x_being_Vector_of_V
for_r_being_Scalar_of_holds_(FunctionalFAF_(f,v1))_._(r_*_x)_=_(r_*')_*_((FunctionalFAF_(f,v1))_._x)
let x be Vector of V; ::_thesis: for r being Scalar of holds (FunctionalFAF (f,v1)) . (r * x) = (r *') * ((FunctionalFAF (f,v1)) . x)
let r be Scalar of ; ::_thesis: (FunctionalFAF (f,v1)) . (r * x) = (r *') * ((FunctionalFAF (f,v1)) . x)
thus (FunctionalFAF (f,v1)) . (r * x) = f . (v1,(r * x)) by BILINEAR:8
.= (f . ((r * x),v1)) *' by A1, Def5
.= ((FunctionalSAF (f,v1)) . (r * x)) *' by BILINEAR:9
.= (r * ((FunctionalSAF (f,v1)) . x)) *' by A1, HAHNBAN1:def_8
.= (r *') * (((FunctionalSAF (f,v1)) . x) *') by COMPLFLD:54
.= (r *') * ((f . (x,v1)) *') by BILINEAR:9
.= (r *') * (f . (v1,x)) by A1, Def5
.= (r *') * ((FunctionalFAF (f,v1)) . x) by BILINEAR:8 ; ::_thesis: verum
end;
hence FunctionalFAF (f,v1) is cmplxhomogeneous by Def1; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) cmplxhomogeneousFAF hermitan -> homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is hermitan & b1 is cmplxhomogeneousFAF holds
b1 is homogeneousSAF
proof
let f be Form of V,V; ::_thesis: ( f is hermitan & f is cmplxhomogeneousFAF implies f is homogeneousSAF )
assume A1: ( f is hermitan & f is cmplxhomogeneousFAF ) ; ::_thesis: f is homogeneousSAF
let w be Vector of V; :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF (f,w) is homogeneous
set F = FunctionalSAF (f,w);
set F2 = FunctionalFAF (f,w);
A2: FunctionalFAF (f,w) is cmplxhomogeneous by A1, Def4;
now__::_thesis:_for_x_being_Vector_of_V
for_r_being_Scalar_of_holds_(FunctionalSAF_(f,w))_._(r_*_x)_=_r_*_((FunctionalSAF_(f,w))_._x)
let x be Vector of V; ::_thesis: for r being Scalar of holds (FunctionalSAF (f,w)) . (r * x) = r * ((FunctionalSAF (f,w)) . x)
let r be Scalar of ; ::_thesis: (FunctionalSAF (f,w)) . (r * x) = r * ((FunctionalSAF (f,w)) . x)
thus (FunctionalSAF (f,w)) . (r * x) = f . ((r * x),w) by BILINEAR:9
.= (f . (w,(r * x))) *' by A1, Def5
.= ((FunctionalFAF (f,w)) . (r * x)) *' by BILINEAR:8
.= ((r *') * ((FunctionalFAF (f,w)) . x)) *' by A2, Def1
.= ((r *') *') * (((FunctionalFAF (f,w)) . x) *') by COMPLFLD:54
.= r * ((f . (w,x)) *') by BILINEAR:8
.= r * (f . (x,w)) by A1, Def5
.= r * ((FunctionalSAF (f,w)) . x) by BILINEAR:9 ; ::_thesis: verum
end;
hence FunctionalSAF (f,w) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;
end;
definition
let V be non empty VectSpStr over F_Complex ;
mode hermitan-Form of V is additiveSAF homogeneousSAF hermitan Form of V,V;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be Functional of V;
let g be cmplxhomogeneous Functional of W;
cluster FormFunctional (f,g) -> cmplxhomogeneousFAF ;
coherence
FormFunctional (f,g) is cmplxhomogeneousFAF
proof
let v be Vector of V; :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF ((FormFunctional (f,g)),v) is cmplxhomogeneous
set fg = FormFunctional (f,g);
set F = FunctionalFAF ((FormFunctional (f,g)),v);
let y be Vector of W; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (FunctionalFAF ((FormFunctional (f,g)),v)) . (a * y) = (a *') * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
let r be Scalar of ; ::_thesis: (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = (r *') * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
A1: FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g by BILINEAR:24;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = (f . v) * (g . (r * y)) by HAHNBAN1:def_6
.= (f . v) * ((r *') * (g . y)) by Def1
.= (r *') * ((f . v) * (g . y))
.= (r *') * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) by A1, HAHNBAN1:def_6 ;
::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneousFAF Form of V,W;
let v be Vector of V;
cluster FunctionalFAF (f,v) -> cmplxhomogeneous ;
coherence
FunctionalFAF (f,v) is cmplxhomogeneous
proof
let y be Vector of W; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (FunctionalFAF (f,v)) . (a * y) = (a *') * ((FunctionalFAF (f,v)) . y)
let r be Scalar of ; ::_thesis: (FunctionalFAF (f,v)) . (r * y) = (r *') * ((FunctionalFAF (f,v)) . y)
set F = FunctionalFAF (f,v);
thus (FunctionalFAF (f,v)) . (r * y) = f . (v,(r * y)) by BILINEAR:8
.= (r *') * (f . (v,y)) by Th27
.= (r *') * ((FunctionalFAF (f,v)) . y) by BILINEAR:8 ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f, g be cmplxhomogeneousFAF Form of V,W;
clusterf + g -> cmplxhomogeneousFAF ;
correctness
coherence
f + g is cmplxhomogeneousFAF ;
proof
let w be Vector of V; :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF ((f + g),w) is cmplxhomogeneous
set Ffg = FunctionalFAF ((f + g),w);
set Ff = FunctionalFAF (f,w);
set Fg = FunctionalFAF (g,w);
let v be Vector of W; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (FunctionalFAF ((f + g),w)) . (a * v) = (a *') * ((FunctionalFAF ((f + g),w)) . v)
let a be Scalar of ; ::_thesis: (FunctionalFAF ((f + g),w)) . (a * v) = (a *') * ((FunctionalFAF ((f + g),w)) . v)
thus (FunctionalFAF ((f + g),w)) . (a * v) = ((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . (a * v) by BILINEAR:13
.= ((FunctionalFAF (f,w)) . (a * v)) + ((FunctionalFAF (g,w)) . (a * v)) by HAHNBAN1:def_3
.= ((a *') * ((FunctionalFAF (f,w)) . v)) + ((FunctionalFAF (g,w)) . (a * v)) by Def1
.= ((a *') * ((FunctionalFAF (f,w)) . v)) + ((a *') * ((FunctionalFAF (g,w)) . v)) by Def1
.= (a *') * (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (g,w)) . v))
.= (a *') * (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) by HAHNBAN1:def_3
.= (a *') * ((FunctionalFAF ((f + g),w)) . v) by BILINEAR:13 ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneousFAF Form of V,W;
let a be Scalar of ;
clustera * f -> cmplxhomogeneousFAF ;
coherence
a * f is cmplxhomogeneousFAF
proof
let w be Vector of V; :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF ((a * f),w) is cmplxhomogeneous
set Ffg = FunctionalFAF ((a * f),w);
set Ff = FunctionalFAF (f,w);
let v be Vector of W; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (FunctionalFAF ((a * f),w)) . (a * v) = (a *') * ((FunctionalFAF ((a * f),w)) . v)
let b be Scalar of ; ::_thesis: (FunctionalFAF ((a * f),w)) . (b * v) = (b *') * ((FunctionalFAF ((a * f),w)) . v)
thus (FunctionalFAF ((a * f),w)) . (b * v) = (a * (FunctionalFAF (f,w))) . (b * v) by BILINEAR:15
.= a * ((FunctionalFAF (f,w)) . (b * v)) by HAHNBAN1:def_6
.= a * ((b *') * ((FunctionalFAF (f,w)) . v)) by Def1
.= (b *') * (a * ((FunctionalFAF (f,w)) . v))
.= (b *') * ((a * (FunctionalFAF (f,w))) . v) by HAHNBAN1:def_6
.= (b *') * ((FunctionalFAF ((a * f),w)) . v) by BILINEAR:15 ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneousFAF Form of V,W;
cluster - f -> cmplxhomogeneousFAF ;
coherence
- f is cmplxhomogeneousFAF ;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f, g be cmplxhomogeneousFAF Form of V,W;
clusterf - g -> cmplxhomogeneousFAF ;
coherence
f - g is cmplxhomogeneousFAF ;
end;
registration
let V, W be non trivial VectSp of F_Complex ;
cluster non trivial V16() V19([: the carrier of V, the carrier of W:]) V20( the carrier of F_Complex) Function-like non constant V30([: the carrier of V, the carrier of W:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Complex:];
existence
ex b1 being Form of V,W st
( b1 is additiveSAF & b1 is homogeneousSAF & b1 is additiveFAF & b1 is cmplxhomogeneousFAF & not b1 is constant & not b1 is trivial )
proof
set g = the non trivial non constant additive cmplxhomogeneous Functional of W;
set f = the non trivial non constant additive homogeneous Functional of V;
take FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) ; ::_thesis: ( FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is additiveSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is homogeneousSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is additiveFAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is cmplxhomogeneousFAF & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is constant & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is trivial )
thus ( FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is additiveSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is homogeneousSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is additiveFAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is cmplxhomogeneousFAF & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is constant & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V, the non trivial non constant additive cmplxhomogeneous Functional of W) is trivial ) ; ::_thesis: verum
end;
end;
definition
let V, W be non empty VectSpStr over F_Complex ;
let f be Form of V,W;
funcf *' -> Form of V,W means :Def8: :: HERMITAN:def 8
for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) *' ;
existence
ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) *'
proof
set K = F_Complex ;
set X = the carrier of V;
set Y = the carrier of W;
set Z = the carrier of F_Complex;
deffunc H1( Element of the carrier of V, Element of the carrier of W) -> Element of the carrier of F_Complex = (f . ($1,$2)) *' ;
consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of F_Complex such that
A1: for x being Element of the carrier of V
for y being Element of the carrier of W holds ff . (x,y) = H1(x,y) from BINOP_1:sch_4();
reconsider ff = ff as Form of V,W ;
take ff ; ::_thesis: for v being Vector of V
for w being Vector of W holds ff . (v,w) = (f . (v,w)) *'
thus for v being Vector of V
for w being Vector of W holds ff . (v,w) = (f . (v,w)) *' by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) *' ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) *' ) holds
b1 = b2
proof
let F, G be Form of V,W; ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds F . (v,w) = (f . (v,w)) *' ) & ( for v being Vector of V
for w being Vector of W holds G . (v,w) = (f . (v,w)) *' ) implies F = G )
assume that
A2: for v being Vector of V
for w being Vector of W holds F . (v,w) = (f . (v,w)) *' and
A3: for v being Vector of V
for w being Vector of W holds G . (v,w) = (f . (v,w)) *' ; ::_thesis: F = G
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_F_._(v,w)_=_G_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds F . (v,w) = G . (v,w)
let w be Vector of W; ::_thesis: F . (v,w) = G . (v,w)
thus F . (v,w) = (f . (v,w)) *' by A2
.= G . (v,w) by A3 ; ::_thesis: verum
end;
hence F = G by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines *' HERMITAN:def_8_:_
for V, W being non empty VectSpStr over F_Complex
for f, b4 being Form of V,W holds
( b4 = f *' iff for v being Vector of V
for w being Vector of W holds b4 . (v,w) = (f . (v,w)) *' );
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be additiveFAF Form of V,W;
clusterf *' -> additiveFAF ;
coherence
f *' is additiveFAF
proof
let v be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((f *'),v) is additive
let w, t be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((f *'),v)) . (w + t) = ((FunctionalFAF ((f *'),v)) . w) + ((FunctionalFAF ((f *'),v)) . t)
set fg = FunctionalFAF ((f *'),v);
thus (FunctionalFAF ((f *'),v)) . (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
.= ((FunctionalFAF ((f *'),v)) . w) + ((f *') . (v,t)) by BILINEAR:8
.= ((FunctionalFAF ((f *'),v)) . w) + ((FunctionalFAF ((f *'),v)) . t) by BILINEAR:8 ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be additiveSAF Form of V,W;
clusterf *' -> additiveSAF ;
coherence
f *' is additiveSAF
proof
let w be Vector of W; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((f *'),w) is additive
let v, t be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF ((f *'),w)) . (v + t) = ((FunctionalSAF ((f *'),w)) . v) + ((FunctionalSAF ((f *'),w)) . t)
set fg = FunctionalSAF ((f *'),w);
thus (FunctionalSAF ((f *'),w)) . (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
.= ((FunctionalSAF ((f *'),w)) . v) + ((f *') . (t,w)) by BILINEAR:9
.= ((FunctionalSAF ((f *'),w)) . v) + ((FunctionalSAF ((f *'),w)) . t) by BILINEAR:9 ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be homogeneousFAF Form of V,W;
clusterf *' -> cmplxhomogeneousFAF ;
coherence
f *' is cmplxhomogeneousFAF
proof
let v be Vector of V; :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF ((f *'),v) is cmplxhomogeneous
let w be Vector of W; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (FunctionalFAF ((f *'),v)) . (a * w) = (a *') * ((FunctionalFAF ((f *'),v)) . w)
let r be Scalar of ; ::_thesis: (FunctionalFAF ((f *'),v)) . (r * w) = (r *') * ((FunctionalFAF ((f *'),v)) . w)
set fg = FunctionalFAF ((f *'),v);
thus (FunctionalFAF ((f *'),v)) . (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 *') * ((FunctionalFAF ((f *'),v)) . w) by BILINEAR:8 ; ::_thesis: verum
end;
end;
registration
let V, W be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneousFAF Form of V,W;
clusterf *' -> homogeneousFAF ;
coherence
f *' is homogeneousFAF
proof
let v be Vector of V; :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((f *'),v) is homogeneous
let w be Vector of W; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of F_Complex holds (FunctionalFAF ((f *'),v)) . (b1 * w) = b1 * ((FunctionalFAF ((f *'),v)) . w)
let r be Scalar of ; ::_thesis: (FunctionalFAF ((f *'),v)) . (r * w) = r * ((FunctionalFAF ((f *'),v)) . w)
set fg = FunctionalFAF ((f *'),v);
thus (FunctionalFAF ((f *'),v)) . (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 * ((FunctionalFAF ((f *'),v)) . w) by BILINEAR:8 ; ::_thesis: verum
end;
end;
registration
let V, W be non trivial VectSp of F_Complex ;
let f be non constant Form of V,W;
clusterf *' -> non constant ;
coherence
not f *' is constant
proof
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def_1;
consider x, y being set 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 being Vector of V, wy being Vector of W such that
A5: y = [vy,wy] by A3, DOMAIN_1:1;
take x ; :: according to FUNCT_1:def_10 ::_thesis: ex b1 being set st
( x in K93((f *')) & b1 in K93((f *')) & not (f *') . x = (f *') . b1 )
take y ; ::_thesis: ( x in K93((f *')) & y in K93((f *')) & not (f *') . x = (f *') . y )
consider vx being Vector of V, wx being Vector of W such that
A6: x = [vx,wx] by A2, DOMAIN_1:1;
now__::_thesis:_not_(f_*')_._(vx,wx)_=_(f_*')_._(vy,wy)
assume (f *') . (vx,wx) = (f *') . (vy,wy) ; ::_thesis: contradiction
then ((f . (vx,wx)) *') *' = ((f *') . (vy,wy)) *' by Def8;
then f . (vx,wx) = ((f . (vy,wy)) *') *' by Def8;
hence contradiction by A4, A6, A5; ::_thesis: verum
end;
hence ( x in K93((f *')) & y in K93((f *')) & not (f *') . x = (f *') . y ) by A2, A3, A1, A6, A5, FUNCT_2:def_1; ::_thesis: verum
end;
end;
theorem Th28: :: HERMITAN:28
for V being non empty VectSpStr over F_Complex
for f being Functional of V
for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Functional of V
for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
let f be Functional of V; ::_thesis: for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
let v be Vector of V; ::_thesis: (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
set g = FormFunctional (f,(f *'));
thus (FormFunctional (f,(f *'))) . (v,v) = (f . v) * ((f *') . v) by BILINEAR:def_10
.= (f . v) * ((f . v) *') by Def2
.= |.(f . v).| ^2 by Th13 ; ::_thesis: verum
end;
registration
let V be non empty VectSpStr over F_Complex ;
let f be Functional of V;
cluster FormFunctional (f,(f *')) -> hermitan diagRvalued diagReR+0valued ;
coherence
( FormFunctional (f,(f *')) is diagReR+0valued & FormFunctional (f,(f *')) is hermitan & FormFunctional (f,(f *')) is diagRvalued )
proof
set g = FormFunctional (f,(f *'));
thus FormFunctional (f,(f *')) is diagReR+0valued ::_thesis: ( FormFunctional (f,(f *')) is hermitan & FormFunctional (f,(f *')) is diagRvalued )
proof
let v be Vector of V; :: according to HERMITAN:def_7 ::_thesis: 0 <= Re ((FormFunctional (f,(f *'))) . (v,v))
( (FormFunctional (f,(f *'))) . (v,v) = (|.(f . v).| ^2) + (0 * **) & (FormFunctional (f,(f *'))) . (v,v) = (Re ((FormFunctional (f,(f *'))) . (v,v))) + ((Im ((FormFunctional (f,(f *'))) . (v,v))) * **) ) by Th28, COMPLEX1:13;
then Re ((FormFunctional (f,(f *'))) . (v,v)) = |.(f . v).| ^2 by COMPLEX1:77;
hence 0 <= Re ((FormFunctional (f,(f *'))) . (v,v)) by XREAL_1:63; ::_thesis: verum
end;
thus FormFunctional (f,(f *')) is hermitan ::_thesis: FormFunctional (f,(f *')) is diagRvalued
proof
let v, w be Vector of V; :: according to HERMITAN:def_5 ::_thesis: (FormFunctional (f,(f *'))) . (v,w) = ((FormFunctional (f,(f *'))) . (w,v)) *'
thus (FormFunctional (f,(f *'))) . (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
.= ((FormFunctional (f,(f *'))) . (w,v)) *' by BILINEAR:def_10 ; ::_thesis: verum
end;
let v be Vector of V; :: according to HERMITAN:def_6 ::_thesis: Im ((FormFunctional (f,(f *'))) . (v,v)) = 0
( (FormFunctional (f,(f *'))) . (v,v) = [**(|.(f . v).| ^2),0**] & (FormFunctional (f,(f *'))) . (v,v) = (Re ((FormFunctional (f,(f *'))) . (v,v))) + ((Im ((FormFunctional (f,(f *'))) . (v,v))) * **) ) by Th28, COMPLEX1:13;
hence Im ((FormFunctional (f,(f *'))) . (v,v)) = 0 by COMPLEX1:77; ::_thesis: verum
end;
end;
registration
let V be non trivial VectSp of F_Complex ;
cluster non trivial V16() V19([: the carrier of V, the carrier of V:]) V20( the carrier of F_Complex) Function-like non constant V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
existence
ex b1 being Form of V,V st
( b1 is diagReR+0valued & b1 is hermitan & b1 is diagRvalued & b1 is additiveSAF & b1 is homogeneousSAF & b1 is additiveFAF & b1 is cmplxhomogeneousFAF & not b1 is constant & not b1 is trivial )
proof
set f = the non trivial non constant additive homogeneous Functional of V;
take FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) ; ::_thesis: ( FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is diagReR+0valued & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is hermitan & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is diagRvalued & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is additiveSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is homogeneousSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is additiveFAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is cmplxhomogeneousFAF & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is constant & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is trivial )
thus ( FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is diagReR+0valued & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is hermitan & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is diagRvalued & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is additiveSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is homogeneousSAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is additiveFAF & FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is cmplxhomogeneousFAF & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is constant & not FormFunctional ( the non trivial non constant additive homogeneous Functional of V,( the non trivial non constant additive homogeneous Functional of V *')) is trivial ) ; ::_thesis: verum
end;
end;
theorem :: HERMITAN:29
for V, W being non empty VectSpStr over F_Complex
for f being Form of V,W holds (f *') *' = f
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for f being Form of V,W holds (f *') *' = f
let f be Form of V,W; ::_thesis: (f *') *' = f
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((f_*')_*')_._(v,w)_=_f_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((f *') *') . (v,w) = f . (v,w)
let w be Vector of W; ::_thesis: ((f *') *') . (v,w) = f . (v,w)
thus ((f *') *') . (v,w) = ((f *') . (v,w)) *' by Def8
.= ((f . (v,w)) *') *' by Def8
.= f . (v,w) ; ::_thesis: verum
end;
hence (f *') *' = f by BINOP_1:2; ::_thesis: verum
end;
theorem :: HERMITAN:30
for V, W being non empty VectSpStr over F_Complex holds (NulForm (V,W)) *' = NulForm (V,W)
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: (NulForm (V,W)) *' = NulForm (V,W)
set f = NulForm (V,W);
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((NulForm_(V,W))_*')_._(v,w)_=_(NulForm_(V,W))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((NulForm (V,W)) *') . (v,w) = (NulForm (V,W)) . (v,w)
let w be Vector of W; ::_thesis: ((NulForm (V,W)) *') . (v,w) = (NulForm (V,W)) . (v,w)
thus ((NulForm (V,W)) *') . (v,w) = ((NulForm (V,W)) . (v,w)) *' by Def8
.= 0. F_Complex by COMPLFLD:47, FUNCOP_1:70
.= (NulForm (V,W)) . (v,w) by FUNCOP_1:70 ; ::_thesis: verum
end;
hence (NulForm (V,W)) *' = NulForm (V,W) by BINOP_1:2; ::_thesis: verum
end;
theorem Th31: :: HERMITAN:31
for V, W being non empty VectSpStr over F_Complex
for f, g being Form of V,W holds (f + g) *' = (f *') + (g *')
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for f, g being Form of V,W holds (f + g) *' = (f *') + (g *')
let f, g be Form of V,W; ::_thesis: (f + g) *' = (f *') + (g *')
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((f_+_g)_*')_._(v,w)_=_((f_*')_+_(g_*'))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((f + g) *') . (v,w) = ((f *') + (g *')) . (v,w)
let w be Vector of W; ::_thesis: ((f + g) *') . (v,w) = ((f *') + (g *')) . (v,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 ; ::_thesis: verum
end;
hence (f + g) *' = (f *') + (g *') by BINOP_1:2; ::_thesis: verum
end;
theorem Th32: :: HERMITAN:32
for V, W being non empty VectSpStr over F_Complex
for f being Form of V,W holds (- f) *' = - (f *')
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for f being Form of V,W holds (- f) *' = - (f *')
let f be Form of V,W; ::_thesis: (- f) *' = - (f *')
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((-_f)_*')_._(v,w)_=_(-_(f_*'))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((- f) *') . (v,w) = (- (f *')) . (v,w)
let w be Vector of W; ::_thesis: ((- f) *') . (v,w) = (- (f *')) . (v,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 ; ::_thesis: verum
end;
hence (- f) *' = - (f *') by BINOP_1:2; ::_thesis: verum
end;
theorem :: HERMITAN:33
for V, W being non empty VectSpStr over F_Complex
for f being Form of V,W
for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for f being Form of V,W
for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')
let f be Form of V,W; ::_thesis: for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')
let a be Element of F_Complex; ::_thesis: (a * f) *' = (a *') * (f *')
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((a_*_f)_*')_._(v,w)_=_((a_*')_*_(f_*'))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((a * f) *') . (v,w) = ((a *') * (f *')) . (v,w)
let w be Vector of W; ::_thesis: ((a * f) *') . (v,w) = ((a *') * (f *')) . (v,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 ; ::_thesis: verum
end;
hence (a * f) *' = (a *') * (f *') by BINOP_1:2; ::_thesis: verum
end;
theorem :: HERMITAN:34
for V, W being non empty VectSpStr over F_Complex
for f, g being Form of V,W holds (f - g) *' = (f *') - (g *')
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for f, g being Form of V,W holds (f - g) *' = (f *') - (g *')
let f, g be Form of V,W; ::_thesis: (f - g) *' = (f *') - (g *')
thus (f - g) *' = (f *') + ((- g) *') by Th31
.= (f *') - (g *') by Th32 ; ::_thesis: verum
end;
theorem Th35: :: HERMITAN:35
for V, W being VectSp of F_Complex
for v being Vector of V
for w, t being Vector of W
for f being 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 F_Complex ; ::_thesis: for v being Vector of V
for w, t being Vector of W
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let v1 be Vector of V; ::_thesis: for w, t being Vector of W
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . (v1,(w - t)) = (f . (v1,w)) - (f . (v1,t))
let w, w2 be Vector of W; ::_thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . (v1,(w - w2)) = (f . (v1,w)) - (f . (v1,w2))
let f be additiveFAF cmplxhomogeneousFAF Form of V,W; ::_thesis: f . (v1,(w - w2)) = (f . (v1,w)) - (f . (v1,w2))
thus f . (v1,(w - w2)) = (f . (v1,w)) + (f . (v1,(- w2))) by BILINEAR:27
.= (f . (v1,w)) + (f . (v1,((- (1_ F_Complex)) * w2))) by VECTSP_1:14
.= (f . (v1,w)) + (((- (1. F_Complex)) *') * (f . (v1,w2))) by Th27
.= (f . (v1,w)) + ((- (1_ F_Complex)) * (f . (v1,w2))) by COMPLFLD:49, COMPLFLD:52
.= (f . (v1,w)) - (f . (v1,w2)) by VECTSP_6:48 ; ::_thesis: verum
end;
theorem Th36: :: HERMITAN:36
for V, W being VectSp of F_Complex
for v, u being Vector of V
for w, t being Vector of W
for f being 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 ; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for f being sesquilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))
let v1, w1 be Vector of V; ::_thesis: for w, t being Vector of W
for f being sesquilinear-Form of V,W holds f . ((v1 - w1),(w - t)) = ((f . (v1,w)) - (f . (v1,t))) - ((f . (w1,w)) - (f . (w1,t)))
let w, w2 be Vector of W; ::_thesis: for f being sesquilinear-Form of V,W holds f . ((v1 - w1),(w - w2)) = ((f . (v1,w)) - (f . (v1,w2))) - ((f . (w1,w)) - (f . (w1,w2)))
let f be sesquilinear-Form of V,W; ::_thesis: f . ((v1 - w1),(w - w2)) = ((f . (v1,w)) - (f . (v1,w2))) - ((f . (w1,w)) - (f . (w1,w2)))
set v3 = f . (v1,w);
set v4 = f . (v1,w2);
set v5 = f . (w1,w);
set v6 = f . (w1,w2);
thus f . ((v1 - w1),(w - w2)) = (f . (v1,(w - w2))) - (f . (w1,(w - w2))) by BILINEAR:35
.= ((f . (v1,w)) - (f . (v1,w2))) - (f . (w1,(w - w2))) by Th35
.= ((f . (v1,w)) - (f . (v1,w2))) - ((f . (w1,w)) - (f . (w1,w2))) by Th35 ; ::_thesis: verum
end;
theorem Th37: :: HERMITAN:37
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of F_Complex
for f being 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 non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of F_Complex
for f being 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)))))
let v1, w1 be Vector of V; ::_thesis: for w, t being Vector of W
for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v1 + (a * w1)),(w + (b * t))) = ((f . (v1,w)) + ((b *') * (f . (v1,t)))) + ((a * (f . (w1,w))) + (a * ((b *') * (f . (w1,t)))))
let w, w2 be Vector of W; ::_thesis: for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v1 + (a * w1)),(w + (b * w2))) = ((f . (v1,w)) + ((b *') * (f . (v1,w2)))) + ((a * (f . (w1,w))) + (a * ((b *') * (f . (w1,w2)))))
let r, s be Element of F_Complex; ::_thesis: for f being sesquilinear-Form of V,W holds f . ((v1 + (r * w1)),(w + (s * w2))) = ((f . (v1,w)) + ((s *') * (f . (v1,w2)))) + ((r * (f . (w1,w))) + (r * ((s *') * (f . (w1,w2)))))
let f be sesquilinear-Form of V,W; ::_thesis: f . ((v1 + (r * w1)),(w + (s * w2))) = ((f . (v1,w)) + ((s *') * (f . (v1,w2)))) + ((r * (f . (w1,w))) + (r * ((s *') * (f . (w1,w2)))))
set v3 = f . (v1,w);
set v4 = f . (v1,w2);
set v5 = f . (w1,w);
set v6 = f . (w1,w2);
thus f . ((v1 + (r * w1)),(w + (s * w2))) = ((f . (v1,w)) + (f . (v1,(s * w2)))) + ((f . ((r * w1),w)) + (f . ((r * w1),(s * w2)))) by BILINEAR:28
.= ((f . (v1,w)) + ((s *') * (f . (v1,w2)))) + ((f . ((r * w1),w)) + (f . ((r * w1),(s * w2)))) by Th27
.= ((f . (v1,w)) + ((s *') * (f . (v1,w2)))) + ((r * (f . (w1,w))) + (f . ((r * w1),(s * w2)))) by BILINEAR:31
.= ((f . (v1,w)) + ((s *') * (f . (v1,w2)))) + ((r * (f . (w1,w))) + (r * (f . (w1,(s * w2))))) by BILINEAR:31
.= ((f . (v1,w)) + ((s *') * (f . (v1,w2)))) + ((r * (f . (w1,w))) + (r * ((s *') * (f . (w1,w2))))) by Th27 ; ::_thesis: verum
end;
theorem Th38: :: HERMITAN:38
for V, W being VectSp of F_Complex
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of F_Complex
for f being 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 ; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of F_Complex
for f being 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)))))
let v1, w1 be Vector of V; ::_thesis: for w, t being Vector of W
for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v1 - (a * w1)),(w - (b * t))) = ((f . (v1,w)) - ((b *') * (f . (v1,t)))) - ((a * (f . (w1,w))) - (a * ((b *') * (f . (w1,t)))))
let w, w2 be Vector of W; ::_thesis: for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v1 - (a * w1)),(w - (b * w2))) = ((f . (v1,w)) - ((b *') * (f . (v1,w2)))) - ((a * (f . (w1,w))) - (a * ((b *') * (f . (w1,w2)))))
let r, s be Element of F_Complex; ::_thesis: for f being sesquilinear-Form of V,W holds f . ((v1 - (r * w1)),(w - (s * w2))) = ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * ((s *') * (f . (w1,w2)))))
let f be sesquilinear-Form of V,W; ::_thesis: f . ((v1 - (r * w1)),(w - (s * w2))) = ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * ((s *') * (f . (w1,w2)))))
set v3 = f . (v1,w);
set v4 = f . (v1,w2);
set v5 = f . (w1,w);
set v6 = f . (w1,w2);
thus f . ((v1 - (r * w1)),(w - (s * w2))) = ((f . (v1,w)) - (f . (v1,(s * w2)))) - ((f . ((r * w1),w)) - (f . ((r * w1),(s * w2)))) by Th36
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((f . ((r * w1),w)) - (f . ((r * w1),(s * w2)))) by Th27
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (f . ((r * w1),(s * w2)))) by BILINEAR:31
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * (f . (w1,(s * w2))))) by BILINEAR:31
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * ((s *') * (f . (w1,w2))))) by Th27 ; ::_thesis: verum
end;
theorem Th39: :: HERMITAN:39
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex
for f being cmplxhomogeneousFAF Form of V,V
for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex
proof
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ; ::_thesis: for f being cmplxhomogeneousFAF Form of V,V
for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex
let f be cmplxhomogeneousFAF Form of V,V; ::_thesis: for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex
let v be Vector of V; ::_thesis: f . (v,(0. V)) = 0. F_Complex
set F = FunctionalFAF (f,v);
thus f . (v,(0. V)) = f . (v,((0. F_Complex) * (0. V))) by VECTSP10:1
.= (FunctionalFAF (f,v)) . ((0. F_Complex) * (0. V)) by BILINEAR:8
.= ((0. F_Complex) *') * ((FunctionalFAF (f,v)) . (0. V)) by Def1
.= 0. F_Complex by COMPLFLD:47, VECTSP_1:6 ; ::_thesis: verum
end;
theorem :: HERMITAN:40
for V being VectSp of F_Complex
for v, w being Vector of V
for f being 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 ; ::_thesis: for v, w being Vector of V
for f being 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)))))
let v1, w be Vector of V; ::_thesis: for f being hermitan-Form of V holds (((f . (v1,w)) + (f . (v1,w))) + (f . (v1,w))) + (f . (v1,w)) = (((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)))))
let f be hermitan-Form of V; ::_thesis: (((f . (v1,w)) + (f . (v1,w))) + (f . (v1,w))) + (f . (v1,w)) = (((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)))))
set v3 = f . (v1,v1);
set v4 = f . (v1,w);
set w2 = f . (w,w);
set w1 = f . (w,v1);
( f . ((v1 + w),(v1 + w)) = ((f . (v1,v1)) + (f . (v1,w))) + ((f . (w,v1)) + (f . (w,w))) & f . ((v1 - w),(v1 - w)) = ((f . (v1,v1)) - (f . (v1,w))) - ((f . (w,v1)) - (f . (w,w))) ) by Th36, BILINEAR:28;
then A1: (f . ((v1 + w),(v1 + w))) - (f . ((v1 - w),(v1 - w))) = (((f . (v1,v1)) + (f . (v1,w))) - (((f . (v1,v1)) - (f . (v1,w))) - ((f . (w,v1)) - (f . (w,w))))) + ((f . (w,v1)) + (f . (w,w)))
.= ((((f . (v1,v1)) + (f . (v1,w))) - ((f . (v1,v1)) - (f . (v1,w)))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w))) by RLVECT_1:29
.= ((((f . (v1,v1)) - ((f . (v1,v1)) - (f . (v1,w)))) + (f . (v1,w))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w)))
.= (((((f . (v1,v1)) - (f . (v1,v1))) + (f . (v1,w))) + (f . (v1,w))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w))) by RLVECT_1:29
.= ((((0. F_Complex) + (f . (v1,w))) + (f . (v1,w))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w))) by RLVECT_1:15
.= (((f . (v1,w)) + (f . (v1,w))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w))) by RLVECT_1:def_4
.= ((f . (v1,w)) + (f . (v1,w))) + ((((f . (w,v1)) - (f . (w,w))) + (f . (w,w))) + (f . (w,v1)))
.= ((f . (v1,w)) + (f . (v1,w))) + (((f . (w,v1)) - ((f . (w,w)) - (f . (w,w)))) + (f . (w,v1))) by RLVECT_1:29
.= ((f . (v1,w)) + (f . (v1,w))) + (((f . (w,v1)) - (0. F_Complex)) + (f . (w,v1))) by RLVECT_1:15
.= ((f . (v1,w)) + (f . (v1,w))) + ((f . (w,v1)) + (f . (w,v1))) by RLVECT_1:13 ;
f . ((v1 + (i_FC * w)),(v1 + (i_FC * w))) = ((f . (v1,v1)) + ((i_FC *') * (f . (v1,w)))) + ((i_FC * (f . (w,v1))) + (i_FC * ((i_FC *') * (f . (w,w))))) by Th37
.= ((f . (v1,v1)) + ((i_FC *') * (f . (v1,w)))) + (i_FC * ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) ;
then A2: i_FC * (f . ((v1 + (i_FC * w)),(v1 + (i_FC * w)))) = (i_FC * ((f . (v1,v1)) + ((i_FC *') * (f . (v1,w))))) + ((i_FC * i_FC) * ((f . (w,v1)) + ((i_FC *') * (f . (w,w)))))
.= ((i_FC * (f . (v1,v1))) + (f . (v1,w))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w)))) by COMPLEX1:7, HAHNBAN1:4, VECTSP_6:48 ;
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
.= ((f . (v1,v1)) - (f . (v1,(i_FC * w)))) - (f . ((i_FC * w),(v1 - (i_FC * w)))) by Th35
.= ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (f . ((i_FC * w),(v1 - (i_FC * w)))) by Th27
.= ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (i_FC * (f . (w,(v1 - (i_FC * w))))) by BILINEAR:31
.= ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (i_FC * ((f . (w,v1)) - (f . (w,(i_FC * w))))) by Th35
.= ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (i_FC * ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))) by Th27 ;
then i_FC * (f . ((v1 - (i_FC * w)),(v1 - (i_FC * w)))) = (i_FC * ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w))))) - (i_FC * (i_FC * ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))))) by VECTSP_1:11
.= (i_FC * ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w))))) - ((i_FC * i_FC) * ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))))
.= (i_FC * ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w))))) - (- ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))) by HAHNBAN1:4, VECTSP_6:48
.= (i_FC * ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w))))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) by COMPLFLD:11
.= ((i_FC * (f . (v1,v1))) - (i_FC * ((i_FC *') * (f . (v1,w))))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) by VECTSP_1:11
.= ((i_FC * (f . (v1,v1))) - (f . (v1,w))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) 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 * (f . (v1,v1))) + (f . (v1,w))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) - ((i_FC * (f . (v1,v1))) - (f . (v1,w)))) - ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) by A2, RLVECT_1:27
.= ((((i_FC * (f . (v1,v1))) + (f . (v1,w))) - ((i_FC * (f . (v1,v1))) - (f . (v1,w)))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) - ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))
.= (((((f . (v1,w)) + (i_FC * (f . (v1,v1)))) - (i_FC * (f . (v1,v1)))) + (f . (v1,w))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) - ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) by RLVECT_1:29
.= ((((f . (v1,w)) + ((i_FC * (f . (v1,v1))) - (i_FC * (f . (v1,v1))))) + (f . (v1,w))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) - ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))
.= ((((f . (v1,w)) + (0. F_Complex)) + (f . (v1,w))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) - ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) by RLVECT_1:15
.= (((f . (v1,w)) + (f . (v1,w))) - ((f . (w,v1)) + ((i_FC *') * (f . (w,w))))) - ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))) by RLVECT_1:def_4
.= ((f . (v1,w)) + (f . (v1,w))) - (((f . (w,v1)) + ((i_FC *') * (f . (w,w)))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))) by RLVECT_1:27
.= ((f . (v1,w)) + (f . (v1,w))) - (((f . (w,v1)) + (f . (w,v1))) + (((i_FC *') * (f . (w,w))) - ((i_FC *') * (f . (w,w)))))
.= ((f . (v1,w)) + (f . (v1,w))) - (((f . (w,v1)) + (f . (w,v1))) + (0. F_Complex)) by RLVECT_1:15
.= ((f . (v1,w)) + (f . (v1,w))) - ((f . (w,v1)) + (f . (w,v1))) 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))))) = ((f . (v1,w)) + (f . (v1,w))) + ((((f . (w,v1)) + (f . (w,v1))) + ((f . (v1,w)) + (f . (v1,w)))) - ((f . (w,v1)) + (f . (w,v1)))) by A1
.= ((f . (v1,w)) + (f . (v1,w))) + ((f . (v1,w)) + (f . (v1,w))) by COMPLFLD:12
.= (((f . (v1,w)) + (f . (v1,w))) + (f . (v1,w))) + (f . (v1,w)) ;
hence (((f . (v1,w)) + (f . (v1,w))) + (f . (v1,w))) + (f . (v1,w)) = (((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))))) ; ::_thesis: verum
end;
definition
let V be non empty VectSpStr over F_Complex ;
let f be Form of V,V;
let v be Vector of V;
func signnorm (f,v) -> real number equals :: HERMITAN:def 9
Re (f . (v,v));
coherence
Re (f . (v,v)) is real number ;
end;
:: deftheorem defines signnorm HERMITAN:def_9_:_
for V being non empty VectSpStr over F_Complex
for f being Form of V,V
for v being Vector of V holds signnorm (f,v) = Re (f . (v,v));
theorem Th41: :: HERMITAN:41
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex
for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V holds
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
proof
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ; ::_thesis: for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V holds
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
let f be diagRvalued diagReR+0valued Form of V,V; ::_thesis: for v being Vector of V holds
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
let v be Vector of V; ::_thesis: ( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
set v1 = f . (v,v);
( 0 <= Re (f . (v,v)) & Im (f . (v,v)) = 0 ) by Def6, Def7;
hence ( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| ) by Th14; ::_thesis: verum
end;
theorem Th42: :: HERMITAN:42
for V being VectSp of F_Complex
for v, w being Vector of V
for f being sesquilinear-Form of V,V
for r being real number
for a being 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 ; ::_thesis: for v, w being Vector of V
for f being sesquilinear-Form of V,V
for r being real number
for a being 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)))
let v1, w be Vector of V; ::_thesis: for f being sesquilinear-Form of V,V
for r being real number
for a being Element of F_Complex st |.a.| = 1 holds
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let f be sesquilinear-Form of V,V; ::_thesis: for r being real number
for a being Element of F_Complex st |.a.| = 1 holds
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let r be real number ; ::_thesis: for a being Element of F_Complex st |.a.| = 1 holds
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let a be Element of F_Complex; ::_thesis: ( |.a.| = 1 implies f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w))) )
assume A1: |.a.| = 1 ; ::_thesis: f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
set r1 = [**r,0**] * a;
set v3 = f . (v1,v1);
set v4 = f . (v1,w);
set w1 = f . (w,v1);
set w2 = f . (w,w);
A2: ([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w))) = ([**(r ^2),0**] * (a * (a *'))) * (f . (w,w))
.= [**((r ^2) * (1 ^2)),0**] * (f . (w,w)) by A1, Th13 ;
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = ((f . (v1,v1)) - ((([**r,0**] * a) *') * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] * a) *') * (f . (w,w))))) by Th38
.= ((f . (v1,v1)) - ((([**r,0**] *') * (a *')) * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] * a) *') * (f . (w,w))))) by COMPLFLD:54
.= ((f . (v1,v1)) - (([**r,0**] * (a *')) * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] * a) *') * (f . (w,w))))) by Th12, COMPLEX1:12
.= ((f . (v1,v1)) - (([**r,0**] * (a *')) * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] *') * (a *')) * (f . (w,w))))) by COMPLFLD:54
.= ((f . (v1,v1)) - ([**r,0**] * ((a *') * (f . (v1,w))))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w))))) by Th12, COMPLEX1:12
.= (((f . (v1,v1)) - ([**r,0**] * ((a *') * (f . (v1,w))))) - ([**r,0**] * (a * (f . (w,v1))))) + (([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w)))) by RLVECT_1:29
.= (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + (([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w)))) ;
hence f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w))) by A2; ::_thesis: verum
end;
theorem Th43: :: HERMITAN:43
for V being VectSp of F_Complex
for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V
for r being real number
for a being 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 ; ::_thesis: for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V
for r being real number
for a being 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)) )
let v1, w be Vector of V; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for r being real number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| holds
( Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) & 0 <= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) )
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for r being real number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| holds
( Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) & 0 <= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) )
let r be real number ; ::_thesis: for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| holds
( Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) & 0 <= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) )
let a be Element of F_Complex; ::_thesis: ( |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| implies ( Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) & 0 <= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) ) )
assume that
A1: |.a.| = 1 and
A2: Re (a * (f . (w,v1))) = |.(f . (w,v1)).| ; ::_thesis: ( Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) & 0 <= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) )
set v3 = f . (v1,v1);
set v4 = f . (v1,w);
set w1 = f . (w,v1);
set w2 = f . (w,w);
set A = signnorm (f,v1);
set B = |.(f . (w,v1)).|;
set C = signnorm (f,w);
A3: ( Re [**r,0**] = r & Im [**r,0**] = 0 ) by COMPLEX1:12;
then A4: Re ([**r,0**] * (a * (f . (w,v1)))) = r * |.(f . (w,v1)).| by A2, Th10;
(a *') * (f . (v1,w)) = (((a *') * (f . (v1,w))) *') *'
.= (((a *') *') * ((f . (v1,w)) *')) *' by COMPLFLD:54
.= (a * (f . (w,v1))) *' by Def5 ;
then A5: Re ([**r,0**] * ((a *') * (f . (v1,w)))) = r * (Re ((a * (f . (w,v1))) *')) by A3, Th10
.= r * |.(f . (w,v1)).| by A2, COMPLEX1:27 ;
( Re [**(r ^2),0**] = r ^2 & Im [**(r ^2),0**] = 0 ) by COMPLEX1:12;
then A6: Re ([**(r ^2),0**] * (f . (w,w))) = (r ^2) * (signnorm (f,w)) by Th10;
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w))) by A1, Th42;
then Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = (Re (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w)))))) + ((signnorm (f,w)) * (r ^2)) by A6, HAHNBAN1:10
.= ((Re ((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1)))))) - (r * |.(f . (w,v1)).|)) + ((signnorm (f,w)) * (r ^2)) by A5, Th9
.= (((signnorm (f,v1)) - (r * |.(f . (w,v1)).|)) - (r * |.(f . (w,v1)).|)) + ((signnorm (f,w)) * (r ^2)) by A4, Th9
.= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) ;
hence ( Re (f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w)))) = ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) & 0 <= ((signnorm (f,v1)) - ((2 * |.(f . (w,v1)).|) * r)) + ((signnorm (f,w)) * (r ^2)) ) by Def7; ::_thesis: verum
end;
theorem Th44: :: HERMITAN:44
for V being VectSp of F_Complex
for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V st signnorm (f,w) = 0 holds
|.(f . (w,v)).| = 0
proof
let V be VectSp of F_Complex ; ::_thesis: for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V st signnorm (f,w) = 0 holds
|.(f . (w,v)).| = 0
let v1, w be Vector of V; ::_thesis: for f being diagReR+0valued hermitan-Form of V st signnorm (f,w) = 0 holds
|.(f . (w,v1)).| = 0
let f be diagReR+0valued hermitan-Form of V; ::_thesis: ( signnorm (f,w) = 0 implies |.(f . (w,v1)).| = 0 )
set w1 = f . (w,v1);
set A = signnorm (f,v1);
set B = |.(f . (w,v1)).|;
set C = signnorm (f,w);
reconsider A = signnorm (f,v1) as Real ;
assume that
A1: signnorm (f,w) = 0 and
A2: |.(f . (w,v1)).| <> 0 ; ::_thesis: contradiction
A3: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| & Im (a * (f . (w,v1))) = 0 ) by Th8;
A4: now__::_thesis:_not_A_<>_0
A5: now__::_thesis:_not_A_>_0
assume A6: A > 0 ; ::_thesis: contradiction
(A - ((2 * |.(f . (w,v1)).|) * (A / |.(f . (w,v1)).|))) + ((signnorm (f,w)) * ((A / |.(f . (w,v1)).|) ^2)) = A - ((A * (2 * |.(f . (w,v1)).|)) / |.(f . (w,v1)).|) by A1, XCMPLX_1:74
.= A - (((A * 2) * |.(f . (w,v1)).|) / |.(f . (w,v1)).|)
.= A - (A + A) by A2, XCMPLX_1:89
.= - A ;
hence contradiction by A3, A6, Th43; ::_thesis: verum
end;
A7: now__::_thesis:_not_A_<_0
assume A8: A < 0 ; ::_thesis: contradiction
0 <= (A - ((2 * |.(f . (w,v1)).|) * 0)) + ((signnorm (f,w)) * (0 ^2)) by A3, Th43;
hence contradiction by A8; ::_thesis: verum
end;
assume A <> 0 ; ::_thesis: contradiction
hence contradiction by A7, A5; ::_thesis: verum
end;
now__::_thesis:_not_A_=_0
assume A9: A = 0 ; ::_thesis: contradiction
A10: now__::_thesis:_not_0_<_|.(f_._(w,v1)).|
assume A11: 0 < |.(f . (w,v1)).| ; ::_thesis: contradiction
0 <= (A - ((2 * |.(f . (w,v1)).|) * 1)) + ((signnorm (f,w)) * (1 ^2)) by A3, Th43;
hence contradiction by A1, A9, A11; ::_thesis: verum
end;
now__::_thesis:_not_|.(f_._(w,v1)).|_<_0
assume A12: |.(f . (w,v1)).| < 0 ; ::_thesis: contradiction
0 <= (A - ((2 * |.(f . (w,v1)).|) * (- 1))) + ((signnorm (f,w)) * ((- 1) ^2)) by A3, Th43;
hence contradiction by A1, A9, A12; ::_thesis: verum
end;
hence contradiction by A2, A10; ::_thesis: verum
end;
hence contradiction by A4; ::_thesis: verum
end;
theorem Th45: :: HERMITAN:45
for V being VectSp of F_Complex
for v, w being Vector of V
for f being 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 ; ::_thesis: for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V holds |.(f . (v,w)).| ^2 <= (signnorm (f,v)) * (signnorm (f,w))
let v1, w be Vector of V; ::_thesis: for f being diagReR+0valued hermitan-Form of V holds |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w))
let f be diagReR+0valued hermitan-Form of V; ::_thesis: |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w))
set v4 = f . (v1,w);
set w1 = f . (w,v1);
set A = signnorm (f,v1);
set B = |.(f . (w,v1)).|;
set C = signnorm (f,w);
reconsider A = signnorm (f,v1), B = |.(f . (w,v1)).|, C = signnorm (f,w) as Real ;
A1: ( C = 0 ^2 implies B ^2 <= A * C ) by Th44;
A2: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| & Im (a * (f . (w,v1))) = 0 ) by Th8;
A3: ( C > 0 implies B ^2 <= A * C )
proof
assume A4: C > 0 ; ::_thesis: B ^2 <= A * C
(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 B ^2 <= A * C ; ::_thesis: verum
end;
B = |.((f . (v1,w)) *').| by Def5
.= |.(f . (v1,w)).| by COMPLEX1:53 ;
hence |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w)) by A1, A3, Def7; ::_thesis: verum
end;
theorem Th46: :: HERMITAN:46
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds |.(f . (v,w)).| ^2 <= |.(f . (v,v)).| * |.(f . (w,w)).|
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds |.(f . (v,w)).| ^2 <= |.(f . (v,v)).| * |.(f . (w,w)).|
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for v, w being Vector of V holds |.(f . (v,w)).| ^2 <= |.(f . (v,v)).| * |.(f . (w,w)).|
let v1, w be Vector of V; ::_thesis: |.(f . (v1,w)).| ^2 <= |.(f . (v1,v1)).| * |.(f . (w,w)).|
set v3 = f . (v1,v1);
set s1 = signnorm (f,v1);
set s2 = signnorm (f,w);
( |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w)) & signnorm (f,v1) = |.(f . (v1,v1)).| ) by Th41, Th45;
hence |.(f . (v1,w)).| ^2 <= |.(f . (v1,v1)).| * |.(f . (w,w)).| by Th41; ::_thesis: verum
end;
theorem Th47: :: HERMITAN:47
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being 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 ; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for v, w being Vector of V holds signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2
let v, w be Vector of V; ::_thesis: signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2
set v3 = f . (v,v);
set v4 = f . (v,w);
set w1 = f . (w,v);
set w2 = f . (w,w);
set sv = signnorm (f,v);
set sw = signnorm (f,w);
set svw = signnorm (f,(v + w));
A1: 0 <= signnorm (f,v) by Def7;
A2: signnorm (f,(v + w)) = Re (((f . (v,v)) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w)))) by BILINEAR:28
.= (Re ((f . (v,v)) + (f . (v,w)))) + (Re ((f . (w,v)) + (f . (w,w)))) by HAHNBAN1:10
.= ((Re (f . (v,v))) + (Re (f . (v,w)))) + (Re ((f . (w,v)) + (f . (w,w)))) by HAHNBAN1:10
.= ((Re (f . (v,v))) + (Re (f . (v,w)))) + ((Re (f . (w,v))) + (Re (f . (w,w)))) by HAHNBAN1:10
.= ((signnorm (f,v)) + ((Re (f . (v,w))) + (Re (f . (w,v))))) + (signnorm (f,w))
.= ((signnorm (f,v)) + ((Re (f . (v,w))) + (Re ((f . (v,w)) *')))) + (signnorm (f,w)) by Def5
.= ((signnorm (f,v)) + (2 * (Re (f . (v,w))))) + (signnorm (f,w)) by Th15
.= ((signnorm (f,v)) + (signnorm (f,w))) + (2 * (Re (f . (v,w)))) ;
A3: 0 <= signnorm (f,w) by Def7;
0 <= |.(f . (v,w)).| by COMPLEX1:46;
then sqrt (|.(f . (v,w)).| ^2) <= sqrt ((signnorm (f,v)) * (signnorm (f,w))) by Th45, SQUARE_1:26;
then |.(f . (v,w)).| <= sqrt ((signnorm (f,v)) * (signnorm (f,w))) by COMPLEX1:46, SQUARE_1:22;
then ( Re (f . (v,w)) <= |.(f . (v,w)).| & |.(f . (v,w)).| <= (sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))) ) by A1, A3, COMPLEX1:54, SQUARE_1:29;
then Re (f . (v,w)) <= (sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))) by XXREAL_0:2;
then 2 * (Re (f . (v,w))) <= 2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w)))) by XREAL_1:64;
then signnorm (f,(v + w)) <= ((signnorm (f,v)) + (signnorm (f,w))) + (2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))))) by A2, XREAL_1:6;
then signnorm (f,(v + w)) <= (((sqrt (signnorm (f,v))) ^2) + (signnorm (f,w))) + (2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))))) by A1, SQUARE_1:def_2;
then signnorm (f,(v + w)) <= (((sqrt (signnorm (f,v))) ^2) + ((sqrt (signnorm (f,w))) ^2)) + (2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))))) by A3, SQUARE_1:def_2;
hence signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2 ; ::_thesis: verum
end;
theorem :: HERMITAN:48
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being 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 ; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds |.(f . ((v + w),(v + w))).| <= ((sqrt |.(f . (v,v)).|) + (sqrt |.(f . (w,w)).|)) ^2
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for v, w being Vector of V holds |.(f . ((v + w),(v + w))).| <= ((sqrt |.(f . (v,v)).|) + (sqrt |.(f . (w,w)).|)) ^2
let v1, w be Vector of V; ::_thesis: |.(f . ((v1 + w),(v1 + w))).| <= ((sqrt |.(f . (v1,v1)).|) + (sqrt |.(f . (w,w)).|)) ^2
set v3 = f . (v1,v1);
set v4 = f . ((v1 + w),(v1 + w));
set s1 = signnorm (f,v1);
set s2 = signnorm (f,w);
set s12 = signnorm (f,(v1 + w));
A1: |.(f . ((v1 + w),(v1 + w))).| = signnorm (f,(v1 + w)) by Th41;
( signnorm (f,(v1 + w)) <= ((sqrt (signnorm (f,v1))) + (sqrt (signnorm (f,w)))) ^2 & |.(f . (v1,v1)).| = signnorm (f,v1) ) by Th41, Th47;
hence |.(f . ((v1 + w),(v1 + w))).| <= ((sqrt |.(f . (v1,v1)).|) + (sqrt |.(f . (w,w)).|)) ^2 by A1, Th41; ::_thesis: verum
end;
theorem Th49: :: HERMITAN:49
for V being VectSp of F_Complex
for f being hermitan-Form of V
for v, w being 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 ; ::_thesis: for f being hermitan-Form of V
for v, w being Element of V holds (signnorm (f,(v + w))) + (signnorm (f,(v - w))) = (2 * (signnorm (f,v))) + (2 * (signnorm (f,w)))
let f be hermitan-Form of V; ::_thesis: for v, w being Element of V holds (signnorm (f,(v + w))) + (signnorm (f,(v - w))) = (2 * (signnorm (f,v))) + (2 * (signnorm (f,w)))
let v1, w be Element of V; ::_thesis: (signnorm (f,(v1 + w))) + (signnorm (f,(v1 - w))) = (2 * (signnorm (f,v1))) + (2 * (signnorm (f,w)))
set v3 = f . (v1,v1);
set v4 = f . (v1,w);
set w1 = f . (w,v1);
set w2 = f . (w,w);
set vp = f . ((v1 + w),(v1 + w));
set vm = f . ((v1 - w),(v1 - w));
set s1 = signnorm (f,v1);
set s2 = signnorm (f,w);
set sp = signnorm (f,(v1 + w));
set sm = signnorm (f,(v1 - w));
f . ((v1 + w),(v1 + w)) = ((f . (v1,v1)) + (f . (v1,w))) + ((f . (w,v1)) + (f . (w,w))) by BILINEAR:28;
then A1: (f . ((v1 + w),(v1 + w))) + (f . ((v1 - w),(v1 - w))) = (((f . (v1,v1)) + (f . (v1,w))) + ((f . (w,v1)) + (f . (w,w)))) + (((f . (v1,v1)) - (f . (v1,w))) - ((f . (w,v1)) - (f . (w,w)))) by Th36
.= (((f . (v1,v1)) + (((f . (v1,w)) + (f . (v1,v1))) - (f . (v1,w)))) + ((f . (w,v1)) + (f . (w,w)))) - ((f . (w,v1)) - (f . (w,w)))
.= (((f . (v1,v1)) + (f . (v1,v1))) + ((f . (w,v1)) + (f . (w,w)))) - ((f . (w,v1)) - (f . (w,w))) by COMPLFLD:12
.= ((f . (v1,v1)) + (f . (v1,v1))) + (((f . (w,v1)) + (f . (w,w))) - ((f . (w,v1)) - (f . (w,w))))
.= ((f . (v1,v1)) + (f . (v1,v1))) + ((((f . (w,v1)) + (f . (w,w))) - (f . (w,v1))) + (f . (w,w))) by RLVECT_1:29
.= ((f . (v1,v1)) + (f . (v1,v1))) + ((f . (w,w)) + (f . (w,w))) by COMPLFLD:12 ;
thus (signnorm (f,(v1 + w))) + (signnorm (f,(v1 - w))) = Re ((f . ((v1 + w),(v1 + w))) + (f . ((v1 - w),(v1 - w)))) by HAHNBAN1:10
.= (Re ((f . (v1,v1)) + (f . (v1,v1)))) + (Re ((f . (w,w)) + (f . (w,w)))) by A1, HAHNBAN1:10
.= ((Re (f . (v1,v1))) + (Re (f . (v1,v1)))) + (Re ((f . (w,w)) + (f . (w,w)))) by HAHNBAN1:10
.= (2 * (Re (f . (v1,v1)))) + ((Re (f . (w,w))) + (Re (f . (w,w)))) by HAHNBAN1:10
.= (2 * (signnorm (f,v1))) + (2 * (signnorm (f,w))) ; ::_thesis: verum
end;
theorem :: HERMITAN:50
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being 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 ; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Element of V holds |.(f . ((v + w),(v + w))).| + |.(f . ((v - w),(v - w))).| = (2 * |.(f . (v,v)).|) + (2 * |.(f . (w,w)).|)
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for v, w being Element of V holds |.(f . ((v + w),(v + w))).| + |.(f . ((v - w),(v - w))).| = (2 * |.(f . (v,v)).|) + (2 * |.(f . (w,w)).|)
let v1, w be Element of V; ::_thesis: |.(f . ((v1 + w),(v1 + w))).| + |.(f . ((v1 - w),(v1 - w))).| = (2 * |.(f . (v1,v1)).|) + (2 * |.(f . (w,w)).|)
set s1 = signnorm (f,v1);
set s2 = signnorm (f,w);
set sp = signnorm (f,(v1 + w));
set sm = signnorm (f,(v1 - w));
A1: ( signnorm (f,(v1 - w)) = |.(f . ((v1 - w),(v1 - w))).| & signnorm (f,v1) = |.(f . (v1,v1)).| ) by Th41;
( (signnorm (f,(v1 + w))) + (signnorm (f,(v1 - w))) = (2 * (signnorm (f,v1))) + (2 * (signnorm (f,w))) & signnorm (f,(v1 + w)) = |.(f . ((v1 + w),(v1 + w))).| ) by Th41, Th49;
hence |.(f . ((v1 + w),(v1 + w))).| + |.(f . ((v1 - w),(v1 - w))).| = (2 * |.(f . (v1,v1)).|) + (2 * |.(f . (w,w)).|) by A1, Th41; ::_thesis: verum
end;
definition
let V be non empty VectSpStr over F_Complex ;
let f be Form of V,V;
func quasinorm f -> RFunctional of V means :Def10: :: HERMITAN:def 10
for v being Element of V holds it . v = sqrt (signnorm (f,v));
existence
ex b1 being RFunctional of V st
for v being Element of V holds b1 . v = sqrt (signnorm (f,v))
proof
set C = the carrier of V;
defpred S1[ Element of the carrier of V, set ] means $2 = sqrt (signnorm (f,$1));
A1: now__::_thesis:_for_x_being_Element_of_the_carrier_of_V_ex_y_being_Element_of_REAL_st_S1[x,y]
let x be Element of the carrier of V; ::_thesis: ex y being Element of REAL st S1[x,y]
reconsider y = sqrt (signnorm (f,x)) as Element of REAL by XREAL_0:def_1;
take y = y; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider F being Function of the carrier of V,REAL such that
A2: for v being Element of V holds S1[v,F . v] from FUNCT_2:sch_3(A1);
reconsider F = F as RFunctional of V ;
take F ; ::_thesis: for v being Element of V holds F . v = sqrt (signnorm (f,v))
thus for v being Element of V holds F . v = sqrt (signnorm (f,v)) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being RFunctional of V st ( for v being Element of V holds b1 . v = sqrt (signnorm (f,v)) ) & ( for v being Element of V holds b2 . v = sqrt (signnorm (f,v)) ) holds
b1 = b2
proof
let h, g be RFunctional of V; ::_thesis: ( ( for v being Element of V holds h . v = sqrt (signnorm (f,v)) ) & ( for v being Element of V holds g . v = sqrt (signnorm (f,v)) ) implies h = g )
assume that
A3: for v being Element of V holds h . v = sqrt (signnorm (f,v)) and
A4: for v being Element of V holds g . v = sqrt (signnorm (f,v)) ; ::_thesis: h = g
now__::_thesis:_for_v_being_Element_of_V_holds_h_._v_=_g_._v
let v be Element of V; ::_thesis: h . v = g . v
thus h . v = sqrt (signnorm (f,v)) by A3
.= g . v by A4 ; ::_thesis: verum
end;
hence h = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines quasinorm HERMITAN:def_10_:_
for V being non empty VectSpStr over F_Complex
for f being Form of V,V
for b3 being RFunctional of V holds
( b3 = quasinorm f iff for v being Element of V holds b3 . v = sqrt (signnorm (f,v)) );
registration
let V be VectSp of F_Complex ;
let f be diagReR+0valued hermitan-Form of V;
cluster quasinorm f -> subadditive homogeneous ;
coherence
( quasinorm f is subadditive & quasinorm f is homogeneous )
proof
set q = quasinorm f;
thus quasinorm f is subadditive ::_thesis: quasinorm f is homogeneous
proof
let v, w be Vector of V; :: according to HAHNBAN1:def_11 ::_thesis: (quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w)
set fvw = signnorm (f,(v + w));
set fv = signnorm (f,v);
set fw = signnorm (f,w);
A1: (quasinorm f) . v = sqrt (signnorm (f,v)) by Def10;
0 <= Re (f . (v,v)) by Def7;
then A2: 0 <= (quasinorm f) . v by A1, SQUARE_1:def_2;
A3: (quasinorm f) . w = sqrt (signnorm (f,w)) by Def10;
0 <= Re (f . (w,w)) by Def7;
then A4: 0 <= (quasinorm f) . w by A3, SQUARE_1:def_2;
( 0 <= Re (f . ((v + w),(v + w))) & (quasinorm f) . (v + w) = sqrt (signnorm (f,(v + w))) ) by Def7, Def10;
then (quasinorm f) . (v + w) <= sqrt ((((quasinorm f) . v) + ((quasinorm f) . w)) ^2) by A1, A3, Th47, SQUARE_1:26;
hence (quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w) by A2, A4, SQUARE_1:22; ::_thesis: verum
end;
let v be Vector of V; :: according to HAHNBAN1:def_14 ::_thesis: for b1 being Element of the carrier of F_Complex holds (quasinorm f) . (b1 * v) = |.b1.| * ((quasinorm f) . v)
let r be Scalar of ; ::_thesis: (quasinorm f) . (r * v) = |.r.| * ((quasinorm f) . 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 (quasinorm f) . (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.| * ((quasinorm f) . v) by Def10 ; ::_thesis: verum
end;
end;
begin
registration
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ;
let f be cmplxhomogeneousFAF Form of V,V;
cluster diagker f -> non empty ;
coherence
not diagker f is empty
proof
set F = F_Complex ;
f . ((0. V),(0. V)) = 0. F_Complex by Th39;
then 0. V in diagker f ;
hence not diagker f is empty ; ::_thesis: verum
end;
end;
theorem :: HERMITAN:51
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds diagker f is linearly-closed
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V holds diagker f is linearly-closed
let f be diagReR+0valued hermitan-Form of V; ::_thesis: diagker f is linearly-closed
set V1 = diagker f;
thus for v, u being Element of V st v in diagker f & u in diagker f holds
v + u in diagker f :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of F_Complex
for b2 being Element of the carrier of V holds
( not b2 in diagker f or b1 * b2 in diagker f )
proof
let v, u be Element of V; ::_thesis: ( v in diagker f & u in diagker f implies v + u in diagker f )
assume that
A1: v in diagker f and
A2: u in diagker f ; ::_thesis: v + u in diagker f
A3: ex b being 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 being 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 v + u in diagker f ; ::_thesis: verum
end;
let a be Element of F_Complex; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in diagker f or a * b1 in diagker f )
let v be Element of V; ::_thesis: ( not v in diagker f or a * v in diagker f )
assume v in diagker f ; ::_thesis: a * v in diagker f
then A7: ex w being 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
.= a * (0. F_Complex) by VECTSP_1:6
.= 0. F_Complex by VECTSP_1:6 ;
hence a * v in diagker f ; ::_thesis: verum
end;
theorem Th52: :: HERMITAN:52
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds diagker f = leftker f
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V holds diagker f = leftker f
let f be diagReR+0valued hermitan-Form of V; ::_thesis: diagker f = leftker f
thus diagker f c= leftker f :: according to XBOOLE_0:def_10 ::_thesis: leftker f c= diagker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in diagker f or x in leftker f )
assume x in diagker f ; ::_thesis: x in leftker f
then consider a being Vector of V such that
A1: a = x and
A2: f . (a,a) = 0. F_Complex ;
now__::_thesis:_for_w_being_Vector_of_V_holds_f_._(a,w)_=_0._F_Complex
let w be Vector of V; ::_thesis: f . (a,w) = 0. F_Complex
|.(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; ::_thesis: verum
end;
hence x in leftker f by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in diagker f )
assume x in leftker f ; ::_thesis: x in diagker f
then consider a being Vector of V such that
A3: a = x and
A4: for w being Vector of V holds f . (a,w) = 0. F_Complex ;
f . (a,a) = 0. F_Complex by A4;
hence x in diagker f by A3; ::_thesis: verum
end;
theorem Th53: :: HERMITAN:53
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds diagker f = rightker f
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V holds diagker f = rightker f
let f be diagReR+0valued hermitan-Form of V; ::_thesis: diagker f = rightker f
thus diagker f c= rightker f :: according to XBOOLE_0:def_10 ::_thesis: rightker f c= diagker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in diagker f or x in rightker f )
assume x in diagker f ; ::_thesis: x in rightker f
then consider a being Vector of V such that
A1: a = x and
A2: f . (a,a) = 0. F_Complex ;
now__::_thesis:_for_w_being_Vector_of_V_holds_f_._(w,a)_=_0._F_Complex
let w be Vector of V; ::_thesis: f . (w,a) = 0. F_Complex
|.(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; ::_thesis: verum
end;
hence x in rightker f by A1; ::_thesis: verum
end;
thus rightker f c= diagker f by BILINEAR:41; ::_thesis: verum
end;
theorem :: HERMITAN:54
for V being non empty VectSpStr over F_Complex
for f being Form of V,V holds diagker f = diagker (f *')
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for f being Form of V,V holds diagker f = diagker (f *')
let f be Form of V,V; ::_thesis: diagker f = diagker (f *')
set K = F_Complex ;
thus diagker f c= diagker (f *') :: according to XBOOLE_0:def_10 ::_thesis: diagker (f *') c= diagker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in diagker f or x in diagker (f *') )
assume x in diagker f ; ::_thesis: x in diagker (f *')
then consider v being Vector of V such that
A1: x = v and
A2: f . (v,v) = 0. F_Complex ;
(f *') . (v,v) = 0. F_Complex by A2, Def8, COMPLFLD:47;
hence x in diagker (f *') by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in diagker (f *') or x in diagker f )
assume x in diagker (f *') ; ::_thesis: x in diagker f
then consider v being Vector of V such that
A3: x = v and
A4: (f *') . (v,v) = 0. F_Complex ;
((f . (v,v)) *') *' = 0. F_Complex by A4, Def8, COMPLFLD:47;
hence x in diagker f by A3; ::_thesis: verum
end;
theorem Th55: :: HERMITAN:55
for V, W being non empty VectSpStr over F_Complex
for f being Form of V,W holds
( leftker f = leftker (f *') & rightker f = rightker (f *') )
proof
let V, W be non empty VectSpStr over F_Complex ; ::_thesis: for f being Form of V,W holds
( leftker f = leftker (f *') & rightker f = rightker (f *') )
let f be Form of V,W; ::_thesis: ( leftker f = leftker (f *') & rightker f = rightker (f *') )
set K = F_Complex ;
thus leftker f c= leftker (f *') :: according to XBOOLE_0:def_10 ::_thesis: ( leftker (f *') c= leftker f & rightker f = rightker (f *') )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in leftker (f *') )
assume x in leftker f ; ::_thesis: x in leftker (f *')
then consider v being Vector of V such that
A1: x = v and
A2: for w being Vector of W holds f . (v,w) = 0. F_Complex ;
now__::_thesis:_for_w_being_Vector_of_W_holds_(f_*')_._(v,w)_=_0._F_Complex
let w be Vector of W; ::_thesis: (f *') . (v,w) = 0. F_Complex
(f . (v,w)) *' = 0. F_Complex by A2, COMPLFLD:47;
hence (f *') . (v,w) = 0. F_Complex by Def8; ::_thesis: verum
end;
hence x in leftker (f *') by A1; ::_thesis: verum
end;
thus leftker (f *') c= leftker f ::_thesis: rightker f = rightker (f *')
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (f *') or x in leftker f )
assume x in leftker (f *') ; ::_thesis: x in leftker f
then consider v being Vector of V such that
A3: x = v and
A4: for w being Vector of W holds (f *') . (v,w) = 0. F_Complex ;
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._(v,w)_=_0._F_Complex
let w be Vector of W; ::_thesis: f . (v,w) = 0. F_Complex
((f *') . (v,w)) *' = 0. F_Complex by A4, COMPLFLD:47;
then ((f . (v,w)) *') *' = 0. F_Complex by Def8;
hence f . (v,w) = 0. F_Complex ; ::_thesis: verum
end;
hence x in leftker f by A3; ::_thesis: verum
end;
thus rightker f c= rightker (f *') :: according to XBOOLE_0:def_10 ::_thesis: rightker (f *') c= rightker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker f or x in rightker (f *') )
assume x in rightker f ; ::_thesis: x in rightker (f *')
then consider w being Vector of W such that
A5: x = w and
A6: for v being Vector of V holds f . (v,w) = 0. F_Complex ;
now__::_thesis:_for_v_being_Vector_of_V_holds_(f_*')_._(v,w)_=_0._F_Complex
let v be Vector of V; ::_thesis: (f *') . (v,w) = 0. F_Complex
(f . (v,w)) *' = 0. F_Complex by A6, COMPLFLD:47;
hence (f *') . (v,w) = 0. F_Complex by Def8; ::_thesis: verum
end;
hence x in rightker (f *') by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (f *') or x in rightker f )
assume x in rightker (f *') ; ::_thesis: x in rightker f
then consider w being Vector of W such that
A7: x = w and
A8: for v being Vector of V holds (f *') . (v,w) = 0. F_Complex ;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(v,w)_=_0._F_Complex
let v be Vector of V; ::_thesis: f . (v,w) = 0. F_Complex
((f *') . (v,w)) *' = 0. F_Complex by A8, COMPLFLD:47;
then ((f . (v,w)) *') *' = 0. F_Complex by Def8;
hence f . (v,w) = 0. F_Complex ; ::_thesis: verum
end;
hence x in rightker f by A7; ::_thesis: verum
end;
theorem Th56: :: HERMITAN:56
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds LKer f = RKer (f *')
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V holds LKer f = RKer (f *')
let f be diagReR+0valued hermitan-Form of V; ::_thesis: LKer f = RKer (f *')
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 LKer f = RKer (f *') by VECTSP_4:29; ::_thesis: verum
end;
theorem Th57: :: HERMITAN:57
for V being VectSp of F_Complex
for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V st Re (f . (v,v)) = 0 holds
f . (v,v) = 0. F_Complex
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V st Re (f . (v,v)) = 0 holds
f . (v,v) = 0. F_Complex
let f be diagRvalued diagReR+0valued Form of V,V; ::_thesis: for v being Vector of V st Re (f . (v,v)) = 0 holds
f . (v,v) = 0. F_Complex
let v be Vector of V; ::_thesis: ( Re (f . (v,v)) = 0 implies f . (v,v) = 0. F_Complex )
assume A1: Re (f . (v,v)) = 0 ; ::_thesis: f . (v,v) = 0. F_Complex
Im (f . (v,v)) = 0 by Def6;
then f . (v,v) = 0 + (0 * **) by A1, COMPLEX1:13;
hence f . (v,v) = 0. F_Complex by COMPLFLD:7; ::_thesis: verum
end;
theorem Th58: :: HERMITAN:58
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds
v = 0. V
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds
v = 0. V
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds
v = 0. V
let v be Vector of V; ::_thesis: ( Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) implies v = 0. V )
assume that
A1: Re (f . (v,v)) = 0 and
A2: ( not f is degenerated-on-left or not f is degenerated-on-right ) ; ::_thesis: v = 0. V
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 } ;
percases ( not f is degenerated-on-left or not f is degenerated-on-right ) by A2;
suppose not f is degenerated-on-left ; ::_thesis: v = 0. V
then {(0. V)} = leftker f by BILINEAR:def_23
.= diagker f by Th52 ;
hence v = 0. V by A3, TARSKI:def_1; ::_thesis: verum
end;
suppose not f is degenerated-on-right ; ::_thesis: v = 0. V
then {(0. V)} = rightker f by BILINEAR:def_24
.= diagker f by Th53 ;
hence v = 0. V by A3, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
definition
let V be non empty VectSpStr over F_Complex ;
let 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 :: HERMITAN:def 11
(RQForm (f *')) *' ;
correctness
coherence
(RQForm (f *')) *' is additiveFAF cmplxhomogeneousFAF Form of V,(VectQuot (W,(RKer (f *'))));
;
end;
:: deftheorem defines RQ*Form HERMITAN:def_11_:_
for V being non empty VectSpStr over F_Complex
for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds RQ*Form f = (RQForm (f *')) *' ;
theorem Th59: :: HERMITAN:59
for V being non empty VectSpStr over F_Complex
for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of V
for w being Vector of W holds (RQ*Form f) . (v,(w + (RKer (f *')))) = f . (v,w)
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of V
for w being Vector of W holds (RQ*Form f) . (v,(w + (RKer (f *')))) = f . (v,w)
let W be VectSp of F_Complex ; ::_thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of V
for w being Vector of W holds (RQ*Form f) . (v,(w + (RKer (f *')))) = f . (v,w)
let f be additiveFAF cmplxhomogeneousFAF Form of V,W; ::_thesis: for v being Vector of V
for w being Vector of W holds (RQ*Form f) . (v,(w + (RKer (f *')))) = f . (v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds (RQ*Form f) . (v,(w + (RKer (f *')))) = f . (v,w)
let w be Vector of W; ::_thesis: (RQ*Form f) . (v,(w + (RKer (f *')))) = f . (v,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) ; ::_thesis: verum
end;
registration
let V, W be VectSp of F_Complex ;
let f be sesquilinear-Form of V,W;
cluster LQForm f -> additiveFAF cmplxhomogeneousFAF ;
coherence
( LQForm f is additiveFAF & LQForm f is cmplxhomogeneousFAF )
proof
set lf = LQForm f;
thus LQForm f is additiveFAF ::_thesis: LQForm f is cmplxhomogeneousFAF
proof
let A be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((LQForm f),A) is additive
set flf = FunctionalFAF ((LQForm f),A);
consider v being Vector of V such that
A1: A = v + (LKer f) by VECTSP10:22;
let w, t be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((LQForm f),A)) . (w + t) = ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)
thus (FunctionalFAF ((LQForm f),A)) . (w + t) = (LQForm f) . (A,(w + t)) by BILINEAR:8
.= f . (v,(w + t)) by A1, BILINEAR:def_20
.= (f . (v,w)) + (f . (v,t)) by BILINEAR:27
.= ((LQForm f) . (A,w)) + (f . (v,t)) by A1, BILINEAR:def_20
.= ((LQForm f) . (A,w)) + ((LQForm f) . (A,t)) by A1, BILINEAR:def_20
.= ((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t)) by BILINEAR:8
.= ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t) by BILINEAR:8 ; ::_thesis: verum
end;
let A be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def_4 ::_thesis: FunctionalFAF ((LQForm f),A) is cmplxhomogeneous
set flf = FunctionalFAF ((LQForm f),A);
consider v being Vector of V such that
A2: A = v + (LKer f) by VECTSP10:22;
let w be Vector of W; :: according to HERMITAN:def_1 ::_thesis: for a being Scalar of holds (FunctionalFAF ((LQForm f),A)) . (a * w) = (a *') * ((FunctionalFAF ((LQForm f),A)) . w)
let r be Scalar of ; ::_thesis: (FunctionalFAF ((LQForm f),A)) . (r * w) = (r *') * ((FunctionalFAF ((LQForm f),A)) . w)
thus (FunctionalFAF ((LQForm f),A)) . (r * w) = (LQForm f) . (A,(r * w)) by BILINEAR:8
.= f . (v,(r * w)) by A2, BILINEAR:def_20
.= (r *') * (f . (v,w)) by Th27
.= (r *') * ((LQForm f) . (A,w)) by A2, BILINEAR:def_20
.= (r *') * ((FunctionalFAF ((LQForm f),A)) . w) by BILINEAR:8 ; ::_thesis: verum
end;
cluster RQ*Form f -> additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF ;
coherence
( RQ*Form f is additiveSAF & RQ*Form f is homogeneousSAF )
proof
set lf = RQ*Form f;
thus RQ*Form f is additiveSAF ::_thesis: RQ*Form f is homogeneousSAF
proof
let A be Vector of (VectQuot (W,(RKer (f *')))); :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((RQ*Form f),A) is additive
set flf = FunctionalSAF ((RQ*Form f),A);
consider w being Vector of W such that
A3: A = w + (RKer (f *')) by VECTSP10:22;
let v, t be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF ((RQ*Form f),A)) . (v + t) = ((FunctionalSAF ((RQ*Form f),A)) . v) + ((FunctionalSAF ((RQ*Form f),A)) . t)
thus (FunctionalSAF ((RQ*Form f),A)) . (v + t) = (RQ*Form f) . ((v + t),A) by BILINEAR:9
.= f . ((v + t),w) by A3, Th59
.= (f . (v,w)) + (f . (t,w)) by BILINEAR:26
.= ((RQ*Form f) . (v,A)) + (f . (t,w)) by A3, Th59
.= ((RQ*Form f) . (v,A)) + ((RQ*Form f) . (t,A)) by A3, Th59
.= ((FunctionalSAF ((RQ*Form f),A)) . v) + ((RQ*Form f) . (t,A)) by BILINEAR:9
.= ((FunctionalSAF ((RQ*Form f),A)) . v) + ((FunctionalSAF ((RQ*Form f),A)) . t) by BILINEAR:9 ; ::_thesis: verum
end;
let A be Vector of (VectQuot (W,(RKer (f *')))); :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((RQ*Form f),A) is homogeneous
set flf = FunctionalSAF ((RQ*Form f),A);
consider w being Vector of W such that
A4: A = w + (RKer (f *')) by VECTSP10:22;
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of F_Complex holds (FunctionalSAF ((RQ*Form f),A)) . (b1 * v) = b1 * ((FunctionalSAF ((RQ*Form f),A)) . v)
let r be Scalar of ; ::_thesis: (FunctionalSAF ((RQ*Form f),A)) . (r * v) = r * ((FunctionalSAF ((RQ*Form f),A)) . v)
thus (FunctionalSAF ((RQ*Form f),A)) . (r * v) = (RQ*Form f) . ((r * v),A) by BILINEAR:9
.= f . ((r * v),w) by A4, Th59
.= r * (f . (v,w)) by BILINEAR:31
.= r * ((RQ*Form f) . (v,A)) by A4, Th59
.= r * ((FunctionalSAF ((RQ*Form f),A)) . v) by BILINEAR:9 ; ::_thesis: verum
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: :: HERMITAN:def 12
for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
it . (A,B) = f . (v,w);
existence
ex b1 being sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) st
for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
b1 . (A,B) = f . (v,w)
proof
set K = F_Complex ;
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set Cv = CosetSet (V,(LKer f));
set aCv = addCoset (V,(LKer f));
set mCv = lmultCoset (V,(LKer f));
set R = RKer (f *');
set wq = VectQuot (W,(RKer (f *')));
set Cw = CosetSet (W,(RKer (f *')));
set aCw = addCoset (W,(RKer (f *')));
set mCw = lmultCoset (W,(RKer (f *')));
defpred S1[ set , set , set ] means for v being Vector of V
for w being Vector of W st $1 = v + (LKer f) & $2 = w + (RKer (f *')) holds
$3 = f . (v,w);
A1: rightker f = rightker (f *') by Th55;
A2: now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_B_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_ex_y_being_Element_of_the_carrier_of_F_Complex_st_S1[A,B,y]
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for B being Vector of (VectQuot (W,(RKer (f *')))) ex y being Element of the carrier of F_Complex st S1[A,B,y]
let B be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: ex y being Element of the carrier of F_Complex st S1[A,B,y]
consider a being Vector of V such that
A3: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of W such that
A4: B = b + (RKer (f *')) by VECTSP10:22;
take y = f . (a,b); ::_thesis: S1[A,B,y]
now__::_thesis:_for_a1_being_Vector_of_V
for_b1_being_Vector_of_W_st_A_=_a1_+_(LKer_f)_&_B_=_b1_+_(RKer_(f_*'))_holds_
y_=_f_._(a1,b1)
let a1 be Vector of V; ::_thesis: for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer (f *')) holds
y = f . (a1,b1)
let b1 be Vector of W; ::_thesis: ( A = a1 + (LKer f) & B = b1 + (RKer (f *')) implies y = f . (a1,b1) )
assume A = a1 + (LKer f) ; ::_thesis: ( B = b1 + (RKer (f *')) implies y = f . (a1,b1) )
then a in a1 + (LKer f) by A3, VECTSP_4:44;
then consider vv being Vector of V such that
A5: vv in LKer f and
A6: a = a1 + vv by VECTSP_4:42;
vv in the carrier of (LKer f) by A5, STRUCT_0:def_5;
then vv in leftker f by BILINEAR:def_18;
then A7: ex aa being Vector of V st
( aa = vv & ( for w0 being Vector of W holds f . (aa,w0) = 0. F_Complex ) ) ;
assume B = b1 + (RKer (f *')) ; ::_thesis: y = f . (a1,b1)
then b in b1 + (RKer (f *')) by A4, VECTSP_4:44;
then consider ww being Vector of W such that
A8: ww in RKer (f *') and
A9: b = b1 + ww by VECTSP_4:42;
ww in the carrier of (RKer (f *')) by A8, STRUCT_0:def_5;
then ww in rightker (f *') by BILINEAR:def_19;
then A10: ex bb being Vector of W st
( bb = ww & ( for v0 being Vector of V holds f . (v0,bb) = 0. F_Complex ) ) 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. F_Complex)) + ((f . (vv,b1)) + (f . (vv,ww))) by A10
.= ((f . (a1,b1)) + (0. F_Complex)) + ((0. F_Complex) + (f . (vv,ww))) by A7
.= (f . (a1,b1)) + ((0. F_Complex) + (f . (vv,ww))) by RLVECT_1:def_4
.= (f . (a1,b1)) + (f . (vv,ww)) by RLVECT_1:4
.= (f . (a1,b1)) + (0. F_Complex) by A7
.= f . (a1,b1) by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence S1[A,B,y] ; ::_thesis: verum
end;
consider ff being Function of [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer (f *')))):], the carrier of F_Complex such that
A11: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *')))) holds S1[A,B,ff . (A,B)] from BINOP_1:sch_3(A2);
reconsider ff = ff as Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) ;
A12: CosetSet (V,(LKer f)) = the carrier of (VectQuot (V,(LKer f))) by VECTSP10:def_6;
A13: now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_FunctionalSAF_(ff,ww)_is_homogeneous
let ww be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: FunctionalSAF (ff,ww) is homogeneous
consider w being Vector of W such that
A14: ww = w + (RKer (f *')) by VECTSP10:22;
set ffw = FunctionalSAF (ff,ww);
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_r_being_Element_of_F_Complex_holds_(FunctionalSAF_(ff,ww))_._(r_*_A)_=_r_*_((FunctionalSAF_(ff,ww))_._A)
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for r being Element of F_Complex holds (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)
let r be Element of F_Complex; ::_thesis: (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)
consider a being Vector of V such that
A15: A = a + (LKer f) by VECTSP10:22;
A16: ( the lmult of (VectQuot (V,(LKer f))) = lmultCoset (V,(LKer f)) & (lmultCoset (V,(LKer f))) . (r,A) = (r * a) + (LKer f) ) by A12, A15, VECTSP10:def_5, VECTSP10:def_6;
thus (FunctionalSAF (ff,ww)) . (r * A) = ff . (( the lmult of (VectQuot (V,(LKer f))) . (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 * ((FunctionalSAF (ff,ww)) . A) by BILINEAR:9 ; ::_thesis: verum
end;
hence FunctionalSAF (ff,ww) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;
A17: CosetSet (W,(RKer (f *'))) = the carrier of (VectQuot (W,(RKer (f *')))) by VECTSP10:def_6;
A18: now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_FunctionalFAF_(ff,vv)_is_cmplxhomogeneous
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: FunctionalFAF (ff,vv) is cmplxhomogeneous
consider v being Vector of V such that
A19: vv = v + (LKer f) by VECTSP10:22;
set ffv = FunctionalFAF (ff,vv);
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))
for_r_being_Element_of_F_Complex_holds_(FunctionalFAF_(ff,vv))_._(r_*_A)_=_(r_*')_*_((FunctionalFAF_(ff,vv))_._A)
let A be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: for r being Element of F_Complex holds (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)
let r be Element of F_Complex; ::_thesis: (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)
consider a being Vector of W such that
A20: A = a + (RKer (f *')) by VECTSP10:22;
A21: ( the lmult of (VectQuot (W,(RKer (f *')))) = lmultCoset (W,(RKer (f *'))) & (lmultCoset (W,(RKer (f *')))) . (r,A) = (r * a) + (RKer (f *')) ) by A17, A20, VECTSP10:def_5, VECTSP10:def_6;
thus (FunctionalFAF (ff,vv)) . (r * A) = ff . (vv,( the lmult of (VectQuot (W,(RKer (f *')))) . (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 *') * ((FunctionalFAF (ff,vv)) . A) by BILINEAR:8 ; ::_thesis: verum
end;
hence FunctionalFAF (ff,vv) is cmplxhomogeneous by Def1; ::_thesis: verum
end;
A22: now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_FunctionalSAF_(ff,ww)_is_additive
let ww be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: FunctionalSAF (ff,ww) is additive
consider w being Vector of W such that
A23: ww = w + (RKer (f *')) by VECTSP10:22;
set ffw = FunctionalSAF (ff,ww);
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(FunctionalSAF_(ff,ww))_._(A_+_B)_=_((FunctionalSAF_(ff,ww))_._A)_+_((FunctionalSAF_(ff,ww))_._B)
let A, B be Vector of (VectQuot (V,(LKer f))); ::_thesis: (FunctionalSAF (ff,ww)) . (A + B) = ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B)
consider a being Vector of V such that
A24: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of V such that
A25: B = b + (LKer f) by VECTSP10:22;
A26: ( the addF of (VectQuot (V,(LKer f))) = addCoset (V,(LKer f)) & (addCoset (V,(LKer f))) . (A,B) = (a + b) + (LKer f) ) by A12, A24, A25, VECTSP10:def_3, VECTSP10:def_6;
thus (FunctionalSAF (ff,ww)) . (A + B) = ff . (( the addF of (VectQuot (V,(LKer f))) . (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
.= ((FunctionalSAF (ff,ww)) . A) + (ff . (B,ww)) by BILINEAR:9
.= ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B) by BILINEAR:9 ; ::_thesis: verum
end;
hence FunctionalSAF (ff,ww) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_FunctionalFAF_(ff,vv)_is_additive
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: FunctionalFAF (ff,vv) is additive
consider v being Vector of V such that
A27: vv = v + (LKer f) by VECTSP10:22;
set ffv = FunctionalFAF (ff,vv);
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_(FunctionalFAF_(ff,vv))_._(A_+_B)_=_((FunctionalFAF_(ff,vv))_._A)_+_((FunctionalFAF_(ff,vv))_._B)
let A, B be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: (FunctionalFAF (ff,vv)) . (A + B) = ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B)
consider a being Vector of W such that
A28: A = a + (RKer (f *')) by VECTSP10:22;
consider b being Vector of W such that
A29: B = b + (RKer (f *')) by VECTSP10:22;
A30: ( the addF of (VectQuot (W,(RKer (f *')))) = addCoset (W,(RKer (f *'))) & (addCoset (W,(RKer (f *')))) . (A,B) = (a + b) + (RKer (f *')) ) by A17, A28, A29, VECTSP10:def_3, VECTSP10:def_6;
thus (FunctionalFAF (ff,vv)) . (A + B) = ff . (vv,( the addF of (VectQuot (W,(RKer (f *')))) . (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
.= ((FunctionalFAF (ff,vv)) . A) + (ff . (vv,B)) by BILINEAR:8
.= ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B) by BILINEAR:8 ; ::_thesis: verum
end;
hence FunctionalFAF (ff,vv) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
then reconsider ff = ff as sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) by A22, A13, A18, Def4, BILINEAR:def_11, BILINEAR:def_12, BILINEAR:def_14;
take ff ; ::_thesis: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
ff . (A,B) = f . (v,w)
thus for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
ff . (A,B) = f . (v,w) by A11; ::_thesis: verum
end;
uniqueness
for b1, b2 being sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) st ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
b1 . (A,B) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
b2 . (A,B) = f . (v,w) ) holds
b1 = b2
proof
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set R = RKer (f *');
set wq = VectQuot (W,(RKer (f *')));
let f1, f2 be sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))); ::_thesis: ( ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
f1 . (A,B) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
f2 . (A,B) = f . (v,w) ) implies f1 = f2 )
assume that
A31: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
f1 . (A,B) = f . (v,w) and
A32: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
f2 . (A,B) = f . (v,w) ; ::_thesis: f1 = f2
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_B_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_f1_._(A,B)_=_f2_._(A,B)
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for B being Vector of (VectQuot (W,(RKer (f *')))) holds f1 . (A,B) = f2 . (A,B)
let B be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: f1 . (A,B) = f2 . (A,B)
consider a being Vector of V such that
A33: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of W such that
A34: B = b + (RKer (f *')) by VECTSP10:22;
thus f1 . (A,B) = f . (a,b) by A31, A33, A34
.= f2 . (A,B) by A32, A33, A34 ; ::_thesis: verum
end;
hence f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines Q*Form HERMITAN:def_12_:_
for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W
for b4 being sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) holds
( b4 = Q*Form f iff for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer (f *'))))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds
b4 . (A,B) = f . (v,w) );
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
not Q*Form f is constant
proof
set K = F_Complex ;
consider v being Vector of V, w being Vector of W such that
A1: f . (v,w) <> 0. F_Complex 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 not Q*Form f is constant by A1, BILINEAR:40; ::_thesis: verum
end;
end;
registration
let V be non empty right_zeroed VectSpStr over F_Complex ;
let W be VectSp of F_Complex ;
let f be additiveFAF cmplxhomogeneousFAF Form of V,W;
cluster RQ*Form f -> additiveFAF non degenerated-on-right cmplxhomogeneousFAF ;
coherence
not RQ*Form f is degenerated-on-right
proof
set K = F_Complex ;
set qf = RQ*Form f;
set R = RKer (f *');
set qW = VectQuot (W,(RKer (f *')));
A1: rightker f = rightker (f *') by Th55;
thus rightker (RQ*Form f) c= {(0. (VectQuot (W,(RKer (f *')))))} :: according to XBOOLE_0:def_10,BILINEAR:def_24 ::_thesis: K203( the carrier of (VectQuot (W,(RKer (f *')))),(0. (VectQuot (W,(RKer (f *')))))) c= rightker (RQ*Form f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (RQ*Form f) or x in {(0. (VectQuot (W,(RKer (f *')))))} )
assume x in rightker (RQ*Form f) ; ::_thesis: x in {(0. (VectQuot (W,(RKer (f *')))))}
then consider ww being Vector of (VectQuot (W,(RKer (f *')))) such that
A2: x = ww and
A3: for v being Vector of V holds (RQ*Form f) . (v,ww) = 0. F_Complex ;
consider w being Vector of W such that
A4: ww = w + (RKer (f *')) by VECTSP10:22;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(v,w)_=_0._F_Complex
let v be Vector of V; ::_thesis: f . (v,w) = 0. F_Complex
thus f . (v,w) = (RQ*Form f) . (v,ww) by A4, Th59
.= 0. F_Complex by A3 ; ::_thesis: verum
end;
then w in rightker f ;
then w in the carrier of (RKer (f *')) by A1, BILINEAR:def_19;
then w in RKer (f *') by STRUCT_0:def_5;
then w + (RKer (f *')) = zeroCoset (W,(RKer (f *'))) by VECTSP_4:49
.= 0. (VectQuot (W,(RKer (f *')))) by VECTSP10:21 ;
hence x in {(0. (VectQuot (W,(RKer (f *')))))} by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in K203( the carrier of (VectQuot (W,(RKer (f *')))),(0. (VectQuot (W,(RKer (f *')))))) or x in rightker (RQ*Form f) )
assume x in {(0. (VectQuot (W,(RKer (f *')))))} ; ::_thesis: x in rightker (RQ*Form f)
then A5: x = 0. (VectQuot (W,(RKer (f *')))) by TARSKI:def_1;
for v being Vector of V holds (RQ*Form f) . (v,(0. (VectQuot (W,(RKer (f *')))))) = 0. F_Complex by BILINEAR:29;
hence x in rightker (RQ*Form f) by A5; ::_thesis: verum
end;
end;
theorem Th60: :: HERMITAN:60
for V being non empty VectSpStr over F_Complex
for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)
proof
set K = F_Complex ;
let V be non empty VectSpStr over F_Complex ; ::_thesis: for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)
let W be VectSp of F_Complex ; ::_thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)
let f be additiveFAF cmplxhomogeneousFAF Form of V,W; ::_thesis: leftker f = leftker (RQ*Form f)
set rf = RQ*Form f;
set qw = VectQuot (W,(RKer (f *')));
thus leftker f c= leftker (RQ*Form f) :: according to XBOOLE_0:def_10 ::_thesis: leftker (RQ*Form f) c= leftker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in leftker (RQ*Form f) )
assume x in leftker f ; ::_thesis: x in leftker (RQ*Form f)
then consider v being Vector of V such that
A1: x = v and
A2: for w being Vector of W holds f . (v,w) = 0. F_Complex ;
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_(RQ*Form_f)_._(v,A)_=_0._F_Complex
let A be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: (RQ*Form f) . (v,A) = 0. F_Complex
consider w being Vector of W such that
A3: A = w + (RKer (f *')) by VECTSP10:22;
thus (RQ*Form f) . (v,A) = f . (v,w) by A3, Th59
.= 0. F_Complex by A2 ; ::_thesis: verum
end;
hence x in leftker (RQ*Form f) by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (RQ*Form f) or x in leftker f )
assume x in leftker (RQ*Form f) ; ::_thesis: x in leftker f
then consider v being Vector of V such that
A4: x = v and
A5: for A being Vector of (VectQuot (W,(RKer (f *')))) holds (RQ*Form f) . (v,A) = 0. F_Complex ;
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._(v,w)_=_0._F_Complex
let w be Vector of W; ::_thesis: f . (v,w) = 0. F_Complex
reconsider A = w + (RKer (f *')) as Vector of (VectQuot (W,(RKer (f *')))) by VECTSP10:23;
thus f . (v,w) = (RQ*Form f) . (v,A) by Th59
.= 0. F_Complex by A5 ; ::_thesis: verum
end;
hence x in leftker f by A4; ::_thesis: verum
end;
theorem Th61: :: HERMITAN:61
for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W holds RKer (f *') = RKer ((LQForm f) *')
proof
set K = F_Complex ;
let V, W be VectSp of F_Complex ; ::_thesis: for f being sesquilinear-Form of V,W holds RKer (f *') = RKer ((LQForm f) *')
let f be sesquilinear-Form of V,W; ::_thesis: RKer (f *') = RKer ((LQForm f) *')
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 RKer (f *') = RKer ((LQForm f) *') by VECTSP_4:29; ::_thesis: verum
end;
theorem Th62: :: HERMITAN:62
for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W holds LKer f = LKer (RQ*Form f)
proof
set K = F_Complex ;
let V, W be VectSp of F_Complex ; ::_thesis: for f being sesquilinear-Form of V,W holds LKer f = LKer (RQ*Form f)
let f be sesquilinear-Form of V,W; ::_thesis: LKer f = LKer (RQ*Form f)
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 LKer f = LKer (RQ*Form f) by VECTSP_4:29; ::_thesis: verum
end;
theorem Th63: :: HERMITAN:63
for V, W being VectSp of F_Complex
for f being 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 F_Complex ; ::_thesis: for f being sesquilinear-Form of V,W holds
( Q*Form f = RQ*Form (LQForm f) & Q*Form f = LQForm (RQ*Form f) )
let f be sesquilinear-Form of V,W; ::_thesis: ( Q*Form f = RQ*Form (LQForm f) & Q*Form f = LQForm (RQ*Form f) )
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set R = RKer (f *');
set wq = VectQuot (W,(RKer (f *')));
set RL = RKer ((LQForm f) *');
set wqr = VectQuot (W,(RKer ((LQForm f) *')));
set LR = LKer (RQ*Form f);
set vql = VectQuot (V,(LKer (RQ*Form f)));
A1: dom (Q*Form f) = [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer (f *')))):] by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(Q*Form_f)_holds_
(Q*Form_f)_._x_=_(RQ*Form_(LQForm_f))_._x
A3: RKer (f *') = RKer ((LQForm f) *') by Th61;
let x be set ; ::_thesis: ( x in dom (Q*Form f) implies (Q*Form f) . x = (RQ*Form (LQForm f)) . x )
assume x in dom (Q*Form f) ; ::_thesis: (Q*Form f) . x = (RQ*Form (LQForm f)) . x
then consider A, B being set such that
A4: A in the carrier of (VectQuot (V,(LKer f))) and
A5: B in the carrier of (VectQuot (W,(RKer (f *')))) and
A6: x = [A,B] by ZFMISC_1:def_2;
reconsider A = A as Vector of (VectQuot (V,(LKer f))) by A4;
consider v being Vector of V such that
A7: A = v + (LKer f) by VECTSP10:22;
reconsider B = B as Vector of (VectQuot (W,(RKer (f *')))) by A5;
consider w being Vector of W such that
A8: B = w + (RKer (f *')) 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 ; ::_thesis: verum
end;
( dom (RQ*Form (LQForm f)) = [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer ((LQForm f) *')))):] & the carrier of (VectQuot (W,(RKer ((LQForm f) *')))) = the carrier of (VectQuot (W,(RKer (f *')))) ) by Th61, FUNCT_2:def_1;
hence Q*Form f = RQ*Form (LQForm f) by A1, A2, FUNCT_1:2; ::_thesis: Q*Form f = LQForm (RQ*Form f)
A9: now__::_thesis:_for_x_being_set_st_x_in_dom_(Q*Form_f)_holds_
(Q*Form_f)_._x_=_(LQForm_(RQ*Form_f))_._x
A10: LKer f = LKer (RQ*Form f) by Th62;
let x be set ; ::_thesis: ( x in dom (Q*Form f) implies (Q*Form f) . x = (LQForm (RQ*Form f)) . x )
assume x in dom (Q*Form f) ; ::_thesis: (Q*Form f) . x = (LQForm (RQ*Form f)) . x
then consider A, B being set such that
A11: A in the carrier of (VectQuot (V,(LKer f))) and
A12: B in the carrier of (VectQuot (W,(RKer (f *')))) and
A13: x = [A,B] by ZFMISC_1:def_2;
reconsider A = A as Vector of (VectQuot (V,(LKer f))) by A11;
consider v being Vector of V such that
A14: A = v + (LKer f) by VECTSP10:22;
reconsider B = B as Vector of (VectQuot (W,(RKer (f *')))) by A12;
consider w being Vector of W such that
A15: B = w + (RKer (f *')) 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 ; ::_thesis: verum
end;
( dom (LQForm (RQ*Form f)) = [: the carrier of (VectQuot (V,(LKer (RQ*Form f)))), the carrier of (VectQuot (W,(RKer (f *')))):] & the carrier of (VectQuot (V,(LKer (RQ*Form f)))) = the carrier of (VectQuot (V,(LKer f))) ) by Th62, FUNCT_2:def_1;
hence Q*Form f = LQForm (RQ*Form f) by A1, A9, FUNCT_1:2; ::_thesis: verum
end;
theorem Th64: :: HERMITAN:64
for V, W being VectSp of F_Complex
for f being 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 F_Complex ; ::_thesis: for f being 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)) )
let f be sesquilinear-Form of V,W; ::_thesis: ( 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)) )
set vq = VectQuot (V,(LKer f));
set wq = VectQuot (W,(RKer (f *')));
set wqr = VectQuot (W,(RKer ((LQForm f) *')));
set vql = VectQuot (V,(LKer (RQ*Form f)));
set rlf = RQ*Form (LQForm f);
set qf = Q*Form f;
set lrf = LQForm (RQ*Form f);
thus leftker (Q*Form f) c= leftker (RQ*Form (LQForm f)) :: according to XBOOLE_0:def_10 ::_thesis: ( leftker (RQ*Form (LQForm f)) c= leftker (Q*Form 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
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (Q*Form f) or x in leftker (RQ*Form (LQForm f)) )
assume x in leftker (Q*Form f) ; ::_thesis: x in leftker (RQ*Form (LQForm f))
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A1: x = vv and
A2: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds (Q*Form f) . (vv,ww) = 0. F_Complex ;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_((LQForm_f)_*'))))_holds_(RQ*Form_(LQForm_f))_._(vv,ww)_=_0._F_Complex
let ww be Vector of (VectQuot (W,(RKer ((LQForm f) *')))); ::_thesis: (RQ*Form (LQForm f)) . (vv,ww) = 0. F_Complex
reconsider w = ww as Vector of (VectQuot (W,(RKer (f *')))) by Th61;
thus (RQ*Form (LQForm f)) . (vv,ww) = (Q*Form f) . (vv,w) by Th63
.= 0. F_Complex by A2 ; ::_thesis: verum
end;
hence x in leftker (RQ*Form (LQForm f)) by A1; ::_thesis: verum
end;
thus leftker (RQ*Form (LQForm f)) c= leftker (Q*Form f) ::_thesis: ( 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
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (RQ*Form (LQForm f)) or x in leftker (Q*Form f) )
assume x in leftker (RQ*Form (LQForm f)) ; ::_thesis: x in leftker (Q*Form f)
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A3: x = vv and
A4: for ww being Vector of (VectQuot (W,(RKer ((LQForm f) *')))) holds (RQ*Form (LQForm f)) . (vv,ww) = 0. F_Complex ;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_(Q*Form_f)_._(vv,ww)_=_0._F_Complex
let ww be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: (Q*Form f) . (vv,ww) = 0. F_Complex
reconsider w = ww as Vector of (VectQuot (W,(RKer ((LQForm f) *')))) by Th61;
thus (Q*Form f) . (vv,ww) = (RQ*Form (LQForm f)) . (vv,w) by Th63
.= 0. F_Complex by A4 ; ::_thesis: verum
end;
hence x in leftker (Q*Form f) by A3; ::_thesis: verum
end;
thus rightker (Q*Form f) c= rightker (RQ*Form (LQForm f)) :: according to XBOOLE_0:def_10 ::_thesis: ( rightker (RQ*Form (LQForm f)) c= rightker (Q*Form f) & leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (Q*Form f) or x in rightker (RQ*Form (LQForm f)) )
assume x in rightker (Q*Form f) ; ::_thesis: x in rightker (RQ*Form (LQForm f))
then consider ww being Vector of (VectQuot (W,(RKer (f *')))) such that
A5: x = ww and
A6: for vv being Vector of (VectQuot (V,(LKer f))) holds (Q*Form f) . (vv,ww) = 0. F_Complex ;
reconsider w = ww as Vector of (VectQuot (W,(RKer ((LQForm f) *')))) by Th61;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(RQ*Form_(LQForm_f))_._(vv,w)_=_0._F_Complex
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: (RQ*Form (LQForm f)) . (vv,w) = 0. F_Complex
thus (RQ*Form (LQForm f)) . (vv,w) = (Q*Form f) . (vv,ww) by Th63
.= 0. F_Complex by A6 ; ::_thesis: verum
end;
hence x in rightker (RQ*Form (LQForm f)) by A5; ::_thesis: verum
end;
thus rightker (RQ*Form (LQForm f)) c= rightker (Q*Form f) ::_thesis: ( leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (RQ*Form (LQForm f)) or x in rightker (Q*Form f) )
assume x in rightker (RQ*Form (LQForm f)) ; ::_thesis: x in rightker (Q*Form f)
then consider ww being Vector of (VectQuot (W,(RKer ((LQForm f) *')))) such that
A7: x = ww and
A8: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQ*Form (LQForm f)) . (vv,ww) = 0. F_Complex ;
reconsider w = ww as Vector of (VectQuot (W,(RKer (f *')))) by Th61;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(Q*Form_f)_._(vv,w)_=_0._F_Complex
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: (Q*Form f) . (vv,w) = 0. F_Complex
thus (Q*Form f) . (vv,w) = (RQ*Form (LQForm f)) . (vv,ww) by Th63
.= 0. F_Complex by A8 ; ::_thesis: verum
end;
hence x in rightker (Q*Form f) by A7; ::_thesis: verum
end;
thus leftker (Q*Form f) c= leftker (LQForm (RQ*Form f)) :: according to XBOOLE_0:def_10 ::_thesis: ( leftker (LQForm (RQ*Form f)) c= leftker (Q*Form f) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (Q*Form f) or x in leftker (LQForm (RQ*Form f)) )
assume x in leftker (Q*Form f) ; ::_thesis: x in leftker (LQForm (RQ*Form f))
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A9: x = vv and
A10: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds (Q*Form f) . (vv,ww) = 0. F_Complex ;
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQ*Form f)))) by Th62;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_(LQForm_(RQ*Form_f))_._(v,ww)_=_0._F_Complex
let ww be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: (LQForm (RQ*Form f)) . (v,ww) = 0. F_Complex
thus (LQForm (RQ*Form f)) . (v,ww) = (Q*Form f) . (vv,ww) by Th63
.= 0. F_Complex by A10 ; ::_thesis: verum
end;
hence x in leftker (LQForm (RQ*Form f)) by A9; ::_thesis: verum
end;
thus leftker (LQForm (RQ*Form f)) c= leftker (Q*Form f) ::_thesis: rightker (Q*Form f) = rightker (LQForm (RQ*Form f))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (LQForm (RQ*Form f)) or x in leftker (Q*Form f) )
assume x in leftker (LQForm (RQ*Form f)) ; ::_thesis: x in leftker (Q*Form f)
then consider vv being Vector of (VectQuot (V,(LKer (RQ*Form f)))) such that
A11: x = vv and
A12: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds (LQForm (RQ*Form f)) . (vv,ww) = 0. F_Complex ;
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th62;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_(f_*'))))_holds_(Q*Form_f)_._(v,ww)_=_0._F_Complex
let ww be Vector of (VectQuot (W,(RKer (f *')))); ::_thesis: (Q*Form f) . (v,ww) = 0. F_Complex
thus (Q*Form f) . (v,ww) = (LQForm (RQ*Form f)) . (vv,ww) by Th63
.= 0. F_Complex by A12 ; ::_thesis: verum
end;
hence x in leftker (Q*Form f) by A11; ::_thesis: verum
end;
thus rightker (Q*Form f) c= rightker (LQForm (RQ*Form f)) :: according to XBOOLE_0:def_10 ::_thesis: rightker (LQForm (RQ*Form f)) c= rightker (Q*Form f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (Q*Form f) or x in rightker (LQForm (RQ*Form f)) )
assume x in rightker (Q*Form f) ; ::_thesis: x in rightker (LQForm (RQ*Form f))
then consider ww being Vector of (VectQuot (W,(RKer (f *')))) such that
A13: x = ww and
A14: for vv being Vector of (VectQuot (V,(LKer f))) holds (Q*Form f) . (vv,ww) = 0. F_Complex ;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_(RQ*Form_f))))_holds_(LQForm_(RQ*Form_f))_._(vv,ww)_=_0._F_Complex
let vv be Vector of (VectQuot (V,(LKer (RQ*Form f)))); ::_thesis: (LQForm (RQ*Form f)) . (vv,ww) = 0. F_Complex
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th62;
thus (LQForm (RQ*Form f)) . (vv,ww) = (Q*Form f) . (v,ww) by Th63
.= 0. F_Complex by A14 ; ::_thesis: verum
end;
hence x in rightker (LQForm (RQ*Form f)) by A13; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (LQForm (RQ*Form f)) or x in rightker (Q*Form f) )
assume x in rightker (LQForm (RQ*Form f)) ; ::_thesis: x in rightker (Q*Form f)
then consider ww being Vector of (VectQuot (W,(RKer (f *')))) such that
A15: x = ww and
A16: for vv being Vector of (VectQuot (V,(LKer (RQ*Form f)))) holds (LQForm (RQ*Form f)) . (vv,ww) = 0. F_Complex ;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(Q*Form_f)_._(vv,ww)_=_0._F_Complex
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: (Q*Form f) . (vv,ww) = 0. F_Complex
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQ*Form f)))) by Th62;
thus (Q*Form f) . (vv,ww) = (LQForm (RQ*Form f)) . (v,ww) by Th63
.= 0. F_Complex by A16 ; ::_thesis: verum
end;
hence x in rightker (Q*Form f) by A15; ::_thesis: verum
end;
registration
let V, W be VectSp of F_Complex ;
let f be sesquilinear-Form of V,W;
cluster RQ*Form (LQForm f) -> additiveFAF non degenerated-on-left non degenerated-on-right cmplxhomogeneousFAF ;
coherence
( not RQ*Form (LQForm f) is degenerated-on-left & not RQ*Form (LQForm f) is degenerated-on-right )
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 ( not RQ*Form (LQForm f) is degenerated-on-left & not RQ*Form (LQForm f) is degenerated-on-right ) by BILINEAR:def_23; ::_thesis: verum
end;
cluster LQForm (RQ*Form f) -> non degenerated-on-left non degenerated-on-right ;
coherence
( not LQForm (RQ*Form f) is degenerated-on-left & not LQForm (RQ*Form f) is degenerated-on-right )
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 ( not LQForm (RQ*Form f) is degenerated-on-left & not LQForm (RQ*Form f) is degenerated-on-right ) by BILINEAR:def_24; ::_thesis: verum
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
( not Q*Form f is degenerated-on-left & not Q*Form f is degenerated-on-right )
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, BILINEAR:def_24;
( leftker (RQ*Form (LQForm f)) = leftker (Q*Form f) & rightker (LQForm (RQ*Form f)) = rightker (Q*Form f) ) by Th64;
hence ( not Q*Form f is degenerated-on-left & not Q*Form f is degenerated-on-right ) by A1, BILINEAR:def_23, BILINEAR:def_24; ::_thesis: verum
end;
end;
begin
definition
let V be non empty VectSpStr over F_Complex ;
let f be Form of V,V;
attrf is positivediagvalued means :Def13: :: HERMITAN:def 13
for v being Vector of V st v <> 0. V holds
0 < Re (f . (v,v));
end;
:: deftheorem Def13 defines positivediagvalued HERMITAN:def_13_:_
for V being non empty VectSpStr over F_Complex
for f being Form of V,V holds
( f is positivediagvalued iff for v being Vector of V st v <> 0. V holds
0 < Re (f . (v,v)) );
registration
let V be non empty right_zeroed VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveSAF positivediagvalued -> diagReR+0valued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is positivediagvalued & b1 is additiveSAF holds
b1 is diagReR+0valued
proof
let f be Form of V,V; ::_thesis: ( f is positivediagvalued & f is additiveSAF implies f is diagReR+0valued )
assume A1: ( f is positivediagvalued & f is additiveSAF ) ; ::_thesis: f is diagReR+0valued
let v be Vector of V; :: according to HERMITAN:def_7 ::_thesis: 0 <= Re (f . (v,v))
percases ( v = 0. V or v <> 0. V ) ;
supposeA2: v = 0. V ; ::_thesis: 0 <= Re (f . (v,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 0 <= Re (f . (v,v)) by A3, COMPLEX1:77; ::_thesis: verum
end;
suppose v <> 0. V ; ::_thesis: 0 <= Re (f . (v,v))
hence 0 <= Re (f . (v,v)) by A1, Def13; ::_thesis: verum
end;
end;
end;
end;
registration
let V be non empty right_zeroed VectSpStr over F_Complex ;
cluster Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveFAF positivediagvalued -> diagReR+0valued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];
coherence
for b1 being Form of V,V st b1 is positivediagvalued & b1 is additiveFAF holds
b1 is diagReR+0valued
proof
let f be Form of V,V; ::_thesis: ( f is positivediagvalued & f is additiveFAF implies f is diagReR+0valued )
assume A1: ( f is positivediagvalued & f is additiveFAF ) ; ::_thesis: f is diagReR+0valued
let v be Vector of V; :: according to HERMITAN:def_7 ::_thesis: 0 <= Re (f . (v,v))
percases ( v = 0. V or v <> 0. V ) ;
supposeA2: v = 0. V ; ::_thesis: 0 <= Re (f . (v,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 0 <= Re (f . (v,v)) by A3, COMPLEX1:77; ::_thesis: verum
end;
suppose v <> 0. V ; ::_thesis: 0 <= Re (f . (v,v))
hence 0 <= Re (f . (v,v)) by A1, Def13; ::_thesis: verum
end;
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 :: HERMITAN:def 14
Q*Form f;
coherence
Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f)))
proof
set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
VectQuot (V,(RKer (f *'))) = VectQuot (V,(LKer f)) by Th56;
then reconsider sc = Q*Form f as Form of (VectQuot (V,(LKer f))),(VectQuot (V,(LKer f))) ;
A1: sc is homogeneousSAF
proof
let w be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF (sc,w) is homogeneous
set fg = FunctionalSAF (sc,w);
let v be Vector of (VectQuot (V,(LKer f))); :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of F_Complex holds (FunctionalSAF (sc,w)) . (b1 * v) = b1 * ((FunctionalSAF (sc,w)) . v)
let r be Scalar of ; ::_thesis: (FunctionalSAF (sc,w)) . (r * v) = r * ((FunctionalSAF (sc,w)) . v)
consider va being 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 (VectQuot (V,(RKer (f *')))) by Th56;
consider wa being Vector of V such that
A4: A = wa + (RKer (f *')) by VECTSP10:22;
thus (FunctionalSAF (sc,w)) . (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 * ((FunctionalSAF (sc,w)) . v) by BILINEAR:9 ; ::_thesis: verum
end;
A5: sc is additiveSAF
proof
let w be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF (sc,w) is additive
set fg = FunctionalSAF (sc,w);
let v1, v2 be Vector of (VectQuot (V,(LKer f))); :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF (sc,w)) . (v1 + v2) = ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2)
consider va being Vector of V such that
A6: v1 = va + (LKer f) by VECTSP10:22;
consider vb being Vector of V such that
A7: v2 = vb + (LKer f) by VECTSP10:22;
reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
consider wa being 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 (FunctionalSAF (sc,w)) . (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
.= ((FunctionalSAF (sc,w)) . v1) + (sc . (v2,w)) by BILINEAR:9
.= ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2) by BILINEAR:9 ; ::_thesis: verum
end;
A10: sc is hermitan
proof
let v, w be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def_5 ::_thesis: sc . (v,w) = (sc . (w,v)) *'
reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
consider wa being 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 (VectQuot (V,(RKer (f *')))) by Th56;
consider va being 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 ; ::_thesis: verum
end;
sc is diagReR+0valued
proof
let v be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def_7 ::_thesis: 0 <= Re (sc . (v,v))
reconsider A = v as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
consider va being 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 0 <= Re (sc . (v,v)) by Def7; ::_thesis: verum
end;
hence Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f))) by A1, A5, A10; ::_thesis: verum
end;
end;
:: deftheorem defines ScalarForm HERMITAN:def_14_:_
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds ScalarForm f = Q*Form f;
theorem :: HERMITAN:65
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for A, B being Vector of (VectQuot (V,(LKer f)))
for v, w being 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 ; ::_thesis: for f being diagReR+0valued hermitan-Form of V
for A, B being Vector of (VectQuot (V,(LKer f)))
for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
let f be diagReR+0valued hermitan-Form of V; ::_thesis: for A, B being Vector of (VectQuot (V,(LKer f)))
for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
let A, B be Vector of (VectQuot (V,(LKer f))); ::_thesis: for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
let v, w be Vector of V; ::_thesis: ( A = v + (LKer f) & B = w + (LKer f) implies (ScalarForm f) . (A,B) = f . (v,w) )
reconsider W = B as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
assume that
A1: A = v + (LKer f) and
A2: B = w + (LKer f) ; ::_thesis: (ScalarForm f) . (A,B) = f . (v,w)
W = w + (RKer (f *')) by A2, Th56;
hence (ScalarForm f) . (A,B) = f . (v,w) by A1, Def12; ::_thesis: verum
end;
theorem Th66: :: HERMITAN:66
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds leftker (ScalarForm f) = leftker (Q*Form f)
proof
let V be VectSp of F_Complex ; ::_thesis: for f being diagReR+0valued hermitan-Form of V holds leftker (ScalarForm f) = leftker (Q*Form f)
let f be diagReR+0valued hermitan-Form of V; ::_thesis: leftker (ScalarForm f) = leftker (Q*Form f)
set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
set qf = Q*Form f;
set qhf = ScalarForm f;
set K = F_Complex ;
thus leftker (ScalarForm f) c= leftker (Q*Form f) :: according to XBOOLE_0:def_10 ::_thesis: leftker (Q*Form f) c= leftker (ScalarForm f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (ScalarForm f) or x in leftker (Q*Form f) )
assume x in leftker (ScalarForm f) ; ::_thesis: x in leftker (Q*Form f)
then consider A being Vector of (VectQuot (V,(LKer f))) such that
A1: x = A and
A2: for B being Vector of (VectQuot (V,(LKer f))) holds (ScalarForm f) . (A,B) = 0. F_Complex ;
now__::_thesis:_for_B_being_Vector_of_(VectQuot_(V,(RKer_(f_*'))))_holds_(Q*Form_f)_._(A,B)_=_0._F_Complex
let B be Vector of (VectQuot (V,(RKer (f *')))); ::_thesis: (Q*Form f) . (A,B) = 0. F_Complex
reconsider w = B as Vector of (VectQuot (V,(LKer f))) by Th56;
thus (Q*Form f) . (A,B) = (ScalarForm f) . (A,w)
.= 0. F_Complex by A2 ; ::_thesis: verum
end;
hence x in leftker (Q*Form f) by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (Q*Form f) or x in leftker (ScalarForm f) )
assume x in leftker (Q*Form f) ; ::_thesis: x in leftker (ScalarForm f)
then consider A being Vector of (VectQuot (V,(LKer f))) such that
A3: x = A and
A4: for B being Vector of (VectQuot (V,(RKer (f *')))) holds (Q*Form f) . (A,B) = 0. F_Complex ;
now__::_thesis:_for_B_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(ScalarForm_f)_._(A,B)_=_0._F_Complex
let B be Vector of (VectQuot (V,(LKer f))); ::_thesis: (ScalarForm f) . (A,B) = 0. F_Complex
reconsider w = B as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
thus (ScalarForm f) . (A,B) = (Q*Form f) . (A,w)
.= 0. F_Complex by A4 ; ::_thesis: verum
end;
hence x in leftker (ScalarForm f) by A3; ::_thesis: verum
end;
theorem :: HERMITAN:67
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds rightker (ScalarForm f) = rightker (Q*Form f) by Th56;
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 diagReR+0valued positivediagvalued ;
coherence
( not ScalarForm f is degenerated-on-left & not ScalarForm f is degenerated-on-right & ScalarForm f is positivediagvalued )
proof
set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
set qh = ScalarForm f;
A1: leftker (ScalarForm f) = leftker (Q*Form f) by Th66
.= {(0. (VectQuot (V,(LKer f))))} by BILINEAR:def_23 ;
rightker (ScalarForm f) = rightker (Q*Form f) by Th56
.= {(0. (VectQuot (V,(RKer (f *')))))} by BILINEAR:def_24
.= {(0. (VectQuot (V,(LKer f))))} by Th56 ;
hence A2: ( not ScalarForm f is degenerated-on-left & not ScalarForm f is degenerated-on-right ) by A1, BILINEAR:def_23, BILINEAR:def_24; ::_thesis: ScalarForm f is positivediagvalued
let A be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def_13 ::_thesis: ( A <> 0. (VectQuot (V,(LKer f))) implies 0 < Re ((ScalarForm f) . (A,A)) )
assume A <> 0. (VectQuot (V,(LKer f))) ; ::_thesis: 0 < Re ((ScalarForm f) . (A,A))
then Re ((ScalarForm f) . (A,A)) <> 0 by A2, Th58;
hence 0 < Re ((ScalarForm f) . (A,A)) by Def7; ::_thesis: verum
end;
end;
registration
let V be non trivial VectSp of F_Complex ;
let f be non constant diagReR+0valued hermitan-Form of V;
cluster ScalarForm f -> non constant diagReR+0valued ;
coherence
not ScalarForm f is constant ;
end;
*