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

let f be diagReR+0valued hermitan-Form of V; :: thesis: diagker f is linearly-closed

set V1 = diagker f;

thus for v, u being Element of V st v in diagker f & u in diagker f holds

v + u in diagker f :: according to VECTSP_4:def 1 :: thesis: for b_{1} being Element of the carrier of F_Complex

for b_{2} being Element of the carrier of V holds

( not b_{2} in diagker f or b_{1} * b_{2} in diagker f )_{1} being Element of the carrier of V holds

( not b_{1} in diagker f or a * b_{1} in diagker f )

let v be Element of V; :: thesis: ( not v in diagker f or a * v in diagker f )

assume v in diagker f ; :: thesis: a * v in diagker f

then A7: ex w being Vector of V st

( w = v & f . (w,w) = 0. F_Complex ) ;

f . ((a * v),(a * v)) = a * (f . (v,(a * v))) by BILINEAR:31

.= a * ((a *') * (0. F_Complex)) by A7, Th27

.= 0. F_Complex ;

hence a * v in diagker f ; :: thesis: verum

let f be diagReR+0valued hermitan-Form of V; :: thesis: diagker f is linearly-closed

set V1 = diagker f;

thus for v, u being Element of V st v in diagker f & u in diagker f holds

v + u in diagker f :: according to VECTSP_4:def 1 :: thesis: for b

for b

( not b

proof

let a be Element of F_Complex; :: thesis: for b
let v, u be Element of V; :: thesis: ( v in diagker f & u in diagker f implies v + u in diagker f )

assume that

A1: v in diagker f and

A2: u in diagker f ; :: thesis: v + u in diagker f

A3: ex b being Vector of V st

( b = u & f . (b,b) = 0. F_Complex ) by A2;

then |.(f . (v,u)).| ^2 <= |.(f . (v,v)).| * 0 by Th46, COMPLFLD:57;

then A4: |.(f . (v,u)).| = 0 by XREAL_1:63;

then 0 = |.((f . (v,u)) *').| by COMPLEX1:53

.= |.(f . (u,v)).| by Def5 ;

then A5: f . (u,v) = 0. F_Complex by COMPLFLD:58;

ex a being Vector of V st

( a = v & f . (a,a) = 0. F_Complex ) by A1;

then A6: f . ((v + u),(v + u)) = ((0. F_Complex) + (f . (v,u))) + ((f . (u,v)) + (0. F_Complex)) by A3, BILINEAR:28

.= (f . (v,u)) + ((f . (u,v)) + (0. F_Complex)) by RLVECT_1:4

.= (f . (v,u)) + (f . (u,v)) by RLVECT_1:4 ;

f . (v,u) = 0. F_Complex by A4, COMPLFLD:58;

then f . ((v + u),(v + u)) = 0. F_Complex by A6, A5, RLVECT_1:4;

hence v + u in diagker f ; :: thesis: verum

end;assume that

A1: v in diagker f and

A2: u in diagker f ; :: thesis: v + u in diagker f

A3: ex b being Vector of V st

( b = u & f . (b,b) = 0. F_Complex ) by A2;

then |.(f . (v,u)).| ^2 <= |.(f . (v,v)).| * 0 by Th46, COMPLFLD:57;

then A4: |.(f . (v,u)).| = 0 by XREAL_1:63;

then 0 = |.((f . (v,u)) *').| by COMPLEX1:53

.= |.(f . (u,v)).| by Def5 ;

then A5: f . (u,v) = 0. F_Complex by COMPLFLD:58;

ex a being Vector of V st

( a = v & f . (a,a) = 0. F_Complex ) by A1;

then A6: f . ((v + u),(v + u)) = ((0. F_Complex) + (f . (v,u))) + ((f . (u,v)) + (0. F_Complex)) by A3, BILINEAR:28

.= (f . (v,u)) + ((f . (u,v)) + (0. F_Complex)) by RLVECT_1:4

.= (f . (v,u)) + (f . (u,v)) by RLVECT_1:4 ;

f . (v,u) = 0. F_Complex by A4, COMPLFLD:58;

then f . ((v + u),(v + u)) = 0. F_Complex by A6, A5, RLVECT_1:4;

hence v + u in diagker f ; :: thesis: verum

( not b

let v be Element of V; :: thesis: ( not v in diagker f or a * v in diagker f )

assume v in diagker f ; :: thesis: a * v in diagker f

then A7: ex w being Vector of V st

( w = v & f . (w,w) = 0. F_Complex ) ;

f . ((a * v),(a * v)) = a * (f . (v,(a * v))) by BILINEAR:31

.= a * ((a *') * (0. F_Complex)) by A7, Th27

.= 0. F_Complex ;

hence a * v in diagker f ; :: thesis: verum