set q = quasinorm f;
A1:
quasinorm f is subadditive
proof
let v,
w be
Vector of
V;
:: according to HAHNBAN1:def 16 :: thesis: (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:
(
signnorm f,
(v + w) = Re (f . (v + w),(v + w)) &
0 <= Re (f . (v + w),(v + w)) &
(quasinorm f) . (v + w) = sqrt (signnorm f,(v + w)) &
signnorm f,
v = Re (f . v,v) &
0 <= Re (f . v,v) &
(quasinorm f) . v = sqrt (signnorm f,v) &
signnorm f,
w = Re (f . w,w) &
0 <= Re (f . w,w) &
(quasinorm f) . w = sqrt (signnorm f,w) )
by Def7, Def10;
then
(
0 <= (quasinorm f) . v &
0 <= (quasinorm f) . w )
by SQUARE_1:def 4;
then A3:
0 + 0 <= ((quasinorm f) . v) + ((quasinorm f) . w)
;
(quasinorm f) . (v + w) <= sqrt ((((quasinorm f) . v) + ((quasinorm f) . w)) ^2 )
by A2, Th50, SQUARE_1:94;
hence
(quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w)
by A3, SQUARE_1:89;
:: thesis: verum
end;
quasinorm f is homogeneous
proof
let v be
Vector of
V;
:: according to HAHNBAN1:def 19 :: thesis: for b1 being Element of the carrier of F_Complex holds (quasinorm f) . (b1 * v) = |.b1.| * ((quasinorm f) . v)let r be
Scalar of ;
:: thesis: (quasinorm f) . (r * v) = |.r.| * ((quasinorm f) . v)
A4:
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 **]
;
A5:
(
0 <= |.r.| ^2 &
0 <= |.r.| &
0 <= Re (f . v,v) )
by Def7, COMPLEX1:132, XREAL_1:65;
thus (quasinorm f) . (r * v) =
sqrt (signnorm f,(r * v))
by Def10
.=
sqrt ((|.r.| ^2 ) * (Re (f . v,v)))
by A4, COMPLEX1:28
.=
(sqrt (|.r.| ^2 )) * (sqrt (Re (f . v,v)))
by A5, SQUARE_1:97
.=
|.r.| * (sqrt (signnorm f,v))
by A5, SQUARE_1:89
.=
|.r.| * ((quasinorm f) . v)
by Def10
;
:: thesis: verum
end;
hence
quasinorm f is Semi-Norm of V
by A1; :: thesis: verum