:: Hermitan Functionals. {C}anonical Construction of Scalar Product in Quotient Vector Space
:: by Jaros{\l}aw Kotowicz
::
:: Received November 12, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

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

theorem Th1: :: HERMITAN:1
for a being complex number st a = a *' holds
Im a = 0
proofend;

theorem Th2: :: HERMITAN:2
for a being Element of COMPLEX st a <> 0c holds
( |.(((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)).| = 1 &amp; Re ((((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)) * a) = |.a.| &amp; Im ((((Re a) / |.a.|) + (((- (Im a)) / |.a.|) * <i>)) * a) = 0 )
proofend;

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

theorem Th4: :: HERMITAN:4
for a being Element of COMPLEX holds a * (a *') = (|.a.| ^2) + (0 * <i>)
proofend;

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 &amp; Re ([**((Re a) / |.a.|),((- (Im a)) / |.a.|)**] * a) = |.a.| &amp; Im ([**((Re a) / |.a.|),((- (Im a)) / |.a.|)**] * a) = 0 )
proofend;

theorem Th8: :: HERMITAN:8
for a being Element of F_Complex ex b being Element of F_Complex st
( |.b.| = 1 &amp; Re (b * a) = |.a.| &amp; Im (b * a) = 0 )
proofend;

theorem Th9: :: HERMITAN:9
for a, b being Element of F_Complex holds
( Re (a - b) = (Re a) - (Re b) &amp; Im (a - b) = (Im a) - (Im b) )
proofend;

theorem Th10: :: HERMITAN:10
for a, b being Element of F_Complex st Im a = 0 holds
( Re (a * b) = (Re a) * (Re b) &amp; Im (a * b) = (Re a) * (Im b) )
proofend;

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

theorem Th12: :: HERMITAN:12
for a being Element of F_Complex st Im a = 0 holds
a = a *'
proofend;

theorem Th13: :: HERMITAN:13
for a being Element of F_Complex holds a * (a *') = |.a.| ^2
proofend;

theorem Th14: :: HERMITAN:14
for a being Element of F_Complex st 0 <= Re a &amp; Im a = 0 holds
|.a.| = Re a
proofend;

theorem Th15: :: HERMITAN:15
for a being Element of F_Complex holds (Re a) + (Re (a *')) = 2 * (Re a)
proofend;

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
proofend;
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
proofend;
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 &amp; b1 is cmplxhomogeneous &amp; b1 is 0-preserving )
proofend;
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
proofend;
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
proofend;
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
proofend;
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) *'
proofend;
uniqueness
 for b1, b2 being Functional of V st ( for v being Vector of V holds b1 . v = (f . v) *' ) &amp; ( for v being Vector of V holds b2 . v = (f . v) *' ) holds
b1 = b2
proofend;
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
proofend;
end;

registration
let V be non empty VectSpStr over F_Complex ;
let f be homogeneous Functional of V;
clusterf *'  ->  cmplxhomogeneous ;
coherence
 f *' is cmplxhomogeneous
proofend;
end;

registration
let V be non empty VectSpStr over F_Complex ;
let f be cmplxhomogeneous Functional of V;
clusterf *'  ->  homogeneous ;
coherence
 f *' is homogeneous
proofend;
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
proofend;
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 &amp; b1 is cmplxhomogeneous &amp; not b1 is constant &amp; not b1 is trivial )
proofend;
end;

theorem :: HERMITAN:16
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds (f *') *' = f
proofend;

theorem :: HERMITAN:17
for V being non empty VectSpStr over F_Complex holds (0Functional V) *' = 0Functional V
proofend;

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

theorem Th19: :: HERMITAN:19
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds (- f) *' = - (f *')
proofend;

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

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

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 )
proofend;

theorem Th23: :: HERMITAN:23
for V being non empty VectSpStr over F_Complex
for f being Functional of V holds ker f = ker (f *')
proofend;

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
proofend;

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
proofend;

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

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
proofend;
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
proofend;
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;
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))
proofend;

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
proofend;

registration
let V, W be non empty VectSpStr over F_Complex ;
cluster NulForm (V,W) ->  cmplxhomogeneousFAF ;
coherence
 NulForm (V,W) is cmplxhomogeneousFAF
proofend;
end;

registration
let V be non empty VectSpStr over F_Complex ;
cluster NulForm (V,V) ->  hermitan ;
coherence
 NulForm (V,V) is hermitan
proofend;
cluster NulForm (V,V) ->  diagReR+0valued ;
coherence
 NulForm (V,V) is diagReR+0valued
proofend;
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
proofend;
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 &amp; b1 is hermitan &amp; b1 is diagRvalued &amp; b1 is additiveSAF &amp; b1 is homogeneousSAF &amp; b1 is additiveFAF &amp; b1 is cmplxhomogeneousFAF )
proofend;
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 &amp; b1 is homogeneousSAF &amp; b1 is additiveFAF &amp; b1 is cmplxhomogeneousFAF )
proofend;
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 &amp; b1 is additiveFAF holds
b1 is additiveSAF
proofend;
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 &amp; b1 is additiveSAF holds
b1 is additiveFAF
proofend;
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 &amp; b1 is homogeneousSAF holds
b1 is cmplxhomogeneousFAF
proofend;
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 &amp; b1 is cmplxhomogeneousFAF holds
b1 is homogeneousSAF
proofend;
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
proofend;
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
proofend;
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 ;
proofend;
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
proofend;
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 &amp; b1 is homogeneousSAF &amp; b1 is additiveFAF &amp; b1 is cmplxhomogeneousFAF &amp; not b1 is constant &amp; not b1 is trivial )
proofend;
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)) *'
proofend;
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)) *' ) &amp; ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) *' ) holds
b1 = b2
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;

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 &amp; FormFunctional (f,(f *')) is hermitan &amp; FormFunctional (f,(f *')) is diagRvalued )
proofend;
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 &amp; b1 is hermitan &amp; b1 is diagRvalued &amp; b1 is additiveSAF &amp; b1 is homogeneousSAF &amp; b1 is additiveFAF &amp; b1 is cmplxhomogeneousFAF &amp; not b1 is constant &amp; not b1 is trivial )
proofend;
end;

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

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

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

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

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

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

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))
proofend;

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)))
proofend;

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)))))
proofend;

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)))))
proofend;

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
proofend;

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)))))
proofend;

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)) &amp; signnorm (f,v) = |.(f . (v,v)).| )
proofend;

::
:: Lemmas for Schwarz inequality
::
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)))
proofend;

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 &amp; 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)) &amp; 0 <= ((signnorm (f,v)) - ((2 * |.(f . (w,v)).|) * r)) + ((signnorm (f,w)) * (r ^2)) )
proofend;

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
proofend;

:: [WP: ] Cauchy-Schwarz_inequality
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))
proofend;

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)).|
proofend;

:: [WP: ] Minkowski_inequality
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
proofend;

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
proofend;

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)))
proofend;

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)).|)
proofend;

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))
proofend;
uniqueness
 for b1, b2 being RFunctional of V st ( for v being Element of V holds b1 . v = sqrt (signnorm (f,v)) ) &amp; ( for v being Element of V holds b2 . v = sqrt (signnorm (f,v)) ) holds
b1 = b2
proofend;
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 &amp; quasinorm f is homogeneous )
proofend;
end;

begin

:: Kernel of Hermitan Forms and Hermitan Forms in Quotinet Vector Spaces
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
proofend;
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
proofend;

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
proofend;

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
proofend;

theorem :: HERMITAN:54
for V being non empty VectSpStr over F_Complex
for f being Form of V,V holds diagker f = diagker (f *')
proofend;

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 *') &amp; rightker f = rightker (f *') )
proofend;

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

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
proofend;

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 &amp; ( not f is degenerated-on-left or not f is degenerated-on-right ) holds
v = 0. V
proofend;

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)
proofend;

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 &amp; LQForm f is cmplxhomogeneousFAF )
proofend;
cluster RQ*Form f ->  additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF ;
coherence
 ( RQ*Form f is additiveSAF &amp; RQ*Form f is homogeneousSAF )
proofend;
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) &amp; 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) &amp; B = w + (RKer (f *')) holds
b1 . (A,B) = f . (v,w)
proofend;
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) &amp; B = w + (RKer (f *')) holds
b1 . (A,B) = f . (v,w) ) &amp; ( 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) &amp; B = w + (RKer (f *')) holds
b2 . (A,B) = f . (v,w) ) holds
b1 = b2
proofend;
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) &amp; 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
proofend;
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
proofend;
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)
proofend;

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

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)
proofend;

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) &amp; Q*Form f = LQForm (RQ*Form f) )
proofend;

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)) &amp; rightker (Q*Form f) = rightker (RQ*Form (LQForm f)) &amp; leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) &amp; rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )
proofend;

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 &amp; not RQ*Form (LQForm f) is degenerated-on-right )
proofend;
cluster LQForm (RQ*Form f) ->  non degenerated-on-left non degenerated-on-right ;
coherence
 ( not LQForm (RQ*Form f) is degenerated-on-left &amp; not LQForm (RQ*Form f) is degenerated-on-right )
proofend;
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 &amp; not Q*Form f is degenerated-on-right )
proofend;
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;
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 &amp; b1 is additiveSAF holds
b1 is diagReR+0valued
proofend;
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 &amp; b1 is additiveFAF holds
b1 is diagReR+0valued
proofend;
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)))
proofend;
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) &amp; B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
proofend;

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)
proofend;

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;

::
:: The From in Quotient Space Generated by Non negative Hermitan Form is the Scalar Product
::
registration
let V be VectSp of F_Complex ;
let f be diagReR+0valued hermitan-Form of V;
cluster ScalarForm f ->  non degenerated-on-left non degenerated-on-right diagReR+0valued positivediagvalued ;
coherence
 ( not ScalarForm f is degenerated-on-left &amp; not ScalarForm f is degenerated-on-right &amp; ScalarForm f is positivediagvalued )
proofend;
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;