:: The 3-fold Product Space of Real Normed Spaces and its Properties
:: by Hiroyuki Okazaki and Kazuhisa Nakasho
::
:: Received November 30, 2021
:: Copyright (c) 2021-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, ARYTM_1, SQUARE_1, RVSUM_1, XXREAL_0, CARD_1,
SUPINF_2, TARSKI, PRVECT_1, PRVECT_2, ZFMISC_1, GROUP_2, ALGSTR_0,
REWRITE1, RELAT_2, METRIC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, BINOP_1, DOMAIN_1, NUMBERS, MULTOP_1, XCMPLX_0,
XXREAL_0, XREAL_0, SQUARE_1, CARD_3, FINSEQ_1, FINSEQ_2, RVSUM_1,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, EUCLID,
LOPBAN_1, PRVECT_1, PRVECT_2, PRVECT_3;
constructors SQUARE_1, LOPBAN_1, RVSUM_1, PRVECT_2, TOPMETR, PRVECT_3,
MULTOP_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, NUMBERS,
XBOOLE_0, VALUED_0, PRVECT_2, FINSEQ_1, CARD_3, LOPBAN_1, RLVECT_1,
NORMSP_1, SUBSET_1, SQUARE_1, RVSUM_1, PRVECT_1, PRVECT_3;
requirements SUBSET, BOOLE, NUMERALS;
definitions PRVECT_2;
equalities EUCLID, PRVECT_2, BINOP_1, RLVECT_1, ALGSTR_0, NORMSP_0, STRUCT_0,
PRVECT_3, XTUPLE_0, ZFMISC_1, MULTOP_1;
theorems TARSKI, XBOOLE_0, XREAL_0, RLVECT_1, FINSEQ_1, FINSEQ_2, RVSUM_1,
TOPREAL6, SQUARE_1, FUNCT_1, FUNCT_2, CARD_3, PRVECT_1, PRVECT_2,
FINSEQ_3, XTUPLE_0, PRVECT_3, ENUMSET1, BORSUK_7, MCART_1;
schemes FUNCT_2;
begin :: 3-Variable Function & 3-fold Cartesian product
reserve v,x,x1,x2,y,z for object,
X,X1,X2,X3 for set;
scheme
FuncEx3A{X, Y, W, Z() -> set, P[object,object,object,object]}:
ex f being Function of [:X(),Y(),W():],Z()
st for x,y,w be object
st x in X() & y in Y() & w in W() holds P[x,y,w,f.(x,y,w)]
provided
A1: for x,y,w be object st x in X() & y in Y() & w in W()
ex z st z in Z() & P[x,y,w,z]
proof
defpred R[object,object] means
for x1,y1,w1 be object st $1 = [x1,y1,w1] holds P[x1,y1,w1,$2];
A2: for x being object st x in [:X(),Y(),W():]
ex z being object st z in Z() & R[x,z]
proof
let x be object;
assume x in [:X(),Y(),W():];
then consider x1,y1,w1 being object such that
A3: x1 in X() & y1 in Y() & w1 in W() and
A4: x = [x1,y1,w1] by MCART_1:68;
consider z such that
A5: z in Z() and
A6: P[x1,y1,w1,z] by A1,A3;
take z;
thus z in Z() by A5;
let x2,y2,w2 be object;
assume
A7a:x = [x2,y2,w2]; then
[x1,y1] = [x2,y2] & w1=w2 by A4,XTUPLE_0:1;
then x1 = x2 & y1=y2 by XTUPLE_0:1;
hence thesis by A6,A7a,A4,XTUPLE_0:1;
end;
consider f being Function of [:X(),Y(),W():],Z() such that
A8: for x being object st x in [:X(),Y(),W():]
holds R[x,f.x] from FUNCT_2:sch 1(A2);
take f;
thus thesis by A8,MCART_1:69;
end;
theorem Th4:
for X,Y,Z be non empty set, D be Function
st dom D = {1,2,3} & D.1 = X & D.2 = Y & D.3 = Z
ex I be Function of [:X,Y,Z:],product D
st I is one-to-one & I is onto
& for x,y,z be object st x in X & y in Y & z in Z
holds I.(x,y,z) = <*x,y,z*>
proof
let X,Y,Z be non empty set, D be Function;
assume A1: dom D ={1,2,3} & D.1 = X & D.2 = Y & D.3 = Z;
defpred P[object,object,object,object] means $4 = <* $1,$2,$3 *>;
A2:for x,y,z be object st x in X & y in Y & z in Z
ex w be object st w in product D & P[x,y,z,w]
proof
let x,y,z be object;
assume A3: x in X & y in Y & z in Z;
A4: dom <*x,y,z*> = Seg len <*x,y,z*> by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45,FINSEQ_3:1;
now let i be object;
assume i in dom <*x,y,z*>; then
i = 1 or i = 2 or i = 3 by A4,ENUMSET1:def 1;
hence <*x,y,z*>.i in D.i by A1,A3;
end;
hence ex w be object st w in product D & P[x,y,z,w] by A4,A1,CARD_3:9;
end;
consider I be Function of [:X,Y,Z:], product D such that
A5: for x,y,z be object st x in X & y in Y & z in Z
holds P[x,y,z,I.(x,y,z)] from FuncEx3A(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,ENUMSET1:def 1;
end; then
A6:product D <> {} by CARD_3:26;
now let w1,w2 be object;
assume A7: w1 in [:X,Y,Z:] & w2 in [:X,Y,Z:] & I.w1=I.w2; then
consider x1,y1,z1 be object such that
A8: x1 in X & y1 in Y & z1 in Z & w1=[x1,y1,z1] by MCART_1:68;
consider x2,y2,z2 be object such that
A9: x2 in X & y2 in Y & z2 in Z & w2=[x2,y2,z2] by A7,MCART_1:68;
<*x1,y1,z1*> = I.(x1,y1,z1) by A5,A8
.= I.(x2,y2,z2) by A7,A8,A9
.= <*x2,y2,z2*> by A5,A9; then
x1 = x2 & y1 = y2 & z1 = z2 by FINSEQ_1:78;
hence w1=w2 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_3:1,FINSEQ_1:def 2;
set x=g.1; set y=g.2;set z=g.3;
A12: len g = 3 by A1,A11,FINSEQ_1:def 3,FINSEQ_3:1;
1 in dom D & 2 in dom D & 3 in dom D by A1,ENUMSET1:def 1; then
A13:x in X & y in Y & z in Z & w=<*x,y,z*>
by A11,A12,A1,FINSEQ_1:45;
reconsider s = [x,y,z] as Element of [:X,Y,Z:] by A13,MCART_1:69;
w = I.(x,y,z) by A5,A13
.= I.s;
hence w in rng I by A6,FUNCT_2:112;
end; then
product D c= rng I by TARSKI:def 3; then
I is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence thesis by A5,A10;
end;
theorem Th5:
for X,Y,Z be non empty set
ex I be Function of [:X,Y,Z:],product <*X,Y,Z*>
st I is one-to-one & I is onto
& for x,y,z be object st x in X & y in Y & z in Z
holds I.(x,y,z) = <*x,y,z*>
proof
let X,Y,Z be non empty set;
dom <*X,Y,Z*> = {1,2,3} & <*X,Y,Z*>.1 = X
& <*X,Y,Z*>.2 = Y & <*X,Y,Z*>.3 = Z by FINSEQ_1:89,FINSEQ_3:1;
hence thesis by Th4;
end;
begin :: 3-fold Product Space of Real Linear Spaces
definition let E,F,G be non empty addLoopStr;
func [:E,F,G:] -> strict non empty addLoopStr equals
[:[:E,F:],G:];
coherence;
end;
definition
let E,F,G be non empty addLoopStr;
let e be Point of E, f be Point of F, g be Point of G;
redefine func [e,f,g] -> Element of [:E,F,G:]; :: redefines [ (XTUPLE_0, definition)
coherence
proof
[e,f,g] in [:the carrier of E,the carrier of F,the carrier of G:];
hence thesis;
end;
end;
registration
let E,F,G be Abelian non empty addLoopStr;
cluster [:E,F,G:] -> Abelian;
coherence;
end;
registration
let E,F,G be add-associative non empty addLoopStr;
cluster [:E,F,G:] -> add-associative;
coherence;
end;
registration
let E,F,G be right_zeroed non empty addLoopStr;
cluster [:E,F,G:] -> right_zeroed;
coherence;
end;
registration
let E,F,G be right_complementable non empty addLoopStr;
cluster [:E,F,G:] -> right_complementable;
coherence;
end;
theorem
for E,F,G be non empty addLoopStr holds
( for x be set holds
(x is Point of [:E,F,G:] iff
ex x1 be Point of E, x2 be Point of F, x3 be Point of G st x=[x1,x2,x3]) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] )
& 0.[:E,F,G:] = [0.E,0.F,0.G]
proof
let E,F,G be non empty addLoopStr;
thus for x be set holds
(x is Point of [:E,F,G:]
iff ex x1 be Point of E, x2 be Point of F,
x3 be Point of G st x=[x1,x2,x3])
proof
let x be set;
hereby assume x is Point of [:E,F,G:]; then
consider x1x2 be Point of [:E,F:], x3 be Point of G such that
A1: x=[x1x2,x3] by PRVECT_3:7;
consider x1 be Point of E, x2 be Point of F such that
A2: x1x2=[x1,x2] by PRVECT_3:7;
take x1,x2,x3;
thus x=[x1,x2,x3] by A1,A2;
end;
thus thesis;
end;
hereby
let x1,y1 be Point of E,x2,y2 be Point of F, x3,y3 be Point of G;
[x1,x2]+[y1,y2] =[x1+y1,x2+y2] by PRVECT_3:7;
hence [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] by PRVECT_3:7;
end;
thus 0.[:E,F,G:] = [0.E,0.F,0.G];
end;
theorem
for E,F,G be add-associative right_zeroed
right_complementable non empty addLoopStr,
x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -[x1,x2,x3] = [-x1,-x2,-x3]
proof
let E,F,G be add-associative right_zeroed
right_complementable non empty addLoopStr,
x1 be Point of E, x2 be Point of F, x3 be Point of G;
thus -[x1,x2,x3] = [-[x1,x2],-x3] by PRVECT_3:8
.= [-x1,-x2,-x3] by PRVECT_3:8;
end;
definition let E,F,G be non empty RLSStruct;
func [:E,F,G:] -> strict non empty RLSStruct equals
[:[:E,F:],G:];
coherence;
end;
definition
let E,F,G be non empty RLSStruct;
let e be Point of E, f be Point of F, g be Point of G;
redefine func [e,f,g] -> Element of [:E,F,G:]; :: redefines [ (XTUPLE_0, definition)
coherence
proof
[e,f,g] in [:the carrier of E,the carrier of F,the carrier of G:];
hence thesis;
end;
end;
registration
let E,F,G be Abelian non empty RLSStruct;
cluster [:E,F,G:] -> Abelian;
coherence;
end;
registration
let E,F,G be add-associative non empty RLSStruct;
cluster [:E,F,G:] -> add-associative;
coherence;
end;
registration
let E,F,G be right_zeroed non empty RLSStruct;
cluster [:E,F,G:] -> right_zeroed;
coherence;
end;
registration
let E,F,G be right_complementable non empty RLSStruct;
cluster [:E,F,G:] -> right_complementable;
coherence;
end;
theorem Th8:
for E,F,G be non empty RLSStruct holds
( for x be set holds
(x is Point of [:E,F,G:]
iff ex x1 be Point of E, x2 be Point of F,
x3 be Point of G st x=[x1,x2,x3]) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] )
& 0.[:E,F,G:] = [0.E,0.F,0.G]
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real
holds a*[x1,x2,x3] = [a*x1,a*x2,a*x3] )
proof
let E,F,G be non empty RLSStruct;
thus
for x be set holds
x is Point of [:E,F,G:]
iff ex x1 be Point of E, x2 be Point of F, x3 be Point of G st x=[x1,x2,x3]
proof
let x be set;
hereby assume x is Point of [:E,F,G:]; then
consider x1x2 be Point of [:E,F:], x3 be Point of G such that
A1: x=[x1x2,x3] by PRVECT_3:9;
consider x1 be Point of E, x2 be Point of F such that
A2: x1x2=[x1,x2] by PRVECT_3:9;
take x1,x2,x3;
thus x=[x1,x2,x3] by A1,A2;
end;
thus thesis;
end;
thus for x1,y1 be Point of E,x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3]
proof
let x1,y1 be Point of E,x2,y2 be Point of F, x3,y3 be Point of G;
[x1,x2]+[y1,y2] =[x1+y1,x2+y2] by PRVECT_3:9;
hence thesis by PRVECT_3:9;
end;
thus 0.[:E,F,G:] = [0.E,0.F,0.G];
let x1 be Point of E, x2 be Point of F,x3 be Point of G, a be Real;
thus a*[x1,x2,x3]=[a*[x1,x2],a*x3] by PRVECT_3:9
.=[a*x1,a*x2,a*x3] by PRVECT_3:9;
end;
theorem
for E,F,G be add-associative right_zeroed
right_complementable non empty RLSStruct,
x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -[x1,x2,x3] = [-x1,-x2,-x3]
proof
let E,F,G be add-associative right_zeroed
right_complementable non empty RLSStruct,
x1 be Point of E, x2 be Point of F, x3 be Point of G;
thus -[x1,x2,x3] = [-[x1,x2],-x3] by PRVECT_3:10
.= [-x1,-x2,-x3] by PRVECT_3:10;
end;
registration
let E,F,G be vector-distributive non empty RLSStruct;
cluster [:E,F,G:] -> vector-distributive;
correctness;
end;
registration
let E,F,G be scalar-distributive non empty RLSStruct;
cluster [:E,F,G:] -> scalar-distributive;
correctness;
end;
registration
let E,F,G be scalar-associative non empty RLSStruct;
cluster [:E,F,G:] -> scalar-associative;
correctness;
end;
registration
let E,F,G be scalar-unital non empty RLSStruct;
cluster [:E,F,G:] -> scalar-unital;
correctness;
end;
registration
let E,F,G be Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative
scalar-unital non empty RLSStruct;
cluster <* E,F,G *> -> RealLinearSpace-yielding;
correctness
proof
let S be set;
assume S in rng <*E,F,G*>; then
consider i be object such that
A1: i in dom <*E,F,G*> & <*E,F,G*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
dom <*E,F,G*> = Seg len <*E,F,G*> by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45,FINSEQ_3:1; then
i=1 or i=2 or i =3 by A1,ENUMSET1:def 1;
hence S is RealLinearSpace by A1;
end;
end;
Lm1:
for E,F,G be 1-sorted, x be object st
x in [: the carrier of E, the carrier of F, the carrier of G :] holds
ex x1 be Point of E, x2 be Point of F, x3 be Point of G st x = [x1,x2,x3]
proof
let E,F,G be 1-sorted, x be object;
assume x in [: the carrier of E, the carrier of F, the carrier of G :]; then
consider x1,x2,x3 be object such that
A1:x1 in the carrier of E & x2 in the carrier of F &
x3 in the carrier of G & x=[x1,x2,x3] by MCART_1:68;
reconsider x1 as Point of E by A1;
reconsider x2 as Point of F by A1;
reconsider x3 as Point of G by A1;
take x1,x2,x3;
thus thesis by A1;
end;
theorem Th11:
for X,Y,Z be RealLinearSpace holds
ex I be Function of [:X,Y,Z:],product <*X,Y,Z*>
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y, z be Point of Z
holds I.(x,y,z) = <*x,y,z*> )
& ( for v,w be Point of [:X,Y,Z:] holds I.(v+w)=(I.v) + (I.w) )
& ( for v be Point of [:X,Y,Z:], r be Real
holds I.(r*v)=r*(I.v) )
& I.(0.[:X,Y,Z:])=0.product <*X,Y,Z*>
proof
let X,Y,Z be RealLinearSpace;
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
set CarrZ = the carrier of Z;
A1: the carrier of [:X,Y,Z:]
=[:the carrier of X,the carrier of Y, the carrier of Z:];
consider I be Function of [:CarrX,CarrY,CarrZ:],
product <*CarrX,CarrY,CarrZ*> such that
A2: I is one-to-one & I is onto
& for x,y,z be object st x in CarrX & y in CarrY
& z in CarrZ
holds I.(x,y,z) = <*x,y,z*> by Th5;
len carr <*X,Y,Z*> = len <*X,Y,Z*> by PRVECT_1:def 11; then
A3:len carr <*X,Y,Z*> = 3 by FINSEQ_1:45; then
A4:dom carr <*X,Y,Z*> = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
len <*X,Y,Z*> = 3 by FINSEQ_1:45; then
A5:dom <*X,Y,Z*> = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
A6:<*X,Y,Z*>.1 = X & <*X,Y,Z*>.2 = Y
& <*X,Y,Z*>.3 = Z;
1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} by ENUMSET1:def 1; then
(carr <*X,Y,Z*>).1 = CarrX & (carr <*X,Y,Z*>).2 = CarrY
& (carr <*X,Y,Z*>).3 = CarrZ by A5,A6,PRVECT_1:def 11; then
A7:carr <*X,Y,Z*> = <* CarrX,CarrY,CarrZ *> by A3,FINSEQ_1:45; then
reconsider I as Function of [:X,Y,Z:],product <*X,Y,Z*>;
A8:for x be Point of X,y be Point of Y,
z be Point of Z holds I.(x,y,z) = <*x,y,z*> by A2;
A9:for v,w be Point of [:X,Y,Z:] holds I.(v+w) = I.v + I.w
proof
let v,w be Point of [:X,Y,Z:];
A10: the carrier of [:X,Y,Z:]
=[:the carrier of X,the carrier of Y, the carrier of Z:];
consider x1 be Point of X, y1 be Point of Y,
z1 be Point of Z such that
A11: v = [x1,y1,z1] by A10,Lm1;
consider x2 be Point of X, y2 be Point of Y, z2 be Point of Z such that
A12: w = [x2,y2,z2] by A10,Lm1;
I.v = I.(x1,y1,z1) & I.w = I.(x2,y2,z2) by A11,A12; then
A13:I.v = <*x1,y1,z1*> & I.w = <*x2,y2,z2*> by A2;
A14:I.(v+w) =I.(x1+x2,y1+y2,z1+z2) by A11,A12,Th8
.= <* x1+x2,y1+y2,z1+z2 *> by A2;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X,Y,Z*>;
reconsider j1=1, j2=2,j3=3
as Element of dom carr <*X,Y,Z*> by A4, ENUMSET1:def 1;
A16: (addop <*X,Y,Z*>).j1
= the addF of (<*X,Y,Z*>.j1) by PRVECT_1:def 12;
A17: ([:addop <*X,Y,Z*>:].(Iv,Iw)).j1
= ((addop <*X,Y,Z*>).j1).(Iv.j1,Iw.j1) by PRVECT_1:def 8
.= x1+x2 by A16,A13;
A18: (addop <*X,Y,Z*>).j2
= the addF of (<*X,Y,Z*>.j2) by PRVECT_1:def 12;
A19: (addop <*X,Y,Z*>).j3
= the addF of (<*X,Y,Z*>.j3) by PRVECT_1:def 12;
A20: ([:addop <*X,Y,Z*>:].(Iv,Iw)).j2
= ((addop <*X,Y,Z*>).j2).(Iv.j2,Iw.j2) by PRVECT_1:def 8
.= y1+y2 by A18,A13;
A21: ([:addop <*X,Y,Z*>:].(Iv,Iw)).j3
= ((addop <*X,Y,Z*>).j3).(Iv.j3,Iw.j3) by PRVECT_1:def 8
.= z1+z2 by A19,A13;
consider Ivw be Function such that
A22: I.v + I.w = Ivw & dom Ivw = dom carr <*X,Y,Z*>
& for i be object st i in dom carr <*X,Y,Z*>
holds Ivw.i in carr (<*X,Y,Z*>).i by CARD_3:def 5;
A23: dom Ivw = Seg 3 by A3,A22,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 3 by A23,FINSEQ_1:def 3;
hence thesis by A14,A22,A17,A20,A21,FINSEQ_1:45;
end;
A24:for v be Point of [:X,Y,Z:], r be Real holds I.(r*v)=r*(I.v)
proof
let v be Point of [:X,Y,Z:], r be Real;
consider x1 be Point of X, y1 be Point of Y,
z1 be Point of Z such that
A25: v = [x1,y1,z1] by A1,Lm1;
A26:I.v =I.(x1,y1,z1) by A25 .= <*x1,y1,z1*> by A2;
A27:I.(r*v) =I.(r*x1,r*y1,r*z1) by A25,Th8
.= <* r*x1,r*y1,r*z1 *> by A2;
reconsider j1=1, j2=2,j3=3 as Element of dom carr <*X,Y,Z*>
by A4, ENUMSET1:def 1;
A29: (multop <*X,Y,Z*>).j1 = the Mult of (<*X,Y,Z*>.j1)
& (multop <*X,Y,Z*>).j2 = the Mult of (<*X,Y,Z*>.j2)
& (multop <*X,Y,Z*>).j3 = the Mult of (<*X,Y,Z*>.j3) by PRVECT_2:def 8;
reconsider Iv = I.v as Element of product carr <*X,Y,Z*>;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
([:multop <*X,Y,Z*>:].(rr,Iv)).j1 = ((multop <*X,Y,Z*>).j1).(r,Iv.j1)
& ([:multop <*X,Y,Z*>:].(rr,Iv)).j2 = ((multop <*X,Y,Z*>).j2).(r,Iv.j2)
& ([:multop <*X,Y,Z*>:].(rr,Iv)).j3
= ((multop <*X,Y,Z*>).j3).(r,Iv.j3) by PRVECT_2:def 2; then
A30: ([:multop <*X,Y,Z*>:].(rr,Iv)).j1 = r*x1
& ([:multop <*X,Y,Z*>:].(rr,Iv)).j2 = r*y1
& ([:multop <*X,Y,Z*>:].(rr,Iv)).j3 = r*z1 by A29,A26;
consider Ivw be Function such that
A31: r*(I.v) = Ivw & dom Ivw = dom carr <*X,Y,Z*>
& for i be object st i in dom carr <*X,Y,Z*>
holds Ivw.i in carr (<*X,Y,Z*>).i by CARD_3:def 5;
A32: dom Ivw = Seg 3 by A3,A31,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 3 by A32,FINSEQ_1:def 3;
hence thesis by A27,A31,A30,FINSEQ_1:45;
end;
I.(0.[:X,Y,Z:]) = I.(0.[:X,Y,Z:] + 0.[:X,Y,Z:])
.= I.(0.[:X,Y,Z:]) + I.(0.[:X,Y,Z:]) by A9; then
I.(0.[:X,Y,Z:]) - I.(0.[:X,Y,Z:]) = I.(0.[:X,Y,Z:]) + (I.(0.[:X,Y,Z:])
- I.(0.[:X,Y,Z:])) by RLVECT_1:28
.= I.(0.[:X,Y,Z:]) + 0.product <*X,Y,Z*> by RLVECT_1:15
.= I.(0.[:X,Y,Z:]);
hence thesis by A8,A9,A24,A2,A7,RLVECT_1:15;
end;
definition
let E,F,G be RealLinearSpace;
let e be Point of E, f be Point of F, g be Point of G;
redefine func <*e,f,g*> -> Element of product <*E,F,G*>; :: redefines <* (FINSEQ_1, definition)
coherence
proof
consider I be Function of [:E,F,G:], product <* E,F,G *> such that
I is one-to-one & I is onto and
A1: for x be Point of E, y be Point of F, z be Point of G
holds I.(x,y,z) = <* x,y,z *> and
( for v,w be Point of [:E,F,G:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:E,F,G:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*E,F,G*> = I.(0.[:E,F,G:]) by Th11;
A2: I.[e,f,g] in rng I by FUNCT_2:112;
I.(e,f,g) = <*e,f,g*> by A1;
hence thesis by A2;
end;
end;
theorem
for E,F,G be RealLinearSpace holds
( for x be set holds
( x is Point of product <*E,F,G*>
iff ex x1 be Point of E, x2 be Point of F, x3 be Point of G st
x=<* x1,x2,x3 *> ) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*x1+y1,x2+y2,x3+y3*> )
& 0.(product <*E,F,G*>) = <* 0.E,0.F,0.G *>
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -<* x1,x2,x3 *> = <* -x1,-x2,-x3 *> )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real
holds a*<*x1,x2,x3*> = <* a*x1,a*x2,a*x3 *> )
proof
let E,F,G be RealLinearSpace;
A1: the carrier of [:E,F,G:]
= [:the carrier of E, the carrier of F, the carrier of G:];
consider I be Function of [:E,F,G:], product <* E,F,G *> such that
A2: I is one-to-one & I is onto
& ( for x be Point of E, y be Point of F
, z be Point of G holds I.(x,y,z) = <* x,y,z *> )
& ( for v,w be Point of [:E,F,G:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:E,F,G:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*E,F,G*> = I.(0.[:E,F,G:]) by Th11;
thus for x be set holds
( x is Point of product <*E,F,G*>
iff ex x1 be Point of E, x2 be Point of F, x3 be Point of G st
x=<* x1,x2,x3 *> )
proof
let y be set;
hereby assume y is Point of product <*E,F,G*>; then
y in the carrier of product <*E,F,G*>; then
y in rng I by A2,FUNCT_2:def 3; then
consider x be Element of the carrier of [:E,F,G:] such that
A4: y = I.x by FUNCT_2:113;
consider x1 be Point of E, x2 be Point of F, x3 be Point of G such that
A5: x=[x1,x2,x3] by A1,Lm1;
take x1,x2,x3;
I.(x1,x2,x3) = <*x1,x2,x3*> by A2;
hence y = <*x1,x2,x3*> by A4,A5;
end;
thus thesis;
end;
thus
A8: for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G holds
<*x1,x2,x3*> + <*y1,y2,y3*> = <*x1+y1,x2+y2,x3+y3*>
proof
let x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G;
A10: [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] by Th8;
I.(x1+y1,x2+y2,x3+y3) = <* x1+y1,x2+y2,x3+y3 *>
& I.(x1,x2,x3) = <* x1,x2,x3 *> & I.(y1,y2,y3) = <* y1,y2,y3 *> by A2;
hence thesis by A2,A10;
end;
thus
A11: 0. product <*E,F,G*> = <* 0.E,0.F,0.G *>
proof
I.(0.E,0.F,0.G) = <* 0.E,0.F,0.G *> by A2;
hence thesis by A2;
end;
thus for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -<*x1,x2,x3*> = <* -x1,-x2,-x3 *>
proof
let x1 be Point of E, x2 be Point of F, x3 be Point of G;
<* x1,x2,x3 *>+<* -x1,-x2,-x3 *> = <* x1+-x1,x2+-x2,x3+-x3 *> by A8
.= <* 0.E,x2+-x2,x3+-x3 *> by RLVECT_1:def 10
.= <* 0.E,0.F,x3+-x3 *> by RLVECT_1:def 10
.= 0.(product <*E,F,G*>) by A11,RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
let x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real;
A14: <* x1,x2,x3 *> = I.(x1,x2,x3) by A2;
I.(a*[x1,x2,x3]) = I.(a*x1,a*x2,a*x3) by Th8
.= <* a*x1,a*x2,a*x3 *> by A2;
hence thesis by A2,A14;
end;
begin ::3-fold Product Space of Real Normed Spaces
definition let E,F,G be non empty NORMSTR;
func [:E,F,G:] -> strict non empty NORMSTR equals
[:[:E,F:],G:];
coherence;
end;
definition
let E,F,G be non empty NORMSTR;
let e be Point of E, f be Point of F, g be Point of G;
redefine func [e,f,g] -> Element of [:E,F,G:]; :: redefines [ (XTUPLE_0, definition)
coherence
proof
[e,f,g] in [:the carrier of E,the carrier of F,the carrier of G:];
hence thesis;
end;
end;
registration
let E,F,G be RealNormSpace;
cluster [:E,F,G:] -> reflexive discerning RealNormSpace-like
scalar-distributive vector-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence;
end;
registration
let E,F,G be RealNormSpace;
cluster <*E,F,G*> -> RealNormSpace-yielding;
correctness
proof
let S be set;
assume S in rng <*E,F,G*>; then
consider i be object such that
A1: i in dom <*E,F,G*> & <*E,F,G*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
dom <*E,F,G*> = Seg len <*E,F,G*> by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45,FINSEQ_3:1; then
i=1 or i=2 or i = 3 by A1,ENUMSET1:def 1;
hence S is RealNormSpace by A1;
end;
end;
theorem Th14:
for E,F,G be RealNormSpace holds
( for x be set holds
( x is Point of [:E,F,G:]
iff ex x1 be Point of E,x2 be Point of F,
x3 be Point of G
st x=[x1,x2,x3]) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] )
& 0.[:E,F,G:] = [0.E,0.F,0.G]
& ( for x1 be Point of E, x2 be Point of F,x3 be Point of G, a be Real
holds a*[x1,x2,x3] = [a*x1,a*x2,a*x3] )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -[x1,x2,x3] = [-x1,-x2,-x3] )
& ( for x1 be Point of E, x2 be Point of F,x3 be Point of G
holds ||. [x1,x2,x3] .|| = sqrt( ||.x1.||^2 + ||.x2.||^2 + ||.x3.||^2 )
&
ex w be Element of REAL 3 st
w = <* ||.x1.||,||.x2.||,||.x3.|| *> & ||. [x1,x2,x3] .|| = |.w.| )
proof
let E,F,G be RealNormSpace;
thus for x be set holds (x is Point of [:E,F,G:]
iff ex x1 be Point of E, x2 be Point of F, x3 be Point of G
st x=[x1,x2,x3])
proof
let x be set;
hereby assume x is Point of [:E,F,G:]; then
consider x1x2 be Point of [:E,F:], x3 be Point of G such that
A1: x=[x1x2,x3] by PRVECT_3:18;
consider x1 be Point of E, x2 be Point of F such that
A2: x1x2=[x1,x2] by PRVECT_3:18;
take x1,x2,x3;
thus x=[x1,x2,x3] by A1,A2;
end;
thus thesis;
end;
hereby
let x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G;
[x1,x2]+[y1,y2] =[x1+y1,x2+y2] by PRVECT_3:18;
hence [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] by PRVECT_3:18;
end;
thus 0.[:E,F,G:] = [0.E,0.F,0.G];
thus A7:for x1 be Point of E, x2 be Point of F,x3 be Point of G, a be Real
holds a*[x1,x2,x3] = [a*x1,a*x2,a*x3]
proof
let x1 be Point of E, x2 be Point of F,x3 be Point of G, a be Real;
thus a*[x1,x2,x3]=[a*[x1,x2],a*x3] by PRVECT_3:18
.=[a*x1,a*x2,a*x3] by PRVECT_3:18;
end;
hereby
let x1 be Point of E, x2 be Point of F, x3 be Point of G;
thus -[x1,x2,x3] = (-1)*[x1,x2,x3] by RLVECT_1:16
.=[(-1)*x1,(-1)*x2,(-1)*x3 ] by A7
.=[-x1,(-1)*x2,(-1)*x3 ] by RLVECT_1:16
.=[-x1,-x2,(-1)*x3 ] by RLVECT_1:16
.= [-x1,-x2,-x3] by RLVECT_1:16;
end;
let x1 be Point of E, y1 be Point of F, z1 be Point of G;
consider v10 be Element of REAL 2 such that
A11: v10=<* ||.[x1,y1].||,||.z1.|| *>
& prod_NORM([:E,F:],G).([x1,y1],z1) = |.v10.| by PRVECT_3:def 6;
consider v20 be Element of REAL 2 such that
A12: v20=<* ||.x1.||,||.y1.|| *>
& prod_NORM(E,F).(x1,y1) = |.v20.| by PRVECT_3:def 6;
reconsider v1=<* ||.x1.||,||.y1.||,||.z1.|| *>
as Element of REAL 3 by FINSEQ_2:104;
A14: 0 <= Sum (sqr v20) by RVSUM_1:86;
A15: ||.[x1,y1].||^2 = Sum (sqr v20) by A14,SQUARE_1:def 2,A12
.= Sum (<*||.x1.||^2,||.y1.||^2 *> ) by A12,TOPREAL6:11
.= ||.x1.||^2 + ||.y1.||^2 by RVSUM_1:77;
A16: Sum (sqr v10) = Sum ( <*||.[x1,y1].||^2,||.z1.||^2 *> ) by TOPREAL6:11,A11
.= ||.x1.||^2 + ||.y1.||^2 + ||.z1.||^2 by A15,RVSUM_1:77;
|.v10.| =|.v1.| by A16,BORSUK_7:17;
hence thesis by A11,A16;
end;
theorem Th15:
for X,Y,Z be RealNormSpace
holds ex I be Function of [:X,Y,Z:],product <*X,Y,Z*>
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y, z be Point of Z
holds I.(x,y,z) = <*x,y,z*> )
& ( for v,w be Point of [:X,Y,Z:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:X,Y,Z:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*X,Y,Z*> = I.(0.[:X,Y,Z:])
& ( for v be Point of [:X,Y,Z:] holds ||. I.v .|| = ||.v.|| )
proof
let X,Y,Z be RealNormSpace;
A1: the carrier of [:X,Y,Z:]
= [:the carrier of X,the carrier of Y, the carrier of Z:];
reconsider X0=X, Y0=Y, Z0=Z as RealLinearSpace;
consider I0 be Function of [:X0,Y0,Z0:], product <*X0,Y0,Z0*> such that
A2: I0 is one-to-one & I0 is onto
& ( for x be Point of X, y be Point of Y,
z be Point of Z holds I0.(x,y,z) = <*x,y,z*> )
& ( for v,w be Point of [:X0,Y0,Z0:] holds I0.(v+w) = I0.v + I0.w )
& ( for v be Point of [:X0,Y0,Z0:], r be Real
holds I0.(r*v)=r*(I0.v) )
& 0. product <*X0,Y0,Z0*> = I0.(0.[:X0,Y0,Z0:]) by Th11;
A3:product <*X,Y,Z*> = NORMSTR(# product carr <*X,Y,Z*>,
zeros <*X,Y,Z*>, [:addop <*X,Y,Z*>:], [:multop <*X,Y,Z*>:],
productnorm <*X,Y,Z*> #) by PRVECT_2:6; then
reconsider I = I0 as Function of [:X,Y,Z:],product <*X,Y,Z*>;
take I;
A4a: for g1, g2 being Point of [:X0,Y0:]
for f1, f2 being Point of Z0 holds
prod_ADD([:X,Y:],Z). ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
proof
let g1, g2 be Point of [:X0,Y0:];
let f1, f2 be Point of Z0;
reconsider gg1=g1,gg2=g2 as Point of [:X,Y:];
reconsider ff1=f1,ff2=f2 as Point of Z;
thus prod_ADD([:X,Y:],Z). ([g1,f1],[g2,f2])
= [(gg1 + gg2),(ff1 + ff2)] by PRVECT_3:def 1
.= [(g1 + g2),(f1 + f2)];
end;
A5a:
for r being Real
for g being Point of [:X0,Y0:]
for f being Point of Z0
holds prod_MLT ([:X,Y:],Z) . (r,[g,f]) = [(r * g),(r * f)]
proof
let r be Real;
let g be Point of [:X0,Y0:];
let f be Point of Z0;
reconsider gg=g as Point of [:X,Y:];
reconsider ff=f as Point of Z;
thus prod_MLT([:X,Y:],Z). (r,[g,f]) = [r*gg,r*ff] by PRVECT_3:def 2
.= [r*g,r*f];
end;
thus I is one-to-one & I is onto
& ( for x be Point of X,y be Point of Y,z be Point of Z
holds I.(x,y,z) = <*x,y,z*> ) by A2,A3;
hereby
let v,w be Point of [:X,Y,Z:];
reconsider v0=v, w0=w as Point of [:X0,Y0,Z0:];
thus I.(v+w) = I0.(v0+w0) by A4a,PRVECT_3:def 1
.= I0.v0 + I0.w0 by A2
.= I.v + I.w by A3;
end;
hereby
let v be Point of [:X,Y,Z:], r be Real;
reconsider v0=v as Point of [:X0,Y0,Z0:];
thus I.(r*v) = I0.(r*v0) by A5a,PRVECT_3:def 2
.= r*(I0.v0) by A2
.= r*(I.v) by A3;
end;
thus 0. product <*X,Y,Z*> = I.(0.[:X,Y,Z:]) by A2,A3;
for v be Point of [:X,Y,Z:] holds ||. I.v .|| = ||.v.||
proof
let v be Point of [:X,Y,Z:];
consider x1 be Point of X, y1 be Point of Y,
z1 be Point of Z such that
A6: v = [x1,y1,z1] by Lm1,A1;
consider v10 be Element of REAL 2 such that
A7: v10=<* ||.[x1,y1].||,||.z1.|| *>
& prod_NORM([:X,Y:],Z).([x1,y1],z1) = |.v10.| by PRVECT_3:def 6;
consider v20 be Element of REAL 2 such that
A8: v20=<* ||.x1.||,||.y1.|| *>
& prod_NORM(X,Y).(x1,y1) = |.v20.| by PRVECT_3:def 6;
reconsider v1=<* ||.x1.||,||.y1.||,||.z1.|| *>
as Element of REAL 3 by FINSEQ_2:104;
A10: 0 <= Sum (sqr v20) by RVSUM_1:86;
A11: ||.[x1,y1].||^2 = Sum (sqr v20) by A10,SQUARE_1:def 2,A8
.= Sum (<*||.x1.||^2,||.y1.||^2 *> ) by A8,TOPREAL6:11
.= ||.x1.||^2 + ||.y1.||^2 by RVSUM_1:77;
A12: Sum (sqr v10) = Sum ( <*||.[x1,y1].||^2,||.z1.||^2 *> ) by TOPREAL6:11,A7
.= ||.x1.||^2 + ||.y1.||^2 + ||.z1.||^2 by A11,RVSUM_1:77
.= Sum (sqr v1) by BORSUK_7:17;
A13: |.v10.| =|.v1.| by A12;
A14:I.v = I.(x1,y1,z1) by A6
.= <*x1,y1,z1*> by A2;
reconsider Iv=I.v as Element of product carr <*X,Y,Z*> by A3;
dom <*X,Y,Z*> = Seg len <*X,Y,Z*> by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45,FINSEQ_3:1; then
reconsider j1=1,j2=2,j3=3 as Element of dom <*X,Y,Z*> by ENUMSET1:def 1;
A17: normsequence(<*X,Y,Z*>,Iv).j1
= (the normF of <*X,Y,Z*>.j1).(Iv.j1) by PRVECT_2:def 11
.= ||.x1.|| by A14;
A18: normsequence(<*X,Y,Z *>,Iv).j2
= (the normF of <*X,Y,Z*>.j2).(Iv.j2) by PRVECT_2:def 11
.= ||.y1.|| by A14;
A19: normsequence(<*X,Y,Z *>,Iv).j3
= (the normF of <*X,Y,Z*>.j3).(Iv.j3) by PRVECT_2:def 11
.= ||.z1.|| by A14;
len normsequence(<*X,Y,Z*>,Iv) = len <*X,Y,Z*> by PRVECT_2:def 11
.= 3 by FINSEQ_1:45; then
normsequence(<*X,Y,Z*>,Iv) = v1 by A17,A18,A19,FINSEQ_1:45;
hence thesis by A13,A7,A6,A3,PRVECT_2:def 12;
end;
hence thesis;
end;
definition
let E,F,G be RealNormSpace;
let e be Point of E, f be Point of F, g be Point of G;
redefine func <*e,f,g*> -> Element of product <*E,F,G*>; :: redefines <* (FINSEQ_1, definition)
coherence
proof
consider I be Function of [:E,F,G:],product <*E,F,G*> such that
I is one-to-one & I is onto and
A1: for x be Point of E, y be Point of F, z be Point of G
holds I.(x,y,z) = <*x,y,z*> and
( for v,w be Point of [:E,F,G:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:E,F,G:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*E,F,G*> = I.(0.[:E,F,G:])
& ( for v be Point of [:E,F,G:] holds ||. I.v .|| = ||.v.|| ) by Th15;
A2: I.[e,f,g] in rng I by FUNCT_2:112;
I.(e,f,g) = <*e,f,g*> by A1;
hence thesis by A2;
end;
end;
theorem
for E,F,G be RealNormSpace holds
( for x be set holds
( x is Point of product <*E,F,G*>
iff ex x1 be Point of E, x2 be Point of F,
x3 be Point of G st x=<* x1,x2,x3 *> ) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds <*x1,x2,x3*> + <*y1,y2,y3*> = <* x1+y1,x2+y2,x3+y3 *> )
& 0.(product <*E,F,G*>) = <* 0.E,0.F,0.G *>
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -<*x1,x2,x3*> = <* -x1,-x2,-x3 *> )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real
holds a*<*x1,x2,x3*> = <* a*x1,a*x2,a*x3 *> )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds
||. <*x1,x2,x3*> .|| = sqrt (||.x1.||^2+||.x2.||^2+||.x3.||^2)
&
ex w be Element of REAL 3 st
w=<* ||.x1.||,||.x2.||,||.x3.|| *> & ||. <*x1,x2,x3*> .|| = |.w.| )
proof
let E,F,G be RealNormSpace;
consider I be Function of [:E,F,G:],product <*E,F,G*> such that
A1: I is one-to-one & I is onto
& ( for x be Point of E, y be Point of F,
z be Point of G holds I.(x,y,z) = <*x,y,z*> )
& ( for v,w be Point of [:E,F,G:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:E,F,G:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*E,F,G*> = I.(0.[:E,F,G:])
& ( for v be Point of [:E,F,G:] holds ||. I.v .|| = ||.v.|| ) by Th15;
thus for x be set holds
(x is Point of product <*E,F,G*>
iff ex x1 be Point of E, x2 be Point of F,
x3 be Point of G st x=<*x1,x2,x3*> )
proof
let y be set;
hereby assume y is Point of product <*E,F,G*>; then
y in the carrier of product <*E,F,G*>; then
y in rng I by A1,FUNCT_2:def 3; then
consider x be Element of the carrier of [:E,F,G:] such that
A3: y = I.x by FUNCT_2:113;
consider x1 be Point of E, x2 be Point of F, x3 be Point of G
such that
A4: x=[x1,x2,x3] by Th14;
take x1,x2,x3;
I.(x1,x2,x3) = <*x1,x2,x3*> by A1;
hence y= <*x1,x2,x3*> by A3,A4;
end;
thus thesis;
end;
thus
A7: for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds <*x1,x2,x3*>+<*y1,y2,y3*> = <* x1+y1,x2+y2,x3+y3 *>
proof
let x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G;
A9: [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] by Th14;
A10: I.(x1+y1,x2+y2,x3+y3) = <* x1+y1,x2+y2,x3+y3 *> by A1;
I.(x1,x2,x3) = <* x1,x2,x3 *> & I.(y1,y2,y3) = <* y1,y2,y3 *> by A1;
hence thesis by A1,A9,A10;
end;
thus
A11: 0. product <*E,F,G*> = <* 0.E,0.F,0.G *>
proof
I.(0.E,0.F,0.G) =<* 0.E,0.F,0.G *> by A1;
hence thesis by A1;
end;
hereby
let x1 be Point of E, x2 be Point of F, x3 be Point of G;
<*x1,x2,x3*>+<* -x1,-x2,-x3 *> = <* x1+-x1,x2+-x2,x3+-x3 *> by A7
.= <* 0.E,x2+-x2,x3+-x3 *> by RLVECT_1:def 10
.= <* 0.E,0.F,x3+-x3 *> by RLVECT_1:def 10
.= 0.(product <*E,F,G*>) by A11,RLVECT_1:def 10;
hence -<*x1,x2,x3*> = <* -x1,-x2,-x3 *> by RLVECT_1:def 10;
end;
hereby
let x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real;
A14: <*x1,x2,x3*> = I.(x1,x2,x3) by A1;
I.(a*[x1,x2,x3]) = I.(a*x1,a*x2,a*x3) by Th14
.= <* a*x1,a*x2,a*x3 *> by A1;
hence a*<*x1,x2,x3*> = <* a*x1,a*x2,a*x3 *> by A14,A1;
end;
let x1 be Point of E, x2 be Point of F, x3 be Point of G;
A16: I.[x1,x2,x3] = I.(x1,x2,x3) .= <*x1,x2,x3*> by A1;
||.[x1,x2,x3].|| = sqrt (||.x1.||^2+||.x2.||^2+||.x3.||^2) by Th14;
hence ||.<*x1,x2,x3*>.|| = sqrt (||.x1.||^2+||.x2.||^2+||.x3.||^2)
by A1,A16;
consider w be Element of REAL 3 such that
A17: w=<* ||.x1.||,||.x2.||,||.x3.|| *> & ||.[x1,x2,x3].|| = |.w.| by Th14;
take w;
thus w=<* ||.x1.||,||.x2.||,||.x3.|| *> by A17;
thus||.<*x1,x2,x3*>.|| = |.w.| by A1,A17,A16;
end;
registration
let E,F,G be complete RealNormSpace;
cluster [:E,F,G:] -> complete;
coherence;
end;