:: Cartesian Products of Family of Real Linear Spaces
:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FUNCT_2, FINSEQ_1,
PRE_TOPC, XBOOLE_0, NORMSP_0, STRUCT_0, RLVECT_1, NORMSP_1, COMPLEX1,
ARYTM_3, REAL_1, PRVECT_3, RFINSEQ, ARYTM_1, SQUARE_1, RVSUM_1, XXREAL_0,
CARD_1, SUPINF_2, SEQ_2, ORDINAL2, TARSKI, NAT_1, PRVECT_1, PRVECT_2,
ZFMISC_1, ORDINAL4, GROUP_2, ALGSTR_0, BINOP_1, EUCLID, REWRITE1,
RSSPACE3, RELAT_2, METRIC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, COMPLEX1, CARD_3, FINSEQ_1,
FINSEQ_2, FINSEQ_4, RVSUM_1, RFINSEQ, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, NORMSP_0, NORMSP_1, EUCLID, RSSPACE3, LOPBAN_1, PRVECT_1,
PRVECT_2;
constructors REAL_1, SQUARE_1, RSSPACE3, COMPLEX1, LOPBAN_1, RVSUM_1, BINOP_2,
PRVECT_2, FINSEQ_4, RFINSEQ, FINSEQOP, TOPMETR;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, FUNCT_2,
NUMBERS, XBOOLE_0, VALUED_0, EUCLID, PRVECT_2, ALGSTR_0, FINSEQ_1,
CARD_3, NORMSP_0, LOPBAN_1, RLVECT_1, NORMSP_1, RELAT_1, SUBSET_1,
SQUARE_1, RVSUM_1, PRVECT_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions PRVECT_2, RLVECT_1, ALGSTR_0;
equalities EUCLID, PRVECT_2, BINOP_1, RLVECT_1, ALGSTR_0, NORMSP_0, STRUCT_0;
expansions PRVECT_2, BINOP_1, NORMSP_0;
theorems TARSKI, XBOOLE_0, XREAL_0, RLVECT_1, FINSEQ_1, FINSEQ_2, RVSUM_1,
NORMSP_0, RFINSEQ, NAT_1, TOPREAL6, SQUARE_1, RELSET_1, RELAT_1, FUNCT_1,
FUNCT_2, NORMSP_1, LOPBAN_1, CARD_3, ALGSTR_0, EUCLID, RSSPACE3,
XXREAL_0, PRVECT_1, PRVECT_2, ZFMISC_1, FINSEQ_3, SUBSET_1, XTUPLE_0,
ORDINAL1;
schemes FUNCT_2, BINOP_1;
begin :: Preliminaries
reserve G,F for RealLinearSpace;
theorem
for D,E,F,G be non empty set
ex I be Function of [: [:D,E:],[:F,G:] :], [:[:D,F:],[:E,G:]:]
st I is one-to-one & I is onto
& for d,e,f,g be set st d in D & e in E & f in F & g in G
holds I.([d,e],[f,g]) = [[d,f],[e,g]]
proof
let D,E,F,G be non empty set;
defpred P0[object,object,object] means
ex d,e,f,g be set
st d in D & e in E & f in F & g in G
& $1=[d,e] & $2=[f,g] & $3= [[d,f],[e,g]];
A1:for x,y be object st x in [:D,E:] & y in [:F,G:]
ex z be object st z in [:[:D,F:],[:E,G:]:] & P0[x,y,z]
proof
let x,y be object;
assume A2: x in [:D,E:] & y in [:F,G:];
consider d,e be object such that
A3: d in D & e in E & x=[d,e] by A2,ZFMISC_1:def 2;
consider f,g be object such that
A4: f in F & g in G & y=[f,g] by A2,ZFMISC_1:def 2;
[d,f] in [:D,F:] & [e,g] in [:E,G:] by A3,A4,ZFMISC_1:87; then
[[d,f],[e,g]] in [:[:D,F:],[:E,G:]:] by ZFMISC_1:87;
hence thesis by A3,A4;
end;
consider I be Function of
[: [:D,E:],[:F,G:] :], [:[:D,F:],[:E,G:]:] such that
A5: for x,y be object st x in [:D,E:] & y in [:F,G:]
holds P0[x,y,I.(x,y)] from BINOP_1:sch 1(A1);
A6: for d,e,f,g be set st d in D & e in E & f in F & g in G
holds I.([d,e],[f,g]) = [[d,f],[e,g]]
proof
let d,e,f,g be set;
assume A7:d in D & e in E & f in F & g in G;
A8:[d,e] in [:D,E:] & [f,g] in [:F,G:] by A7,ZFMISC_1:87;
consider d1,e1,f1,g1 be set such that
A9: d1 in D & e1 in E & f1 in F & g1 in G
& [d,e]=[d1,e1] & [f,g]=[f1,g1]
& I.([d,e],[f,g])= [[d1,f1],[e1,g1]] by A8,A5;
d1=d & e1=e & f1=f & g1=g by A9,XTUPLE_0:1;
hence I.([d,e],[f,g])= [[d,f],[e,g]] by A9;
end;
A10:I is one-to-one
proof
now let z1,z2 be object;
assume A11: z1 in [: [:D,E:],[:F,G:] :] & z2 in [: [:D,E:],[:F,G:] :]
& I.z1=I.z2;
consider de1,fg1 be object such that
A12: de1 in [:D,E:] & fg1 in [:F,G:] & z1=[de1,fg1]
by A11,ZFMISC_1:def 2;
consider d1,e1 be object such that
A13: d1 in D & e1 in E & de1=[d1,e1] by A12,ZFMISC_1:def 2;
consider f1,g1 be object such that
A14: f1 in F & g1 in G & fg1=[f1,g1] by A12,ZFMISC_1:def 2;
consider de2,fg2 be object such that
A15: de2 in [:D,E:] & fg2 in [:F,G:] & z2=[de2,fg2]
by A11,ZFMISC_1:def 2;
consider d2,e2 be object such that
A16: d2 in D & e2 in E & de2=[d2,e2] by A15,ZFMISC_1:def 2;
consider f2,g2 be object such that
A17: f2 in F & g2 in G & fg2=[f2,g2] by A15,ZFMISC_1:def 2;
[[d1,f1],[e1,g1]] = I.([d1,e1],[f1,g1]) by A6,A13,A14
.= I.([d2,e2],[f2,g2]) by A11,A12,A13,A14,A15,A16,A17
.= [[d2,f2],[e2,g2]] by A6,A16,A17;
then [d1,f1] = [d2,f2] & [e1,g1] = [e2,g2] by XTUPLE_0:1;
then d1=d2 & f1=f2 & e1=e2 & g1=g2 by XTUPLE_0:1;
hence z1=z2 by A12,A13,A14,A15,A16,A17;
end;
hence thesis by FUNCT_2:19;
end;
I is onto
proof
now let w be object;
assume A18: w in [: [:D,F:],[:E,G:] :];
consider df,eg be object such that
A19: df in [:D,F:] & eg in [:E,G:] & w=[df,eg] by A18,ZFMISC_1:def 2;
consider d,f be object such that
A20: d in D & f in F & df=[d,f] by A19,ZFMISC_1:def 2;
consider e,g be object such that
A21: e in E & g in G & eg=[e,g] by A19,ZFMISC_1:def 2;
A22: [d,e] in [:D,E:] & [f,g] in [:F,G:] by A20,A21,ZFMISC_1:87;
reconsider z = [[d,e],[f,g]] as Element of [:[:D,E:],[:F,G:]:]
by A22,ZFMISC_1:87;
w = I.([d,e],[f,g]) by A6,A19,A20,A21; then
w = I.z;
hence w in rng I by FUNCT_2:112;
end;
then [:[:D,F:],[:E,G:]:] c= rng I by TARSKI:def 3;
then [:[:D,F:],[:E,G:]:] = rng I by XBOOLE_0:def 10;
hence thesis by FUNCT_2:def 3;
end;
hence thesis by A6,A10;
end;
theorem Th2:
for X be non empty set, D be Function st dom D = {1} & D.1 = X
ex I be Function of X,product D
st I is one-to-one & I is onto
& for x be object st x in X holds I.x = <*x*>
proof
let X be non empty set, D be Function;
assume A1: dom D ={1} & D.1 = X;
defpred P[object,object] means $2 = <* $1 *>;
A2:for x be object st x in X
ex z be object st z in product D & P[x,z]
proof
let x be object;
assume A3: x in X;
A4: dom <*x*> = Seg len <*x*> by FINSEQ_1:def 3
.= {1} by FINSEQ_1:2,40;
now let i be object;
assume i in dom <*x*>; then
i = 1 by A4,TARSKI:def 1;
hence <*x*>.i in D.i by A1,A3;
end; then
<*x*> in product D by A4,A1,CARD_3:9;
hence ex z be object st z in product D & P[x,z];
end;
consider I be Function of X, product D such that
A5: for x be object st x in X holds P[x,I.x] from FUNCT_2:sch 1(A2);
now assume {} in rng D; then
ex x be object st x in dom D & D.x={} by FUNCT_1:def 3;
hence contradiction by A1,TARSKI:def 1;
end; then
A6:product D <> {} by CARD_3:26;
now let z1,z2 be object;
assume A7: z1 in X & z2 in X & I.z1=I.z2;
<*z1*> = I.z1 by A5,A7
.= <*z2*> by A5,A7;
hence z1 = z2 by FINSEQ_1:76;
end; then
A8:I is one-to-one by A6,FUNCT_2:19;
now let w be object;
assume w in product D; then
consider g be Function such that
A9: w = g & dom g = dom D
& for i be object st i in dom D holds g.i in D.i by CARD_3:def 5;
reconsider g as FinSequence by A1,A9,FINSEQ_1:2,def 2;
set x = g.1;
A10: len g = 1 by A1,A9,FINSEQ_1:2,def 3;
1 in dom D by A1,TARSKI:def 1; then
A11:x in X & w=<*x*> by A9,A10,A1,FINSEQ_1:40; then
w = I.x by A5;
hence w in rng I by A11,A6,FUNCT_2:112;
end; then
product D c= rng I by TARSKI:def 3; then
product D = rng I by XBOOLE_0:def 10; then
I is onto by FUNCT_2:def 3;
hence thesis by A5,A8;
end;
theorem Th3:
for X,Y be non empty set, D be Function
st dom D = {1,2} & D.1 = X & D.2 = Y
ex I be Function of [:X,Y:],product D
st I is one-to-one & I is onto
& for x,y be object st x in X & y in Y holds I.(x,y) = <*x,y*>
proof
let X,Y be non empty set, D be Function;
assume A1: dom D ={1,2} & D.1 = X & D.2 = Y;
defpred P[object,object,object] means $3 = <* $1,$2 *>;
A2:for x,y be object st x in X & y in Y
ex z be object st z in product D & P[x,y,z]
proof
let x,y be object;
assume A3: x in X & y in Y;
A4: dom <*x,y*> = Seg len <*x,y*> by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:2,44;
now let i be object;
assume i in dom <*x,y*>; then
i = 1 or i = 2 by A4,TARSKI:def 2;
hence <*x,y*>.i in D.i by A1,A3;
end; then
<*x,y*> in product D by A4,A1,CARD_3:9;
hence ex z be object st z in product D & P[x,y,z];
end;
consider I be Function of [:X,Y:], product D such that
A5: for x,y be object st x in X & y in Y
holds P[x,y,I.(x,y)] from BINOP_1:sch 1(A2);
now assume {} in rng D; then
ex x be object st x in dom D & D.x={} by FUNCT_1:def 3;
hence contradiction by A1,TARSKI:def 2;
end; then
A6:product D <> {} by CARD_3:26;
now let z1,z2 be object;
assume A7: z1 in [:X,Y:] & z2 in [:X,Y:] & I.z1=I.z2; then
consider x1,y1 be object such that
A8: x1 in X & y1 in Y & z1=[x1,y1] by ZFMISC_1:def 2;
consider x2,y2 be object such that
A9: x2 in X & y2 in Y & z2=[x2,y2] by A7,ZFMISC_1:def 2;
<*x1,y1*> = I.(x1,y1) by A5,A8
.= I.(x2,y2) by A7,A8,A9
.= <*x2,y2*> by A5,A9; then
x1 = x2 & y1 = y2 by FINSEQ_1:77;
hence z1=z2 by A8,A9;
end; then
A10:I is one-to-one by A6,FUNCT_2:19;
now let w be object;
assume w in product D; then
consider g be Function such that
A11: w = g & dom g = dom D
& for i be object st i in dom D holds g.i in D.i by CARD_3:def 5;
reconsider g as FinSequence by A1,A11,FINSEQ_1:2,def 2;
set x=g.1; set y=g.2;
A12: len g = 2 by A1,A11,FINSEQ_1:2,def 3;
1 in dom D & 2 in dom D by A1,TARSKI:def 2; then
A13:x in X & y in Y & w=<*x,y*> by A11,A12,A1,FINSEQ_1:44;
reconsider z = [x,y] as Element of [:X,Y:] by A13,ZFMISC_1:87;
w = I.(x,y) by A5,A13
.= I.z;
hence w in rng I by A6,FUNCT_2:112;
end; then
product D c= rng I by TARSKI:def 3; then
product D = rng I by XBOOLE_0:def 10; then
I is onto by FUNCT_2:def 3;
hence thesis by A5,A10;
end;
theorem Th4:
for X be non empty set
ex I be Function of X,product <*X*>
st I is one-to-one & I is onto
& for x be object st x in X holds I.x = <*x*>
proof
let X be non empty set;
dom <*X*> = {1} & <*X*>.1 = X by FINSEQ_1:2,38;
hence thesis by Th2;
end;
registration
let X,Y be non-empty non empty FinSequence;
cluster X^Y -> non-empty;
correctness
proof
now let z be object;
assume A1:z in dom (X^Y); then
reconsider k=z as Element of NAT;
per cases by A1,FINSEQ_1:25;
suppose A2: k in dom X; then
X.k = (X^Y).k by FINSEQ_1:def 7;
hence (X^Y).z is non empty by A2;
end;
suppose ex n be Nat st n in dom Y & k=len X + n; then
consider n be Nat such that
A3: n in dom Y & k = len X + n;
Y.n = (X^Y).k by A3,FINSEQ_1:def 7;
hence (X^Y).z is non empty by A3;
end;
end;
hence thesis by FUNCT_1:def 9;
end;
end;
theorem Th5:
for X,Y be non empty set
ex I be Function of [:X,Y:],product <*X,Y*>
st I is one-to-one & I is onto
& for x,y be object st x in X & y in Y holds I.(x,y) = <*x,y*>
proof
let X,Y be non empty set;
dom <*X,Y*> = {1,2} & <*X,Y*>.1 = X & <*X,Y*>.2 = Y
by FINSEQ_1:2,89;
hence thesis by Th3;
end;
theorem Th6:
for X,Y be non-empty non empty FinSequence
ex I be Function of [: product X,product Y :],product(X^Y)
st I is one-to-one & I is onto
& for x,y be FinSequence st x in product X & y in product Y
holds I.(x,y) = x^y
proof
let X,Y be non-empty non empty FinSequence;
defpred P[object,object,object] means
ex x,y be FinSequence st x=$1 & y=$2 & $3 = x^y;
A1:for x,y be object st x in product X & y in product Y
ex z be object st z in product (X^Y) & P[x,y,z]
proof
let x,y be object;
assume A2: x in product X & y in product Y; then
consider g be Function such that
A3: x = g & dom g = dom X
& for z be object st z in dom X holds g.z in X.z by CARD_3:def 5;
A4:dom g = Seg len X by A3,FINSEQ_1:def 3; then
reconsider g as FinSequence by FINSEQ_1:def 2;
consider h be Function such that
A5: y = h & dom h = dom Y
& for z be object st z in dom Y holds h.z in Y.z by A2,CARD_3:def 5;
A6:dom h = Seg len Y by A5,FINSEQ_1:def 3; then
reconsider h as FinSequence by FINSEQ_1:def 2;
A7:len g = len X & len h = len Y by A4,A6,FINSEQ_1:def 3;
A8:dom (g^h) = Seg (len g + len h) by FINSEQ_1:def 7
.= Seg len (X^Y) by A7,FINSEQ_1:22
.= dom (X^Y) by FINSEQ_1:def 3;
for z be object st z in dom (X^Y) holds (g^h).z in (X^Y).z
proof
let z be object;
assume A9:z in dom (X^Y); then
reconsider k=z as Element of NAT;
per cases by A9,FINSEQ_1:25;
suppose A10: k in dom X; then
A11: g.k in X.k by A3;
g.k = (g^h).k by A10,A3,FINSEQ_1:def 7;
hence (g^h).z in (X^Y).z by A11,A10,FINSEQ_1:def 7;
end;
suppose ex n be Nat st n in dom Y & k=len X + n; then
consider n be Nat such that
A12: n in dom Y & k=len X + n;
A13: h.n in Y.n by A12,A5;
h.n = (g^h).k by A12,A7,A5,FINSEQ_1:def 7;
hence (g^h).z in (X^Y).z by A13,A12,FINSEQ_1:def 7;
end;
end; then
(g^h) in product (X^Y) by A8,CARD_3:9;
hence thesis by A3,A5;
end;
consider I be Function of [:product X,product Y:], product (X^Y) such that
A14: for x,y be object st x in product X & y in product Y
holds P[x,y,I.(x,y)] from BINOP_1:sch 1(A1);
A15:
for x,y be FinSequence st x in product X & y in product Y
holds I.(x,y) = x^y
proof
let x,y be FinSequence;
assume x in product X & y in product Y; then
ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y)=x1^y1 by A14;
hence thesis;
end;
now let z1,z2 be object;
assume A16: z1 in [:product X,product Y:] & z2 in [:product X,product Y:]
& I.z1=I.z2;
consider x1,y1 be object such that
A17: x1 in product X & y1 in product Y & z1=[x1,y1]
by A16,ZFMISC_1:def 2;
consider x2,y2 be object such that
A18: x2 in product X & y2 in product Y & z2=[x2,y2]
by A16,ZFMISC_1:def 2;
consider xx1,yy1 be FinSequence such that
A19: xx1=x1 & yy1=y1 & I.(x1,y1) = xx1^yy1 by A14,A17;
consider xx2,yy2 be FinSequence such that
A20: xx2=x2 & yy2=y2 & I.(x2,y2) = xx2^yy2 by A14,A18;
A21:dom xx1 = dom X by A17,A19,CARD_3:9
.= dom xx2 by A18,A20,CARD_3:9;
xx1 = (xx1^yy1) | (dom xx1) by FINSEQ_1:21
.= xx2 by A16,A17,A18,A19,A20,A21,FINSEQ_1:21;
hence z1=z2 by A16,A17,A18,A19,A20,FINSEQ_1:33;
end; then
A22:I is one-to-one by FUNCT_2:19;
now let w be object;
assume w in product (X^Y); then
consider g be Function such that
A23: w = g & dom g = dom (X^Y)
& for i be object st i in dom (X^Y) holds g.i in (X^Y).i
by CARD_3:def 5;
A24: dom g = Seg len (X^Y) by A23,FINSEQ_1:def 3; then
reconsider g as FinSequence by FINSEQ_1:def 2;
set x = g | (len X);
set y = g/^(len X);
A26: x^y = g by RFINSEQ:8;
A27:len(X^Y) = len X + len Y by FINSEQ_1:22; then
A28:len X <=len(X^Y) by NAT_1:11;
A29:len g= len (X^Y) by A24,FINSEQ_1:def 3; then
len(g|len X) = len X by A27,FINSEQ_1:59,NAT_1:11; then
A30:dom x = Seg len X by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3;
for z be object st z in dom X holds x.z in X.z
proof
let z be object;
assume A31:z in dom X; then
reconsider k = z as Element of NAT;
A32: dom X c= dom (X^Y) by FINSEQ_1:26;
A33: x.k = g.k by A31,A26,A30,FINSEQ_1:def 7;
X.k = (X^Y).k by A31,FINSEQ_1:def 7;
hence x.z in X.z by A33,A23,A31,A32;
end; then
A34: x in product X by A30,CARD_3:9;
dom x = Seg len X by A30,FINSEQ_1:def 3; then
A35:len x = len X by FINSEQ_1:def 3;
len y = len g - len X by A28,A29,RFINSEQ:def 1
.= len Y by A29,A27; then
Seg len y = dom Y by FINSEQ_1:def 3; then
A36:dom y = dom Y by FINSEQ_1:def 3;
for z be object st z in dom Y holds y.z in Y.z
proof
let z be object;
assume A37:z in dom Y; then
reconsider k=z as Element of NAT;
A38: y.k = g.(len X + k) by A37,A26,A35,A36,FINSEQ_1:def 7;
Y.k = (X^Y).(len X + k) by A37,FINSEQ_1:def 7;
hence y.z in Y.z by A38,A23,A37,FINSEQ_1:28;
end; then
A39: y in product Y by A36,CARD_3:9;
reconsider z = [x,y] as Element of [:product X,product Y:]
by A34,A39,ZFMISC_1:87;
w = I.(x,y) by A23,A26,A15,A34,A39
.= I.z;
hence w in rng I by FUNCT_2:112;
end; then
product (X^Y) c= rng I by TARSKI:def 3; then
product (X^Y) = rng I by XBOOLE_0:def 10; then
I is onto by FUNCT_2:def 3;
hence thesis by A15,A22;
end;
Lm1:
for G,F be non empty 1-sorted, x be set st
x in [: the carrier of G, the carrier of F :] holds
ex x1 be Point of G, x2 be Point of F st x = [x1,x2] by SUBSET_1:43;
definition
let G,F be non empty addLoopStr;
func prod_ADD(G,F) -> BinOp of [:the carrier of G,the carrier of F:] means
:Def1:
for g1,g2 be Point of G, f1,f2 be Point of F
holds it.([g1,f1],[g2,f2]) = [g1+g2,f1+f2];
existence
proof
defpred ADP[object,object,object] means
ex g1,g2 be Point of G,f1,f2 be Point of F
st $1=[g1,f1] & $2=[g2,f2] & $3= [g1+g2,f1+f2];
A1:for x,y be object st x in [:the carrier of G,the carrier of F:]
& y in [:the carrier of G,the carrier of F:]
ex z be object st z in [:the carrier of G,the carrier of F:] & ADP[x,y,z]
proof
let x,y be object;
assume A2: x in [:the carrier of G,the carrier of F:]
& y in [:the carrier of G,the carrier of F:]; then
consider x1 be Point of G, x2 be Point of F such that
A3: x=[x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A4: y=[y1,y2] by Lm1,A2;
reconsider z = [x1+y1,x2+y2]
as Element of [:the carrier of G,the carrier of F:];
z in [:the carrier of G,the carrier of F:] & ADP[x,y,z] by A3,A4;
hence thesis;
end;
consider ADGF be Function of [:[:the carrier of G,the carrier of F:],
[:the carrier of G,the carrier of F:] :],
[:the carrier of G,the carrier of F:] such that
A5: for x,y be object st x in [:the carrier of G,the carrier of F:]
& y in [:the carrier of G,the carrier of F:]
holds ADP[x,y,ADGF.(x,y)] from BINOP_1:sch 1(A1);
now let g1,g2 be Point of G, f1,f2 be Point of F;
consider gg1,gg2 be Point of G, ff1,ff2 be Point of F such that
A6: [g1,f1] = [gg1,ff1] & [g2,f2] = [gg2,ff2]
& ADGF.([g1,f1],[g2,f2])= [gg1+gg2,ff1+ff2] by A5;
g1=gg1 & f1=ff1 & g2=gg2 & f2=ff2 by A6,XTUPLE_0:1;
hence ADGF.([g1,f1],[g2,f2]) = [g1+g2,f1+f2] by A6;
end;
hence thesis;
end;
uniqueness
proof
let H1,H2 be BinOp of [:the carrier of G,the carrier of F:];
assume
A7: for g1,g2 be Point of G, f1,f2 be Point of F
holds H1.([g1,f1],[g2,f2]) = [g1+g2,f1+f2];
assume
A8: for g1,g2 be Point of G, f1,f2 be Point of F
holds H2.([g1,f1],[g2,f2]) = [g1+g2,f1+f2];
now let x,y be Element of [:the carrier of G,the carrier of F:];
consider x1 be Point of G, x2 be Point of F such that
A9: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A10: y = [y1,y2] by Lm1;
thus H1.(x,y) = [x1+y1,x2+y2] by A7,A9,A10
.= H2.(x,y) by A8,A9,A10;
end;
hence H1=H2;
end;
end;
definition let G,F be non empty RLSStruct;
func prod_MLT(G,F) -> Function of
[:REAL, [:the carrier of G,the carrier of F:] :],
[:the carrier of G,the carrier of F:] means :Def2:
for r be Real, g be Point of G, f be Point of F
holds it.(r,[g,f]) = [r*g,r*f];
existence
proof
defpred MLT[object,object,object] means
ex r be Element of REAL, g be Point of G, f be Point of F
st r = $1 & $2=[g,f] & $3= [r*g,r*f];
set CarrG = the carrier of G;
set CarrF = the carrier of F;
A1:for x,y be object st x in REAL & y in [:CarrG,CarrF:]
ex z be object st z in [:CarrG,CarrF:] & MLT[x,y,z]
proof
let x,y be object;
assume A2: x in REAL & y in [:CarrG,CarrF:]; then
reconsider r=x as Element of REAL;
consider y1 be Point of G, y2 be Point of F such that
A3: y = [y1,y2] by A2,Lm1;
set z = [r*y1,r*y2];
z in [:CarrG,CarrF:] & MLT[x,y,z] by A3;
hence thesis;
end;
consider MLTGF be Function of [:REAL,[:CarrG,CarrF:] :],[:CarrG,CarrF:]
such that
A4: for x,y be object st x in REAL & y in [:CarrG,CarrF:]
holds MLT[x,y,MLTGF.(x,y)] from BINOP_1:sch 1(A1);
now let r be Real, g be Point of G, f be Point of F;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
MLT[rr,[g,f],MLTGF.(rr,[g,f])] by A4; then
consider rr be Element of REAL, gg be Point of G,
ff be Point of F such that
A5: rr=r & [g,f]=[gg,ff] & MLTGF.(r,[g,f]) = [rr*gg,r*ff];
g=gg & f=ff by A5,XTUPLE_0:1;
hence MLTGF.(r,[g,f]) = [r*g,r*f] by A5;
end;
hence thesis;
end;
uniqueness
proof
let H1,H2 be Function of
[:REAL, [:the carrier of G,the carrier of F:] :],
[:the carrier of G,the carrier of F:];
assume
A6: for r be Real, g be Point of G, f be Point of F
holds H1.(r,[g,f]) = [r*g,r*f];
assume
A7: for r be Real, g be Point of G, f be Point of F
holds H2.(r,[g,f]) = [r*g,r*f];
now let r be Element of REAL ,x be Element of
[:the carrier of G,the carrier of F:];
consider x1 be Point of G, x2 be Point of F such that
A8: x = [x1,x2] by Lm1;
thus H1.(r,x) = [r*x1,r*x2] by A6,A8
.= H2.(r,x) by A7,A8;
end;
hence H1=H2;
end;
end;
definition let G,F be non empty addLoopStr;
func prod_ZERO(G,F) -> Element of [:the carrier of G,the carrier of F:]
equals [0.G,0.F];
correctness;
end;
definition let G,F be non empty addLoopStr;
func [:G,F:] -> strict non empty addLoopStr equals
addLoopStr (# [:the carrier of G,the carrier of F:],
prod_ADD(G,F), prod_ZERO(G,F) #);
correctness;
end;
definition let G,F be non empty addLoopStr;
let g be Element of G, f be Element of F;
redefine func [g,f] -> Element of [:G,F:]; :: redefines [ (TARSKI, definition)
coherence
proof
[g,f] in the carrier of [:G,F:];
hence thesis;
end;
end;
registration
let G,F be Abelian non empty addLoopStr;
cluster [:G,F:] -> Abelian;
correctness
proof
let x,y be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A2: y = [y1,y2] by Lm1;
thus x+y = [x1+y1,x2+y2] by A1,A2,Def1
.= y+x by A1,A2,Def1;
end;
end;
registration
let G,F be add-associative non empty addLoopStr;
cluster [:G,F:] -> add-associative;
correctness
proof
let x,y,z be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A2: y = [y1,y2] by Lm1;
consider z1 be Point of G, z2 be Point of F such that
A3: z = [z1,z2] by Lm1;
A4: (x1+y1)+z1 = x1+(y1+z1) & (x2+y2)+z2 = x2+(y2+z2) by RLVECT_1:def 3;
thus (x+y)+z = prod_ADD(G,F).([x1+y1,x2+y2],[z1,z2]) by A1,A2,A3,Def1
.= [(x1+y1)+z1,(x2+y2)+z2] by Def1
.=prod_ADD(G,F).([x1,x2],[(y1+z1),(y2+z2)] ) by A4,Def1
.=x+(y+z) by A1,A2,A3,Def1;
end;
end;
registration
let G,F be right_zeroed non empty addLoopStr;
cluster [:G,F:] -> right_zeroed;
correctness
proof
let x be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x=[x1,x2] by Lm1;
x1+0.G = x1 & x2+0.F = x2 by RLVECT_1:def 4;
hence x+0.[:G,F:] =x by A1,Def1;
end;
end;
registration
let G,F be right_complementable non empty addLoopStr;
cluster [:G,F:] -> right_complementable;
correctness
proof
let x be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G such that
A2: x1+y1 = 0.G by ALGSTR_0:def 11;
consider y2 be Point of F such that
A3: x2+y2 = 0.F by ALGSTR_0:def 11;
reconsider y=[y1,y2] as Element of [:G,F:];
take y;
thus thesis by A1,A2,A3,Def1;
end;
end;
theorem
for G,F be non empty addLoopStr holds
( for x be set holds
(x is Point of [:G,F:]
iff ex x1 be Point of G, x2 be Point of F st x=[x1,x2]) )
& ( for x,y be Point of [:G,F:],
x1,y1 be Point of G ,x2,y2 be Point of F
st x=[x1,x2] & y=[y1,y2] holds x+y = [x1+y1,x2+y2] )
& 0.[:G,F:] = [0.G,0.F] by Lm1,Def1;
theorem
for G,F be add-associative right_zeroed
right_complementable non empty addLoopStr,
x be Point of [:G,F:], x1 be Point of G, x2 be Point of F
st x=[x1,x2] holds -x = [-x1,-x2]
proof
let G,F be add-associative right_zeroed right_complementable
non empty addLoopStr;
let x be Point of [:G,F:];
let x1 be Point of G, x2 be Point of F;
assume A1: x=[x1,x2];
reconsider y = [-x1,-x2 ] as Point of [:G,F:];
x+y = [x1+-x1,x2+-x2] by A1,Def1
.= [0.G,x2+-x2] by RLVECT_1:def 10
.= 0.[:G,F:] by RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
registration
let G,F be Abelian add-associative
right_zeroed right_complementable strict non empty addLoopStr;
cluster [:G,F:] -> strict Abelian add-associative
right_zeroed right_complementable;
correctness;
end;
definition let G,F be non empty RLSStruct;
func [:G,F:] -> strict non empty RLSStruct equals
RLSStruct (# [:the carrier of G,the carrier of F:],
prod_ZERO(G,F), prod_ADD(G,F), prod_MLT(G,F) #);
correctness;
end;
definition let G,F be non empty RLSStruct;
let g be Element of G, f be Element of F;
redefine func [g,f] -> Element of [:G,F:]; :: redefines [ (TARSKI, definition)
coherence
proof
[g,f] in the carrier of [:G,F:];
hence thesis;
end;
end;
registration
let G,F be Abelian non empty RLSStruct;
cluster [:G,F:] -> Abelian;
correctness
proof
let x,y be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A2: y = [y1,y2] by Lm1;
x+y = [x1+y1,x2+y2] by A1,A2,Def1;
hence x+y = y+x by A1,A2,Def1;
end;
end;
registration
let G,F be add-associative non empty RLSStruct;
cluster [:G,F:] -> add-associative;
correctness
proof
let x,y,z be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A2: y = [y1,y2] by Lm1;
consider z1 be Point of G, z2 be Point of F such that
A3: z = [z1,z2] by Lm1;
A4:(x1+y1)+z1 = x1+(y1+z1) & (x2+y2)+z2 = x2+(y2+z2) by RLVECT_1:def 3;
thus (x+y)+z = prod_ADD(G,F).([x1+y1,x2+y2],[z1,z2]) by A1,A2,A3,Def1
.= [x1+(y1+z1),x2+(y2+z2)] by A4,Def1
.=prod_ADD(G,F).([x1,x2],[(y1+z1),(y2+z2)] ) by Def1
.=x+(y+z) by A1,A2,A3,Def1;
end;
end;
registration
let G,F be right_zeroed non empty RLSStruct;
cluster [:G,F:] -> right_zeroed;
correctness
proof
let x be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
x1+0.G = x1 & x2+0.F = x2 by RLVECT_1:def 4;
hence x+0.[:G,F:] = x by A1,Def1;
end;
end;
registration
let G,F be right_complementable non empty RLSStruct;
cluster [:G,F:] -> right_complementable;
correctness
proof
let x be Element of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G such that
A2: x1+y1 = 0.G by ALGSTR_0:def 11;
consider y2 be Point of F such that
A3: x2+y2 = 0.F by ALGSTR_0:def 11;
reconsider y=[y1,y2] as Element of [:G,F:];
take y;
thus thesis by A1,A2,A3,Def1;
end;
end;
theorem Th9:
for G,F be non empty RLSStruct holds
( for x be set holds
(x is Point of [:G,F:]
iff ex x1 be Point of G, x2 be Point of F st x=[x1,x2]) )
& ( for x,y be Point of [:G,F:], x1,y1 be Point of G, x2,y2 be Point of F
st x=[x1,x2] & y=[y1,y2] holds x+y = [x1+y1,x2+y2] )
& 0.[:G,F:] = [0.G,0.F]
& ( for x be Point of [:G,F:], x1 be Point of G, x2 be Point of F,
a be Real
st x=[x1,x2] holds a*x = [a*x1,a*x2] )
by Def2,Def1,Lm1;
theorem
for G,F be add-associative right_zeroed
right_complementable non empty RLSStruct,
x be Point of [:G,F:], x1 be Point of G, x2 be Point of F
st x=[x1,x2] holds -x = [-x1,-x2]
proof
let G,F be add-associative right_zeroed right_complementable
non empty RLSStruct;
let x be Point of [:G,F:], x1 be Point of G, x2 be Point of F;
assume A1: x=[x1,x2];
reconsider y = [-x1,-x2 ] as Point of [:G,F:];
x+y = [x1+-x1,x2+-x2] by A1,Def1
.= [0.G,x2+-x2] by RLVECT_1:def 10
.= 0.[:G,F:] by RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
registration
let G,F be vector-distributive non empty RLSStruct;
cluster [:G,F:] -> vector-distributive;
correctness
proof
let a0 be Real, x,y be VECTOR of [:G,F:];
reconsider a=a0 as Element of REAL by XREAL_0:def 1;
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A2: y = [y1,y2] by Lm1;
A3: a*(x1+y1) = a0*x1 + a0*y1 & a*(x2+y2) = a0*x2 + a0*y2
by RLVECT_1:def 5;
thus a0*(x+y) = prod_MLT(G,F).(a,[x1+y1,x2+y2]) by A1,A2,Def1
.= [a*(x1+y1),a*(x2+y2)] by Def2
.= prod_ADD(G,F).([a*x1,a*x2],[a*y1,a*y2]) by A3,Def1
.= prod_ADD(G,F).(prod_MLT(G,F).(a,[x1,x2]),[a*y1,a*y2]) by Def2
.= a0*x + a0*y by A1,A2,Def2;
end;
end;
registration
let G,F be scalar-distributive non empty RLSStruct;
cluster [:G,F:] -> scalar-distributive;
correctness
proof
let a0,b0 be Real, x be VECTOR of [:G,F:];
reconsider a=a0, b=b0 as Element of REAL by XREAL_0:def 1;
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
A2: (a+b)*x1 = a0*x1 + b0*x1 & (a+b)*x2 = a0*x2 + b0*x2
by RLVECT_1:def 6;
thus (a0+b0)*x = [(a+b)*x1,(a+b)*x2] by A1,Def2
.= prod_ADD(G,F).([a*x1,a*x2],[b*x1,b*x2]) by A2,Def1
.= prod_ADD(G,F).(prod_MLT(G,F).(a,[x1,x2]),[b*x1,b*x2]) by Def2
.= a0*x + b0*x by A1,Def2;
end;
end;
registration
let G,F be scalar-associative non empty RLSStruct;
cluster [:G,F:] -> scalar-associative;
correctness
proof
let a0,b0 be Real, x be VECTOR of [:G,F:];
reconsider a=a0, b=b0 as Element of REAL by XREAL_0:def 1;
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
A2: (a*b)*x1 = a0 * (b0*x1) & (a*b)*x2 = a0 * (b0*x2) by RLVECT_1:def 7;
thus (a0*b0)*x = [(a*b)*x1,(a*b)*x2] by A1,Def2
.= prod_MLT(G,F).(a,[b*x1,b*x2]) by A2,Def2
.= a0*(b0*x) by A1,Def2;
end;
end;
registration
let G,F be scalar-unital non empty RLSStruct;
cluster [:G,F:] -> scalar-unital;
correctness
proof
let x be VECTOR of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
1*x1 = x1 & 1*x2 = x2 by RLVECT_1:def 8;
hence 1*x = x by A1,Def2;
end;
end;
registration
let G be Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative
scalar-unital non empty RLSStruct;
cluster <* G *> -> RealLinearSpace-yielding;
correctness
proof
let S be set;
assume S in rng <*G*>; then
consider i be object such that
A1: i in dom <*G*> & <*G*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
dom <*G*> = {1} by FINSEQ_1:2,def 8; then
i = 1 by A1,TARSKI:def 1;
hence S is RealLinearSpace by A1;
end;
end;
registration
let G,F be Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative
scalar-unital non empty RLSStruct;
cluster <* G,F *> -> RealLinearSpace-yielding;
correctness
proof
let S be set;
assume S in rng <*G,F*>; then
consider i be object such that
A1: i in dom <*G,F*> & <*G,F*>.i = S by FUNCT_1:def 3;
dom <*G,F*> = {1,2} by FINSEQ_1:2,89; then
i=1 or i=2 by A1,TARSKI:def 2;
hence S is RealLinearSpace by A1;
end;
end;
begin :: Cartesian Product of Real Linear Spaces
theorem Th11:
for X be RealLinearSpace holds
ex I be Function of X, product <*X*>
st I is one-to-one & I is onto
& ( for x be Point of X holds I.x = <*x*> )
& ( for v,w be Point of X holds I.(v+w) = I.v + I.w )
& ( for v be Point of X, r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.X)=0.product <*X*>
proof
let X be RealLinearSpace;
set CarrX = the carrier of X;
consider I be Function of CarrX,product <*CarrX*> such that
A1: I is one-to-one & I is onto
& for x be object st x in CarrX holds I.x = <*x*> by Th4;
len carr <*X*> = len <*X*> by PRVECT_1:def 11; then
A2:len carr <*X*> = 1 by FINSEQ_1:40;
A3:dom <*X*> = {1} by FINSEQ_1:2,def 8;
A4:<*X*>.1 = X;
1 in {1} by TARSKI:def 1; then
(carr <*X*>).1= the carrier of X by A3,A4,PRVECT_1:def 11; then
A5:carr <*X*> = <* CarrX *> by A2,FINSEQ_1:40; then
reconsider I as Function of X,product <*X*>;
A6:for x be Point of X holds I.x = <*x*> by A1;
A7:for v,w be Point of X holds I.(v+w) = I.v + I.w
proof
let v,w be Point of X;
A8:I.v = <*v*> & I.w = <*w*> & I.(v+w) = <*v+w*> by A1;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X*>;
1 in {1} by TARSKI:def 1; then
reconsider j1=1 as Element of dom carr <*X*> by A2,FINSEQ_1:2,def 3;
A10: (addop <*X*>).j1 = the addF of (<*X*>.j1) by PRVECT_1:def 12;
A11: ([:addop <*X*>:].(Iv,Iw)).j1
= ((addop <*X*>).j1).(Iv.j1,Iw.j1) by PRVECT_1:def 8
.= v+w by A10,A8;
consider Ivw be Function such that
A12: I.v + I.w = Ivw & dom Ivw = dom carr <*X*>
& for i be object st i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i
by CARD_3:def 5;
A13: dom Ivw = Seg 1 by A2,A12,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by A13,FINSEQ_1:def 3;
hence thesis by A8,A12,A11,FINSEQ_1:40;
end;
A14:for v be Point of X, r be Element of REAL holds I.(r*v)=r*(I.v)
proof
let v be Point of X, r be Element of REAL;
A15:I.v = <*v*> & I.(r*v) = <* r*v *> by A1;
1 in {1} by TARSKI:def 1; then
reconsider j1=1 as Element of dom carr <*X*> by A2,FINSEQ_1:2,def 3;
A17: (multop <*X*>).j1 = the Mult of (<*X*>.j1) by PRVECT_2:def 8;
reconsider Iv = I.v as Element of product carr <*X*>;
A18: ([:multop <*X*>:].(r,Iv)).j1
= ((multop <*X*>).j1).(r,Iv.j1) by PRVECT_2:def 2
.= r*v by A17,A15;
consider Ivw be Function such that
A19: r*(I.v) = Ivw & dom Ivw = dom carr <*X*>
& for i be object st i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i
by CARD_3:def 5;
A20: dom Ivw = Seg 1 by A2,A19,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by A20,FINSEQ_1:def 3;
hence thesis by A15,A19,A18,FINSEQ_1:40;
end;
I.(0.X) = I.(0.X + 0.X)
.= I.(0.X) + I.(0.X) by A7; then
I.(0.X) - I.(0.X)
= I.(0.X) + (I.(0.X) - I.(0.X)) by RLVECT_1:28
.= I.(0.X) + 0.product <*X*> by RLVECT_1:15
.= I.(0.X); then
0.product <*X*> = I.(0.X) by RLVECT_1:15;
hence thesis by A1,A6,A5,A7,A14;
end;
registration
let G,F be non empty RealLinearSpace-yielding FinSequence;
cluster G^F -> RealLinearSpace-yielding;
correctness
proof
let S be set;
assume S in rng (G^F); then
consider i be object such that
A1: i in dom (G^F) & (G^F).i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
per cases by A1,FINSEQ_1:25;
suppose A2: i in dom G; then
A3: (G^F).i = G.i by FINSEQ_1:def 7;
G.i in rng G by A2,FUNCT_1:3;
hence S is RealLinearSpace by A3,A1,PRVECT_2:def 3;
end;
suppose ex n be Nat st n in dom F & i=len G + n; then
consider n be Nat such that
A4: n in dom F & i=len G + n;
A5: (G^F).i = F.n by A4,FINSEQ_1:def 7;
F.n in rng F by A4,FUNCT_1:3;
hence S is RealLinearSpace by A5,A1,PRVECT_2:def 3;
end;
end;
end;
theorem Th12:
for X,Y be RealLinearSpace holds
ex I be Function of [:X,Y:],product <*X,Y*>
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> )
& ( for v,w be Point of [:X,Y:] holds I.(v+w)=(I.v) + (I.w) )
& ( for v be Point of [:X,Y:], r be Real
holds I.(r*v)=r*(I.v) )
& I.(0.[:X,Y:])=0.product <*X,Y*>
proof
let X,Y be RealLinearSpace;
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
consider I be Function of [:CarrX,CarrY:],product <*CarrX,CarrY*> such that
A1: I is one-to-one & I is onto
& for x,y be object st x in CarrX & y in CarrY
holds I.(x,y) = <*x,y*> by Th5;
len carr <*X,Y*> = len <*X,Y*> by PRVECT_1:def 11; then
A2:len carr <*X,Y*> = 2 by FINSEQ_1:44; then
A3:dom carr <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
len <*X,Y*> = 2 by FINSEQ_1:44; then
A4:dom <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
A5:<*X,Y*>.1 = X & <*X,Y*>.2 = Y;
1 in {1,2} & 2 in {1,2} by TARSKI:def 2; then
(carr <*X,Y*>).1 = CarrX & (carr <*X,Y*>).2 = CarrY
by A4,A5,PRVECT_1:def 11; then
A6:carr <*X,Y*> = <* CarrX,CarrY *> by A2,FINSEQ_1:44; then
reconsider I as Function of [:X,Y:],product <*X,Y*>;
A7:for x be Point of X,y be Point of Y holds I.(x,y) = <*x,y*> by A1;
A8:for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:X,Y:];
consider x1 be Point of X, y1 be Point of Y such that
A9: v = [x1,y1] by Lm1;
consider x2 be Point of X, y2 be Point of Y such that
A10: w = [x2,y2] by Lm1;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A9,A10; then
A11:I.v = <*x1,y1*> & I.w = <*x2,y2*> by A1;
A12:I.(v+w) =I.(x1+x2,y1+y2) by A9,A10,Def1
.= <* x1+x2,y1+y2 *> by A1;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X,Y*>;
reconsider j1=1, j2=2 as Element of dom (carr <*X,Y*>)
by A3,TARSKI:def 2;
A14: (addop <*X,Y*>).j1 = the addF of (<*X,Y*>.j1) by PRVECT_1:def 12;
A15: ([:addop <*X,Y*>:].(Iv,Iw)).j1
= ((addop <*X,Y*>).j1).(Iv.j1,Iw.j1) by PRVECT_1:def 8
.= x1+x2 by A14,A11;
A16: (addop <*X,Y*>).j2 = the addF of (<*X,Y*>.j2) by PRVECT_1:def 12;
A17: ([:addop <*X,Y*>:].(Iv,Iw)).j2
= ((addop <*X,Y*>).j2).(Iv.j2,Iw.j2) by PRVECT_1:def 8
.= y1+y2 by A16,A11;
consider Ivw be Function such that
A18: I.v + I.w = Ivw & dom Ivw = dom carr <*X,Y*>
& for i be object st i in dom carr <*X,Y*>
holds Ivw.i in carr (<*X,Y*>).i by CARD_3:def 5;
A19: dom Ivw = Seg 2 by A2,A18,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by A19,FINSEQ_1:def 3;
hence thesis by A12,A18,A15,A17,FINSEQ_1:44;
end;
A20:for v be Point of [:X,Y:], r be Real holds I.(r*v)=r*(I.v)
proof
let v be Point of [:X,Y:], r be Real;
consider x1 be Point of X, y1 be Point of Y such that
A21: v = [x1,y1] by Lm1;
A22:I.v =I.(x1,y1) by A21 .= <*x1,y1*> by A1;
A23:I.(r*v) =I.(r*x1,r*y1) by A21,Def2 .= <* r*x1,r*y1 *> by A1;
reconsider j1=1, j2=2 as Element of dom carr <*X,Y*> by A3,TARSKI:def 2;
A25: (multop <*X,Y*>).j1 = the Mult of (<*X,Y*>.j1)
& (multop <*X,Y*>).j2 = the Mult of (<*X,Y*>.j2) by PRVECT_2:def 8;
reconsider Iv = I.v as Element of product carr <*X,Y*>;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
([:multop <*X,Y*>:].(rr,Iv)).j1 = ((multop <*X,Y*>).j1).(r,Iv.j1)
& ([:multop <*X,Y*>:].(rr,Iv)).j2 = ((multop <*X,Y*>).j2).(r,Iv.j2)
by PRVECT_2:def 2; then
A26: ([:multop <*X,Y*>:].(rr,Iv)).j1 = r*x1
& ([:multop <*X,Y*>:].(rr,Iv)).j2 = r*y1 by A25,A22;
consider Ivw be Function such that
A27: r*(I.v) = Ivw & dom Ivw = dom carr <*X,Y*>
& for i be object st i in dom carr <*X,Y*>
holds Ivw.i in carr (<*X,Y*>).i
by CARD_3:def 5;
A28: dom Ivw = Seg 2 by A2,A27,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by A28,FINSEQ_1:def 3;
hence thesis by A23,A27,A26,FINSEQ_1:44;
end;
I.(0.[:X,Y:]) = I.(0.[:X,Y:] + 0.[:X,Y:])
.= I.(0.[:X,Y:]) + I.(0.[:X,Y:]) by A8; then
I.(0.[:X,Y:]) - I.(0.[:X,Y:])
= I.(0.[:X,Y:]) + (I.(0.[:X,Y:]) - I.(0.[:X,Y:])) by RLVECT_1:28
.= I.(0.[:X,Y:]) + 0.product <*X,Y*> by RLVECT_1:15
.= I.(0.[:X,Y:]); then
0.product <*X,Y*> = I.(0.[:X,Y:]) by RLVECT_1:15;
hence thesis by A7,A8,A20,A1,A6;
end;
Lm2:
for X be non-empty non empty FinSequence, x be set
st x in product X holds x is FinSequence
proof
let X be non-empty non empty FinSequence, x be set;
assume x in product X; then
consider g be Function such that
A1: x = g & dom g = dom X
& for i be object st i in dom X holds g.i in X.i by CARD_3:def 5;
dom g = Seg len X by A1,FINSEQ_1:def 3;
hence x is FinSequence by A1,FINSEQ_1:def 2;
end;
theorem Th13:
for X,Y be non empty RealLinearSpace-Sequence
holds ex I be Function of [:product X,product Y:],product (X^Y)
st I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of product Y
holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1 )
& ( for v,w be Point of [:product X,product Y:]
holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:product X,product Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[:product X,product Y:]) = 0.product (X^Y)
proof
let X,Y be non empty RealLinearSpace-Sequence;
reconsider CX = carr X, CY = carr Y as non-empty non empty FinSequence;
A1:len CX = len X & len CY = len Y
& len carr (X^Y) = len (X^Y) by PRVECT_1:def 11;
consider I be Function of [:product CX,product CY:],product (CX^CY)
such that
A2: I is one-to-one & I is onto
& for x,y be FinSequence st x in product CX & y in product CY
holds I.(x,y) = x^y by Th6;
set PX = product X;
set PY = product Y;
len carr (X^Y) = len X + len Y & len (CX^CY) =len X + len Y
by A1,FINSEQ_1:22; then
A3:dom carr (X^Y) = dom (CX^CY) by FINSEQ_3:29;
A4:for k be Nat st k in dom carr (X^Y) holds carr (X^Y).k = (CX^CY).k
proof
let k be Nat;
assume A5: k in dom carr (X^Y); then
reconsider k1=k as Element of dom (X^Y) by A1,FINSEQ_3:29;
A6: carr (X^Y).k = the carrier of ((X^Y).k1) by PRVECT_1:def 11;
A7: k in dom (X^Y) by A1,A5,FINSEQ_3:29;
per cases by A7,FINSEQ_1:25;
suppose A8: k in dom X; then
A9: k in dom CX by A1,FINSEQ_3:29;
reconsider k2=k1 as Element of dom X by A8;
thus carr (X^Y).k = the carrier of (X.k2) by A6,FINSEQ_1:def 7
.= CX.k by PRVECT_1:def 11
.= (CX^CY).k by A9,FINSEQ_1:def 7;
end;
suppose ex n be Nat st n in dom Y & k=len X + n; then
consider n be Nat such that
A10: n in dom Y & k=len X + n;
A11: n in dom CY by A1,A10,FINSEQ_3:29;
reconsider n1=n as Element of dom Y by A10;
thus carr (X^Y).k = the carrier of (Y.n1) by A6,A10,FINSEQ_1:def 7
.= CY.n by PRVECT_1:def 11
.= (CX^CY).k by A11,A10,A1,FINSEQ_1:def 7;
end;
end; then
A12:carr (X^Y) = CX^CY by A3,FINSEQ_1:13;
reconsider I as Function of [:PX,PY:] ,product (X^Y) by A3,A4,FINSEQ_1:13;
A13:for x be Point of product X, y be Point of product Y
holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1
proof
let x be Point of PX, y be Point of PY;
reconsider x1=x, y1=y as FinSequence by Lm2;
I.(x,y) = x1^y1 by A2;
hence thesis;
end;
A14:for v,w be Point of [:PX,PY:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:PX,PY:];
consider x1 be Point of PX, y1 be Point of PY such that
A15: v = [x1,y1] by Lm1;
consider x2 be Point of PX, y2 be Point of PY such that
A16: w = [x2,y2] by Lm1;
reconsider xx1=x1, xx2=x2 as FinSequence by Lm2;
reconsider yy1=y1, yy2=y2 as FinSequence by Lm2;
reconsider xx12=x1+x2, yy12=y1+y2 as FinSequence by Lm2;
A17: dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX
& dom yy1 = dom CY & dom yy2 = dom CY & dom yy12 = dom CY by CARD_3:9;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A15,A16; then
A18:I.v = xx1^yy1 & I.w = xx2^yy2 by A2;
I.(v+w) = I.(x1+x2,y1+y2) by A15,A16,Def1; then
A19:I.(v+w) = xx12^yy12 by A2; then
A20: dom (xx12^yy12) = dom carr (X^Y) by CARD_3:9;
reconsider Iv = I.v, Iw = I.w as Element of product carr (X^Y);
reconsider Ivw = I.v + I.w as FinSequence by Lm2;
A21:dom Ivw = dom carr (X^Y) by CARD_3:9;
for j0 be Nat st j0 in dom Ivw holds Ivw.j0 = (xx12^yy12).j0
proof
let j0 be Nat;
assume j0 in dom Ivw; then
reconsider j=j0 as Element of dom carr (X^Y) by CARD_3:9;
A22: Ivw.j0 = ((addop (X^Y)).j).(Iv.j,Iw.j) by PRVECT_1:def 8
.= (the addF of (X^Y).j).(Iv.j,Iw.j) by PRVECT_1:def 12;
per cases by A22,A3,FINSEQ_1:25;
suppose A23: j0 in dom CX; then
j0 in dom X by A1,FINSEQ_3:29; then
A24: (X^Y).j = X.j0 by FINSEQ_1:def 7;
A25: Iv.j = xx1.j & Iw.j = xx2.j by A23,A17,A18,FINSEQ_1:def 7;
A26: (xx12^yy12).j0 = xx12.j0 by A23,A17,FINSEQ_1:def 7;
reconsider j1=j0 as Element of dom carr X by A23;
(the addF of (X^Y).j).(Iv.j,Iw.j)
=((addop X ).j1).(xx1.j1,xx2.j1) by A24,A25,PRVECT_1:def 12
.= (xx12^yy12).j0 by A26,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A22;
end;
suppose ex n be Nat st n in dom CY & j0=len CX + n; then
consider n be Nat such that
A27: n in dom CY & j0=len CX + n;
A28: len CX= len xx1 & len CX = len xx2 & len CX= len xx12
by A17,FINSEQ_3:29;
n in dom Y by A1,A27,FINSEQ_3:29; then
A29: (X^Y).j = Y.n by A27,A1,FINSEQ_1:def 7;
A30: Iv.j = yy1.n & Iw.j = yy2.n by A17,A18,A27,A28,FINSEQ_1:def 7;
A31: (xx12^yy12).j0 = yy12.n by A27,A28,A17,FINSEQ_1:def 7;
reconsider j1=n as Element of dom carr Y by A27;
(the addF of (X^Y).j).(Iv.j,Iw.j)
= ((addop Y).j1).(yy1.j1,yy2.j1) by A29,A30,PRVECT_1:def 12
.= (xx12^yy12).j0 by A31,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A22;
end;
end;
hence thesis by A19,A20,A21,FINSEQ_1:13;
end;
A32:for v be Point of [:PX,PY:], r be Element of REAL holds I.(r*v)=r*(I.v)
proof
let v be Point of [:PX,PY:],r be Element of REAL;
consider x1 be Point of PX, y1 be Point of PY such that
A33: v = [x1,y1] by Lm1;
reconsider xx1=x1, yy1=y1 as FinSequence by Lm2;
reconsider rxx1=r*x1, ryy1=r*y1 as FinSequence by Lm2;
A34: dom xx1 = dom CX & dom yy1 = dom CY
& dom rxx1 = dom CX & dom ryy1 = dom CY by CARD_3:9;
A35:I.v = I.(x1,y1) by A33 .= xx1^yy1 by A2;
A36:I.(r*v) = I.(r*x1,r*y1) by A33,Def2 .= rxx1^ryy1 by A2;
reconsider Iv = I.v as Element of product carr (X^Y);
reconsider rIv=r*I.v as FinSequence by Lm2;
A37:dom rIv = dom carr (X^Y) by CARD_3:9;
A38: dom (rxx1^ryy1) = dom carr (X^Y) by A36,CARD_3:9;
for j0 be Nat st j0 in dom rIv holds rIv.j0 = (rxx1^ryy1).j0
proof
let j0 be Nat;
assume A39:j0 in dom rIv; then
reconsider j=j0 as Element of dom carr (X^Y) by CARD_3:9;
A40: rIv.j0 = ((multop (X^Y)).j).(r,Iv.j) by PRVECT_2:def 2
.= (the Mult of (X^Y).j).(r,Iv.j) by PRVECT_2:def 8;
per cases by A3,A39,A37,FINSEQ_1:25;
suppose A41: j0 in dom CX; then
j0 in dom X by A1,FINSEQ_3:29; then
A42: (X^Y).j = X.j0 by FINSEQ_1:def 7;
A43: Iv.j = xx1.j by A41,A34,A35,FINSEQ_1:def 7;
A44: (rxx1^ryy1).j0 = rxx1.j0 by A41,A34,FINSEQ_1:def 7;
reconsider j1=j0 as Element of dom carr X by A41;
(the Mult of (X^Y).j).(r,Iv.j)
= ((multop X ).j1).(r,xx1.j1) by A42,A43,PRVECT_2:def 8
.= (rxx1^ryy1).j0 by A44,PRVECT_2:def 2;
hence rIv.j0 = (rxx1^ryy1).j0 by A40;
end;
suppose ex n be Nat st n in dom CY & j0=len CX + n; then
consider n be Nat such that
A45: n in dom CY & j0=len CX + n;
A46: len CX= len xx1 & len CX= len rxx1 by A34,FINSEQ_3:29;
n in dom Y by A45,A1,FINSEQ_3:29; then
A47: (X^Y).j = Y.n by A45,A1,FINSEQ_1:def 7;
A48: Iv.j = yy1.n by A35,A45,A34,A46,FINSEQ_1:def 7;
A49: (rxx1^ryy1).j0 = ryy1.n by A45,A46,A34,FINSEQ_1:def 7;
reconsider j1=n as Element of dom carr Y by A45;
(the Mult of (X^Y).j).(r,Iv.j)
= ((multop Y ).j1).(r,yy1.j1) by A47,A48,PRVECT_2:def 8
.= (rxx1^ryy1).j0 by A49,PRVECT_2:def 2;
hence rIv.j0 = (rxx1^ryy1).j0 by A40;
end;
end;
hence thesis by A36,A38,A37,FINSEQ_1:13;
end;
I.(0.[:PX,PY:]) = I.(0.[:PX,PY:] + 0.[:PX,PY:])
.= I.(0.[:PX,PY:]) + I.(0.[:PX,PY:]) by A14; then
I.(0.[:PX,PY:]) - I.(0.[:PX,PY:])
= I.(0.[:PX,PY:]) + (I.(0.[:PX,PY:]) - I.(0.[:PX,PY:])) by RLVECT_1:28
.= I.(0.[:PX,PY:]) + 0. product (X^Y) by RLVECT_1:15
.= I.(0.[:PX,PY:]); then
0. product (X^Y) = I.(0.[:PX,PY:]) by RLVECT_1:15;
hence thesis by A13,A14,A32,A2,A12;
end;
theorem
for G,F be RealLinearSpace holds
( for x be set holds
( x is Point of product <*G,F*>
iff ex x1 be Point of G, x2 be Point of F st x=<* x1,x2 *> ) )
& ( for x,y be Point of product <*G,F*>,
x1,y1 be Point of G ,x2,y2 be Point of F
st x = <*x1,x2*> & y = <*y1,y2*>
holds x+y = <*x1+y1,x2+y2*> )
& 0.(product <*G,F*>) = <* 0.G,0.F *>
& ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F
st x=<* x1,x2 *> holds -x = <* -x1,-x2 *> )
& ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F,
a be Real
st x = <*x1,x2*> holds a*x = <* a*x1,a*x2 *> )
proof
let G,F be RealLinearSpace;
consider I be Function of [:G,F:], product <* G,F *> such that
A1: I is one-to-one & I is onto
& ( for x be Point of G, y be Point of F holds I.(x,y) = <* x,y *> )
& ( for v,w be Point of [:G,F:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:G,F:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*G,F*> = I.(0.[:G,F:]) by Th12;
thus
A2: for x be set holds
( x is Point of product <*G,F*>
iff ex x1 be Point of G, x2 be Point of F st x=<* x1,x2 *> )
proof
let y be set;
hereby assume y is Point of product <*G,F*>; then
y in the carrier of product <*G,F*>; then
y in rng I by A1,FUNCT_2:def 3; then
consider x be Element of the carrier of [:G,F:] such that
A3: y = I.x by FUNCT_2:113;
consider x1 be Point of G, x2 be Point of F such that
A4: x=[x1,x2] by Lm1;
take x1,x2;
I.(x1,x2) = <*x1,x2*> by A1;
hence y = <*x1,x2*> by A3,A4;
end;
now assume ex x1 be Point of G, x2 be Point of F st y = <*x1,x2*>; then
consider x1 be Point of G, x2 be Point of F such that
A5: y = <*x1,x2*>;
A6: I.[x1,x2] in rng I by FUNCT_2:112;
I.(x1,x2) = <*x1,x2*> by A1;
hence y is Point of product <*G,F*> by A5,A6;
end;
hence thesis;
end;
thus
A7: for x,y be Point of product <*G,F*>,
x1,y1 be Point of G, x2,y2 be Point of F
st x = <*x1,x2*> & y = <*y1,y2*>
holds x+y = <*x1+y1,x2+y2*>
proof
let x,y be Point of product <*G,F*>;
let x1,y1 be Point of G, x2,y2 be Point of F;
assume A8: x = <*x1,x2*> & y = <*y1,y2*>;
reconsider z=[x1,x2], w=[y1,y2] as Point of [:G,F:];
A9: z+w = [x1+y1,x2+y2] by Def1;
I.(x1+y1,x2+y2) = <* x1+y1,x2+y2 *>
& I.(x1,x2) = <* x1,x2 *> & I.(y1,y2) = <* y1,y2 *> by A1;
hence <* x1+y1,x2+y2 *> =x+y by A1,A9,A8;
end;
thus
A10: 0. product <*G,F*> = <* 0.G,0.F *>
proof
I.(0.G,0.F) = <* 0.G,0.F *> by A1;
hence thesis by A1;
end;
thus for x be Point of product <*G,F*>,
x1 be Point of G, x2 be Point of F
st x = <*x1,x2*> holds -x = <* -x1,-x2 *>
proof
let x be Point of product <*G,F*>;
let x1 be Point of G, x2 be Point of F;
assume A11: x=<* x1,x2 *>;
reconsider y = <* -x1,-x2 *> as Point of product <*G,F*> by A2;
x+y = <* x1+-x1,x2+-x2 *> by A7,A11
.= <* 0.G,x2+-x2 *> by RLVECT_1:def 10
.= 0.(product <*G,F*>) by A10,RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
thus for x be Point of product <*G,F*>,
x1 be Point of G, x2 be Point of F, a be Real
st x=<* x1,x2 *> holds a*x = <* a*x1,a*x2 *>
proof
let x be Point of product <*G,F*>;
let x1 be Point of G, x2 be Point of F, a be Real;
assume A12: x=<* x1,x2 *>;
reconsider a0=a as Element of REAL by XREAL_0:def 1;
reconsider y=[x1,x2] as Point of [:G,F:];
A13: <* x1,x2 *> = I.(x1,x2) by A1;
I.(a*y) = I.(a0*x1,a0*x2) by Th9
.= <* a0*x1,a0*x2 *> by A1;
hence thesis by A1,A12,A13;
end;
end;
begin :: Cartesian Product of Real Normed Linear Spaces
definition let G,F be non empty NORMSTR;
func prod_NORM(G,F) -> Function of
[:the carrier of G,the carrier of F:], REAL means :Def6:
for g be Point of G, f be Point of F
holds ex v be Element of REAL 2
st v= <* ||.g.||,||.f.|| *> & it.(g,f) = |.v.|;
existence
proof
defpred NRM[object,object,object] means
ex g be Point of G, f be Point of F, v be Element of REAL 2
st $1=g & $2=f & v=<* ||.g.||,||.f.|| *> & $3 = |.v.|;
A1:for x,y be object st x in the carrier of G & y in the carrier of F
ex z be object st z in REAL & NRM[x,y,z]
proof
let x,y be object;
assume A2: x in the carrier of G & y in the carrier of F; then
reconsider g=x as Point of G;
reconsider f=y as Point of F by A2;
reconsider v=<* ||.g.||,||.f.|| *> as Element of REAL 2 by FINSEQ_2:101;
|.v.| in REAL by XREAL_0:def 1;
hence thesis;
end;
consider NORMGF be Function of [:the carrier of G,the carrier of F:], REAL
such that
A3: for x,y be object st x in the carrier of G & y in the carrier of F
holds NRM[x,y,NORMGF.(x,y)] from BINOP_1:sch 1(A1);
now let g be Point of G, f be Point of F;
ex gg be Point of G, ff be Point of F, v be Element of REAL 2 st
g=gg & f=ff & v=<* ||.gg.||,||.ff.|| *> & NORMGF.(g,f) = |.v.| by A3;
hence ex v be Element of REAL 2 st
v=<* ||.g.||,||.f.|| *> & NORMGF.(g,f) = |. v .|;
end;
hence thesis;
end;
uniqueness
proof
let H1,H2 be Function of [:the carrier of G,the carrier of F:],REAL;
assume
A4: for g be Point of G, f be Point of F
ex v be Element of REAL 2 st v=<* ||.g.||,||.f.|| *> & H1.(g,f) = |.v.|;
assume
A5: for g be Point of G, f be Point of F
ex v be Element of REAL 2 st v=<* ||.g.||,||.f.|| *> & H2.(g,f) = |.v.|;
now let g be Element of the carrier of G, f be Element of the carrier of F;
A6:ex v1 be Element of REAL 2 st
v1=<* ||.g.||,||.f.|| *> & H1.(g,f) = |.v1.| by A4;
ex v2 be Element of REAL 2 st
v2=<* ||.g.||,||.f.|| *> & H2.(g,f) = |.v2.| by A5;
hence H1.(g,f) = H2.(g,f) by A6;
end;
hence H1=H2;
end;
end;
definition let G,F be non empty NORMSTR;
func [:G,F:] -> strict non empty NORMSTR equals
NORMSTR (# [:the carrier of G,the carrier of F:],
prod_ZERO(G,F), prod_ADD(G,F), prod_MLT(G,F), prod_NORM(G,F) #);
correctness;
end;
definition let G,F be non empty NORMSTR;
let g be Element of G, f be Element of F;
redefine func [g,f] -> Element of [:G,F:]; :: redefines [ (TARSKI, definition)
coherence
proof
[g,f] in the carrier of [:G,F:];
hence thesis;
end;
end;
registration
let G,F be RealNormSpace;
cluster [:G,F:] -> reflexive discerning RealNormSpace-like;
correctness
proof
now let x be Point of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A1: x = [x1,x2] by Lm1;
consider v be Element of REAL 2 such that
A2: v=<* ||.x1.||,||.x2.|| *> & prod_NORM(G,F).(x1,x2) = |.v.|
by Def6;
assume x = 0.[:G,F:]; then
x1=0.G & x2=0.F by A1,XTUPLE_0:1; then
||.x1.||=0 & ||.x2.|| =0; then
v=0*2 by A2,FINSEQ_2:61;
hence ||.x.|| = 0 by A2,A1,EUCLID:7;
end; then
||. 0.[:G,F:] .|| = 0;
hence [:G,F:] is reflexive;
now let x be Point of [:G,F:];
consider x1 be Point of G, x2 be Point of F such that
A3: x=[x1,x2] by Lm1;
consider v be Element of REAL 2 such that
A4: v=<* ||.x1.||,||.x2.|| *> & prod_NORM(G,F).(x1,x2) = |.v.|
by Def6;
assume ||.x.|| = 0; then
v =0*2 by A4,A3,EUCLID:8; then
A5: v=<* 0,0 *> by FINSEQ_2:61;
||.x1.|| = v.1 & ||.x2.|| = v.2 by A4; then
||.x1.|| = 0 & ||.x2.|| = 0 by A5; then
x1 = 0.G & x2 = 0.F by NORMSP_0:def 5;
hence x=0.[:G,F:] by A3;
end;
hence [:G,F:] is discerning;
now let x,y be Point of [:G,F:], a be Real;
consider x1 be Point of G, x2 be Point of F such that
A6: x = [x1,x2] by Lm1;
consider y1 be Point of G, y2 be Point of F such that
A7: y = [y1,y2] by Lm1;
consider v be Element of REAL 2 such that
A8: v=<* ||.x1.||,||.x2.|| *> & prod_NORM(G,F).(x1,x2) = |.v.|
by Def6;
consider z be Element of REAL 2 such that
A9: z=<* ||.y1.||,||.y2.|| *> & prod_NORM(G,F).(y1,y2) = |.z.|
by Def6;
thus ||.a * x.|| = |.a.| * ||.x.||
proof
consider w be Element of REAL 2 such that
A10: w=<* ||. a*x1 .||,||. a*x2 .|| *> &
prod_NORM(G,F).(a*x1,a*x2) = |.w.| by Def6;
reconsider aa= |.a.| ,xx1 = ||.x1.||, xx2=||.x2.|| as Real;
||. a*x1 .|| = |.a.|*||.x1.|| & ||. a*x2 .||=|.a.|*||.x2.||
by NORMSP_1:def 1; then
w = aa * |[ xx1,xx2 ]| by A10,EUCLID:58
.= |.a.|* v by A8,EUCLID:65; then
|.w.| = |.|.a.|.|*|.v.| by EUCLID:11
.= |.a.|*|.v.|;
hence thesis by A8,A10,A6,Def2;
end;
thus ||.x + y.|| <= ||.x.|| + ||.y.||
proof
consider w be Element of REAL 2 such that
A11: w=<* ||. x1+y1 .||,||. x2+y2 .|| *>
& prod_NORM(G,F).(x1+y1,x2+y2) = |.w.| by Def6;
A12: ||.x + y.|| = |.w.| by A11,A6,A7,Def1;
A13: ||. x1+y1 .||<=||.x1.|| + ||.y1.|| &
||. x2+y2 .||<=||.x2.|| + ||.y2.|| by NORMSP_1:def 1;
reconsider t1 = ||.x1.|| + ||.y1.||, t2= ||.x2.|| + ||.y2.||
as Element of REAL
by XREAL_0:def 1;
reconsider t = <*t1,t2*> as FinSequence of REAL;
A14: len w = 2 & len t = 2 by A11,FINSEQ_1:44;
now let i be Element of NAT;
assume i in Seg len w; then
A15: i in Seg 2 by A11,FINSEQ_1:44;
per cases by A15,FINSEQ_1:2,TARSKI:def 2;
suppose A16: i=1; then
w.i = ||. x1+y1 .|| by A11;
hence 0 <= w.i & w.i <= t.i by A13,A16,NORMSP_1:4;
end;
suppose A17: i=2; then
w.i = ||. x2+y2 .|| by A11;
hence 0 <= w.i & w.i <= t.i by A13,A17,NORMSP_1:4;
end;
end; then
A18: |.w.| <= |.t.| by A14,PRVECT_2:2;
t = |[ ||.x1.||,||.x2.|| ]| + |[ ||.y1.||,||.y2.|| ]| by EUCLID:56
.= v + z by A8,A9,EUCLID:64; then
|.t.| <= |.v.| + |.z.| by EUCLID:12;
hence thesis by A12,A6,A8,A7,A9,A18,XXREAL_0:2;
end;
end;
hence thesis by NORMSP_1:def 1;
end;
end;
registration
let G,F be reflexive discerning RealNormSpace-like
scalar-distributive vector-distributive scalar-associative
scalar-unital Abelian add-associative
right_zeroed right_complementable non empty NORMSTR;
cluster [:G,F:] -> strict reflexive discerning RealNormSpace-like
scalar-distributive vector-distributive scalar-associative
scalar-unital Abelian add-associative right_zeroed right_complementable;
correctness
proof
reconsider G0 = G, F0 = F as RealLinearSpace;
the RLSStruct of [:G,F:] = [:G0,F0:];
hence thesis by RSSPACE3:2;
end;
end;
registration
let G be reflexive discerning RealNormSpace-like scalar-distributive
vector-distributive scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable non empty NORMSTR;
cluster <*G*> -> RealNormSpace-yielding;
correctness
proof
let S be set;
assume S in rng <*G*>; then
consider i be object such that
A1: i in dom <*G*> & <*G*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
len <*G*> = 1 by FINSEQ_1:40; then
dom <*G*> = {1} by FINSEQ_1:2,def 3; then
i=1 by A1,TARSKI:def 1;
hence S is RealNormSpace by A1;
end;
end;
registration
let G,F be reflexive discerning RealNormSpace-like scalar-distributive
vector-distributive scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable non empty NORMSTR;
cluster <*G,F*> -> RealNormSpace-yielding;
correctness
proof
let S be set;
assume S in rng <*G,F*>; then
consider i be object such that
A1: i in dom <*G,F*> & <*G,F*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
dom <*G,F*> = {1,2} by FINSEQ_1:2,89; then
i=1 or i=2 by A1,TARSKI:def 2;
hence S is RealNormSpace by A1;
end;
end;
theorem Th15:
for X,Y be RealNormSpace
holds ex I be Function of [:X,Y:],product <*X,Y*>
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> )
& ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:X,Y:], r be Real
holds I.(r*v)=r*(I.v) )
& 0. product <*X,Y*> = I.(0.[:X,Y:])
& ( for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| )
proof
let X,Y be RealNormSpace;
reconsider X0=X, Y0=Y as RealLinearSpace;
consider I0 be Function of [:X0,Y0:],product <*X0,Y0*> such that
A1: I0 is one-to-one & I0 is onto
& ( for x be Point of X, y be Point of Y holds I0.(x,y) = <*x,y*> )
& ( for v,w be Point of [:X0,Y0:] holds I0.(v+w) = I0.v + I0.w )
& ( for v be Point of [:X0,Y0:], r be 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;
thus I is one-to-one & I is onto
& ( for x be Point of X,y be Point of Y
holds I.(x,y) = <*x,y*> ) by A1,A2;
thus for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:X,Y:];
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;
end;
thus for v be Point of [:X,Y:], r be Real
holds I.(r*v)=r*(I.v)
proof
let v be Point of [:X,Y:], r be Real;
reconsider v0=v as Point of [:X0,Y0:];
thus I.(r*v) = I0.(r*v0)
.= r*(I0.v0) by A1
.= r*(I.v) by A2;
end;
thus 0. product <*X,Y*> = I.(0.[:X,Y:]) by A1,A2;
for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.||
proof
let v be Point of [:X,Y:];
consider x1 be Point of X, y1 be Point of Y such that
A3: v = [x1,y1] by Lm1;
consider v1 be 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;
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,89;
A7: normsequence(<*X,Y*>,Iv).j1
= (the normF of <*X,Y*>.j1).(Iv.j1) by PRVECT_2:def 11
.= ||.x1.|| by A5;
A8: normsequence(<*X,Y *>,Iv).j2
= (the normF of <*X,Y*>.j2).(Iv.j2) by PRVECT_2:def 11
.= ||.y1.|| by A5;
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 thesis by A4,A3,A2,PRVECT_2:def 12;
end;
hence thesis;
end;
theorem Th16:
for X be RealNormSpace
holds ex I be Function of X ,product <*X*>
st I is one-to-one & I is onto
& ( for x be Point of X holds I.x = <*x*> )
& ( for v,w be Point of X holds I.(v+w) = I.v + I.w )
& ( for v be Point of X, r be Element of REAL holds I.(r*v)=r*(I.v) )
& 0. product <*X*> = I.(0.X)
& ( for v be Point of X holds ||. I.v .|| = ||.v.|| )
proof
let X be RealNormSpace;
reconsider X0= X as RealLinearSpace;
consider I0 be Function of X0,product <*X0*> such that
A1: I0 is one-to-one & I0 is onto
& ( for x be Point of X holds I0.x = <*x*> )
& ( for v,w be Point of X0 holds I0.(v+w) = I0.v + I0.w )
& ( for v be Point of X0, r be 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;
thus I is one-to-one & I is onto
& ( for x be Point of X holds I.x = <*x*> ) by A1,A2;
thus for v,w be Point of X holds I.(v+w) = I.v + I.w
proof
let v,w be Point of X;
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;
end;
thus for v be Point of X, r be Element of REAL holds I.(r*v)=r*(I.v)
proof
let v be Point of X, r be Element of REAL;
reconsider v0=v as Point of X0;
thus I.(r*v) = r*(I0.v0) by A1 .= r*(I.v) by A2;
end;
thus 0. product <*X*> = I.(0.X) by A1,A2;
thus for v be Point of X holds ||. I.v .|| = ||.v.||
proof
let v be Point of X;
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;
1 in {1} by TARSKI:def 1; then
reconsider j1=1 as Element of dom <*X*> by FINSEQ_1:2,def 8;
A7: normsequence(<*X*>,Iv).j1
= (the normF of (<*X*>.j1)).(Iv.j1) by PRVECT_2:def 11
.= ||.v.|| by A5;
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 thesis by A4,A2,PRVECT_2:def 12;
end;
end;
registration
let G,F be non empty RealNormSpace-yielding FinSequence;
cluster G^F -> non empty RealNormSpace-yielding;
correctness
proof
for S be set st S in rng (G^F) holds S is RealNormSpace
proof
let S be set;
assume S in rng (G^F); then
consider i be object such that
A1: i in dom (G^F) & (G^F).i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
per cases by A1,FINSEQ_1:25;
suppose A2: i in dom G; then
G.i in rng G by FUNCT_1:3; then
G.i is RealNormSpace by PRVECT_2:def 10;
hence S is RealNormSpace by A1,A2,FINSEQ_1:def 7;
end;
suppose ex n be Nat st n in dom F & i=len G + n; then
consider n be Nat such that
A3: n in dom F & i=len G + n;
F.n in rng F by A3,FUNCT_1:3; then
F.n is RealNormSpace by PRVECT_2:def 10;
hence S is RealNormSpace by A1,A3,FINSEQ_1:def 7;
end;
end;
hence thesis;
end;
end;
Lm3:
for F1,F2 be FinSequence of REAL holds sqr (F1^F2) = sqr(F1)^sqr(F2)
by RVSUM_1:144;
theorem Th17:
for X,Y be non empty RealNormSpace-Sequence
holds ex I be Function of [:product X,product Y:],product (X^Y)
st I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of product Y
holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1 )
& ( for v,w be Point of [:product X,product Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:product X,product Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[:product X,product Y:]) = 0.product (X^Y)
& ( for v be Point of [:product X,product Y:] holds ||. I.v .|| = ||.v.|| )
proof
let X,Y be non empty RealNormSpace-Sequence;
reconsider X0=X, Y0=Y as non empty 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 be Point of PX, f1,f2 be Point of PY
holds (prod_ADD(PX0,PY0)).([g1,f1],[g2,f2]) = [g1+g2,f1+f2]
proof
let g1,g2 be Point of PX, f1,f2 be Point of PY;
reconsider g10=g1, g20=g2 as Point of PX0 by A1;
reconsider f10=f1, f20=f2 as Point of PY0 by A1;
g10+g20 =g1+g2 & f10+f20 =f1+f2 by A1;
hence (prod_ADD(PX0,PY0)).([g1,f1],[g2,f2])
= [g1+g2,f1+f2] by Def1;
end;
A3:for r be Real, g be Point of PX, f be Point of PY
holds (prod_MLT(PX0,PY0)).(r,[g,f]) = [r*g,r*f]
proof
let r be Real, g be Point of PX, f be Point of PY;
reconsider g0=g as Point of PX0 by A1;
reconsider f0=f as Point of PY0 by A1;
r*g0=r*g & r*f0=r*f by A1;
hence (prod_MLT(PX0,PY0)).(r,[g,f]) = [r*g,r*f] by Def2;
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 be Function of [:PX0,PY0:], product (X0^Y0) such that
A5: I0 is one-to-one & I0 is onto
& ( for x be Point of PX0, y be Point of PY0
ex x1,y1 be FinSequence st x=x1 & y=y1 & I0.(x,y) = x1^y1 )
& ( for v,w be Point of [:PX0,PY0:] holds I0.(v+w) = I0.v + I0.w )
& ( for v be Point of [:PX0,PY0:], r be Element of REAL
holds I0.(r*v)=r*(I0.v) )
& 0. product (X0^Y0) = I0.(0.[:PX0,PY0:]) 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 [:PX,PY:],product (X^Y) by A1;
take I;
thus I is one-to-one & I is onto by A5,A6;
thus for x be Point of PX, y be Point of PY
holds ex x1,y1 be FinSequence
st x=x1 & y=y1 & I.(x,y) = x1^y1 by A1,A5;
A7:
for x,y be FinSequence
st x in the carrier of product X & y in the carrier of product Y
holds I.(x,y) = x^y
proof
let x,y be FinSequence;
assume x in the carrier of product X
& y in the carrier of product Y; then
ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1 by A1,A5;
hence thesis;
end;
thus for v,w be Point of [:PX,PY:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:PX,PY:];
reconsider v0=v, w0=w as Point of [:PX0,PY0:] by A1;
v+w = v0+w0 by A2,A1,Def1; then
I.(v+w) = I0.v0 + I0.w0 by A5;
hence I.(v+w) = I.v + I.w by A6;
end;
thus for v be Point of [:PX,PY:], r be Element of REAL
holds I.(r*v)=r*(I.v)
proof
let v be Point of [:PX,PY:], r be Element of REAL;
reconsider v0=v as Point of [:PX0,PY0:] by A1;
r*v = r*v0 by A3,A1,Def2; then
I.(r*v) = r*(I0.v0) by A5;
hence I.(r*v) = r*(I.v) by A6;
end;
thus 0. product (X^Y) = I.(0.[:PX,PY:]) by A1,A5,A6;
for v be Point of [:PX,PY:] holds ||. I.v .|| = ||.v.||
proof
let v be Point of [:PX,PY:];
consider x1 be Point of PX, y1 be Point of PY such that
A8: v = [x1,y1] by Lm1;
consider v1 be Element of REAL 2 such that
A9:v1=<* ||.x1.||,||.y1.|| *> &
prod_NORM(PX,PY).(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 be 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;
assume k in dom normsequence((X^Y),Iv); 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 by A19,FINSEQ_1:25;
suppose A23: k in dom X;
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;
end;
suppose ex n be Nat st n in dom Y & k=len X + n; then
consider n be 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;
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 thesis by A14,A12,A16,A9,A8,RVSUM_1:75;
end;
hence thesis;
end;
theorem Th18:
for G,F be RealNormSpace holds
( for x be set holds
( x is Point of [:G,F:]
iff ex x1 be Point of G ,x2 be Point of F st x=[x1,x2]) )
& ( for x,y be Point of [:G,F:], x1,y1 be Point of G, x2,y2 be Point of F
st x=[x1,x2] & y=[y1,y2] holds x+y = [x1+y1,x2+y2] )
& 0.[:G,F:] = [0.G,0.F]
& ( for x be Point of [:G,F:], x1 be Point of G, x2 be Point of F
st x=[x1,x2] holds -x = [-x1,-x2] )
& ( for x be Point of [:G,F:], x1 be Point of G, x2 be Point of F,
a be Real
st x=[x1,x2] holds a*x = [a*x1,a*x2] )
& ( for x be Point of [:G,F:], x1 be Point of G, x2 be Point of F
st x=[x1,x2] holds
ex w be Element of REAL 2 st
w=<* ||.x1.||,||.x2.|| *> & ||.x.|| = |.w.| )
proof
let G,F be RealNormSpace;
thus for x be set holds
( x is Point of [:G,F:]
iff ex x1 be Point of G, x2 be Point of F st x=[x1,x2] ) by Lm1;
thus for x,y be Point of [:G,F:], x1,y1 be Point of G,x2,y2 be Point of F
st x=[x1,x2] & y=[y1,y2] holds x+y = [x1+y1,x2+y2] by Def1;
thus 0.[:G,F:] = [0.G,0.F];
thus for x be Point of [:G,F:], x1 be Point of G ,x2 be Point of F
st x=[x1,x2] holds -x = [-x1,-x2]
proof
let x be Point of [:G,F:];
let x1 be Point of G, x2 be Point of F;
assume A1: x=[x1,x2];
reconsider y= [-x1,-x2 ] as Point of [:G,F:];
x+y = [x1+-x1,x2+-x2] by A1,Def1
.= [0.G,x2+-x2] by RLVECT_1:def 10
.= 0.[:G,F:] by RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
thus for x be Point of [:G,F:], x1 be Point of G,
x2 be Point of F, a be Real
st x=[x1,x2] holds a*x = [a*x1,a*x2]
by Def2;
thus for x be Point of [:G,F:], x1 be Point of G ,x2 be Point of F
st x=[x1,x2] holds
ex w be Element of REAL 2
st w=<* ||.x1.||,||.x2.|| *> & ||.x.|| = |.w.|
proof
let x be Point of [:G,F:], x1 be Point of G, x2 be Point of F;
assume A2: x=[x1,x2];
ex w be Element of REAL 2 st
w=<* ||.x1.||,||.x2.|| *> & prod_NORM(G,F).(x1,x2) = |.w.| by Def6;
hence thesis by A2;
end;
end;
theorem
for G,F be RealNormSpace holds
( for x be set holds
( x is Point of product <*G,F*>
iff ex x1 be Point of G, x2 be Point of F st x=<* x1,x2 *> ) )
& ( for x,y be Point of product <*G,F*>,
x1,y1 be Point of G, x2,y2 be Point of F
st x=<*x1,x2*> & y=<*y1,y2*> holds x+y = <* x1+y1,x2+y2 *> )
& 0.(product <*G,F*>) = <* 0.G,0.F *>
& ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F
st x=<*x1,x2*> holds -x = <* -x1,-x2 *> )
& ( for x be Point of product <*G,F*>,
x1 be Point of G, x2 be Point of F, a be Real
st x=<*x1,x2*> holds a*x = <* a*x1,a*x2 *> )
& ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F
st x=<*x1,x2*> holds
ex w be Element of REAL 2 st
w=<* ||.x1.||,||.x2.|| *> & ||.x.|| = |.w.| )
proof
let G,F be RealNormSpace;
consider I be Function of [:G,F:] ,product <*G,F*> such that
A1: I is one-to-one & I is onto
& ( for x be Point of G, y be Point of F holds I.(x,y) = <*x,y*> )
& ( for v,w be Point of [:G,F:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:G,F:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*G,F*> = I.(0.[:G,F:])
& ( for v be Point of [:G,F:] holds ||. I.v .|| = ||.v.|| ) by Th15;
thus
A2: for x be set holds
(x is Point of product <*G,F*>
iff ex x1 be Point of G, x2 be Point of F st x=<*x1,x2*> )
proof
let y be set;
hereby assume y is Point of product <*G,F*>; then
y in the carrier of product <*G,F*>; then
y in rng I by A1,FUNCT_2:def 3; then
consider x be Element of the carrier of [:G,F:] such that
A3: y = I.x by FUNCT_2:113;
consider x1 be Point of G, x2 be Point of F such that
A4: x=[x1,x2] by Lm1;
take x1,x2;
I.(x1,x2) = <*x1,x2*> by A1;
hence y= <*x1,x2*> by A3,A4;
end;
hereby assume ex x1 be Point of G, x2 be Point of F st
y=<* x1,x2 *>; then
consider x1 be Point of G, x2 be Point of F such that
A5: y=<*x1,x2*>;
A6: I.([x1,x2]) in rng I by FUNCT_2:112;
I.(x1,x2) = <*x1,x2*> by A1;
hence y is Point of product <*G,F*> by A5,A6;
end;
end;
thus
A7: for x,y be Point of product <*G,F*>,
x1,y1 be Point of G, x2,y2 be Point of F
st x=<*x1,x2*> & y=<*y1,y2*> holds x+y = <* x1+y1,x2+y2 *>
proof
let x,y be Point of product <*G,F*>;
let x1,y1 be Point of G, x2,y2 be Point of F;
assume A8: x=<*x1,x2*> & y=<*y1,y2*>;
reconsider z=[x1,x2], w=[y1,y2] as Point of [:G,F:];
A9: z+w = [x1+y1,x2+y2] by Def1;
A10: I.(x1+y1,x2+y2) = <* x1+y1,x2+y2 *> by A1;
I.(x1,x2) = <* x1,x2 *> & I.(y1,y2) = <* y1,y2 *> by A1;
hence <* x1+y1,x2+y2 *> = x+y by A1,A9,A10,A8;
end;
thus
A11: 0. product <*G,F*> = <* 0.G,0.F *>
proof
I.(0.G,0.F) =<* 0.G,0.F *> by A1;
hence thesis by A1;
end;
thus for x be Point of product <*G,F*>,
x1 be Point of G, x2 be Point of F
st x=<*x1,x2*> holds -x = <* -x1,-x2 *>
proof
let x be Point of product <*G,F*>;
let x1 be Point of G, x2 be Point of F;
assume A12: x=<* x1,x2 *>;
reconsider y=<* -x1,-x2 *> as Point of product <*G,F*> by A2;
x+y = <* x1+-x1,x2+-x2 *> by A7,A12
.= <* 0.G,x2+-x2 *> by RLVECT_1:def 10
.= 0.(product <*G,F*>) by A11,RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
thus for x be Point of product <*G,F*>,
x1 be Point of G, x2 be Point of F, a be Real
st x=<*x1,x2*> holds a*x = <* a*x1,a*x2 *>
proof
let x be Point of product <*G,F*>;
let x1 be Point of G, x2 be Point of F, a be Real;
assume A13: x=<*x1,x2*>;
reconsider a0=a as Element of REAL by XREAL_0:def 1;
reconsider y=[x1,x2] as Point of [:G,F:];
A14: <*x1,x2*> = I.(x1,x2) by A1;
I.(a*y) = I.(a0*x1,a0*x2) by Th18
.= <* a0*x1,a0*x2 *> by A1;
hence thesis by A13,A14,A1;
end;
thus for x be Point of product <*G,F*>,
x1 be Point of G, x2 be Point of F st x=<*x1,x2*>
holds ex w be Element of REAL 2 st
w=<* ||.x1.||,||.x2.|| *> & ||.x.|| = |.w.|
proof
let x be Point of product <*G,F*>;
let x1 be Point of G, x2 be Point of F;
assume A15: x=<*x1,x2*>;
reconsider y=[x1,x2] as Point of [:G,F:];
consider w be Element of REAL 2 such that
A16: w=<* ||.x1.||,||.x2.|| *> & ||.y.|| = |.w.| by Th18;
take w;
A17: I.y = I.(x1,x2) .=x by A1,A15;
thus w=<* ||.x1.||,||.x2.|| *> by A16;
thus||.x.|| = |.w.| by A1,A16,A17;
end;
end;
registration
let X,Y be complete RealNormSpace;
cluster [:X,Y:] -> complete;
coherence
proof
A1:dom <*X,Y*> ={1,2} by FINSEQ_1:2,89;
now let i be Element of dom <*X,Y*>;
i=1 or i=2 by A1,TARSKI:def 2;
hence <*X,Y*>.i is complete;
end; then
A2:product <*X,Y*> is complete by PRVECT_2:14;
consider I be Function of [:X,Y:], product <*X,Y*> such that
A3: I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> )
& ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:X,Y:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*X,Y*> = I.(0.[:X,Y:])
& ( for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| ) by Th15;
A4:now let v,w be Point of [:X,Y:];
thus I.(v-w) = I.(v+(-1)*w) by RLVECT_1:16
.= I.v + I.((-1)*w) by A3
.= I.v + (-1)*(I.w) by A3
.= I.v - I.w by RLVECT_1:16;
end;
A5:now let v,w be Point of [:X,Y:];
thus ||. I.v-I.w .|| = ||. I.(v-w) .|| by A4
.= ||. v-w .|| by A3;
end;
now let seq be sequence of [:X,Y:];
assume A6: seq is Cauchy_sequence_by_Norm;
reconsider Iseq = I*seq as sequence of product <*X,Y*>;
now let r be Real;
assume r > 0; then
consider k be Nat such that
A7: for n,m be Nat st n >= k & m >= k
holds ||.( seq.n) - (seq.m).|| < r by A6,RSSPACE3:8;
take k;
let n, m be Nat;
A8: n in NAT & m in NAT by ORDINAL1:def 12;
assume n >= k & m >= k; then
A9: ||. seq.n - seq.m .|| < r by A7;
NAT = dom seq by FUNCT_2:def 1; then
Iseq.n= I.(seq.n) & Iseq.m= I.(seq.m) by FUNCT_1:13,A8;
hence ||. Iseq.n - Iseq.m .|| < r by A9,A5;
end; then
Iseq is Cauchy_sequence_by_Norm by RSSPACE3:8; then
A10: Iseq is convergent by A2,LOPBAN_1:def 15;
dom (I") = rng I & rng (I") = dom I by A3,FUNCT_1:33; then
dom (I") = the carrier of product <*X,Y*> &
rng (I") = the carrier of [:X,Y:] by A3,FUNCT_2:def 1,def 3; then
reconsider Lseq = I".(lim Iseq) as Point of [:X,Y:] by FUNCT_1:3;
rng I = the carrier of product <*X,Y*> by A3,FUNCT_2:def 3; then
A11: I.Lseq = lim Iseq by A3,FUNCT_1:35;
now let r be Real;
assume 0 < r; then
consider m be Nat such that
A12: for n be Nat
st m <= n holds ||. Iseq.n - lim Iseq .|| < r by A10,NORMSP_1:def 7;
take m;
let n be Nat;
A13: n in NAT by ORDINAL1:def 12;
assume m <= n; then
A14: ||. Iseq.n - lim Iseq .|| < r by A12;
NAT = dom seq by FUNCT_2:def 1; then
Iseq.n = I.(seq.n) by FUNCT_1:13,A13;
hence ||. seq.n - Lseq .|| < r by A11,A5,A14;
end;
hence seq is convergent by NORMSP_1:def 6;
end;
hence thesis by LOPBAN_1:def 15;
end;
end;
theorem
for X,Y be non empty RealNormSpace-Sequence
holds ex I be Function of product <* product X,product Y *>,product (X^Y)
st I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of product Y
holds ex x1,y1 be FinSequence
st x=x1 & y=y1 & I.<*x,y*> = x1^y1 )
& ( for v,w be Point of product <* product X,product Y *>
holds I.(v+w) = I.v + I.w )
& ( for v be Point of product <* product X,product Y *>,
r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.(product <* product X,product Y *>)) = 0.product (X^Y)
& ( for v be Point of product <* product X,product Y *>
holds ||. I.v .|| = ||.v.|| )
proof
let X,Y be non empty RealNormSpace-Sequence;
set PX = product X;
set PY = product Y;
set PXY = product(X^Y);
consider K be Function of [:PX,PY:],PXY such that
A1: K is one-to-one & K is onto
& ( for x be Point of PX, y be Point of PY
holds ex x1,y1 be FinSequence st x=x1 & y=y1 & K.(x,y) = x1^y1 )
& ( for v,w be Point of [:PX,PY:] holds K.(v+w) = K.v + K.w )
& ( for v be Point of [:PX,PY:], r be Element of REAL
holds K.(r*v)=r*(K.v) )
& K.(0.[:PX,PY:]) = 0.PXY
& ( for v be Point of [:PX,PY:] holds ||. K.v .|| = ||.v.|| ) by Th17;
consider J be Function of [:PX,PY:],product<*PX,PY*> such that
A2: J is one-to-one & J is onto
& ( for x be Point of PX, y be Point of PY holds J.(x,y) = <*x,y*> )
& ( for v,w be Point of [:PX,PY:] holds J.(v+w) = J.v + J.w )
& ( for v be Point of [:PX,PY:], r be Real
holds J.(r*v)=r*(J.v) )
& 0. product <*PX,PY*> = J.(0.[:PX,PY:])
& ( for v be Point of [:PX,PY:] holds ||. J.v .|| = ||.v.|| ) by Th15;
A3:rng J = the carrier of product <*PX,PY*> by A2,FUNCT_2:def 3; then
reconsider JB=J" as Function of the carrier of product <*PX,PY*>,
the carrier of [:PX,PY:] by A2,FUNCT_2:25;
A4:dom (J") = rng J & rng (J") = dom J by A2,FUNCT_1:33; then
A5:dom (J") = the carrier of product <*PX,PY*> by A2,FUNCT_2:def 3;
A6:rng (J") = the carrier of [:PX,PY:] by A4,FUNCT_2:def 1;
reconsider I= K*JB as Function of product <*PX,PY*>,PXY;
take I;
thus I is one-to-one by A1,A2;
rng K = the carrier of PXY by A1,FUNCT_2:def 3; then
rng I = the carrier of PXY by A6,FUNCT_2:14;
hence I is onto by FUNCT_2:def 3;
thus for x be Point of PX, y be Point of PY
holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.<*x,y*> = x1^y1
proof
let x be Point of PX, y be Point of PY;
consider x1,y1 be FinSequence such that
A7: x=x1 & y=y1 & K.(x,y) = x1^y1 by A1;
A8: J.(x,y) = <*x,y*> by A2;
[x,y] in the carrier of [:PX,PY:]; then
A9: [x,y] in dom J by FUNCT_2:def 1;
I.<*x,y*> = K.(JB.(J.[x,y])) by A8,A5,FUNCT_1:13; then
I.<*x,y*> = x1^y1 by A7,A9,A2,FUNCT_1:34;
hence thesis by A7;
end;
thus for v,w be Point of product <*PX,PY*> holds I.(v+w) = I.v + I.w
proof
let v,w be Point of product <*PX,PY*>;
consider x be Element of the carrier of [:PX,PY:] such that
A10: v=J.x by A3,FUNCT_2:113;
consider y be Element of the carrier of [:PX,PY:] such that
A11: w=J.y by A3,FUNCT_2:113;
x in the carrier of [:PX,PY:] & y in the carrier of [:PX,PY:]
& x + y in the carrier of [:PX,PY:]; then
x in dom J & y in dom J & x + y in dom J by FUNCT_2:def 1; then
A12:JB.v = x & JB.w = y & JB.(J.(x+y)) = x+y by A10,A11,A2,FUNCT_1:34;
v in rng J & w in rng J by A3; then
A13:v in dom JB & w in dom JB by A2,FUNCT_1:33;
v+w = J.(x+y) by A10,A11,A2; then
I.(v+w) = K.(x+y) by A12,A5,FUNCT_1:13
.= K.x + K.y by A1
.= (K*JB).v + K.(JB.w) by A12,A13,FUNCT_1:13;
hence I.(v+w) = I.v + I.w by A13,FUNCT_1:13;
end;
thus for v be Point of product <*PX,PY*>, r be Element of REAL
holds I.(r*v)=r*(I.v)
proof
let v be Point of product <*PX,PY*>, r be Element of REAL;
consider x be Element of the carrier of [:PX,PY:] such that
A14: v=J.x by A3,FUNCT_2:113;
x in the carrier of [:PX,PY:]; then
x in dom J by FUNCT_2:def 1; then
A15:JB.v = x by A14,A2,FUNCT_1:34;
v in rng J by A3; then
A16:v in dom JB by A2,FUNCT_1:33;
r*x in the carrier of [:PX,PY:]; then
A17: r*x in dom J by FUNCT_2:def 1;
r*v =J.(r*x) by A14,A2; then
I.(r*v) = K.(JB.(J.(r*x))) by A5,FUNCT_1:13;
hence I.(r*v) = K.(r*x) by A17,A2,FUNCT_1:34
.= r*(K.x) by A1
.= r*(I.v) by A15,A16,FUNCT_1:13;
end;
thus I.(0.(product<*PX,PY*>)) = 0.product(X^Y)
proof
0.([:PX,PY:]) in the carrier of [:PX,PY:]; then
A18:0.([:PX,PY:]) in dom J by FUNCT_2:def 1;
0. product <*PX,PY*> in rng J by A3; then
0.(product <*PX,PY*>) in dom JB by A2,FUNCT_1:33; then
I.(0.(product <*PX,PY*>)) = K.(JB.(J.(0.([:PX,PY:])))) by A2,FUNCT_1:13;
hence I.(0.(product <*PX,PY*>)) = 0.PXY by A1,A18,A2,FUNCT_1:34;
end;
thus for v be Point of product <*PX,PY*> holds ||. I.v .|| = ||.v.||
proof
let v be Point of product <*PX,PY*>;
consider x be Element of the carrier of [:PX,PY:] such that
A19: v=J.x by A3,FUNCT_2:113;
x in the carrier of [:PX,PY:]; then
A20:x in dom J by FUNCT_2:def 1;
v in rng J by A3; then
v in dom JB by A2,FUNCT_1:33; then
I.v = K.(JB.(J.x)) by A19,FUNCT_1:13
.= K.x by A20,A2,FUNCT_1:34; then
||. I.v .|| =||.x.|| by A1;
hence ||. I.v .|| = ||.v.|| by A2,A19;
end;
end;
theorem Th21:
for X,Y be non empty RealLinearSpace
holds ex I be Function of [:X,Y:],[:X,product <*Y*>:]
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y holds I.(x,y) = [x,<*y*>] )
& ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:X,Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[:X,Y:]) = 0.([:X,product<*Y*>:])
proof
let X,Y be non empty RealLinearSpace;
consider J be Function of Y,product <*Y*> such that
A1: J is one-to-one & J is onto
& ( for y be Point of Y holds J.y = <*y*> )
& ( for v,w be Point of Y holds J.(v+w) = J.v + J.w )
& ( for v be Point of Y, r be Element of REAL holds J.(r*v)=r*(J.v) )
& J.(0.Y)=0.product <*Y*> by Th11;
defpred P[object,object,object] means $3 = [ $1,<* $2 *> ];
A2:for x,y be object st x in the carrier of X & y in the carrier of Y
ex z be object st z in the carrier of [:X,product <*Y*>:] & P[x,y,z]
proof
let x,y be object;
assume A3: x in the carrier of X & y in the carrier of Y; then
reconsider y0=y as Point of Y;
J.y0 = <*y0*> by A1; then
[x,<*y*>] in [:the carrier of X,the carrier of product <*Y*>:]
by A3,ZFMISC_1:87;
hence thesis;
end;
consider I be Function of [:the carrier of X,the carrier of Y:],
the carrier of [:X,product <*Y*>:] such that
A4: for x,y be object st x in the carrier of X & y in the carrier of Y
holds P[x,y,I.(x,y)] from BINOP_1:sch 1(A2);
reconsider I as Function of [:X,Y:],[:X, product <*Y*>:];
take I;
now let z1,z2 be object;
assume A5: z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:]
& I.z1=I.z2;
consider x1,y1 be object such that
A6: x1 in the carrier of X & y1 in the carrier of Y & z1=[x1,y1]
by A5,ZFMISC_1:def 2;
consider x2,y2 be object such that
A7: x2 in the carrier of X & y2 in the carrier of Y & z2=[x2,y2]
by A5,ZFMISC_1:def 2;
[x1,<*y1*>] = I.(x1,y1) by A4,A6
.= I.(x2,y2) by A5,A6,A7
.= [x2,<*y2*>] by A4,A7; then
x1=x2 & <*y1*>=<*y2*> by XTUPLE_0:1;
hence z1=z2 by A6,A7,FINSEQ_1:76;
end;
hence I is one-to-one by FUNCT_2:19;
now let w be object;
assume w in the carrier of [:X, product <*Y*>:]; then
consider x,y1 be object such that
A8: x in the carrier of X & y1 in the carrier of product <*Y*> &
w=[x,y1] by ZFMISC_1:def 2;
y1 in rng J by A1,A8,FUNCT_2:def 3; then
consider y be object such that
A9: y in the carrier of Y & y1=J.y by FUNCT_2:11;
reconsider z = [x,y] as Element of [:the carrier of X,the carrier of Y:]
by A8,A9,ZFMISC_1:87;
J.y = <*y*> by A9,A1; then
w = I.(x,y) by A4,A8,A9; then
w = I.z;
hence w in rng I by FUNCT_2:4;
end; then
the carrier of [:X, product <*Y*>:] c= rng I by TARSKI:def 3; then
the carrier of [:X, product <*Y*>:] = rng I by XBOOLE_0:def 10;
hence I is onto by FUNCT_2:def 3;
thus for x be Point of X, y be Point of Y holds I.(x,y) = [x,<*y*>] by A4;
thus for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:X,Y:];
consider x1 be Point of X, x2 be Point of Y such that
A10: v=[x1,x2] by Lm1;
consider y1 be Point of X, y2 be Point of Y such that
A11: w=[y1,y2] by Lm1;
A12: I.(v+w) = I.(x1+y1,x2+y2) by A10,A11,Def1
.= [x1+y1,<*x2+y2*>] by A4;
I.v = I.(x1,x2) & I.w = I.(y1,y2) by A10,A11; then
A13: I.v = [x1,<*x2*>] & I.w = [y1,<*y2*>] by A4;
A14: J.x2 = <*x2*> & J.y2 = <*y2*> by A1; then
reconsider xx2=<*x2*> as Point of product <*Y*>;
reconsider yy2=<*y2*> as Point of product <*Y*> by A14;
<*x2+y2*> = J.(x2+y2) by A1
.= xx2+yy2 by A14,A1;
hence I.v + I.w = I.(v+w) by A12,A13,Def1;
end;
thus for v be Point of [:X,Y:], r be Element of REAL
holds I.(r*v)=r*(I.v)
proof
let v be Point of [:X,Y:], r be Element of REAL;
consider x1 be Point of X, x2 be Point of Y such that
A15: v=[x1,x2] by Lm1;
A16: I.(r*v) = I.(r*x1,r*x2) by A15,Th9
.= [r*x1,<*r*x2*>] by A4;
A17: I.v = I.(x1,x2) by A15
.= [x1,<*x2*>] by A4;
A18: J.x2 = <*x2*> by A1; then
reconsider xx2=<*x2*> as Point of product <*Y*>;
<* r*x2 *> = J.(r*x2) by A1
.= r*xx2 by A18,A1;
hence r*(I.v) = I.(r*v) by A16,A17,Th9;
end;
A19:<*0.Y*> = 0.product <*Y*> by A1;
I.(0.[:X,Y:]) = I.(0.X,0.Y);
hence I.(0.[:X,Y:]) = 0.([:X,product <*Y*>:]) by A19,A4;
end;
theorem
for X be non empty RealLinearSpace-Sequence, Y be RealLinearSpace
holds ex I be Function of [:product X,Y:],product(X^<*Y*>)
st I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of Y
ex x1,y1 be FinSequence st x=x1 & <*y*> =y1 & I.(x,y) = x1^y1 )
& ( for v,w be Point of [:product X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:product X,Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[:product X,Y:]) = 0.product (X^<*Y*>)
proof
let X be non empty RealLinearSpace-Sequence;
let Y be non empty RealLinearSpace;
consider I be Function of [:product X,Y:],[:product X, product <*Y*>:]
such that
A1: I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of Y holds
I.(x,y) = [x,<*y*>] )
& ( for v,w be Point of [:product X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:product X,Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[:product X,Y:]) =0.([:product X,product <*Y*>:]) by Th21;
consider J be Function of [:product X,product <*Y*>:],product (X^<*Y*>)
such that
A2: J is one-to-one & J is onto
& ( for x be Point of product X, y be Point of product<*Y*>
ex x1,y1 be FinSequence st x=x1 & y=y1 & J.(x,y) = x1^y1 )
& ( for v,w be Point of [:product X,product <*Y*>:]
holds J.(v+w) = J.v + J.w )
& ( for v be Point of [:product X,product <*Y*>:], r be Element of REAL
holds J.(r*v)=r*(J.v) )
& J.(0.[:product X,product <*Y*>:]) = 0.product (X^<*Y*>) by Th13;
set K=J*I;
reconsider K as Function of [:product X,Y:],product (X^<*Y*>);
take K;
thus K is one-to-one by A1,A2;
A3:rng J = the carrier of product (X^<*Y*>) by A2,FUNCT_2:def 3;
rng I = the carrier of [:product X,product <*Y*>:] by A1,FUNCT_2:def 3;
then
rng(J*I) = J.:(the carrier of [:product X,product <*Y*>:]) by RELAT_1:127
.= the carrier of product (X^<*Y*>) by A3,RELSET_1:22;
hence K is onto by FUNCT_2:def 3;
thus for x be Point of product X, y be Point of Y
holds ex x1,y1 be FinSequence st x=x1 & <*y*> =y1 & K.(x,y) = x1^y1
proof
let x be Point of product X, y be Point of Y;
A4: I.(x,y) = [x,<*y*>] by A1;
[x,y] in the carrier of [:product X,Y:]; then
[x,<*y*>] in the carrier of [:product X,product <*Y*>:]
by A4,FUNCT_2:5; then
reconsider yy=<*y*> as Point of product <*Y*> by ZFMISC_1:87;
consider x1,y1 be FinSequence such that
A5: x=x1 & yy=y1 & J.(x,yy) = x1^y1 by A2;
J.(x,yy) = J.(I.([x,y])) by A4
.= K.(x,y) by FUNCT_2:15;
hence thesis by A5;
end;
thus for v,w be Point of [:product X,Y:] holds K.(v+w) = K.v + K.w
proof
let v,w be Point of [:product X,Y:];
thus K.(v+w) = J.(I.(v+w)) by FUNCT_2:15
.= J.(I.v + I.w) by A1
.= J.(I.v) + J.(I.w) by A2
.= K.v + J.(I.w) by FUNCT_2:15
.= K.v + K.w by FUNCT_2:15;
end;
thus for v be Point of [:product X,Y:], r be Element of REAL
holds K.(r*v)=r*(K.v)
proof
let v be Point of [:product X,Y:], r be Element of REAL;
thus K.(r*v) = J.(I.(r*v)) by FUNCT_2:15
.= J.(r*(I.v)) by A1
.= r*(J.(I.v)) by A2
.= r*(K.v) by FUNCT_2:15;
end;
thus K.(0.[:product X,Y:]) = 0.product (X^<*Y*>) by A1,A2,FUNCT_2:15;
end;
theorem Th23:
for X ,Y be non empty RealNormSpace
ex I be Function of [:X,Y:],[:X,product<*Y*>:]
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y holds I.(x,y) = [x,<*y*>] )
& ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:X,Y:], r be Element of REAL holds I.(r*v)=r*(I.v) )
& I.(0.[:X,Y:]) = 0.([:X,product <*Y*>:])
& ( for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| )
proof
let X,Y be non empty RealNormSpace;
consider J be Function of Y, product <*Y*> such that
A1: J is one-to-one & J is onto
& ( for y be Point of Y holds J.y = <*y*> )
& ( for v,w be Point of Y holds J.(v+w) = J.v + J.w )
& ( for v be Point of Y, r be Element of REAL holds J.(r*v)=r*(J.v) )
& J.(0.Y)=0.product <*Y*>
& ( for v be Point of Y holds ||. J.v .|| = ||.v.|| ) by Th16;
defpred P[object,object,object] means $3 = [ $1,<* $2 *> ];
A2:for x,y be object st x in the carrier of X & y in the carrier of Y
ex z be object st z in the carrier of [:X,product <*Y*>:] & P[x,y,z]
proof
let x,y be object;
assume A3: x in the carrier of X & y in the carrier of Y; then
reconsider y0=y as Point of Y;
J.y0 = <* y0 *> by A1; then
[x,<*y*>] in [:the carrier of X,the carrier of product <*Y*>:]
by A3,ZFMISC_1:87;
hence thesis;
end;
consider I be Function of [:the carrier of X,the carrier of Y:],
the carrier of [:X,product <*Y*>:] such that
A4: for x,y be object st x in the carrier of X & y in the carrier of Y
holds P[x,y,I.(x,y)] from BINOP_1:sch 1(A2);
reconsider I as Function of [:X,Y:],[:X, product <*Y*>:];
take I;
thus I is one-to-one
proof
now let z1,z2 be object;
assume A5: z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:]
& I.z1=I.z2; then
consider x1,y1 be object such that
A6: x1 in the carrier of X & y1 in the carrier of Y & z1=[x1,y1]
by ZFMISC_1:def 2;
consider x2,y2 be object such that
A7: x2 in the carrier of X & y2 in the carrier of Y & z2=[x2,y2]
by A5,ZFMISC_1:def 2;
A8: [x1,<*y1*>] = I.(x1,y1) by A4,A6
.= I.(x2,y2) by A5,A6,A7
.= [x2,<*y2*>] by A4,A7; then
<*y1*> = <*y2*> by XTUPLE_0:1; then
y1 = y2 by FINSEQ_1:76;
hence z1=z2 by A6,A7,A8,XTUPLE_0:1;
end;
hence thesis by FUNCT_2:19;
end;
thus I is onto
proof
now let w be object;
assume w in the carrier of [:X, product <*Y*>:]; then
consider x,y1 be object such that
A9: x in the carrier of X & y1 in the carrier of product <*Y*>
& w=[x,y1] by ZFMISC_1:def 2;
y1 in rng J by A1,A9,FUNCT_2:def 3; then
consider y be object such that
A10: y in the carrier of Y & y1=J.y by FUNCT_2:11;
A11: J.y = <*y*> by A10,A1;
reconsider z = [x,y] as Element of
[:the carrier of X,the carrier of Y:] by A9,A10,ZFMISC_1:87;
w = I.(x,y) by A4,A9,A10,A11
.= I.z;
hence w in rng I by FUNCT_2:4;
end; then
the carrier of [:X,product <*Y*>:] c= rng I by TARSKI:def 3; then
the carrier of [:X, product <*Y*>:] = rng I by XBOOLE_0:def 10;
hence thesis by FUNCT_2:def 3;
end;
thus for x be Point of X, y be Point of Y holds I.(x,y) = [x,<*y*>] by A4;
thus for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:X,Y:];
consider x1 be Point of X, x2 be Point of Y such that
A12: v=[x1,x2] by Lm1;
consider y1 be Point of X, y2 be Point of Y such that
A13: w=[y1,y2] by Lm1;
A14: I.(v+w) = I.(x1+y1,x2+y2) by A12,A13,Def1
.= [x1+y1,<*x2+y2*>] by A4;
I.v = I.(x1,x2) & I.w = I.(y1,y2) by A12,A13; then
A15: I.v = [x1,<*x2*>] & I.w = [y1,<*y2*>] by A4;
A16: J.x2 = <*x2*> & J.y2 = <*y2*> by A1; then
reconsider xx2=<*x2*> as Point of product <*Y*>;
reconsider yy2=<*y2*> as Point of product <*Y*> by A16;
<*x2+y2*> = J.(x2+y2) by A1
.= xx2+yy2 by A16,A1;
hence I.v + I.w = I.(v+w) by A14,A15,Def1;
end;
thus for v be Point of [:X,Y:], r be Element of REAL holds I.(r*v)=r*(I.v)
proof
let v be Point of [:X,Y:], r be Element of REAL;
consider x1 be Point of X, x2 be Point of Y such that
A17: v=[x1,x2] by Lm1;
A18: I.(r*v) = I.(r*x1,r*x2) by A17,Th18
.= [r*x1,<*r*x2*>] by A4;
A19: I.v = I.(x1,x2) by A17
.= [x1,<*x2*>] by A4;
A20: J.x2 = <*x2*> by A1; then
reconsider xx2=<*x2*> as Point of product <*Y*>;
<* r*x2 *> = J.(r*x2) by A1
.= r*xx2 by A20,A1;
hence r*(I.v) = I.(r*v) by A18,A19,Th18;
end;
A21:<*0.Y *> = 0.product <*Y*> by A1;
I.(0.[: X,Y:]) = I.(0.X,0.Y);
hence I.(0.[:X,Y:]) = 0.([:X,product <*Y*>:]) by A21,A4;
thus for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.||
proof
let v be Point of [:X,Y:];
consider x1 be Point of X, x2 be Point of Y such that
A22: v=[x1,x2] by Lm1;
A23: J.x2 = <*x2*> by A1; then
reconsider xx2=<*x2*> as Point of product <*Y*>;
A24:ex w be Element of REAL 2 st
w=<* ||.x1.||,||.x2.|| *> & ||.v.|| = |.w.| by A22,Th18;
I.v = I.(x1,x2) by A22
.= [x1,<*x2*>] by A4; then
ex s be Element of REAL 2 st s=<* ||.x1.||,||.xx2.|| *> &
||. I.v .|| = |.s.| by Th18;
hence ||. I.v .|| = ||.v.|| by A23,A1,A24;
end;
end;
theorem
for X be non empty RealNormSpace-Sequence, Y be RealNormSpace
ex I be Function of [:product X,Y:],product(X^<*Y*>)
st I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of Y
ex x1,y1 be FinSequence st x=x1 & <*y*>=y1 & I.(x,y) = x1^y1 )
& ( for v,w be Point of [:product X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:product X,Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[:product X,Y:]) = 0.product(X^<*Y*>)
& ( for v be Point of [:product X,Y:] holds ||. I.v .|| = ||.v.|| )
proof
let X be non empty RealNormSpace-Sequence, Y be RealNormSpace;
consider I be Function of [:product X,Y:],[:product X,product <*Y*>:]
such that
A1: I is one-to-one & I is onto
& ( for x be Point of product X, y be Point of Y holds
I.(x,y) = [x,<*y*>] )
& ( for v,w be Point of [:product X,Y:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:product X,Y:], r be Element of REAL
holds I.(r*v)=r*(I.v) )
& I.(0.[: product X,Y:]) = 0.([:product X,product <*Y*>:])
& ( for v be Point of [:product X,Y:] holds ||. I.v .|| = ||.v.|| )
by Th23;
consider J be Function of [:product X,product <*Y*>:],product(X^<*Y*>)
such that
A2: J is one-to-one & J is onto
& ( for x be Point of product X, y be Point of product <*Y*>
ex x1,y1 be FinSequence st x=x1 & y=y1 & J.(x,y) = x1^y1 )
& ( for v,w be Point of [:product X,product <*Y*>:]
holds J.(v+w) = J.v + J.w )
& ( for v be Point of [:product X,product <*Y*>:], r be Element of REAL
holds J.(r*v)=r*(J.v) )
& J.(0.[:product X,product <*Y*>:]) = 0.product (X^<*Y*>)
& ( for v be Point of [:product X,product <*Y*>:]
holds ||. J.v .|| = ||.v.|| ) by Th17;
set K=J*I;
reconsider K as Function of [:product X,Y:],product (X^<*Y*>);
take K;
thus K is one-to-one by A1,A2;
A3:rng J = the carrier of product (X^<*Y*>) by A2,FUNCT_2:def 3;
rng I = the carrier of [:product X,product<*Y*>:] by A1,FUNCT_2:def 3; then
rng(J*I) = J.:(the carrier of [:product X,product <*Y*>:]) by RELAT_1:127
.= the carrier of product (X^<*Y*>) by A3,RELSET_1:22;
hence K is onto by FUNCT_2:def 3;
thus for x be Point of product X, y be Point of Y
ex x1,y1 be FinSequence st x=x1 & <*y*> =y1 & K.(x,y) = x1^y1
proof
let x be Point of product X, y be Point of Y;
A4: I.(x,y) = [x,<*y*>] by A1;
[x,y] in the carrier of [: product X,Y:]; then
[x,<*y*>] in the carrier of [:product X,product <*Y*>:]
by A4,FUNCT_2:5; then
reconsider yy=<*y*> as Point of product <*Y*> by ZFMISC_1:87;
consider x1,y1 be FinSequence such that
A5: x=x1 & yy=y1 & J.(x,yy) = x1^y1 by A2;
J.(x,yy) = J.(I.([x,y])) by A4
.= K.(x,y) by FUNCT_2:15;
hence thesis by A5;
end;
thus for v,w be Point of [:product X,Y:] holds K.(v+w) = K.v + K.w
proof
let v,w be Point of [:product X,Y:];
thus K.(v+w) = J.(I.(v+w)) by FUNCT_2:15
.= J.(I.v + I.w) by A1
.= J.(I.v) + J.(I.w) by A2
.= K.v + J.(I.w) by FUNCT_2:15
.=K.v + K.w by FUNCT_2:15;
end;
thus for v be Point of [:product X,Y:], r be Element of REAL
holds K.(r*v)=r*(K.v)
proof
let v be Point of [:product X,Y:], r be Element of REAL;
thus K.(r*v) = J.(I.(r*v)) by FUNCT_2:15
.= J.(r* (I.v)) by A1
.= r* (J.(I.v)) by A2
.= r* (K.v) by FUNCT_2:15;
end;
thus K.(0.[:product X,Y:]) = 0.product (X^<*Y*>) by A1,A2,FUNCT_2:15;
thus for v be Point of [:product X,Y:] holds ||. K.v .|| = ||.v.||
proof
let v be Point of [:product X,Y:];
thus ||. K.v .|| = ||. J.(I.v) .|| by FUNCT_2:15
.= ||. I.v .|| by A2
.= ||.v.|| by A1;
end;
end;