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

let f be diagReR+0valued hermitan-Form of V; :: thesis: leftker (ScalarForm f) = leftker (Q*Form f)

set vq = VectQuot (V,(LKer f));

set vr = VectQuot (V,(RKer (f *')));

set qf = Q*Form f;

set qhf = ScalarForm f;

set K = F_Complex ;

thus leftker (ScalarForm f) c= leftker (Q*Form f) :: according to XBOOLE_0:def 10 :: thesis: leftker (Q*Form f) c= leftker (ScalarForm f)

assume x in leftker (Q*Form f) ; :: thesis: x in leftker (ScalarForm f)

then consider A being Vector of (VectQuot (V,(LKer f))) such that

A3: x = A and

A4: for B being Vector of (VectQuot (V,(RKer (f *')))) holds (Q*Form f) . (A,B) = 0. F_Complex ;

let f be diagReR+0valued hermitan-Form of V; :: thesis: leftker (ScalarForm f) = leftker (Q*Form f)

set vq = VectQuot (V,(LKer f));

set vr = VectQuot (V,(RKer (f *')));

set qf = Q*Form f;

set qhf = ScalarForm f;

set K = F_Complex ;

thus leftker (ScalarForm f) c= leftker (Q*Form f) :: according to XBOOLE_0:def 10 :: thesis: leftker (Q*Form f) c= leftker (ScalarForm f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (Q*Form f) or x in leftker (ScalarForm f) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (ScalarForm f) or x in leftker (Q*Form f) )

assume x in leftker (ScalarForm f) ; :: thesis: x in leftker (Q*Form f)

then consider A being Vector of (VectQuot (V,(LKer f))) such that

A1: x = A and

A2: for B being Vector of (VectQuot (V,(LKer f))) holds (ScalarForm f) . (A,B) = 0. F_Complex ;

end;assume x in leftker (ScalarForm f) ; :: thesis: x in leftker (Q*Form f)

then consider A being Vector of (VectQuot (V,(LKer f))) such that

A1: x = A and

A2: for B being Vector of (VectQuot (V,(LKer f))) holds (ScalarForm f) . (A,B) = 0. F_Complex ;

now :: thesis: for B being Vector of (VectQuot (V,(RKer (f *')))) holds (Q*Form f) . (A,B) = 0. F_Complex

hence
x in leftker (Q*Form f)
by A1; :: thesis: verumlet B be Vector of (VectQuot (V,(RKer (f *')))); :: thesis: (Q*Form f) . (A,B) = 0. F_Complex

reconsider w = B as Vector of (VectQuot (V,(LKer f))) by Th56;

thus (Q*Form f) . (A,B) = (ScalarForm f) . (A,w)

.= 0. F_Complex by A2 ; :: thesis: verum

end;reconsider w = B as Vector of (VectQuot (V,(LKer f))) by Th56;

thus (Q*Form f) . (A,B) = (ScalarForm f) . (A,w)

.= 0. F_Complex by A2 ; :: thesis: verum

assume x in leftker (Q*Form f) ; :: thesis: x in leftker (ScalarForm f)

then consider A being Vector of (VectQuot (V,(LKer f))) such that

A3: x = A and

A4: for B being Vector of (VectQuot (V,(RKer (f *')))) holds (Q*Form f) . (A,B) = 0. F_Complex ;

now :: thesis: for B being Vector of (VectQuot (V,(LKer f))) holds (ScalarForm f) . (A,B) = 0. F_Complex

hence
x in leftker (ScalarForm f)
by A3; :: thesis: verumlet B be Vector of (VectQuot (V,(LKer f))); :: thesis: (ScalarForm f) . (A,B) = 0. F_Complex

reconsider w = B as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

thus (ScalarForm f) . (A,B) = (Q*Form f) . (A,w)

.= 0. F_Complex by A4 ; :: thesis: verum

end;reconsider w = B as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

thus (ScalarForm f) . (A,B) = (Q*Form f) . (A,w)

.= 0. F_Complex by A4 ; :: thesis: verum