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)

proof

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 ;

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

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

hence x in leftker (Q*Form f) by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (Q*Form f) or x in 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 ;

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

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

hence x in leftker (ScalarForm f) by A3; :: thesis: verum