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: signnorm f,(v + w) = Re (((f . v,v) + (f . v,w)) + ((f . w,v) + (f . w,w))) by BILINEAR:29
.= (Re ((f . v,v) + (f . v,w))) + (Re ((f . w,v) + (f . w,w))) by HAHNBAN1:16
.= ((Re (f . v,v)) + (Re (f . v,w))) + (Re ((f . w,v) + (f . w,w))) by HAHNBAN1:16
.= ((Re (f . v,v)) + (Re (f . v,w))) + ((Re (f . w,v)) + (Re (f . w,w))) by HAHNBAN1:16
.= ((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 Th18
.= ((signnorm f,v) + (signnorm f,w)) + (2 * (Re (f . v,w))) ;
A2: Re (f . v,w) <= |.(f . v,w).| by COMPLEX1:140;
0 <= |.(f . v,w).| by COMPLEX1:132;
then A3: 0 <= |.(f . v,w).| * |.(f . v,w).| ;
A4: ( 0 <= signnorm f,v & 0 <= signnorm f,w ) by Def7;
sqrt (|.(f . v,w).| ^2 ) <= sqrt ((signnorm f,v) * (signnorm f,w)) by A3, Th48, SQUARE_1:94;
then |.(f . v,w).| <= sqrt ((signnorm f,v) * (signnorm f,w)) by COMPLEX1:132, SQUARE_1:89;
then |.(f . v,w).| <= (sqrt (signnorm f,v)) * (sqrt (signnorm f,w)) by A4, SQUARE_1:97;
then Re (f . v,w) <= (sqrt (signnorm f,v)) * (sqrt (signnorm f,w)) by A2, XXREAL_0:2;
then 2 * (Re (f . v,w)) <= 2 * ((sqrt (signnorm f,v)) * (sqrt (signnorm f,w))) by XREAL_1:66;
then signnorm f,(v + w) <= ((signnorm f,v) + (signnorm f,w)) + (2 * ((sqrt (signnorm f,v)) * (sqrt (signnorm f,w)))) by A1, XREAL_1:8;
then signnorm f,(v + w) <= (((sqrt (signnorm f,v)) ^2 ) + (signnorm f,w)) + (2 * ((sqrt (signnorm f,v)) * (sqrt (signnorm f,w)))) by A4, SQUARE_1:def 4;
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 A4, SQUARE_1:def 4;
hence signnorm f,(v + w) <= ((sqrt (signnorm f,v)) + (sqrt (signnorm f,w))) ^2 ; :: thesis: verum