The abstract of the Mizar article:

Hermitan Functionals. Canonical Construction of Scalar Product in Quotient Vector Space

by

Jaroslaw Kotowicz

Received November 12, 2002

MML identifier: HERMITAN

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, VECTSP_1, ARYTM_1, HAHNBAN, FUNCT_1, GRCAT_1, UNIALG_1,
      RELAT_1, HAHNBAN1, RLSUB_1, REALSET1, SEQM_3, GROUP_6, VECTSP10,
      BILINEAR, HERMITAN, COMPLEX1, ABSVALUE, ARYTM_3, SQUARE_1, COMPLFLD,
      ARYTM, XCMPLX_0;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0,
      XCMPLX_0, XREAL_0, REAL_1, STRUCT_0, DOMAIN_1, FUNCT_1, ABSVALUE,
      REALSET1, RLVECT_1, BINOP_1, VECTSP_1, RELSET_1, FUNCT_2, SQUARE_1,
      COMPLEX1, SEQM_3, VECTSP_4, COMPLFLD, HAHNBAN1, VECTSP10, BILINEAR;
 constructors REAL_1, DOMAIN_1, SQUARE_1, BINOP_1, MONOID_0, BILINEAR,
      COMPLEX1, MEMBERED, ARYTM_0;
 clusters STRUCT_0, XREAL_0, SUBSET_1, RELSET_1, SQUARE_1, COMPLFLD, HAHNBAN1,
      VECTSP10, BILINEAR, COMPLEX1, MEMBERED, NUMBERS;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;


begin
::Auxiliary Facts about Complex Numbers

theorem :: HERMITAN:1
for a be Element of COMPLEX st a = a*' holds Im a = 0;

theorem :: HERMITAN:2
for a be Element of COMPLEX st a <> 0c holds
 |.[*(Re a)/|.a.|, (-Im a)/|.a.|*].| = 1 &
 Re ([*(Re a)/|.a.|, (-Im a)/|.a.|*] * a) = |.a.| &
 Im ([*(Re a)/|.a.|, (-Im a)/|.a.|*] * a)= 0;

theorem :: HERMITAN:3
  for a be Element of COMPLEX ex b be Element of COMPLEX st
  |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a)= 0;

theorem :: HERMITAN:4
for a be Element of COMPLEX holds a*a*' = [*|.a.|^2,0*];

theorem :: HERMITAN:5
for a be Element of F_Complex st a = a*' holds Im a = 0;

theorem :: HERMITAN:6
i_FC*' = <i>";

theorem :: HERMITAN:7
i_FC * i_FC*' = 1_ F_Complex;

theorem :: HERMITAN:8
for a be Element of F_Complex st a <> 0.F_Complex holds
 |.[**(Re a)/|.a.|, (-Im a)/|.a.|**].| = 1 &
 Re ([**(Re a)/|.a.|, (-Im a)/|.a.|**] * a) = |.a.| &
 Im ([**(Re a)/|.a.|, (-Im a)/|.a.|**] * a)= 0;

theorem :: HERMITAN:9
for a be Element of F_Complex
 ex b be Element of F_Complex st
  |.b.| =1 & Re (b * a) = |.a.| & Im (b * a)= 0;

theorem :: HERMITAN:10
for a,b be Element of F_Complex holds
  Re (a - b) = Re a - Re b & Im (a - b) = Im a - Im b;

theorem :: HERMITAN:11
for a,b be Element of F_Complex st Im a = 0 holds
  Re (a*b) = Re a * Re b & Im (a*b) = Re a * Im b;

theorem :: HERMITAN:12
  for a,b be Element of F_Complex
 st Im a = 0 & Im b = 0 holds Im (a*b) = 0;

theorem :: HERMITAN:13
for a be Element of F_Complex holds Re a = Re (a*');

theorem :: HERMITAN:14
for a be Element of F_Complex st Im a = 0 holds a = a*';

theorem :: HERMITAN:15
for r,s be Real holds [**r,0**]*[**s,0**] =[**r*s,0**];

theorem :: HERMITAN:16
for a be Element of F_Complex holds a*a*' = [**|.a.|^2,0**];

theorem :: HERMITAN:17
for a be Element of F_Complex st 0 <= Re a & Im a = 0
 holds |.a.| = Re a;

theorem :: HERMITAN:18
for a be Element of F_Complex holds Re a + Re (a*') = 2 * Re a;

begin
::Antilinear Functionals in Complex Vector Spaces

definition
 let V be non empty VectSpStr over F_Complex;
 let f be Functional of V;
attr f is cmplxhomogeneous means
:: HERMITAN:def 1
   for v be Vector of V, a be Scalar of V holds f.(a*v) = (a*')*f.v;
end;

definition
  let V be non empty VectSpStr over F_Complex;
cluster 0Functional(V) -> cmplxhomogeneous;
end;

definition
 let V be add-associative right_zeroed right_complementable VectSp-like
           (non empty VectSpStr over F_Complex);
cluster cmplxhomogeneous -> 0-preserving Functional of V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster additive cmplxhomogeneous 0-preserving Functional of V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
mode antilinear-Functional of V is additive cmplxhomogeneous Functional of V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f,g be cmplxhomogeneous Functional of V;
cluster f+g -> cmplxhomogeneous;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f be cmplxhomogeneous Functional of V;
cluster -f -> cmplxhomogeneous;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let a be Scalar of V;
 let f be cmplxhomogeneous Functional of V;
cluster a*f -> cmplxhomogeneous;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f,g be cmplxhomogeneous Functional of V;
cluster f-g -> cmplxhomogeneous;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f be Functional of V;
func f*' -> Functional of V means
:: HERMITAN:def 2
 for v be Vector of V holds it.v = (f.v)*';
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f be additive Functional of V;
cluster f*' -> additive;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f be homogeneous Functional of V;
cluster f*' -> cmplxhomogeneous;
end;

definition
 let V be non empty VectSpStr over F_Complex;
 let f be cmplxhomogeneous Functional of V;
cluster f*' -> homogeneous;
end;

definition
 let V be non trivial VectSp of F_Complex;
 let f be non constant Functional of V;
cluster f*' -> non constant;
end;

definition
 let V be non trivial VectSp of F_Complex;
cluster additive cmplxhomogeneous non constant non trivial Functional of V;
end;

theorem :: HERMITAN:19
  for V be non empty VectSpStr over F_Complex, f be Functional of V holds
(f*')*'=f;

theorem :: HERMITAN:20
  for V be non empty VectSpStr over F_Complex holds
(0Functional(V))*' = 0Functional(V);

theorem :: HERMITAN:21
for V be non empty VectSpStr over F_Complex, f,g be Functional of V holds
(f+g)*'=f*'+ g*';

theorem :: HERMITAN:22
for V be non empty VectSpStr over F_Complex, f be Functional of V holds
(-f)*'=-(f*');

theorem :: HERMITAN:23
  for V be non empty VectSpStr over F_Complex
 for f be Functional of V, a be Scalar of V holds (a*f)*' = a*' * (f*');

theorem :: HERMITAN:24
  for V be non empty VectSpStr over F_Complex, f,g be Functional of V holds
(f-g)*'=f*'- g*';

theorem :: HERMITAN:25
for V be non empty VectSpStr over F_Complex, f be Functional of V
for v be Vector of V holds f.v = 0.F_Complex iff f*'.v = 0.F_Complex;

theorem :: HERMITAN:26
for V be non empty VectSpStr over F_Complex, f be Functional of V holds
 ker f = ker f*';

theorem :: HERMITAN:27
  for V be add-associative right_zeroed right_complementable
         VectSp-like (non empty VectSpStr over F_Complex)
for f be antilinear-Functional of V holds ker f is lineary-closed;

theorem :: HERMITAN:28
for V be VectSp of F_Complex, W be Subspace of V
for f be antilinear-Functional of V st the carrier of W c= ker f*'
 holds QFunctional(f,W) is cmplxhomogeneous;

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*'));
end;

theorem :: HERMITAN:29
for V be VectSp of F_Complex, f be antilinear-Functional of V
for A be Vector of VectQuot(V,Ker (f*')), v be Vector of V
 st A = v+Ker (f*') holds (QcFunctional(f)).A = f.v;

definition
 let V be non trivial VectSp of F_Complex;
 let f be non constant antilinear-Functional of V;
cluster QcFunctional(f) -> non constant;
end;

definition
 let V be VectSp of F_Complex;
 let f be antilinear-Functional of V;
cluster QcFunctional(f) -> non degenerated;
end;

begin
::Sesquilinear Forms in Complex Vector Spaces

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be Form of V,W;
attr f is cmplxhomogeneousFAF means
:: HERMITAN:def 4
   for v be Vector of V holds FunctionalFAF(f,v) is cmplxhomogeneous;
end;

theorem :: HERMITAN:30
for V,W be non empty VectSpStr over F_Complex
for v be Vector of V,w be Vector of W, a be Element of F_Complex
for f be Form of V,W st f is cmplxhomogeneousFAF holds
 f.[v,a*w] = (a*')*f.[v,w];

definition
 let V be non empty VectSpStr over F_Complex;
 let f be Form of V,V;
attr f is hermitan means
:: HERMITAN:def 5
  for v,u be Vector of V holds f.[v,u] = (f.[u,v])*';
attr f is diagRvalued means
:: HERMITAN:def 6
  for v be Vector of V holds Im (f.[v,v]) = 0;
attr f is diagReR+0valued means
:: HERMITAN:def 7
    for v be Vector of V holds 0 <= Re (f.[v,v]);
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
cluster NulForm(V,W) -> cmplxhomogeneousFAF;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster NulForm(V,V) -> hermitan;
cluster NulForm(V,V) -> diagReR+0valued;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster hermitan -> diagRvalued Form of V,V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster diagReR+0valued hermitan diagRvalued additiveSAF homogeneousSAF
          additiveFAF cmplxhomogeneousFAF Form of V,V;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF Form of V,W;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
mode sesquilinear-Form of V,W is
 additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF Form of V,W;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster hermitan additiveFAF -> additiveSAF Form of V,V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster hermitan additiveSAF -> additiveFAF Form of V,V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster hermitan homogeneousSAF -> cmplxhomogeneousFAF Form of V,V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
cluster hermitan cmplxhomogeneousFAF -> homogeneousSAF Form of V,V;
end;

definition
 let V be non empty VectSpStr over F_Complex;
mode hermitan-Form of V is hermitan additiveSAF homogeneousSAF Form of V,V;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be Functional of V, g be cmplxhomogeneous Functional of W;
cluster FormFunctional(f,g) -> cmplxhomogeneousFAF;
end;

definition
 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;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f,g be cmplxhomogeneousFAF Form of V,W;
cluster f+g -> cmplxhomogeneousFAF;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be cmplxhomogeneousFAF Form of V,W;
 let a be Scalar of V;
cluster a*f -> cmplxhomogeneousFAF;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be cmplxhomogeneousFAF Form of V,W;
cluster -f -> cmplxhomogeneousFAF;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f,g be cmplxhomogeneousFAF Form of V,W;
cluster f-g -> cmplxhomogeneousFAF;
end;

definition
 let V,W be non trivial VectSp of F_Complex;
cluster additiveSAF homogeneousSAF additiveFAF cmplxhomogeneousFAF
          non constant non trivial Form of V,W;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be Form of V,W;
func f*' -> Form of V,W means
:: HERMITAN:def 8
 for v be Vector of V, w be Vector of W holds it.[v,w] = (f.[v,w])*';
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be additiveFAF Form of V,W;
cluster f*' -> additiveFAF;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be additiveSAF Form of V,W;
cluster f*' -> additiveSAF;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be homogeneousFAF Form of V,W;
cluster f*' -> cmplxhomogeneousFAF;
end;

definition
 let V,W be non empty VectSpStr over F_Complex;
 let f be cmplxhomogeneousFAF Form of V,W;
cluster f*' -> homogeneousFAF;
end;

definition
 let V,W be non trivial VectSp of F_Complex;
 let f be non constant Form of V,W;
cluster f*' -> non constant;
end;

theorem :: HERMITAN:31
for V be non empty VectSpStr over F_Complex, f be Functional of V,
v be Vector of V
holds (FormFunctional(f,f*')).[v,v] = [**|. f.v .|^2, 0 **];

definition
 let V be non empty VectSpStr over F_Complex;
 let f be Functional of V;
cluster FormFunctional(f,f*') -> diagReR+0valued hermitan diagRvalued;
end;

definition
 let V be non trivial VectSp of F_Complex;
cluster diagReR+0valued hermitan diagRvalued additiveSAF homogeneousSAF
          additiveFAF cmplxhomogeneousFAF non constant non trivial Form of V,V;
end;

theorem :: HERMITAN:32
  for V,W be non empty VectSpStr over F_Complex, f be Form of V,W
holds (f*')*' = f;

theorem :: HERMITAN:33
  for V,W be non empty VectSpStr over F_Complex holds
(NulForm(V,W))*' = NulForm(V,W);

theorem :: HERMITAN:34
for V,W be non empty VectSpStr over F_Complex, f,g be Form of V,W holds
(f+g)*'=f*'+ g*';

theorem :: HERMITAN:35
for V,W be non empty VectSpStr over F_Complex, f be Form of V,W holds
(-f)*'=-(f*');

theorem :: HERMITAN:36
  for V,W be non empty VectSpStr over F_Complex
 for f be Form of V,W, a be Element of F_Complex holds (a*f)*' = a*' * (f*');

theorem :: HERMITAN:37
  for V,W be non empty VectSpStr over F_Complex, f,g be Form of V,W holds
(f-g)*'=f*'- g*';

theorem :: HERMITAN:38
for V,W be VectSp of F_Complex, v be Vector of V, w,t be Vector of W
for f be additiveFAF cmplxhomogeneousFAF Form of V,W holds
 f.[v,w-t] = f.[v,w] - f.[v,t];

theorem :: HERMITAN:39
for V,W be VectSp of F_Complex, v,u be Vector of V, w,t be Vector of W
for f be sesquilinear-Form of V,W holds
 f.[v-u,w-t] = f.[v,w] - f.[v,t] -(f.[u,w] - f.[u,t]);

theorem :: HERMITAN:40
for V,W be add-associative right_zeroed right_complementable
             VectSp-like (non empty VectSpStr over F_Complex)
for v,u be Vector of V, w,t be Vector of W
for a,b be Element of F_Complex
 for f be sesquilinear-Form of V,W holds
   f.[v+a*u,w+b*t] = f.[v,w] + b*' * f.[v,t] + (a*f.[u,w] + a*(b*' *f.[u,t]));

theorem :: HERMITAN:41
for V,W be VectSp of F_Complex, v,u be Vector of V, w,t be Vector of W
for a,b be Element of F_Complex
 for f be sesquilinear-Form of V,W holds
   f.[v-a*u,w-b*t] = f.[v,w] - b*'*f.[v,t] - (a*f.[u,w] - a*(b*'*f.[u,t]));

theorem :: HERMITAN:42
for V be add-associative right_zeroed right_complementable
             VectSp-like (non empty VectSpStr over F_Complex)
for f be cmplxhomogeneousFAF Form of V,V
 for v be Vector of V holds f.[v,0.V] = 0.F_Complex;

theorem :: HERMITAN:43
:: Polarization Formulae
  for V be VectSp of F_Complex, v,w be Vector of V, f be hermitan-Form of V
 holds
  f.[v,w] + f.[v,w] + f.[v,w] + f.[v,w]
   = f.[v+w,v+w] - f.[v-w,v-w]
    +i_FC *f.[v+i_FC*w,v+i_FC*w] -i_FC *f.[v-i_FC*w,v-i_FC*w];

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]);
end;

theorem :: HERMITAN:44
for V be add-associative right_zeroed right_complementable
         VectSp-like (non empty VectSpStr over F_Complex)
for f be diagReR+0valued diagRvalued Form of V,V
for v be Vector of V holds
   |. f.[v,v] .| = Re (f.[v,v]) & signnorm (f,v) = |. f.[v,v] .|;

::
:: Lemmas for Schwarz inequality
::

theorem :: HERMITAN:45
for V be VectSp of F_Complex, v,w be Vector of V
for f be sesquilinear-Form of V,V, r be Real,
a be Element of F_Complex st
|.a.| =1 & Re (a * f.[w,v]) = |.f.[w,v].| & Im (a * f.[w,v])= 0
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];

theorem :: HERMITAN:46
for V be VectSp of F_Complex, v,w be Vector of V
for f be diagReR+0valued hermitan-Form of V, r be Real,
a be Element of F_Complex st
|.a.| =1 & Re (a * f.[w,v]) = |.f.[w,v].| & Im (a * f.[w,v])= 0
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;

theorem :: HERMITAN:47
for V be VectSp of F_Complex, v,w be Vector of V
for f be diagReR+0valued hermitan-Form of V
st signnorm(f,w)= 0 holds |.f.[w,v].| = 0;

theorem :: HERMITAN:48
:: Schwarz inequality
for V be VectSp of F_Complex, v,w be Vector of V
for f be diagReR+0valued hermitan-Form of V
holds |. f.[v,w] .|^2 <= signnorm(f,v) * signnorm(f,w);

theorem :: HERMITAN:49
:: Schwarz inequality - second version
for V be VectSp of F_Complex
for f be diagReR+0valued hermitan-Form of V
 for v,w be Vector of V holds |. f.[v,w] .|^2 <= |. f.[v,v].| * |. f.[w,w] .|;

theorem :: HERMITAN:50
::Minkowski inequality
for V be VectSp of F_Complex
for f be diagReR+0valued hermitan-Form of V
 for v,w be Vector of V holds
 signnorm(f,v+w) <= (sqrt(signnorm(f,v)) + sqrt(signnorm(f,w)))^2;

theorem :: HERMITAN:51
::Minkowski inequality - second version
  for V be VectSp of F_Complex
for f be diagReR+0valued hermitan-Form of V
 for v,w be Vector of V holds
 |. f.[v+w,v+w] .| <= (sqrt(|. f.[v,v] .|) + sqrt(|. f.[w,w] .|))^2;

theorem :: HERMITAN:52
:: Parallerogram equality
for V be VectSp of F_Complex
for f be hermitan-Form of V
 for v,w be Element of V holds
 signnorm(f,v+w) + signnorm(f,v-w) =2* signnorm(f,v)+ 2*signnorm(f,w);

theorem :: HERMITAN:53
:: Parallerogram equality - second version (stronger assumption)
  for V be VectSp of F_Complex
for f be diagReR+0valued hermitan-Form of V
 for v,w be Element of V holds
 |. f.[v+w,v+w] .| + |. f.[v-w,v-w] .| = 2*|. f.[v,v] .| + 2*|. f.[w,w] .|;

definition
  let V be non empty VectSpStr over F_Complex;
  let f be Form of V,V;
func quasinorm(f) -> RFunctional of V means
:: HERMITAN:def 10
   for v be Element of V holds it.v = sqrt (signnorm(f,v));
end;

definition
  let V be VectSp of F_Complex;
  let f be diagReR+0valued hermitan-Form of V;
redefine func quasinorm(f) -> Semi-Norm of V;
end;

begin
:: Kernel of Hermitan Forms and Hermitan Forms in Quotinet Vector Spaces

definition
 let V be add-associative right_zeroed right_complementable
           VectSp-like (non empty VectSpStr over F_Complex);
 let f be cmplxhomogeneousFAF Form of V,V;
cluster diagker f -> non empty;
end;

theorem :: HERMITAN:54
  for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
 holds diagker f is lineary-closed;

theorem :: HERMITAN:55
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
 holds diagker f = leftker f;

theorem :: HERMITAN:56
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
 holds diagker f = rightker f;

theorem :: HERMITAN:57
  for V be non empty VectSpStr over F_Complex, f be Form of V,V holds
diagker f = diagker f*';

theorem :: HERMITAN:58
for V,W be non empty VectSpStr over F_Complex, f be Form of V,W holds
leftker f = leftker f*' & rightker f = rightker f*';

theorem :: HERMITAN:59
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
holds LKer f = RKer (f*');

theorem :: HERMITAN:60
for V be VectSp of F_Complex, f be diagReR+0valued diagRvalued Form of V,V
for v be Vector of V st Re (f.[v,v])= 0 holds f.[v,v]= 0.F_Complex;

theorem :: HERMITAN:61
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V,
v be Vector of V st
 Re (f.[v,v])= 0 &
(f is non degenerated-on-left or f is non degenerated-on-right) holds v=0.V;

definition
 let V be non empty VectSpStr over F_Complex, W  be VectSp of F_Complex;
 let f be additiveFAF cmplxhomogeneousFAF Form of V,W;
func RQ*Form(f) -> additiveFAF cmplxhomogeneousFAF
Form of V,VectQuot(W,RKer (f*')) equals
:: HERMITAN:def 11
 (RQForm(f*'))*';
end;

theorem :: HERMITAN:62
for V be non empty VectSpStr over F_Complex, W  be VectSp of F_Complex
for f be additiveFAF cmplxhomogeneousFAF Form of V,W
for v be Vector of V, w be Vector of W holds
(RQ*Form(f)).[v,w+RKer (f*')] = f.[v,w];

definition
 let V,W be VectSp of F_Complex;
 let f be sesquilinear-Form of V,W;
cluster LQForm(f) -> additiveFAF cmplxhomogeneousFAF;
cluster RQ*Form(f) -> additiveSAF homogeneousSAF;
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
:: HERMITAN:def 12
for A be Vector of VectQuot(V,LKer f), B be Vector of VectQuot(W, RKer(f*'))
 for v be Vector of V, w be Vector of W
 st A = v + LKer f & B = w + RKer (f*') holds it.[A,B]= f.[v,w];
end;

definition
 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;
end;

definition
 let V be right_zeroed (non empty VectSpStr over F_Complex),
     W be VectSp of F_Complex;
 let f be additiveFAF cmplxhomogeneousFAF Form of V,W;
cluster RQ*Form(f) -> non degenerated-on-right;
end;

theorem :: HERMITAN:63
for V be non empty VectSpStr over F_Complex, W be VectSp of F_Complex
for f be additiveFAF cmplxhomogeneousFAF Form of V,W holds
leftker f = leftker (RQ*Form f);

theorem :: HERMITAN:64
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds
RKer f*' = RKer (LQForm f)*';

theorem :: HERMITAN:65
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds
LKer f = LKer (RQ*Form f);

theorem :: HERMITAN:66
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W
 holds Q*Form(f) = RQ*Form(LQForm(f)) & Q*Form(f) = LQForm(RQ*Form(f));

theorem :: HERMITAN:67
for V,W be VectSp of F_Complex, f be sesquilinear-Form of V,W holds
 leftker Q*Form(f) = leftker (RQ*Form(LQForm(f))) &
 rightker Q*Form(f) = rightker (RQ*Form(LQForm(f))) &
 leftker Q*Form(f) = leftker (LQForm(RQ*Form(f))) &
 rightker Q*Form(f) = rightker (LQForm(RQ*Form(f)));

definition
 let V,W be VectSp of F_Complex;
 let f be sesquilinear-Form of V,W;
cluster RQ*Form(LQForm(f)) -> non degenerated-on-left non degenerated-on-right;
cluster LQForm(RQ*Form(f)) -> non degenerated-on-left non degenerated-on-right;
end;

definition
 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;
end;

begin
:: Scalar Product in Quotient Vector Space Generated by Nonnegative Hermitan Form

definition
 let V be non empty VectSpStr over F_Complex;
 let f be Form of V,V;
attr f is positivediagvalued means
:: HERMITAN:def 13
for v be Vector of V st v <> 0.V holds 0 < Re (f.[v,v]);
end;

definition
 let V be right_zeroed (non empty VectSpStr over F_Complex);
 cluster positivediagvalued additiveSAF -> diagReR+0valued Form of V,V;
end;

definition
 let V be right_zeroed (non empty VectSpStr over F_Complex);
 cluster positivediagvalued additiveFAF -> diagReR+0valued Form of V,V;
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);
end;

theorem :: HERMITAN:68
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
 for A,B be Vector of VectQuot(V,LKer(f)), v,w be Vector of V st
  A = v + LKer f & B = w + LKer f holds (ScalarForm(f)).[A,B] = f.[v,w];

theorem :: HERMITAN:69
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
holds leftker ScalarForm(f) = leftker Q*Form(f);

theorem :: HERMITAN:70
for V be VectSp of F_Complex, f be diagReR+0valued hermitan-Form of V
holds rightker ScalarForm(f) = rightker Q*Form(f);

::
:: The From in Quotient Space Generated by Non negative Hermitan Form is the Scalar Product
::

definition
 let V be VectSp of F_Complex;
 let f be diagReR+0valued hermitan-Form of V;
cluster ScalarForm(f) -> non degenerated-on-left non degenerated-on-right
            positivediagvalued;
end;

definition
 let V be non trivial VectSp of F_Complex;
 let f be diagReR+0valued non constant hermitan-Form of V;
cluster ScalarForm(f) -> non constant;
end;