let V be VectSp of F_Complex ; for f being diagReR+0valued hermitan-Form of V holds diagker f is linearly-closed
let f be diagReR+0valued hermitan-Form of V; 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
VECTSP_4:def 1 for b1 being Element of the carrier of F_Complex
for b2 being Element of the carrier of V holds
( not b2 in diagker f or b1 * b2 in diagker f )proof
let v,
u be
Element of
V;
( 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
;
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
;
verum
end;
let a be Element of F_Complex; for b1 being Element of the carrier of V holds
( not b1 in diagker f or a * b1 in diagker f )
let v be Element of V; ( not v in diagker f or a * v in diagker f )
assume
v in diagker f
; 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
; verum