:: 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-2016 Association of Mizar Users

environ

vocabularies HIDDEN, SEQ_1, SUBSET_1, NUMBERS, FUNCT_1, COMPLEX1, ARYTM_1, SEQ_2, ORDINAL2, CARD_1, ARYTM_3, XXREAL_0, FINSEQ_1, NAT_1, RVSUM_1, SQUARE_1, RELAT_1, CARD_3, FINSEQ_2, ZFMISC_1, MCART_1, PRVECT_1, XBOOLE_0, RLVECT_1, GROUP_2, STRUCT_0, ALGSTR_0, BINOP_1, VECTSP_1, REAL_1, SUPINF_2, FUNCT_6, FINSEQOP, SETWISEO, NORMSP_1, TARSKI, PRE_TOPC, EUCLID, FUNCT_2, REAL_NS1, REWRITE1, RSSPACE3, PRVECT_2, NORMSP_0, METRIC_1, RELAT_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_3, XCMPLX_0, XXREAL_0, NUMBERS, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, RVSUM_1, STRUCT_0, ALGSTR_0, FUNCT_2, FUNCT_3, BINOP_1, REAL_1, SEQ_1, COMSEQ_2, SEQ_2, RLVECT_1, VECTSP_1, SETWISEO, FINSEQ_1, FINSEQ_2, FINSEQOP, SQUARE_1, PRE_TOPC, EUCLID, PRVECT_1, NORMSP_0, NORMSP_1, RSSPACE3, LOPBAN_1, REAL_NS1;
definitions RLVECT_1, NORMSP_1, ALGSTR_0, NORMSP_0;
theorems BINOP_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQOP, SETWISEO, TARSKI, CARD_3, RLVECT_1, RELAT_1, RVSUM_1, ABSVALUE, FVSUM_1, SEQ_2, PRVECT_1, NORMSP_1, SQUARE_1, EUCLID, XREAL_1, LOPBAN_1, RSSPACE3, REAL_NS1, XXREAL_0, VALUED_1, XREAL_0, NORMSP_0, CARD_1, ORDINAL1;
schemes FUNCT_1, BINOP_1, FUNCT_2, FINSEQ_1, PRVECT_1, CLASSES1;
registrations STRUCT_0, FINSEQ_2, FINSEQ_1, CARD_3, RLVECT_1, PRVECT_1, XREAL_0, MEMBERED, NORMSP_1, REAL_NS1, ORDINAL1, FUNCT_1, FUNCT_2, RELAT_1, XBOOLE_0, NUMBERS, VALUED_0, NORMSP_0, CARD_1, EUCLID, SQUARE_1;
constructors HIDDEN, FUNCT_3, FINSEQOP, REAL_1, SEQ_2, COMPLEX1, SQUARE_1, BINOP_2, SETWISEO, PRVECT_1, RSSPACE3, LOPBAN_1, REAL_NS1, RVSUM_1, NORMSP_1, RELSET_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RLVECT_1, FINSEQ_2, EUCLID, STRUCT_0, SQUARE_1, ALGSTR_0, NORMSP_0, ORDINAL1;
expansions RLVECT_1, NORMSP_1;


theorem :: PRVECT_2:1
for s, t being Real_Sequence
for g being Real st ( for n being Element of NAT holds t . n = |.((s . n) - g).| ) holds
( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )
proof end;

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 & x . i <= y . i ) ) holds
|.x.| <= |.y.|
proof end;

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
proof end;

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 & ( 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 & ( for i being set st i in dom f holds
b1 . i is Function of [:X,(f . i):],(f . i) ) )
proof end;
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 & ( 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
proof end;
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 & ( for i being set st i in dom F holds
p . i is Function of [:X,(F . i):],(F . i) ) ) )
proof end;

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 func p . 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
proof end;

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))
proof end;
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)) ) & ( 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
proof end;
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;
attr R 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 V33() FinSequence-like FinSubsequence-like countable RealLinearSpace-yielding for set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is RealLinearSpace-yielding )
proof end;
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 func G . j -> RealLinearSpace;
coherence
G . j is RealLinearSpace
proof end;
end;

definition
let G be RealLinearSpace-Sequence;
func carr G -> Domain-Sequence means :Def4: :: PRVECT_2:def 4
( len it = len G & ( 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 & ( for j being Element of dom G holds b1 . j = the carrier of (G . j) ) )
proof end;
uniqueness
for b1, b2 being Domain-Sequence st len b1 = len G & ( for j being Element of dom G holds b1 . j = the carrier of (G . j) ) & len b2 = len G & ( for j being Element of dom G holds b2 . j = the carrier of (G . j) ) holds
b1 = b2
proof end;
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 & ( 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 func G . j -> RealLinearSpace;
coherence
G . j is RealLinearSpace
proof end;
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) & ( 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) & ( for j being Element of dom (carr G) holds b1 . j = the addF of (G . j) ) )
proof end;
uniqueness
for b1, b2 being BinOps of carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the addF of (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the addF of (G . j) ) holds
b1 = b2
proof end;
func complop G -> UnOps of carr G means :Def6: :: PRVECT_2:def 6
( len it = len (carr G) & ( 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) & ( for j being Element of dom (carr G) holds b1 . j = comp (G . j) ) )
proof end;
uniqueness
for b1, b2 being UnOps of carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = comp (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = comp (G . j) ) holds
b1 = b2
proof end;
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)
proof end;
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) ) & ( for j being Element of dom (carr G) holds b2 . j = the ZeroF of (G . j) ) holds
b1 = b2
proof end;
func multop G -> MultOps of REAL , carr G means :Def8: :: PRVECT_2:def 8
( len it = len (carr G) & ( 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) & ( for j being Element of dom (carr G) holds b1 . j = the Mult of (G . j) ) )
proof end;
uniqueness
for b1, b2 being MultOps of REAL , carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the Mult of (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the Mult of (G . j) ) holds
b1 = b2
proof end;
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) & ( 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) & ( 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) & ( 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 & the addF of LS is associative holds
( LS is Abelian & LS is add-associative )
by BINOP_1:def 2, BINOP_1:def 3;

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
by BINOP_1:3;

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)) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . (v1,w1)) . i = vi + wi ) )
proof end;

Lm4: for G being RealLinearSpace-Sequence
for r being Element of 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)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:(multop G):] . (r,v)) . i = r * vi ) )
proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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

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 & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
proof end;
end;

definition
let R be Relation;
attr R 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 V33() FinSequence-like FinSubsequence-like countable RealNormSpace-yielding for set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is RealNormSpace-yielding )
proof end;
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 func G . j -> RealNormSpace;
coherence
G . j is RealNormSpace
proof end;
end;

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 ;
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 & ( 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 & ( for j being Element of dom G holds b1 . j = the normF of (G . j) . (x . j) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL (len G) st len b1 = len G & ( for j being Element of dom G holds b1 . j = the normF of (G . j) . (x . j) ) & len b2 = len G & ( for j being Element of dom G holds b2 . j = the normF of (G . j) . (x . j) ) holds
b1 = b2
proof end;
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 & ( 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)).|
proof end;
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)).| ) & ( for x being Element of product (carr G) holds b2 . x = |.(normsequence (G,x)).| ) holds
b1 = b2
proof end;
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 & 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 & the normF of b1 = productnorm G )
proof end;
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 & the normF of b1 = productnorm G & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = product G & 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 & 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) #)
proof end;

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)).|
proof end;

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 & z = [:(addop G):] . (x,y) holds
(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i
proof end;

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
proof end;

Lm6: for G being RealNormSpace-Sequence holds
( product G is reflexive & product G is discerning & product G is RealNormSpace-like )
proof end;

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 & product G is discerning & product G is RealNormSpace-like & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital & product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable )
proof end;
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 & xi = y . i holds
||.xi.|| <= ||.x.||
proof end;

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

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 & zx = x & yi = zy . i & zy = y holds
||.(yi - xi).|| <= ||.(y - x).||
proof end;

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 & seq is convergent & lim seq = x0 holds
for i being Element of dom G ex seqi being sequence of (G . i) st
( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
proof end;

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 & ( for i being Element of dom G ex seqi being sequence of (G . i) st
( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) ) holds
( seq is convergent & lim seq = x0 )
proof end;

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
proof end;