set q = quasinorm f;
thus
quasinorm f is subadditive
quasinorm f is homogeneous proof
let v,
w be
Vector of
V;
HAHNBAN1:def 11 (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);
A1:
(quasinorm f) . v = sqrt (signnorm (f,v))
by Def10;
0 <= Re (f . (v,v))
by Def7;
then A2:
0 <= (quasinorm f) . v
by A1, SQUARE_1:def 2;
A3:
(quasinorm f) . w = sqrt (signnorm (f,w))
by Def10;
0 <= Re (f . (w,w))
by Def7;
then A4:
0 <= (quasinorm f) . w
by A3, SQUARE_1:def 2;
(
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 A1, A3, Th47, SQUARE_1:26;
hence
(quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w)
by A2, A4, SQUARE_1:22;
verum
end;
let v be Vector of V; HAHNBAN1:def 14 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)
A5:
( 0 <= |.r.| ^2 & 0 <= Re (f . (v,v)) )
by Def7, XREAL_1:63;
A6: f . ((r * v),(r * v)) =
r * (f . (v,(r * v)))
by BILINEAR:31
.=
r * ((r *') * (f . (v,v)))
by Th27
.=
(r * (r *')) * (f . (v,v))
.=
[**(|.r.| ^2),0**] * (f . (v,v))
by Th13
.=
[**(|.r.| ^2),0**] * [**(Re (f . (v,v))),(Im (f . (v,v)))**]
by COMPLEX1:13
.=
[**(|.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 A6, COMPLEX1:12
.=
(sqrt (|.r.| ^2)) * (sqrt (Re (f . (v,v))))
by A5, SQUARE_1:29
.=
|.r.| * (sqrt (signnorm (f,v)))
by COMPLEX1:46, SQUARE_1:22
.=
|.r.| * ((quasinorm f) . v)
by Def10
; verum