let X, Y, Z be RealNormSpace; ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )
A1:
the carrier of [:X,Y,Z:] = [: the carrier of X, the carrier of Y, the carrier of Z:]
;
reconsider X0 = X, Y0 = Y, Z0 = Z as RealLinearSpace ;
consider I0 being Function of [:X0,Y0,Z0:],(product <*X0,Y0,Z0*>) such that
A2:
( I0 is one-to-one & I0 is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I0 . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X0,Y0,Z0:] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:X0,Y0,Z0:]
for r being Real holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0,Z0*>) = I0 . (0. [:X0,Y0,Z0:]) )
by Th11;
A3:
product <*X,Y,Z*> = NORMSTR(# (product (carr <*X,Y,Z*>)),(zeros <*X,Y,Z*>),[:(addop <*X,Y,Z*>):],[:(multop <*X,Y,Z*>):],(productnorm <*X,Y,Z*>) #)
by PRVECT_2:6;
then reconsider I = I0 as Function of [:X,Y,Z:],(product <*X,Y,Z*>) ;
take
I
; ( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )
A4a:
for g1, g2 being Point of [:X0,Y0:]
for f1, f2 being Point of Z0 holds (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
proof
let g1,
g2 be
Point of
[:X0,Y0:];
for f1, f2 being Point of Z0 holds (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]let f1,
f2 be
Point of
Z0;
(prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
reconsider gg1 =
g1,
gg2 =
g2 as
Point of
[:X,Y:] ;
reconsider ff1 =
f1,
ff2 =
f2 as
Point of
Z ;
thus (prod_ADD ([:X,Y:],Z)) . (
[g1,f1],
[g2,f2]) =
[(gg1 + gg2),(ff1 + ff2)]
by PRVECT_3:def 1
.=
[(g1 + g2),(f1 + f2)]
;
verum
end;
A5a:
for r being Real
for g being Point of [:X0,Y0:]
for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]
proof
let r be
Real;
for g being Point of [:X0,Y0:]
for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]let g be
Point of
[:X0,Y0:];
for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]let f be
Point of
Z0;
(prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]
reconsider gg =
g as
Point of
[:X,Y:] ;
reconsider ff =
f as
Point of
Z ;
thus (prod_MLT ([:X,Y:],Z)) . (
r,
[g,f]) =
[(r * gg),(r * ff)]
by PRVECT_3:def 2
.=
[(r * g),(r * f)]
;
verum
end;
thus
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) )
by A2, A3; ( ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )
thus
0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:])
by A2, A3; for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||
for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||
proof
let v be
Point of
[:X,Y,Z:];
||.(I . v).|| = ||.v.||
consider x1 being
Point of
X,
y1 being
Point of
Y,
z1 being
Point of
Z such that A6:
v = [x1,y1,z1]
by Lm1, A1;
consider v10 being
Element of
REAL 2
such that A7:
(
v10 = <*||.[x1,y1].||,||.z1.||*> &
(prod_NORM ([:X,Y:],Z)) . (
[x1,y1],
z1)
= |.v10.| )
by PRVECT_3:def 6;
consider v20 being
Element of
REAL 2
such that A8:
(
v20 = <*||.x1.||,||.y1.||*> &
(prod_NORM (X,Y)) . (
x1,
y1)
= |.v20.| )
by PRVECT_3:def 6;
reconsider v1 =
<*||.x1.||,||.y1.||,||.z1.||*> as
Element of
REAL 3
by FINSEQ_2:104;
A10:
0 <= Sum (sqr v20)
by RVSUM_1:86;
A11:
||.[x1,y1].|| ^2 =
Sum (sqr v20)
by A10, SQUARE_1:def 2, A8
.=
Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*>
by A8, TOPREAL6:11
.=
(||.x1.|| ^2) + (||.y1.|| ^2)
by RVSUM_1:77
;
A12:
Sum (sqr v10) =
Sum <*(||.[x1,y1].|| ^2),(||.z1.|| ^2)*>
by TOPREAL6:11, A7
.=
((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.z1.|| ^2)
by A11, RVSUM_1:77
.=
Sum (sqr v1)
by BORSUK_7:17
;
A13:
|.v10.| = |.v1.|
by A12;
A14:
I . v =
I . (
x1,
y1,
z1)
by A6
.=
<*x1,y1,z1*>
by A2
;
reconsider Iv =
I . v as
Element of
product (carr <*X,Y,Z*>) by A3;
dom <*X,Y,Z*> =
Seg (len <*X,Y,Z*>)
by FINSEQ_1:def 3
.=
{1,2,3}
by FINSEQ_1:45, FINSEQ_3:1
;
then reconsider j1 = 1,
j2 = 2,
j3 = 3 as
Element of
dom <*X,Y,Z*> by ENUMSET1:def 1;
A17:
(normsequence (<*X,Y,Z*>,Iv)) . j1 =
the
normF of
(<*X,Y,Z*> . j1) . (Iv . j1)
by PRVECT_2:def 11
.=
||.x1.||
by A14
;
A18:
(normsequence (<*X,Y,Z*>,Iv)) . j2 =
the
normF of
(<*X,Y,Z*> . j2) . (Iv . j2)
by PRVECT_2:def 11
.=
||.y1.||
by A14
;
A19:
(normsequence (<*X,Y,Z*>,Iv)) . j3 =
the
normF of
(<*X,Y,Z*> . j3) . (Iv . j3)
by PRVECT_2:def 11
.=
||.z1.||
by A14
;
len (normsequence (<*X,Y,Z*>,Iv)) =
len <*X,Y,Z*>
by PRVECT_2:def 11
.=
3
by FINSEQ_1:45
;
then
normsequence (
<*X,Y,Z*>,
Iv)
= v1
by A17, A18, A19, FINSEQ_1:45;
hence
||.(I . v).|| = ||.v.||
by A13, A7, A6, A3, PRVECT_2:def 12;
verum
end;
hence
for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||
; verum