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

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

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

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

then consider a being Vector of V such that

A3: a = x and

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

f . (a,a) = 0. F_Complex by A4;

hence x in diagker f by A3; :: thesis: verum

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

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker f or x in diagker f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in diagker f or x in leftker f )

assume x in diagker f ; :: thesis: x in leftker 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 leftker 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 . (a,w) = 0. F_Complex

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

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

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

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

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

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

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

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

then consider a being Vector of V such that

A3: a = x and

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

f . (a,a) = 0. F_Complex by A4;

hence x in diagker f by A3; :: thesis: verum