let X, Y be RealNormSpace-Sequence; ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
reconsider X0 = X, Y0 = Y as RealLinearSpace-Sequence ;
set PX = product X;
set PY = product Y;
set PX0 = product X0;
set PY0 = product Y0;
reconsider CX = carr X, CY = carr Y as non-empty non empty FinSequence ;
reconsider CX0 = carr X0, CY0 = carr Y0 as non-empty non empty FinSequence ;
A1:
( product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) & product Y = NORMSTR(# (product (carr Y)),(zeros Y),[:(addop Y):],[:(multop Y):],(productnorm Y) #) )
by PRVECT_2:6;
A2:
for g1, g2 being Point of (product X)
for f1, f2 being Point of (product Y) holds (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
proof
let g1,
g2 be
Point of
(product X);
for f1, f2 being Point of (product Y) holds (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]let f1,
f2 be
Point of
(product Y);
(prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
reconsider g10 =
g1,
g20 =
g2 as
Point of
(product X0) by A1;
reconsider f10 =
f1,
f20 =
f2 as
Point of
(product Y0) by A1;
(
g10 + g20 = g1 + g2 &
f10 + f20 = f1 + f2 )
by A1;
hence
(prod_ADD ((product X0),(product Y0))) . (
[g1,f1],
[g2,f2])
= [(g1 + g2),(f1 + f2)]
by Def1;
verum
end;
A3:
for r being Real
for g being Point of (product X)
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
proof
let r be
Real;
for g being Point of (product X)
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]let g be
Point of
(product X);
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]let f be
Point of
(product Y);
(prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
reconsider g0 =
g as
Point of
(product X0) by A1;
reconsider f0 =
f as
Point of
(product Y0) by A1;
(
r * g0 = r * g &
r * f0 = r * f )
by A1;
hence
(prod_MLT ((product X0),(product Y0))) . (
r,
[g,f])
= [(r * g),(r * f)]
by Def2;
verum
end;
A4:
( len (carr (X ^ Y)) = len (X ^ Y) & len (carr (X0 ^ Y0)) = len (X0 ^ Y0) & len CX = len X & len CY = len Y & len CX0 = len X0 & len CY0 = len Y0 )
by PRVECT_1:def 11;
consider I0 being Function of [:(product X0),(product Y0):],(product (X0 ^ Y0)) such that
A5:
( I0 is one-to-one & I0 is onto & ( for x being Point of (product X0)
for y being Point of (product Y0) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I0 . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X0),(product Y0):] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:(product X0),(product Y0):]
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product (X0 ^ Y0)) = I0 . (0. [:(product X0),(product Y0):]) )
by Th13;
A6:
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 [:(product X),(product Y):],(product (X ^ Y)) by A1;
take
I
; ( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
thus
( I is one-to-one & I is onto )
by A5, A6; ( ( for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
thus
for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )
by A1, A5; ( ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
A7:
for x, y being FinSequence st x in the carrier of (product X) & y in the carrier of (product Y) holds
I . (x,y) = x ^ y
thus
for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w)
( ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
thus
for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v)
( I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
thus
0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):])
by A1, A5, A6; for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||
for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||
proof
let v be
Point of
[:(product X),(product Y):];
||.(I . v).|| = ||.v.||
consider x1 being
Point of
(product X),
y1 being
Point of
(product Y) such that A8:
v = [x1,y1]
by Lm1;
consider v1 being
Element of
REAL 2
such that A9:
(
v1 = <*||.x1.||,||.y1.||*> &
(prod_NORM ((product X),(product Y))) . (
x1,
y1)
= |.v1.| )
by Def6;
reconsider Ix1 =
x1,
Iy1 =
y1 as
FinSequence by A1, Lm2;
A10:
(
dom Ix1 = dom (carr X) &
dom Iy1 = dom (carr Y) )
by A1, CARD_3:9;
A11:
I . v =
I . (
x1,
y1)
by A8
.=
Ix1 ^ Iy1
by A7
;
reconsider Iv =
I . v as
Element of
product (carr (X ^ Y)) by A6;
reconsider Ix =
x1 as
Element of
product (carr X) by A1;
reconsider Iy =
y1 as
Element of
product (carr Y) by A1;
A12:
||.(I . v).|| =
|.(normsequence ((X ^ Y),Iv)).|
by A6, PRVECT_2:def 12
.=
sqrt (Sum (sqr (normsequence ((X ^ Y),Iv))))
;
A13:
(
len (normsequence ((X ^ Y),Iv)) = len (X ^ Y) &
len (normsequence (X,Ix)) = len X &
len (normsequence (Y,Iy)) = len Y )
by PRVECT_2:def 11;
reconsider x12 =
||.x1.|| ^2 ,
y12 =
||.y1.|| ^2 as
Real ;
A14:
|.v1.| =
sqrt (Sum <*x12,y12*>)
by A9, TOPREAL6:11
.=
sqrt ((||.x1.|| ^2) + (||.y1.|| ^2))
by RVSUM_1:77
;
A15:
(
0 <= Sum (sqr (normsequence (X,Ix))) &
0 <= Sum (sqr (normsequence (Y,Iy))) )
by RVSUM_1:86;
(
||.x1.|| ^2 = |.(normsequence (X,Ix)).| ^2 &
||.y1.|| ^2 = |.(normsequence (Y,Iy)).| ^2 )
by A1, PRVECT_2:def 12;
then A16:
(
||.x1.|| ^2 = Sum (sqr (normsequence (X,Ix))) &
||.y1.|| ^2 = Sum (sqr (normsequence (Y,Iy))) )
by A15, SQUARE_1:def 2;
len (normsequence ((X ^ Y),Iv)) =
(len (normsequence (X,Ix))) + (len (normsequence (Y,Iy)))
by A13, FINSEQ_1:22
.=
len ((normsequence (X,Ix)) ^ (normsequence (Y,Iy)))
by FINSEQ_1:22
;
then A17:
dom (normsequence ((X ^ Y),Iv)) = dom ((normsequence (X,Ix)) ^ (normsequence (Y,Iy)))
by FINSEQ_3:29;
for
k being
Nat st
k in dom (normsequence ((X ^ Y),Iv)) holds
(normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
proof
let k be
Nat;
( k in dom (normsequence ((X ^ Y),Iv)) implies (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k )
assume
k in dom (normsequence ((X ^ Y),Iv))
;
(normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
then A18:
k in Seg (len (normsequence ((X ^ Y),Iv)))
by FINSEQ_1:def 3;
then A19:
k in dom (X ^ Y)
by A13, FINSEQ_1:def 3;
reconsider k1 =
k as
Element of
dom (X ^ Y) by A18, A13, FINSEQ_1:def 3;
A20:
(normsequence ((X ^ Y),Iv)) . k = the
normF of
((X ^ Y) . k1) . (Iv . k1)
by PRVECT_2:def 11;
A21:
(
dom Ix1 = Seg (len (carr X)) &
dom Iy1 = Seg (len (carr Y)) )
by A10, FINSEQ_1:def 3;
then A22:
(
dom Ix1 = dom X &
dom Iy1 = dom Y )
by A4, FINSEQ_1:def 3;
per cases
( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) )
by A19, FINSEQ_1:25;
suppose A23:
k in dom X
;
(normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
len X = len (normsequence (X,Ix))
by PRVECT_2:def 11;
then A24:
k in dom (normsequence (X,Ix))
by A23, FINSEQ_3:29;
reconsider k2 =
k1 as
Element of
dom X by A23;
A25:
Iv . k = Ix1 . k
by A23, A22, A11, FINSEQ_1:def 7;
thus (normsequence ((X ^ Y),Iv)) . k =
the
normF of
(X . k2) . (Iv . k2)
by A20, FINSEQ_1:def 7
.=
(normsequence (X,Ix)) . k2
by A25, PRVECT_2:def 11
.=
((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
by A24, FINSEQ_1:def 7
;
verum end; suppose
ex
n being
Nat st
(
n in dom Y &
k = (len X) + n )
;
(normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . kthen consider n being
Nat such that A26:
(
n in dom Y &
k = (len X) + n )
;
len Y = len (normsequence (Y,Iy))
by PRVECT_2:def 11;
then A27:
n in dom (normsequence (Y,Iy))
by A26, FINSEQ_3:29;
reconsider n1 =
n as
Element of
dom Y by A26;
len Ix1 = len X
by A21, A4, FINSEQ_1:def 3;
then A28:
Iv . k = Iy1 . n
by A11, A26, A22, FINSEQ_1:def 7;
thus (normsequence ((X ^ Y),Iv)) . k =
the
normF of
(Y . n1) . (Iv . k1)
by A20, A26, FINSEQ_1:def 7
.=
(normsequence (Y,Iy)) . n1
by A28, PRVECT_2:def 11
.=
((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
by A27, A26, A13, FINSEQ_1:def 7
;
verum end;
end;
then
normsequence (
(X ^ Y),
Iv)
= (normsequence (X,Ix)) ^ (normsequence (Y,Iy))
by A17, FINSEQ_1:13;
then
sqr (normsequence ((X ^ Y),Iv)) = (sqr (normsequence (X,Ix))) ^ (sqr (normsequence (Y,Iy)))
by Lm3;
hence
||.(I . v).|| = ||.v.||
by A14, A12, A16, A9, A8, RVSUM_1:75;
verum
end;
hence
for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||
; verum