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 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;
:: thesis: ( v in diagker f & u in diagker f implies v + u in diagker f )
assume A1:
(
v in diagker f &
u in diagker f )
;
:: thesis: v + u in diagker f
then consider a being
Vector of
V such that A2:
(
a = v &
f . a,
a = 0. F_Complex )
;
consider b being
Vector of
V such that A3:
(
b = u &
f . b,
b = 0. F_Complex )
by A1;
A4:
f . (v + u),
(v + u) =
((0. F_Complex ) + (f . v,u)) + ((f . u,v) + (0. F_Complex ))
by A2, A3, BILINEAR:29
.=
(f . v,u) + ((f . u,v) + (0. F_Complex ))
by RLVECT_1:10
.=
(f . v,u) + (f . u,v)
by RLVECT_1:10
;
(
|.(f . v,u).| ^2 <= |.(f . v,v).| * 0 &
0 <= |.(f . v,u).| ^2 )
by A3, Th49, COMPLFLD:93, XREAL_1:65;
then
|.(f . v,u).| ^2 = 0
;
then A5:
|.(f . v,u).| = 0
;
then A6:
f . v,
u = 0. F_Complex
by COMPLFLD:94;
0 =
|.((f . v,u) *' ).|
by A5, COMPLEX1:139
.=
|.(f . u,v).|
by Def5
;
then
f . u,
v = 0. F_Complex
by COMPLFLD:94;
then
f . (v + u),
(v + u) = 0. F_Complex
by A4, A6, RLVECT_1:10;
hence
v + u in diagker f
;
:: thesis: verum
end;
let a be Element of F_Complex ; :: thesis: 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; :: thesis: ( not v in diagker f or a * v in diagker f )
assume
v in diagker f
; :: thesis: a * v in diagker f
then consider w being Vector of V such that
A7:
( w = v & f . w,w = 0. F_Complex )
;
f . (a * v),(a * v) =
a * (f . v,(a * v))
by BILINEAR:32
.=
a * ((a *' ) * (0. F_Complex ))
by A7, Th30
.=
a * (0. F_Complex )
by VECTSP_1:36
.=
0. F_Complex
by VECTSP_1:36
;
hence
a * v in diagker f
; :: thesis: verum