let X be RealNormSpace; ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
reconsider X0 = X as RealLinearSpace ;
consider I0 being Function of X0,(product <*X0*>) such that
A1:
( I0 is one-to-one & I0 is onto & ( for x being Point of X holds I0 . x = <*x*> ) & ( for v, w being Point of X0 holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of X0
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0*>) = I0 . (0. X0) )
by Th11;
A2:
product <*X*> = NORMSTR(# (product (carr <*X*>)),(zeros <*X*>),[:(addop <*X*>):],[:(multop <*X*>):],(productnorm <*X*>) #)
by PRVECT_2:6;
then reconsider I = I0 as Function of X,(product <*X*>) ;
take
I
; ( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
thus
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) )
by A1, A2; ( ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
thus
for v, w being Point of X holds I . (v + w) = (I . v) + (I . w)
( ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )proof
let v,
w be
Point of
X;
I . (v + w) = (I . v) + (I . w)
reconsider v0 =
v,
w0 =
w as
Point of
X0 ;
thus I . (v + w) =
(I0 . v0) + (I0 . w0)
by A1
.=
(I . v) + (I . w)
by A2
;
verum
end;
thus
for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v)
( 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
thus
0. (product <*X*>) = I . (0. X)
by A1, A2; for v being Point of X holds ||.(I . v).|| = ||.v.||
thus
for v being Point of X holds ||.(I . v).|| = ||.v.||
verumproof
let v be
Point of
X;
||.(I . v).|| = ||.v.||
A3:
len <*||.v.||*> = 1
by FINSEQ_1:40;
reconsider vv =
||.v.|| as
Element of
REAL ;
reconsider v1 =
<*vv*> as
Element of
REAL 1
by FINSEQ_2:92, A3;
reconsider v2 =
||.v.|| ^2 as
Real ;
A4:
|.v1.| =
sqrt (Sum <*v2*>)
by RVSUM_1:55
.=
sqrt (||.v.|| ^2)
by RVSUM_1:73
.=
||.v.||
by NORMSP_1:4, SQUARE_1:22
;
A5:
I . v = <*v*>
by A1;
reconsider Iv =
I . v as
Element of
product (carr <*X*>) by A2;
A6:
<*v*> . 1
= v
by FINSEQ_1:40;
1
in {1}
by TARSKI:def 1;
then reconsider j1 = 1 as
Element of
dom <*X*> by FINSEQ_1:2, FINSEQ_1:def 8;
A7:
(normsequence (<*X*>,Iv)) . j1 =
the
normF of
(<*X*> . j1) . (Iv . j1)
by PRVECT_2:def 11
.=
||.v.||
by A5, A6, FINSEQ_1:40
;
len (normsequence (<*X*>,Iv)) =
len <*X*>
by PRVECT_2:def 11
.=
1
by FINSEQ_1:40
;
then
normsequence (
<*X*>,
Iv)
= v1
by A7, FINSEQ_1:40;
hence
||.(I . v).|| = ||.v.||
by A4, A2, PRVECT_2:def 12;
verum
end;