:: HERMITAN semantic presentation

Lm1: 0 = [**0,0**]
;

theorem Th1: :: HERMITAN:1

for a being complex number st a = a *' holds
Im a = 0

proof end;

theorem Th2: :: HERMITAN:2

for a being Element of COMPLEX st a <> 0c holds
( |.[*((Re a) / |.a.|),((- (Im a)) / |.a.|)*].| = 1 & Re ([*((Re a) / |.a.|),((- (Im a)) / |.a.|)*] * a) = |.a.| & Im ([*((Re a) / |.a.|),((- (Im a)) / |.a.|)*] * a) = 0 )

proof end;

theorem :: HERMITAN:3

for a being Element of COMPLEX ex b being Element of COMPLEX st
( |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a) = 0 )

proof end;

theorem Th4: :: HERMITAN:4

for a being Element of COMPLEX holds a * (a *' ) = (|.a.| ^2 ) + (0 * )

proof end;

theorem Th5: :: HERMITAN:5

for a being Element of F_Complex st a = a *' holds
Im a = 0 by Th1;

i_FC *' = (Re i_FC ) - ((Im i_FC ) * ) by COMPLEX1:def 15
.= (Re ) - ((Im ) * )
.= 0 - (1 * ) by COMPLEX1:17 ;

then Lm2: i_FC *' = "
;

theorem :: HERMITAN:6

canceled;

theorem Th7: :: HERMITAN:7

i_FC * (i_FC *' ) = 1. F_Complex

proof end;

theorem Th8: :: HERMITAN:8

for a being Element of F_Complex st a <> 0. F_Complex holds
( |.[**((Re a) / |.a.|),((- (Im a)) / |.a.|)**].| = 1 & Re ([**((Re a) / |.a.|),((- (Im a)) / |.a.|)**] * a) = |.a.| & Im ([**((Re a) / |.a.|),((- (Im a)) / |.a.|)**] * a) = 0 )

proof end;

Lm3: the unity of F_Complex = 1r by COMPLFLD:def 1
.= 1. F_Complex by COMPLFLD:10 ;

theorem Th9: :: HERMITAN:9

for a being Element of F_Complex ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a) = 0 )

proof end;

theorem Th10: :: HERMITAN:10

for a, b being Element of F_Complex holds
( Re (a - b) = (Re a) - (Re b) & Im (a - b) = (Im a) - (Im b) )

proof end;

theorem Th11: :: HERMITAN:11

for a, b being Element of F_Complex st Im a = 0 holds
( Re (a * b) = (Re a) * (Re b) & Im (a * b) = (Re a) * (Im b) )

proof end;

theorem :: HERMITAN:12

for a, b being Element of F_Complex st Im a = 0 & Im b = 0 holds
Im (a * b) = 0

proof end;

Lm4: for a being Element of F_Complex holds Re a = Re (a *' )
by COMPLEX1:112;

theorem :: HERMITAN:13

canceled;

theorem Th14: :: HERMITAN:14

for a being Element of F_Complex st Im a = 0 holds
a = a *'

proof end;

theorem Th15: :: HERMITAN:15

for r, s being Real holds [**r,0**] * [**s,0**] = [**(r * s),0**] by COMPLFLD:6;

theorem Th16: :: HERMITAN:16

for a being Element of F_Complex holds a * (a *' ) = [**(|.a.| ^2 ),0**]

proof end;

theorem Th17: :: HERMITAN:17

for a being Element of F_Complex st 0 <= Re a & Im a = 0 holds
|.a.| = Re a

proof end;

theorem Th18: :: HERMITAN:18

for a being Element of F_Complex holds (Re a) + (Re (a *' )) = 2 * (Re a)

proof end;

definition

let V be non empty VectSpStr of F_Complex ;
let f be Functional of V;
attr f 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 :

registration

let V be non empty VectSpStr of F_Complex ;
cluster 0Functional V -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

let V be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex ;
cluster cmplxhomogeneous -> 0-preserving Relation of the carrier of V,the carrier of F_Complex ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster additive 0-preserving cmplxhomogeneous Relation of the carrier of V,the carrier of F_Complex ;
existence

proof end;

end;

definition

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

end;

registration

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

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
let f be cmplxhomogeneous Functional of V;
cluster - f -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

end;

definition

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

proof end;

uniqueness

proof end;

end;

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

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let V be non trivial VectSp of F_Complex ;
cluster non constant additive 0-preserving non trivial cmplxhomogeneous Relation of the carrier of V,the carrier of F_Complex ;
existence

proof end;

end;

theorem :: HERMITAN:19

for V being non empty VectSpStr of F_Complex
for f being Functional of V holds (f *' ) *' = f

proof end;

theorem :: HERMITAN:20

for V being non empty VectSpStr of F_Complex holds (0Functional V) *' = 0Functional V

proof end;

theorem Th21: :: HERMITAN:21

for V being non empty VectSpStr of F_Complex
for f, g being Functional of V holds (f + g) *' = (f *' ) + (g *' )

proof end;

theorem Th22: :: HERMITAN:22

for V being non empty VectSpStr of F_Complex
for f being Functional of V holds (- f) *' = - (f *' )

proof end;

theorem :: HERMITAN:23

for V being non empty VectSpStr of F_Complex
for f being Functional of V
for a being Scalar of holds (a * f) *' = (a *' ) * (f *' )

proof end;

theorem :: HERMITAN:24

for V being non empty VectSpStr of F_Complex
for f, g being Functional of V holds (f - g) *' = (f *' ) - (g *' )

proof end;

theorem Th25: :: HERMITAN:25

for V being non empty VectSpStr of 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 Th26: :: HERMITAN:26

for V being non empty VectSpStr of F_Complex
for f being Functional of V holds ker f = ker (f *' )

proof end;

theorem :: HERMITAN:27

for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex
for f being antilinear-Functional of V holds ker f is lineary-closed

proof end;

theorem Th28: :: HERMITAN:28

for V being VectSp of F_Complex
for W being Subspace of V
for f being antilinear-Functional of V st the carrier of W c= ker (f *' ) holds
QFunctional f,W is cmplxhomogeneous

proof end;

definition

let V be VectSp of F_Complex ;
let f be antilinear-Functional of V;
func QcFunctional f -> antilinear-Functional of (VectQuot V,(Ker (f *' ))) equals :: HERMITAN:def 3
QFunctional f,(Ker (f *' ));
correctness

proof end;

end;

:: deftheorem defines QcFunctional HERMITAN:def 3 :

theorem Th29: :: HERMITAN:29

for V being VectSp of F_Complex
for f being antilinear-Functional of V
for A being Vector of (VectQuot V,(Ker (f *' )))
for v being Vector of V st A = v + (Ker (f *' )) holds
(QcFunctional f) . A = f . v

proof end;

registration

let V be non trivial VectSp of F_Complex ;
let f be V72 antilinear-Functional of V;
cluster QcFunctional f -> V72 0-preserving ;
coherence

proof end;

end;

registration

let V be VectSp of F_Complex ;
let f be antilinear-Functional of V;
cluster QcFunctional f -> 0-preserving non degenerated ;
coherence

proof end;

end;

definition

let V, W be non empty VectSpStr of F_Complex ;
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;

end;

:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def 4 :

theorem Th30: :: HERMITAN:30

for V, W being non empty VectSpStr of F_Complex
for v being Vector of V
for w being Vector of W
for a being Element of F_Complex
for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . [v,(a * w)] = (a *' ) * (f . [v,w])

proof end;

definition

let V be non empty VectSpStr of F_Complex ;
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]) *' ;
attr f is diagRvalued means :Def6: :: HERMITAN:def 6
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]);

end;

:: deftheorem Def5 defines hermitan HERMITAN:def 5 :

:: deftheorem Def6 defines diagRvalued HERMITAN:def 6 :

:: deftheorem Def7 defines diagReR+0valued HERMITAN:def 7 :

Lm5: now

let V be non empty VectSpStr of F_Complex ; :: thesis:
let f be Functional of V; :: thesis:
set 0F = 0Functional V;
let v1, w be Vector of V; :: thesis:
thus (FormFunctional f,(0Functional V)) . [v1,w] = (f . v1) * ((0Functional V) . w) by BILINEAR:def 11
.= (f . v1) * (0. F_Complex ) by HAHNBAN1:22
.= 0. F_Complex by VECTSP_1:39 ; :: thesis:

end;

Lm6: for V being non empty VectSpStr of F_Complex
for f being Functional of V holds FormFunctional f,(0Functional V) is hermitan

proof end;

registration

let V, W be non empty VectSpStr of F_Complex ;
cluster NulForm V,W -> cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster NulForm V,V -> cmplxhomogeneousFAF hermitan ;
coherence

proof end;

cluster NulForm V,V -> cmplxhomogeneousFAF diagReR+0valued ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster hermitan -> diagRvalued Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
existence

proof end;

end;

registration

let V, W be non empty VectSpStr of F_Complex ;
cluster additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Relation of [:the carrier of V,the carrier of W:],the carrier of F_Complex ;
existence

proof end;

end;

definition

let V, W be non empty VectSpStr of 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 of F_Complex ;
cluster additiveFAF hermitan -> additiveSAF Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster additiveSAF hermitan -> additiveFAF Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster homogeneousSAF hermitan -> cmplxhomogeneousFAF Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster cmplxhomogeneousFAF hermitan -> homogeneousSAF Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

definition

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

end;

registration

let V, W be non empty VectSpStr of F_Complex ;
let f be Functional of V;
let g be cmplxhomogeneous Functional of W;
cluster FormFunctional f,g -> cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let V, W be non empty VectSpStr of F_Complex ;
let f be cmplxhomogeneousFAF Form of V,W;
let v be Vector of V;
cluster FunctionalFAF f,v -> cmplxhomogeneous ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

end;

registration

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

end;

registration

let V, W be non trivial VectSp of F_Complex ;
cluster non constant non trivial additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF Relation of [:the carrier of V,the carrier of W:],the carrier of F_Complex ;
existence

proof end;

end;

definition

let V, W be non empty VectSpStr of F_Complex ;
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

proof end;

uniqueness

proof end;

end;

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

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th31: :: HERMITAN:31

for V being non empty VectSpStr of F_Complex
for f being Functional of V
for v being Vector of V holds (FormFunctional f,(f *' )) . [v,v] = [**(|.(f . v).| ^2 ),0**]

proof end;

registration

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

proof end;

end;

registration

let V be non trivial VectSp of F_Complex ;
cluster non constant non trivial additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
existence

proof end;

end;

theorem :: HERMITAN:32

for V, W being non empty VectSpStr of F_Complex
for f being Form of V,W holds (f *' ) *' = f

proof end;

theorem :: HERMITAN:33

for V, W being non empty VectSpStr of F_Complex holds (NulForm V,W) *' = NulForm V,W

proof end;

theorem Th34: :: HERMITAN:34

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

proof end;

theorem Th35: :: HERMITAN:35

for V, W being non empty VectSpStr of F_Complex
for f being Form of V,W holds (- f) *' = - (f *' )

proof end;

theorem :: HERMITAN:36

for V, W being non empty VectSpStr of F_Complex
for f being Form of V,W
for a being Element of F_Complex holds (a * f) *' = (a *' ) * (f *' )

proof end;

theorem :: HERMITAN:37

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

proof end;

theorem Th38: :: HERMITAN:38

for V, W being VectSp of F_Complex
for v being Vector of V
for w, t being Vector of W
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . [v,(w - t)] = (f . [v,w]) - (f . [v,t])

proof end;

theorem Th39: :: HERMITAN:39

for V, W being VectSp of F_Complex
for v, u being Vector of V
for w, t being Vector of W
for f being sesquilinear-Form of V,W holds f . [(v - u),(w - t)] = ((f . [v,w]) - (f . [v,t])) - ((f . [u,w]) - (f . [u,t]))

proof end;

theorem Th40: :: HERMITAN:40

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

proof end;

theorem Th41: :: HERMITAN:41

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

proof end;

theorem Th42: :: HERMITAN:42

for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of 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:43

for V being VectSp of F_Complex
for v, w being Vector of V
for f being hermitan-Form of V holds (((f . [v,w]) + (f . [v,w])) + (f . [v,w])) + (f . [v,w]) = (((f . [(v + w),(v + w)]) - (f . [(v - w),(v - w)])) + (i_FC * (f . [(v + (i_FC * w)),(v + (i_FC * w))]))) - (i_FC * (f . [(v - (i_FC * w)),(v - (i_FC * w))]))

proof end;

definition

let V be non empty VectSpStr of 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 ;

end;

:: deftheorem defines signnorm HERMITAN:def 9 :

theorem Th44: :: HERMITAN:44

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

proof end;

theorem Th45: :: HERMITAN:45

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

proof end;

theorem Th46: :: HERMITAN:46

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

proof end;

theorem Th47: :: HERMITAN:47

for V being VectSp of F_Complex
for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V st signnorm f,w = 0 holds
|.(f . [w,v]).| = 0

proof end;

theorem Th48: :: HERMITAN:48

for V being VectSp of F_Complex
for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V holds |.(f . [v,w]).| ^2 <= (signnorm f,v) * (signnorm f,w)

proof end;

theorem Th49: :: HERMITAN:49

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds |.(f . [v,w]).| ^2 <= |.(f . [v,v]).| * |.(f . [w,w]).|

proof end;

theorem Th50: :: HERMITAN:50

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds signnorm f,(v + w) <= ((sqrt (signnorm f,v)) + (sqrt (signnorm f,w))) ^2

proof end;

theorem :: HERMITAN:51

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds |.(f . [(v + w),(v + w)]).| <= ((sqrt |.(f . [v,v]).|) + (sqrt |.(f . [w,w]).|)) ^2

proof end;

theorem Th52: :: HERMITAN:52

for V being VectSp of F_Complex
for f being hermitan-Form of V
for v, w being Element of V holds (signnorm f,(v + w)) + (signnorm f,(v - w)) = (2 * (signnorm f,v)) + (2 * (signnorm f,w))

proof end;

theorem :: HERMITAN:53

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being Element of V holds |.(f . [(v + w),(v + w)]).| + |.(f . [(v - w),(v - w)]).| = (2 * |.(f . [v,v]).|) + (2 * |.(f . [w,w]).|)

proof end;

definition

let V be non empty VectSpStr of 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines quasinorm HERMITAN:def 10 :

definition

let V be VectSp of F_Complex ;
let f be diagReR+0valued hermitan-Form of V;
:: original: quasinorm
redefine func quasinorm f -> Semi-Norm of V;
coherence

proof end;

end;

registration

let V be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F_Complex ;
let f be cmplxhomogeneousFAF Form of V,V;
cluster diagker f -> non empty ;
coherence

proof end;

end;

theorem :: HERMITAN:54

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

proof end;

theorem Th55: :: HERMITAN:55

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

proof end;

theorem Th56: :: HERMITAN:56

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

proof end;

theorem :: HERMITAN:57

for V being non empty VectSpStr of F_Complex
for f being Form of V,V holds diagker f = diagker (f *' )

proof end;

theorem Th58: :: HERMITAN:58

for V, W being non empty VectSpStr of F_Complex
for f being Form of V,W holds
( leftker f = leftker (f *' ) & rightker f = rightker (f *' ) )

proof end;

theorem Th59: :: HERMITAN:59

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

proof end;

theorem Th60: :: HERMITAN:60

for V being VectSp of F_Complex
for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V st Re (f . [v,v]) = 0 holds
f . [v,v] = 0. F_Complex

proof end;

theorem Th61: :: HERMITAN:61

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v being Vector of V st Re (f . [v,v]) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds
v = 0. V

proof end;

definition

let V be non empty VectSpStr of 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 ;

end;

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

theorem Th62: :: HERMITAN:62

for V being non empty VectSpStr of F_Complex
for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of V
for w being Vector of W holds (RQ*Form f) . [v,(w + (RKer (f *' )))] = f . [v,w]

proof end;

registration

let V, W be VectSp of F_Complex ;
let f be sesquilinear-Form of V,W;
cluster LQForm f -> additiveFAF cmplxhomogeneousFAF ;
coherence

proof end;

cluster RQ*Form f -> additiveFAF additiveSAF homogeneousSAF cmplxhomogeneousFAF ;
coherence

proof end;

end;

definition

let V, W be VectSp of F_Complex ;
let f be sesquilinear-Form of V,W;
func Q*Form f -> sesquilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer (f *' ))) means :Def12: :: HERMITAN:def 12
for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer (f *' )))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *' )) holds
it . [A,B] = f . [v,w];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Q*Form HERMITAN:def 12 :

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

proof end;

end;

registration

let V be non empty right_zeroed VectSpStr of 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

proof end;

end;

theorem Th63: :: HERMITAN:63

for V being non empty VectSpStr of F_Complex
for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)

proof end;

theorem Th64: :: HERMITAN:64

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

proof end;

theorem Th65: :: HERMITAN:65

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

proof end;

theorem Th66: :: HERMITAN:66

for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W holds
( Q*Form f = RQ*Form (LQForm f) & Q*Form f = LQForm (RQ*Form f) )

proof end;

theorem Th67: :: HERMITAN:67

for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W holds
( leftker (Q*Form f) = leftker (RQ*Form (LQForm f)) & rightker (Q*Form f) = rightker (RQ*Form (LQForm f)) & leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )

proof end;

registration

let V, W be VectSp of F_Complex ;
let f be sesquilinear-Form of V,W;
cluster RQ*Form (LQForm f) -> additiveFAF additiveSAF homogeneousSAF non degenerated-on-left non degenerated-on-right cmplxhomogeneousFAF ;
coherence

proof end;

cluster LQForm (RQ*Form f) -> additiveFAF non degenerated-on-left non degenerated-on-right cmplxhomogeneousFAF ;
coherence

proof end;

end;

registration

let V, W be VectSp of F_Complex ;
let f be sesquilinear-Form of V,W;
cluster Q*Form f -> non degenerated-on-left non degenerated-on-right ;
coherence

proof end;

end;

definition

let V be non empty VectSpStr of F_Complex ;
let f be Form of V,V;
attr f 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 :

registration

let V be non empty right_zeroed VectSpStr of F_Complex ;
cluster additiveSAF positivediagvalued -> diagReR+0valued Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

registration

let V be non empty right_zeroed VectSpStr of F_Complex ;
cluster additiveFAF positivediagvalued -> diagReR+0valued Relation of [:the carrier of V,the carrier of V:],the carrier of F_Complex ;
coherence

proof end;

end;

definition

let V be VectSp of F_Complex ;
let f be diagReR+0valued hermitan-Form of V;
func ScalarForm f -> diagReR+0valued hermitan-Form of (VectQuot V,(LKer f)) equals :: HERMITAN:def 14
Q*Form f;
coherence

proof end;

end;

:: deftheorem defines ScalarForm HERMITAN:def 14 :

theorem :: HERMITAN:68

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

proof end;

theorem Th69: :: HERMITAN:69

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

proof end;

theorem Th70: :: HERMITAN:70

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

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

proof end;

end;

registration

let V be non trivial VectSp of F_Complex ;
let f be non constant diagReR+0valued hermitan-Form of V;
cluster ScalarForm f -> non constant non degenerated-on-left non degenerated-on-right diagReR+0valued positivediagvalued ;
coherence ;

end;