:: The Product Space of Real Normed Spaces and Its Properties
:: by Noboru Endou , Yasunari Shidama and Keiichi Miyajima
::
:: Received July 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem :: PRVECT_2:1
for s, t being Real_Sequence
for g being real number st ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) holds
( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )
proofend;

theorem Th2: :: PRVECT_2:2
for x, y being FinSequence of REAL st len x = len y & ( for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i &amp; x . i <= y . i ) ) holds
|.x.| <= |.y.|
proofend;

theorem Th3: :: PRVECT_2:3
for F being FinSequence of REAL st ( for i being Element of NAT st i in dom F holds
F . i = 0 ) holds
Sum F = 0
proofend;

definition
let f be Function;
let X be set ;
mode MultOps of X,f ->  Function means :Def1: :: PRVECT_2:def 1
( dom it = dom f &amp; ( for i being set st i in dom f holds
it . i is Function of [:X,(f . i):],(f . i) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for i being set st i in dom f holds
b1 . i is Function of [:X,(f . i):],(f . i) ) )
proofend;
end;

:: deftheorem Def1 defines MultOps PRVECT_2:def_1_:_
 for f being Function
for X being set
for b3 being Function holds
( b3 is MultOps of X,f iff ( dom b3 = dom f &amp; ( for i being set st i in dom f holds
b3 . i is Function of [:X,(f . i):],(f . i) ) ) );

registration
let F be Domain-Sequence;
let X be set ;
cluster  ->  FinSequence-like for MultOps of X,F;
coherence
 for b1 being MultOps of X,F holds b1 is FinSequence-like
proofend;
end;

theorem Th4: :: PRVECT_2:4
for X being set
for F being Domain-Sequence
for p being FinSequence holds
( p is MultOps of X,F iff ( len p = len F &amp; ( for i being set st i in dom F holds
p . i is Function of [:X,(F . i):],(F . i) ) ) )
proofend;

definition
let F be Domain-Sequence;
let X be set ;
let p be MultOps of X,F;
let i be Element of dom F;
:: original:.
redefine funcp . i ->  Function of [:X,(F . i):],(F . i);
coherence
 p . i is Function of [:X,(F . i):],(F . i) by Th4;
end;

theorem Th5: :: PRVECT_2:5
for X being non empty set
for F being Domain-Sequence
for f, g being Function of [:X,(product F):],(product F) st ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) holds
f = g
proofend;

definition
let F be Domain-Sequence;
let X be non empty set ;
let p be MultOps of X,F;
func[:p:] ->  Function of [:X,(product F):],(product F) means :Def2: :: PRVECT_2:def 2
 for x being Element of X
for d being Element of product F
for i being Element of dom F holds (it . (x,d)) . i = (p . i) . (x,(d . i));
existence
 ex b1 being Function of [:X,(product F):],(product F) st
for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b1 . (x,d)) . i = (p . i) . (x,(d . i))
proofend;
uniqueness
 for b1, b2 being Function of [:X,(product F):],(product F) st ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b1 . (x,d)) . i = (p . i) . (x,(d . i)) ) &amp; ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b2 . (x,d)) . i = (p . i) . (x,(d . i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines [: PRVECT_2:def_2_:_
 for F being Domain-Sequence
for X being non empty set
for p being MultOps of X,F
for b4 being Function of [:X,(product F):],(product F) holds
( b4 = [:p:] iff for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b4 . (x,d)) . i = (p . i) . (x,(d . i)) );

definition
let R be Relation;
attrR is RealLinearSpace-yielding  means :Def3: :: PRVECT_2:def 3
 for S being set st S in rng R holds
S is RealLinearSpace;
end;

:: deftheorem Def3 defines RealLinearSpace-yielding PRVECT_2:def_3_:_
 for R being Relation holds
( R is RealLinearSpace-yielding iff for S being set st S in rng R holds
S is RealLinearSpace );

registration
cluster Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable RealLinearSpace-yielding for set ;
existence
 ex b1 being FinSequence st
( not b1 is empty &amp; b1 is RealLinearSpace-yielding )
proofend;
end;

definition
mode RealLinearSpace-Sequence is non empty RealLinearSpace-yielding FinSequence;
end;

definition
let G be RealLinearSpace-Sequence;
let j be Element of dom G;
:: original:.
redefine funcG . j ->  RealLinearSpace;
coherence
 G . j is RealLinearSpace
proofend;
end;

definition
let G be RealLinearSpace-Sequence;
func carr G ->  Domain-Sequence means :Def4: :: PRVECT_2:def 4
( len it = len G &amp; ( for j being Element of dom G holds it . j = the carrier of (G . j) ) );
existence
 ex b1 being Domain-Sequence st
( len b1 = len G &amp; ( for j being Element of dom G holds b1 . j = the carrier of (G . j) ) )
proofend;
uniqueness
 for b1, b2 being Domain-Sequence st len b1 = len G &amp; ( for j being Element of dom G holds b1 . j = the carrier of (G . j) ) &amp; len b2 = len G &amp; ( for j being Element of dom G holds b2 . j = the carrier of (G . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines carr PRVECT_2:def_4_:_
 for G being RealLinearSpace-Sequence
for b2 being Domain-Sequence holds
( b2 = carr G iff ( len b2 = len G &amp; ( for j being Element of dom G holds b2 . j = the carrier of (G . j) ) ) );

definition
let G be RealLinearSpace-Sequence;
let j be Element of dom (carr G);
:: original:.
redefine funcG . j ->  RealLinearSpace;
coherence
 G . j is RealLinearSpace
proofend;
end;

definition
let G be RealLinearSpace-Sequence;
func addop G ->  BinOps of carr G means :Def5: :: PRVECT_2:def 5
( len it = len (carr G) &amp; ( for j being Element of dom (carr G) holds it . j = the addF of (G . j) ) );
existence
 ex b1 being BinOps of carr G st
( len b1 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b1 . j = the addF of (G . j) ) )
proofend;
uniqueness
 for b1, b2 being BinOps of carr G st len b1 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b1 . j = the addF of (G . j) ) &amp; len b2 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b2 . j = the addF of (G . j) ) holds
b1 = b2
proofend;
func complop G ->  UnOps of carr G means :Def6: :: PRVECT_2:def 6
( len it = len (carr G) &amp; ( for j being Element of dom (carr G) holds it . j = comp (G . j) ) );
existence
 ex b1 being UnOps of carr G st
( len b1 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b1 . j = comp (G . j) ) )
proofend;
uniqueness
 for b1, b2 being UnOps of carr G st len b1 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b1 . j = comp (G . j) ) &amp; len b2 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b2 . j = comp (G . j) ) holds
b1 = b2
proofend;
func zeros G ->  Element of product (carr G) means :Def7: :: PRVECT_2:def 7
 for j being Element of dom (carr G) holds it . j = the ZeroF of (G . j);
existence
 ex b1 being Element of product (carr G) st
for j being Element of dom (carr G) holds b1 . j = the ZeroF of (G . j)
proofend;
uniqueness
 for b1, b2 being Element of product (carr G) st ( for j being Element of dom (carr G) holds b1 . j = the ZeroF of (G . j) ) &amp; ( for j being Element of dom (carr G) holds b2 . j = the ZeroF of (G . j) ) holds
b1 = b2
proofend;
func multop G ->  MultOps of REAL , carr G means :Def8: :: PRVECT_2:def 8
( len it = len (carr G) &amp; ( for j being Element of dom (carr G) holds it . j = the Mult of (G . j) ) );
existence
 ex b1 being MultOps of REAL , carr G st
( len b1 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b1 . j = the Mult of (G . j) ) )
proofend;
uniqueness
 for b1, b2 being MultOps of REAL , carr G st len b1 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b1 . j = the Mult of (G . j) ) &amp; len b2 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b2 . j = the Mult of (G . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines addop PRVECT_2:def_5_:_
 for G being RealLinearSpace-Sequence
for b2 being BinOps of carr G holds
( b2 = addop G iff ( len b2 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b2 . j = the addF of (G . j) ) ) );

:: deftheorem Def6 defines complop PRVECT_2:def_6_:_
 for G being RealLinearSpace-Sequence
for b2 being UnOps of carr G holds
( b2 = complop G iff ( len b2 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b2 . j = comp (G . j) ) ) );

:: deftheorem Def7 defines zeros PRVECT_2:def_7_:_
 for G being RealLinearSpace-Sequence
for b2 being Element of product (carr G) holds
( b2 = zeros G iff for j being Element of dom (carr G) holds b2 . j = the ZeroF of (G . j) );

:: deftheorem Def8 defines multop PRVECT_2:def_8_:_
 for G being RealLinearSpace-Sequence
for b2 being MultOps of REAL , carr G holds
( b2 = multop G iff ( len b2 = len (carr G) &amp; ( for j being Element of dom (carr G) holds b2 . j = the Mult of (G . j) ) ) );

definition
let G be RealLinearSpace-Sequence;
func product G ->  non empty strict RLSStruct  equals :: PRVECT_2:def 9
 RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #);
coherence
 RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) is non empty strict RLSStruct ;
end;

:: deftheorem  defines product PRVECT_2:def_9_:_
 for G being RealLinearSpace-Sequence holds product G = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #);

Lm1:  for LS being non empty addLoopStr st the addF of LS is commutative &amp; the addF of LS is associative holds
( LS is Abelian &amp; LS is add-associative )
proofend;

Lm2:  for LS being non empty addLoopStr st the ZeroF of LS is_a_unity_wrt the addF of LS holds
LS is right_zeroed
proofend;

Lm3:  for G being RealLinearSpace-Sequence
for v1, w1 being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) &amp; ( for vi, wi being VECTOR of (G . i) st vi = v1 . i &amp; wi = w1 . i holds
([:(addop G):] . (v1,w1)) . i = vi + wi ) )
proofend;

Lm4:  for G being RealLinearSpace-Sequence
for r being Real
for v being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) &amp; ( for vi being VECTOR of (G . i) st vi = v . i holds
([:(multop G):] . (r,v)) . i = r * vi ) )
proofend;

Lm5:  for G being RealLinearSpace-Sequence holds
( product G is vector-distributive &amp; product G is scalar-distributive &amp; product G is scalar-associative &amp; product G is scalar-unital )
proofend;

registration
let G be RealLinearSpace-Sequence;
cluster product G ->  non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( product G is Abelian &amp; product G is add-associative &amp; product G is right_zeroed &amp; product G is right_complementable &amp; product G is vector-distributive &amp; product G is scalar-distributive &amp; product G is scalar-associative &amp; product G is scalar-unital )
proofend;
end;

begin

definition
let R be Relation;
attrR is RealNormSpace-yielding  means :Def10: :: PRVECT_2:def 10
 for x being set st x in rng R holds
x is RealNormSpace;
end;

:: deftheorem Def10 defines RealNormSpace-yielding PRVECT_2:def_10_:_
 for R being Relation holds
( R is RealNormSpace-yielding iff for x being set st x in rng R holds
x is RealNormSpace );

registration
cluster Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable RealNormSpace-yielding for set ;
existence
 ex b1 being FinSequence st
( not b1 is empty &amp; b1 is RealNormSpace-yielding )
proofend;
end;

definition
mode RealNormSpace-Sequence is non empty RealNormSpace-yielding FinSequence;
end;

definition
let G be RealNormSpace-Sequence;
let j be Element of dom G;
:: original:.
redefine funcG . j ->  RealNormSpace;
coherence
 G . j is RealNormSpace
proofend;
end;

Lm6:  for g being RealNormSpace-yielding FinSequence holds g is RealLinearSpace-yielding
proofend;

registration
cluster Relation-like Function-like FinSequence-like RealNormSpace-yielding  ->  RealLinearSpace-yielding for set ;
coherence
 for b1 being FinSequence st b1 is RealNormSpace-yielding holds
b1 is RealLinearSpace-yielding by Lm6;
end;

definition
let G be RealNormSpace-Sequence;
let x be Element of product (carr G);
func normsequence (G,x) ->  Element of REAL (len G) means :Def11: :: PRVECT_2:def 11
( len it = len G &amp; ( for j being Element of dom G holds it . j = the normF of (G . j) . (x . j) ) );
existence
 ex b1 being Element of REAL (len G) st
( len b1 = len G &amp; ( for j being Element of dom G holds b1 . j = the normF of (G . j) . (x . j) ) )
proofend;
uniqueness
 for b1, b2 being Element of REAL (len G) st len b1 = len G &amp; ( for j being Element of dom G holds b1 . j = the normF of (G . j) . (x . j) ) &amp; len b2 = len G &amp; ( for j being Element of dom G holds b2 . j = the normF of (G . j) . (x . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines normsequence PRVECT_2:def_11_:_
 for G being RealNormSpace-Sequence
for x being Element of product (carr G)
for b3 being Element of REAL (len G) holds
( b3 = normsequence (G,x) iff ( len b3 = len G &amp; ( for j being Element of dom G holds b3 . j = the normF of (G . j) . (x . j) ) ) );

definition
let G be RealNormSpace-Sequence;
func productnorm G ->  Function of (product (carr G)),REAL means :Def12: :: PRVECT_2:def 12
 for x being Element of product (carr G) holds it . x = |.(normsequence (G,x)).|;
existence
 ex b1 being Function of (product (carr G)),REAL st
for x being Element of product (carr G) holds b1 . x = |.(normsequence (G,x)).|
proofend;
uniqueness
 for b1, b2 being Function of (product (carr G)),REAL st ( for x being Element of product (carr G) holds b1 . x = |.(normsequence (G,x)).| ) &amp; ( for x being Element of product (carr G) holds b2 . x = |.(normsequence (G,x)).| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines productnorm PRVECT_2:def_12_:_
 for G being RealNormSpace-Sequence
for b2 being Function of (product (carr G)),REAL holds
( b2 = productnorm G iff for x being Element of product (carr G) holds b2 . x = |.(normsequence (G,x)).| );

definition
let G be RealNormSpace-Sequence;
func product G ->  non empty strict NORMSTR  means :Def13: :: PRVECT_2:def 13
( RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = product G &amp; the normF of it = productnorm G );
existence
 ex b1 being non empty strict NORMSTR st
( RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = product G &amp; the normF of b1 = productnorm G )
proofend;
uniqueness
 for b1, b2 being non empty strict NORMSTR st RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = product G &amp; the normF of b1 = productnorm G &amp; RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = product G &amp; the normF of b2 = productnorm G holds
b1 = b2 ;
end;

:: deftheorem Def13 defines product PRVECT_2:def_13_:_
 for G being RealNormSpace-Sequence
for b2 being non empty strict NORMSTR holds
( b2 = product G iff ( RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = product G &amp; the normF of b2 = productnorm G ) );

theorem Th6: :: PRVECT_2:6
for G being RealNormSpace-Sequence holds product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #)
proofend;

theorem Th7: :: PRVECT_2:7
for G being RealNormSpace-Sequence
for x being VECTOR of (product G)
for y being Element of product (carr G) st x = y holds
||.x.|| = |.(normsequence (G,y)).|
proofend;

theorem Th8: :: PRVECT_2:8
for G being RealNormSpace-Sequence
for x, y, z being Element of product (carr G)
for i being Element of NAT st i in dom x &amp; z = [:(addop G):] . (x,y) holds
(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i
proofend;

theorem Th9: :: PRVECT_2:9
for G being RealNormSpace-Sequence
for x being Element of product (carr G)
for i being Element of NAT st i in dom x holds
0 <= (normsequence (G,x)) . i
proofend;

Lm7:  for G being RealNormSpace-Sequence holds
( product G is reflexive &amp; product G is discerning &amp; product G is RealNormSpace-like )
proofend;

registration
let G be RealNormSpace-Sequence;
cluster product G ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;
coherence
 ( product G is reflexive &amp; product G is discerning &amp; product G is RealNormSpace-like &amp; product G is vector-distributive &amp; product G is scalar-distributive &amp; product G is scalar-associative &amp; product G is scalar-unital &amp; product G is Abelian &amp; product G is add-associative &amp; product G is right_zeroed &amp; product G is right_complementable )
proofend;
end;

theorem Th10: :: PRVECT_2:10
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of (product G)
for y being Element of product (carr G)
for xi being Point of (G . i) st y = x &amp; xi = y . i holds
||.xi.|| <= ||.x.||
proofend;

Lm8:  for RNS being RealNormSpace
for S being sequence of RNS
for g being Point of RNS holds
( S is convergent &amp; lim S = g iff ( ||.(S - g).|| is convergent &amp; lim ||.(S - g).|| = 0 ) )
proofend;

theorem Th11: :: PRVECT_2:11
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of (product G)
for xi, yi being Point of (G . i)
for zx, zy being Element of product (carr G) st xi = zx . i &amp; zx = x &amp; yi = zy . i &amp; zy = y holds
||.(yi - xi).|| <= ||.(y - x).||
proofend;

theorem :: PRVECT_2:12
for G being RealNormSpace-Sequence
for seq being sequence of (product G)
for x0 being Point of (product G)
for y0 being Element of product (carr G) st x0 = y0 &amp; seq is convergent &amp; lim seq = x0 holds
for i being Element of dom G ex seqi being sequence of (G . i) st
( seqi is convergent &amp; y0 . i = lim seqi &amp; ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m &amp; seqi . m = seqm . i ) ) )
proofend;

theorem Th13: :: PRVECT_2:13
for G being RealNormSpace-Sequence
for seq being sequence of (product G)
for x0 being Point of (product G)
for y0 being Element of product (carr G) st x0 = y0 &amp; ( for i being Element of dom G ex seqi being sequence of (G . i) st
( seqi is convergent &amp; y0 . i = lim seqi &amp; ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m &amp; seqi . m = seqm . i ) ) ) ) holds
( seq is convergent &amp; lim seq = x0 )
proofend;

theorem :: PRVECT_2:14
for G being RealNormSpace-Sequence st ( for i being Element of dom G holds G . i is complete ) holds
product G is complete
proofend;