:: by Jaros{\l}aw Kotowicz

::

:: Received November 12, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

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

;

theorem Th2: :: HERMITAN:2

for a being 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 )

( |.(((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 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 )

( |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a) = 0 )

proof 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) )

( Re (a - b) = (Re a) - (Re b) & Im (a - b) = (Im a) - (Im b) )

proof 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) )

( Re (a * b) = (Re a) * (Re b) & Im (a * b) = (Re a) * (Im b) )

proof end;

:: deftheorem Def1 defines cmplxhomogeneous HERMITAN:def 1 :

for V being non empty ModuleStr 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) );

for V being non empty ModuleStr 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 ModuleStr over F_Complex ;

coherence

0Functional V is cmplxhomogeneous

end;
coherence

0Functional V is cmplxhomogeneous

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex ;

for b_{1} being Functional of V st b_{1} is cmplxhomogeneous holds

b_{1} is 0-preserving

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

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is cmplxhomogeneous & b_{1} is 0-preserving )

end;
cluster V1() V4( the carrier of V) V5( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) additive 0-preserving V190() cmplxhomogeneous for Element of bool [: the carrier of V, the carrier of F_Complex:];

existence ex b

( b

proof end;

definition

let V be non empty ModuleStr over F_Complex ;

mode antilinear-Functional of V is additive cmplxhomogeneous Functional of V;

end;
mode antilinear-Functional of V is additive cmplxhomogeneous Functional of V;

registration

let V be non empty ModuleStr over F_Complex ;

let f, g be cmplxhomogeneous Functional of V;

coherence

f + g is cmplxhomogeneous

end;
let f, g be cmplxhomogeneous Functional of V;

coherence

f + g is cmplxhomogeneous

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

let f be cmplxhomogeneous Functional of V;

coherence

- f is cmplxhomogeneous

end;
let f be cmplxhomogeneous Functional of V;

coherence

- f is cmplxhomogeneous

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

let a be Scalar of ;

let f be cmplxhomogeneous Functional of V;

coherence

a * f is cmplxhomogeneous

end;
let a be Scalar of ;

let f be cmplxhomogeneous Functional of V;

coherence

a * f is cmplxhomogeneous

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

let f, g be cmplxhomogeneous Functional of V;

coherence

f - g is cmplxhomogeneous ;

end;
let f, g be cmplxhomogeneous Functional of V;

coherence

f - g is cmplxhomogeneous ;

definition

let V be non empty ModuleStr over F_Complex ;

let f be Functional of V;

f *' is Functional of V

for b_{1} being Functional of V holds

( b_{1} = f *' iff for v being Vector of V holds b_{1} . v = (f . v) *' )

end;
let f be Functional of V;

:: original: *'

redefine func f *' -> Functional of V means :Def2: :: HERMITAN:def 2

for v being Vector of V holds it . v = (f . v) *' ;

coherence redefine func f *' -> Functional of V means :Def2: :: HERMITAN:def 2

for v being Vector of V holds it . v = (f . v) *' ;

f *' is Functional of V

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def2 defines *' HERMITAN:def 2 :

for V being non empty ModuleStr over F_Complex

for f, b_{3} being Functional of V holds

( b_{3} = f *' iff for v being Vector of V holds b_{3} . v = (f . v) *' );

for V being non empty ModuleStr over F_Complex

for f, b

( b

registration

let A be non empty addMagma ;

let f be additive Function of A,F_Complex;

coherence

for b_{1} being Function of A,F_Complex st b_{1} = f *' holds

b_{1} is additive

end;
let f be additive Function of A,F_Complex;

coherence

for b

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

let f be homogeneous Functional of V;

coherence

for b_{1} being Functional of V st b_{1} = f *' holds

b_{1} is cmplxhomogeneous

end;
let f be homogeneous Functional of V;

coherence

for b

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

let f be cmplxhomogeneous Functional of V;

coherence

for b_{1} being Functional of V st b_{1} = f *' holds

b_{1} is homogeneous

end;
let f be cmplxhomogeneous Functional of V;

coherence

for b

b

proof end;

registration

let V be non trivial VectSp of F_Complex ;

let f be non constant Functional of V;

coherence

not f *' is constant

end;
let f be non constant Functional of V;

coherence

not f *' is constant

proof end;

registration

let V be non trivial VectSp of F_Complex ;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is cmplxhomogeneous & not b_{1} is constant & not b_{1} is trivial )

end;
cluster V1() V4( the carrier of V) V5( the carrier of F_Complex) non trivial Function-like non constant V30( the carrier of V, the carrier of F_Complex) additive V190() cmplxhomogeneous for Element of bool [: the carrier of V, the carrier of F_Complex:];

existence ex b

( b

proof end;

theorem :: HERMITAN:16

theorem Th18: :: HERMITAN:18

for V being non empty ModuleStr over F_Complex

for f, g being Functional of V holds (f + g) *' = (f *') + (g *')

for f, g being Functional of V holds (f + g) *' = (f *') + (g *')

proof end;

theorem Th19: :: HERMITAN:19

for V being non empty ModuleStr over F_Complex

for f being Functional of V holds (- f) *' = - (f *')

for f being Functional of V holds (- f) *' = - (f *')

proof end;

theorem :: HERMITAN:20

for V being non empty ModuleStr over F_Complex

for f being Functional of V

for a being Scalar of holds (a * f) *' = (a *') * (f *')

for f being Functional of V

for a being Scalar of holds (a * f) *' = (a *') * (f *')

proof end;

theorem :: HERMITAN:21

for V being non empty ModuleStr over F_Complex

for f, g being Functional of V holds (f - g) *' = (f *') - (g *')

for f, g being Functional of V holds (f - g) *' = (f *') - (g *')

proof end;

theorem Th22: :: HERMITAN:22

for V being non empty ModuleStr 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 )

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

theorem :: HERMITAN:24

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex

for f being antilinear-Functional of V holds ker f is linearly-closed

for f being antilinear-Functional of V holds ker f is linearly-closed

proof 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

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

definition

let V be VectSp of F_Complex ;

let f be antilinear-Functional of V;

coherence

QFunctional (f,(Ker (f *'))) is antilinear-Functional of (VectQuot (V,(Ker (f *'))));

end;
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 QFunctional (f,(Ker (f *')));

coherence

QFunctional (f,(Ker (f *'))) is antilinear-Functional of (VectQuot (V,(Ker (f *'))));

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

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

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

registration

let V be non trivial VectSp of F_Complex ;

let f be V23() antilinear-Functional of V;

coherence

not QcFunctional f is constant

end;
let f be V23() antilinear-Functional of V;

coherence

not QcFunctional f is constant

proof end;

registration

let V be VectSp of F_Complex ;

let f be antilinear-Functional of V;

coherence

not QcFunctional f is degenerated

end;
let f be antilinear-Functional of V;

coherence

not QcFunctional f is degenerated

proof end;

::Sesquilinear Forms in Complex Vector Spaces

definition

let V, W be non empty ModuleStr over F_Complex ;

let f be Form of V,W;

end;
let f be Form of V,W;

attr f is cmplxhomogeneousFAF means :Def4: :: HERMITAN:def 4

for v being Vector of V holds FunctionalFAF (f,v) is cmplxhomogeneous ;

for v being Vector of V holds FunctionalFAF (f,v) is cmplxhomogeneous ;

:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def 4 :

for V, W being non empty ModuleStr 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 );

for V, W being non empty ModuleStr 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 ModuleStr 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))

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

definition

let V be non empty ModuleStr over F_Complex ;

let f be Form of V,V;

end;
let f be Form of V,V;

attr f is hermitan means :Def5: :: HERMITAN:def 5

for v, u being Vector of V holds f . (v,u) = (f . (u,v)) *' ;

for v, u being Vector of V holds f . (v,u) = (f . (u,v)) *' ;

attr f is diagRvalued means :Def6: :: HERMITAN:def 6

for v being Vector of V holds Im (f . (v,v)) = 0 ;

for v being Vector of V holds Im (f . (v,v)) = 0 ;

attr f is diagReR+0valued means :Def7: :: HERMITAN:def 7

for v being Vector of V holds 0 <= Re (f . (v,v));

for v being Vector of V holds 0 <= Re (f . (v,v));

:: deftheorem Def5 defines hermitan HERMITAN:def 5 :

for V being non empty ModuleStr 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)) *' );

for V being non empty ModuleStr 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 ModuleStr 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 );

for V being non empty ModuleStr 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 ModuleStr 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)) );

for V being non empty ModuleStr 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 ModuleStr 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

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 ModuleStr 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 ; :: thesis: verum

end;
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 ; :: thesis: verum

Lm3: for V being non empty ModuleStr over F_Complex

for f being Functional of V holds FormFunctional (f,(0Functional V)) is hermitan

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

coherence

NulForm (V,W) is cmplxhomogeneousFAF

end;
coherence

NulForm (V,W) is cmplxhomogeneousFAF

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

coherence

NulForm (V,V) is hermitan

NulForm (V,V) is diagReR+0valued

end;
coherence

NulForm (V,V) is hermitan

proof end;

coherence NulForm (V,V) is diagReR+0valued

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is hermitan holds

b_{1} is diagRvalued

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

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

ex b_{1} being Form of V,V st

( b_{1} is diagReR+0valued & b_{1} is hermitan & b_{1} is diagRvalued & b_{1} is additiveSAF & b_{1} is homogeneousSAF & b_{1} is additiveFAF & b_{1} is cmplxhomogeneousFAF )

end;
cluster V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of F_Complex) Function-like V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF V190() cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];

existence ex b

( b

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

ex b_{1} being Form of V,W st

( b_{1} is additiveSAF & b_{1} is homogeneousSAF & b_{1} is additiveFAF & b_{1} is cmplxhomogeneousFAF )

end;
cluster V1() V4([: the carrier of V, the carrier of W:]) V5( the carrier of F_Complex) Function-like V30([: the carrier of V, the carrier of W:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF V190() cmplxhomogeneousFAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Complex:];

existence ex b

( b

proof end;

definition

let V, W be non empty ModuleStr over F_Complex ;

mode sesquilinear-Form of V,W is additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Form of V,W;

end;
mode sesquilinear-Form of V,W is additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Form of V,W;

registration

let V be non empty ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is hermitan & b_{1} is additiveFAF holds

b_{1} is additiveSAF

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

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is hermitan & b_{1} is additiveSAF holds

b_{1} is additiveFAF

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

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is hermitan & b_{1} is homogeneousSAF holds

b_{1} is cmplxhomogeneousFAF

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

b

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is hermitan & b_{1} is cmplxhomogeneousFAF holds

b_{1} is homogeneousSAF

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

b

proof end;

definition

let V be non empty ModuleStr over F_Complex ;

mode hermitan-Form of V is additiveSAF homogeneousSAF hermitan Form of V,V;

end;
mode hermitan-Form of V is additiveSAF homogeneousSAF hermitan Form of V,V;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be Functional of V;

let g be cmplxhomogeneous Functional of W;

coherence

FormFunctional (f,g) is cmplxhomogeneousFAF

end;
let f be Functional of V;

let g be cmplxhomogeneous Functional of W;

coherence

FormFunctional (f,g) is cmplxhomogeneousFAF

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be cmplxhomogeneousFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is cmplxhomogeneous

end;
let f be cmplxhomogeneousFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is cmplxhomogeneous

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f, g be cmplxhomogeneousFAF Form of V,W;

correctness

coherence

f + g is cmplxhomogeneousFAF ;

end;
let f, g be cmplxhomogeneousFAF Form of V,W;

correctness

coherence

f + g is cmplxhomogeneousFAF ;

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be cmplxhomogeneousFAF Form of V,W;

let a be Scalar of ;

coherence

a * f is cmplxhomogeneousFAF

end;
let f be cmplxhomogeneousFAF Form of V,W;

let a be Scalar of ;

coherence

a * f is cmplxhomogeneousFAF

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be cmplxhomogeneousFAF Form of V,W;

coherence

- f is cmplxhomogeneousFAF ;

end;
let f be cmplxhomogeneousFAF Form of V,W;

coherence

- f is cmplxhomogeneousFAF ;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f, g be cmplxhomogeneousFAF Form of V,W;

coherence

f - g is cmplxhomogeneousFAF ;

end;
let f, g be cmplxhomogeneousFAF Form of V,W;

coherence

f - g is cmplxhomogeneousFAF ;

registration

let V, W be non trivial VectSp of F_Complex ;

ex b_{1} being Form of V,W st

( b_{1} is additiveSAF & b_{1} is homogeneousSAF & b_{1} is additiveFAF & b_{1} is cmplxhomogeneousFAF & not b_{1} is constant & not b_{1} is trivial )

end;
cluster V1() V4([: the carrier of V, the carrier of W:]) V5( the carrier of F_Complex) non trivial Function-like non constant V30([: the carrier of V, the carrier of W:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF V190() cmplxhomogeneousFAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of F_Complex:];

existence ex b

( b

proof end;

definition

let V, W be non empty ModuleStr over F_Complex ;

let f be Form of V,W;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) *'

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) *' ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . (v,w)) *' ) holds

b_{1} = b_{2}

end;
let f be Form of V,W;

func f *' -> 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 for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) *' ;

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof end;

:: deftheorem Def8 defines *' HERMITAN:def 8 :

for V, W being non empty ModuleStr over F_Complex

for f, b_{4} being Form of V,W holds

( b_{4} = f *' iff for v being Vector of V

for w being Vector of W holds b_{4} . (v,w) = (f . (v,w)) *' );

for V, W being non empty ModuleStr over F_Complex

for f, b

( b

for w being Vector of W holds b

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be additiveFAF Form of V,W;

coherence

f *' is additiveFAF

end;
let f be additiveFAF Form of V,W;

coherence

f *' is additiveFAF

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be additiveSAF Form of V,W;

coherence

f *' is additiveSAF

end;
let f be additiveSAF Form of V,W;

coherence

f *' is additiveSAF

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be homogeneousFAF Form of V,W;

coherence

f *' is cmplxhomogeneousFAF

end;
let f be homogeneousFAF Form of V,W;

coherence

f *' is cmplxhomogeneousFAF

proof end;

registration

let V, W be non empty ModuleStr over F_Complex ;

let f be cmplxhomogeneousFAF Form of V,W;

coherence

f *' is homogeneousFAF

end;
let f be cmplxhomogeneousFAF Form of V,W;

coherence

f *' is homogeneousFAF

proof end;

registration

let V, W be non trivial VectSp of F_Complex ;

let f be non constant Form of V,W;

coherence

not f *' is constant

end;
let f be non constant Form of V,W;

coherence

not f *' is constant

proof end;

theorem Th28: :: HERMITAN:28

for V being non empty ModuleStr over F_Complex

for f being Functional of V

for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2

for f being Functional of V

for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2

proof end;

registration

let V be non empty ModuleStr over F_Complex ;

let f be Functional of V;

coherence

( FormFunctional (f,(f *')) is diagReR+0valued & FormFunctional (f,(f *')) is hermitan & FormFunctional (f,(f *')) is diagRvalued )

end;
let f be Functional of V;

coherence

( FormFunctional (f,(f *')) is diagReR+0valued & FormFunctional (f,(f *')) is hermitan & FormFunctional (f,(f *')) is diagRvalued )

proof end;

registration

let V be non trivial VectSp of F_Complex ;

ex b_{1} being Form of V,V st

( b_{1} is diagReR+0valued & b_{1} is hermitan & b_{1} is diagRvalued & b_{1} is additiveSAF & b_{1} is homogeneousSAF & b_{1} is additiveFAF & b_{1} is cmplxhomogeneousFAF & not b_{1} is constant & not b_{1} is trivial )

end;
cluster V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of F_Complex) non trivial Function-like non constant V30([: the carrier of V, the carrier of V:], the carrier of F_Complex) additiveFAF additiveSAF homogeneousSAF V190() cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of F_Complex:];

existence ex b

( b

proof end;

theorem Th31: :: HERMITAN:31

for V, W being non empty ModuleStr over F_Complex

for f, g being Form of V,W holds (f + g) *' = (f *') + (g *')

for f, g being Form of V,W holds (f + g) *' = (f *') + (g *')

proof end;

theorem :: HERMITAN:33

for V, W being non empty ModuleStr over F_Complex

for f being Form of V,W

for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')

for f being Form of V,W

for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')

proof end;

theorem :: HERMITAN:34

for V, W being non empty ModuleStr over F_Complex

for f, g being Form of V,W holds (f - g) *' = (f *') - (g *')

for f, g being Form of V,W holds (f - g) *' = (f *') - (g *')

proof 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))

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

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 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 ModuleStr 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)))))

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

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

theorem Th39: :: HERMITAN:39

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr 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

for f being cmplxhomogeneousFAF Form of V,V

for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex

proof 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)))))

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

definition

let V be non empty ModuleStr over F_Complex ;

let f be Form of V,V;

let v be Vector of V;

coherence

Re (f . (v,v)) is Real ;

end;
let f be Form of V,V;

let v be Vector of V;

coherence

Re (f . (v,v)) is Real ;

:: deftheorem defines signnorm HERMITAN:def 9 :

for V being non empty ModuleStr over F_Complex

for f being Form of V,V

for v being Vector of V holds signnorm (f,v) = Re (f . (v,v));

for V being non empty ModuleStr 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 ModuleStr 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)).| )

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

::

:: Lemmas for Schwarz inequality

::

:: 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

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

for v, w being Vector of V

for f being sesquilinear-Form of V,V

for r being Real

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

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

for v, w being Vector of V

for f being diagReR+0valued hermitan-Form of V

for r being Real

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

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

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

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

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

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

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

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

definition

let V be non empty ModuleStr over F_Complex ;

let f be Form of V,V;

ex b_{1} being RFunctional of V st

for v being Element of V holds b_{1} . v = sqrt (signnorm (f,v))

for b_{1}, b_{2} being RFunctional of V st ( for v being Element of V holds b_{1} . v = sqrt (signnorm (f,v)) ) & ( for v being Element of V holds b_{2} . v = sqrt (signnorm (f,v)) ) holds

b_{1} = b_{2}

end;
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 for v being Element of V holds it . v = sqrt (signnorm (f,v));

ex b

for v being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines quasinorm HERMITAN:def 10 :

for V being non empty ModuleStr over F_Complex

for f being Form of V,V

for b_{3} being RFunctional of V holds

( b_{3} = quasinorm f iff for v being Element of V holds b_{3} . v = sqrt (signnorm (f,v)) );

for V being non empty ModuleStr over F_Complex

for f being Form of V,V

for b

( b

registration

let V be VectSp of F_Complex ;

let f be diagReR+0valued hermitan-Form of V;

coherence

( quasinorm f is subadditive & quasinorm f is homogeneous )

end;
let f be diagReR+0valued hermitan-Form of V;

coherence

( quasinorm f is subadditive & quasinorm f is homogeneous )

proof end;

:: 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 ModuleStr over F_Complex ;

let f be cmplxhomogeneousFAF Form of V,V;

coherence

not diagker f is empty

end;
let f be cmplxhomogeneousFAF Form of V,V;

coherence

not diagker f is empty

proof 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

for f being diagReR+0valued hermitan-Form of V holds diagker f is linearly-closed

proof 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

for f being diagReR+0valued hermitan-Form of V holds diagker f = leftker f

proof 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

for f being diagReR+0valued hermitan-Form of V holds diagker f = rightker f

proof end;

theorem :: HERMITAN:54

for V being non empty ModuleStr over F_Complex

for f being Form of V,V holds diagker f = diagker (f *')

for f being Form of V,V holds diagker f = diagker (f *')

proof end;

theorem Th55: :: HERMITAN:55

for V, W being non empty ModuleStr over F_Complex

for f being Form of V,W holds

( leftker f = leftker (f *') & rightker f = rightker (f *') )

for f being Form of V,W holds

( leftker f = leftker (f *') & rightker f = rightker (f *') )

proof 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 *')

for f being diagReR+0valued hermitan-Form of V holds LKer f = RKer (f *')

proof 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

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

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

definition

let V be non empty ModuleStr over F_Complex ;

let W be VectSp of F_Complex ;

let f be additiveFAF cmplxhomogeneousFAF Form of V,W;

coherence

(RQForm (f *')) *' is additiveFAF cmplxhomogeneousFAF Form of V,(VectQuot (W,(RKer (f *'))));

;

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

coherence

(RQForm (f *')) *' is additiveFAF cmplxhomogeneousFAF Form of V,(VectQuot (W,(RKer (f *'))));

;

:: deftheorem defines RQ*Form HERMITAN:def 11 :

for V being non empty ModuleStr 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 *')) *' ;

for V being non empty ModuleStr 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 ModuleStr 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)

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

registration

let V, W be VectSp of F_Complex ;

let f be sesquilinear-Form of V,W;

coherence

( LQForm f is additiveFAF & LQForm f is cmplxhomogeneousFAF )

( RQ*Form f is additiveSAF & RQ*Form f is homogeneousSAF )

end;
let f be sesquilinear-Form of V,W;

coherence

( LQForm f is additiveFAF & LQForm f is cmplxhomogeneousFAF )

proof end;

coherence ( RQ*Form f is additiveSAF & RQ*Form f is homogeneousSAF )

proof end;

definition

let V, W be VectSp of F_Complex ;

let f be sesquilinear-Form of V,W;

ex b_{1} 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

b_{1} . (A,B) = f . (v,w)

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (A,B) = f . (v,w) ) holds

b_{1} = b_{2}

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

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof 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 b_{4} being sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) holds

( b_{4} = 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

b_{4} . (A,B) = f . (v,w) );

for V, W being VectSp of F_Complex

for f being sesquilinear-Form of V,W

for b

( b

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

b

registration

let V, W be non trivial VectSp of F_Complex ;

let f be non constant sesquilinear-Form of V,W;

coherence

not Q*Form f is constant

end;
let f be non constant sesquilinear-Form of V,W;

coherence

not Q*Form f is constant

proof end;

registration

let V be non empty right_zeroed ModuleStr over F_Complex ;

let W be VectSp of F_Complex ;

let f be additiveFAF cmplxhomogeneousFAF Form of V,W;

coherence

not RQ*Form f is degenerated-on-right

end;
let W be VectSp of F_Complex ;

let f be additiveFAF cmplxhomogeneousFAF Form of V,W;

coherence

not RQ*Form f is degenerated-on-right

proof end;

theorem Th60: :: HERMITAN:60

for V being non empty ModuleStr 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)

for W being VectSp of F_Complex

for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)

proof 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) *')

for f being sesquilinear-Form of V,W holds RKer (f *') = RKer ((LQForm f) *')

proof 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)

for f being sesquilinear-Form of V,W holds LKer f = LKer (RQ*Form f)

proof 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) )

for f being sesquilinear-Form of V,W holds

( Q*Form f = RQ*Form (LQForm f) & Q*Form f = LQForm (RQ*Form f) )

proof 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)) )

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

registration

let V, W be VectSp of F_Complex ;

let f be sesquilinear-Form of V,W;

( not RQ*Form (LQForm f) is degenerated-on-left & not RQ*Form (LQForm f) is degenerated-on-right )

( not LQForm (RQ*Form f) is degenerated-on-left & not LQForm (RQ*Form f) is degenerated-on-right )

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

coherence ( not LQForm (RQ*Form f) is degenerated-on-left & not LQForm (RQ*Form f) is degenerated-on-right )

proof end;

registration

let V, W be VectSp of F_Complex ;

let f be sesquilinear-Form of V,W;

coherence

( not Q*Form f is degenerated-on-left & not Q*Form f is degenerated-on-right )

end;
let f be sesquilinear-Form of V,W;

coherence

( not Q*Form f is degenerated-on-left & not Q*Form f is degenerated-on-right )

proof end;

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

definition

let V be non empty ModuleStr over F_Complex ;

let f be Form of V,V;

end;
let f be Form of V,V;

attr f is positivediagvalued means :: HERMITAN:def 13

for v being Vector of V st v <> 0. V holds

0 < Re (f . (v,v));

for v being Vector of V st v <> 0. V holds

0 < Re (f . (v,v));

:: deftheorem defines positivediagvalued HERMITAN:def 13 :

for V being non empty ModuleStr 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)) );

for V being non empty ModuleStr 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 ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is positivediagvalued & b_{1} is additiveSAF holds

b_{1} is diagReR+0valued

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

b

proof end;

registration

let V be non empty right_zeroed ModuleStr over F_Complex ;

for b_{1} being Form of V,V st b_{1} is positivediagvalued & b_{1} is additiveFAF holds

b_{1} is diagReR+0valued

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

b

proof end;

definition

let V be VectSp of F_Complex ;

let f be diagReR+0valued hermitan-Form of V;

Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f)))

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

Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f)))

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

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)

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

for f being diagReR+0valued hermitan-Form of V holds leftker (ScalarForm f) = leftker (Q*Form f)

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

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

::

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

( not ScalarForm f is degenerated-on-left & not ScalarForm f is degenerated-on-right & ScalarForm f is positivediagvalued )

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

registration

let V be non trivial VectSp of F_Complex ;

let f be non constant diagReR+0valued hermitan-Form of V;

coherence

not ScalarForm f is constant ;

end;
let f be non constant diagReR+0valued hermitan-Form of V;

coherence

not ScalarForm f is constant ;