:: HERMITAN semantic presentation

begin

Lm1:  0 = 0 + (0 * <i>)
;

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.|) * <i>)).| = 1 & Re ((((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)) * a) = |.a.| & Im ((((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)) * a) = 0 )
proof
let z be Element of COMPLEX ; ::_thesis: ( z <> 0c implies ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0 ) )
set r = |.z.|;
set a = ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>);
assume  z <> 0c ; ::_thesis: ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * 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.|) * <i>)) = (Re z) / |.z.| & Im (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) = (- (Im z)) / |.z.| ) by COMPLEX1:12;
then ((Re (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>))) ^2) + ((Im (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>))) ^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.|) * <i>)).| = 1 by SQUARE_1:18; ::_thesis: ( Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0 )
thus  Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * 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.|) * <i>)) * z) = 0
thus  Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * 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.|) * <i>) ; ::_thesis: ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0 )
thus  ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * 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 * <i>)
proof
let z be Element of COMPLEX ; ::_thesis: z * (z *') = (|.z.| ^2) + (0 * <i>)
 ( 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 * <i>) 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.|) * <i>);
A1: [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z = (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * 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)) * <i>) 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 * <i>) 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 * <i>) & (FormFunctional (f,(f *'))) . (v,v) = (Re ((FormFunctional (f,(f *'))) . (v,v))) + ((Im ((FormFunctional (f,(f *'))) . (v,v))) * <i>) ) 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))) * <i>) ) 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 * <i>) 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;