let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V holds diagker f = rightker f

let f be diagReR+0valued hermitan-Form of V; :: thesis: diagker f = rightker f

thus diagker f c= rightker f :: according to XBOOLE_0:def 10 :: thesis: rightker f c= diagker f

let f be diagReR+0valued hermitan-Form of V; :: thesis: diagker f = rightker f

thus diagker f c= rightker f :: according to XBOOLE_0:def 10 :: thesis: rightker f c= diagker f

proof

thus
rightker f c= diagker f
by BILINEAR:41; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in diagker f or x in rightker f )

assume x in diagker f ; :: thesis: x in rightker f

then consider a being Vector of V such that

A1: a = x and

A2: f . (a,a) = 0. F_Complex ;

end;assume x in diagker f ; :: thesis: x in rightker f

then consider a being Vector of V such that

A1: a = x and

A2: f . (a,a) = 0. F_Complex ;

now :: thesis: for w being Vector of V holds f . (w,a) = 0. F_Complex

hence
x in rightker f
by A1; :: thesis: verumlet w be Vector of V; :: thesis: f . (w,a) = 0. F_Complex

|.(f . (w,a)).| ^2 <= |.(f . (w,w)).| * 0 by A2, Th46, COMPLFLD:57;

then |.(f . (w,a)).| = 0 by XREAL_1:63;

hence f . (w,a) = 0. F_Complex by COMPLFLD:58; :: thesis: verum

end;|.(f . (w,a)).| ^2 <= |.(f . (w,w)).| * 0 by A2, Th46, COMPLFLD:57;

then |.(f . (w,a)).| = 0 by XREAL_1:63;

hence f . (w,a) = 0. F_Complex by COMPLFLD:58; :: thesis: verum