let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2
let f be diagReR+0valued hermitan-Form of V; :: thesis: for v, w being Vector of V holds signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2
let v, w be Vector of V; :: thesis: signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2
set v3 = f . (v,v);
set v4 = f . (v,w);
set w1 = f . (w,v);
set w2 = f . (w,w);
set sv = signnorm (f,v);
set sw = signnorm (f,w);
set svw = signnorm (f,(v + w));
A1: 0 <= signnorm (f,v) by Def7;
A2: signnorm (f,(v + w)) = Re (((f . (v,v)) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w)))) by BILINEAR:28
.= (Re ((f . (v,v)) + (f . (v,w)))) + (Re ((f . (w,v)) + (f . (w,w)))) by HAHNBAN1:10
.= ((Re (f . (v,v))) + (Re (f . (v,w)))) + (Re ((f . (w,v)) + (f . (w,w)))) by HAHNBAN1:10
.= ((Re (f . (v,v))) + (Re (f . (v,w)))) + ((Re (f . (w,v))) + (Re (f . (w,w)))) by HAHNBAN1:10
.= ((signnorm (f,v)) + ((Re (f . (v,w))) + (Re (f . (w,v))))) + (signnorm (f,w))
.= ((signnorm (f,v)) + ((Re (f . (v,w))) + (Re ((f . (v,w)) *')))) + (signnorm (f,w)) by Def5
.= ((signnorm (f,v)) + (2 * (Re (f . (v,w))))) + (signnorm (f,w)) by Th15
.= ((signnorm (f,v)) + (signnorm (f,w))) + (2 * (Re (f . (v,w)))) ;
A3: 0 <= signnorm (f,w) by Def7;
0 <= |.(f . (v,w)).| by COMPLEX1:46;
then sqrt (|.(f . (v,w)).| ^2) <= sqrt ((signnorm (f,v)) * (signnorm (f,w))) by Th45, SQUARE_1:26;
then |.(f . (v,w)).| <= sqrt ((signnorm (f,v)) * (signnorm (f,w))) by COMPLEX1:46, SQUARE_1:22;
then ( Re (f . (v,w)) <= |.(f . (v,w)).| & |.(f . (v,w)).| <= (sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))) ) by A1, A3, COMPLEX1:54, SQUARE_1:29;
then Re (f . (v,w)) <= (sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))) by XXREAL_0:2;
then 2 * (Re (f . (v,w))) <= 2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w)))) by XREAL_1:64;
then signnorm (f,(v + w)) <= ((signnorm (f,v)) + (signnorm (f,w))) + (2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))))) by A2, XREAL_1:6;
then signnorm (f,(v + w)) <= (((sqrt (signnorm (f,v))) ^2) + (signnorm (f,w))) + (2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))))) by A1, SQUARE_1:def 2;
then signnorm (f,(v + w)) <= (((sqrt (signnorm (f,v))) ^2) + ((sqrt (signnorm (f,w))) ^2)) + (2 * ((sqrt (signnorm (f,v))) * (sqrt (signnorm (f,w))))) by A3, SQUARE_1:def 2;
hence signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2 ; :: thesis: verum