set q = quasinorm f;
A1:
quasinorm f is subadditive
proof
let v,
w be
Vector of
V;
HAHNBAN1:def 16 (quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w)
set fvw =
signnorm f,
(v + w);
set fv =
signnorm f,
v;
set fw =
signnorm f,
w;
A2:
(quasinorm f) . v = sqrt (signnorm f,v)
by Def10;
0 <= Re (f . v,v)
by Def7;
then A3:
0 <= (quasinorm f) . v
by A2, SQUARE_1:def 4;
A4:
(quasinorm f) . w = sqrt (signnorm f,w)
by Def10;
0 <= Re (f . w,w)
by Def7;
then A5:
0 <= (quasinorm f) . w
by A4, SQUARE_1:def 4;
(
0 <= Re (f . (v + w),(v + w)) &
(quasinorm f) . (v + w) = sqrt (signnorm f,(v + w)) )
by Def7, Def10;
then
(quasinorm f) . (v + w) <= sqrt ((((quasinorm f) . v) + ((quasinorm f) . w)) ^2 )
by A2, A4, Th50, SQUARE_1:94;
hence
(quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w)
by A3, A5, SQUARE_1:89;
verum
end;
quasinorm f is homogeneous
proof
let v be
Vector of
V;
HAHNBAN1:def 19 for b1 being Element of the carrier of F_Complex holds (quasinorm f) . (b1 * v) = |.b1.| * ((quasinorm f) . v)let r be
Scalar of ;
(quasinorm f) . (r * v) = |.r.| * ((quasinorm f) . v)
A6:
(
0 <= |.r.| ^2 &
0 <= Re (f . v,v) )
by Def7, XREAL_1:65;
A7:
f . (r * v),
(r * v) =
r * (f . v,(r * v))
by BILINEAR:32
.=
r * ((r *' ) * (f . v,v))
by Th30
.=
(r * (r *' )) * (f . v,v)
.=
[**(|.r.| ^2 ),0 **] * (f . v,v)
by Th16
.=
[**(|.r.| ^2 ),0 **] * [**(Re (f . v,v)),(Im (f . v,v))**]
by COMPLEX1:29
.=
[**(|.r.| ^2 ),0 **] * [**(Re (f . v,v)),0 **]
by Def6
.=
[**((|.r.| ^2 ) * (Re (f . v,v))),0 **]
;
thus (quasinorm f) . (r * v) =
sqrt (signnorm f,(r * v))
by Def10
.=
sqrt ((|.r.| ^2 ) * (Re (f . v,v)))
by A7, COMPLEX1:28
.=
(sqrt (|.r.| ^2 )) * (sqrt (Re (f . v,v)))
by A6, SQUARE_1:97
.=
|.r.| * (sqrt (signnorm f,v))
by COMPLEX1:132, SQUARE_1:89
.=
|.r.| * ((quasinorm f) . v)
by Def10
;
verum
end;
hence
quasinorm f is Semi-Norm of V
by A1; verum