let X, Y be RealNormSpace; ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
reconsider X0 = X, Y0 = Y as RealLinearSpace ;
consider I0 being Function of [:X0,Y0:],(product <*X0,Y0*>) such that
A1:
( I0 is one-to-one & I0 is onto & ( for x being Point of X
for y being Point of Y holds I0 . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X0,Y0:] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:X0,Y0:]
for r being Real holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0*>) = I0 . (0. [:X0,Y0:]) )
by Th12;
A2:
product <*X,Y*> = NORMSTR(# (product (carr <*X,Y*>)),(zeros <*X,Y*>),[:(addop <*X,Y*>):],[:(multop <*X,Y*>):],(productnorm <*X,Y*>) #)
by PRVECT_2:6;
then reconsider I = I0 as Function of [:X,Y:],(product <*X,Y*>) ;
take
I
; ( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
thus
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> ) )
by A1, A2; ( ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
thus
for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)
( ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )proof
let v,
w be
Point of
[:X,Y:];
I . (v + w) = (I . v) + (I . w)
reconsider v0 =
v,
w0 =
w as
Point of
[:X0,Y0:] ;
thus I . (v + w) =
I0 . (v0 + w0)
.=
(I0 . v0) + (I0 . w0)
by A1
.=
(I . v) + (I . w)
by A2
;
verum
end;
thus
for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v)
( 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
thus
0. (product <*X,Y*>) = I . (0. [:X,Y:])
by A1, A2; for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.||
for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.||
proof
let v be
Point of
[:X,Y:];
||.(I . v).|| = ||.v.||
consider x1 being
Point of
X,
y1 being
Point of
Y such that A3:
v = [x1,y1]
by Lm1;
consider v1 being
Element of
REAL 2
such that A4:
(
v1 = <*||.x1.||,||.y1.||*> &
(prod_NORM (X,Y)) . (
x1,
y1)
= |.v1.| )
by Def6;
A5:
I . v =
I . (
x1,
y1)
by A3
.=
<*x1,y1*>
by A1
;
reconsider Iv =
I . v as
Element of
product (carr <*X,Y*>) by A2;
A6:
(
<*x1,y1*> . 1
= x1 &
<*x1,y1*> . 2
= y1 )
by FINSEQ_1:44;
( 1
in {1,2} & 2
in {1,2} )
by TARSKI:def 2;
then reconsider j1 = 1,
j2 = 2 as
Element of
dom <*X,Y*> by FINSEQ_1:2, FINSEQ_1:89;
A7:
(normsequence (<*X,Y*>,Iv)) . j1 =
the
normF of
(<*X,Y*> . j1) . (Iv . j1)
by PRVECT_2:def 11
.=
||.x1.||
by A5, A6, FINSEQ_1:44
;
A8:
(normsequence (<*X,Y*>,Iv)) . j2 =
the
normF of
(<*X,Y*> . j2) . (Iv . j2)
by PRVECT_2:def 11
.=
||.y1.||
by A5, A6, FINSEQ_1:44
;
len (normsequence (<*X,Y*>,Iv)) =
len <*X,Y*>
by PRVECT_2:def 11
.=
2
by FINSEQ_1:44
;
then
normsequence (
<*X,Y*>,
Iv)
= v1
by A4, A7, A8, FINSEQ_1:44;
hence
||.(I . v).|| = ||.v.||
by A4, A3, A2, PRVECT_2:def 12;
verum
end;
hence
for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.||
; verum