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

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 b₁ being Function st
( dom b₁ = dom f & ( for i being set st i in dom f holds
b₁ . 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 b₃ being Function holds
( b₃ is MultOps of X,f iff ( dom b₃ = dom f & ( for i being set st i in dom f holds
b₃ . 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 b₁ being MultOps of X,F holds b₁ 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 b₁ 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 (b₁ . (x,d)) . i = (p . i) . (x,(d . i))

proof end;

uniqueness
for b₁, b₂ 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 (b₁ . (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 (b₂ . (x,d)) . i = (p . i) . (x,(d . i)) ) holds
b₁ = b₂

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 b₄ being Function of [:X,(product F):],(product F) holds
( b₄ = [:p:] iff for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b₄ . (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 b₁ being FinSequence st
( not b₁ is empty & b₁ 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;

registration

cluster Relation-like RealLinearSpace-yielding -> non-empty-addLoopStr-yielding for set ;

coherence
for b₁ being Relation st b₁ is RealLinearSpace-yielding holds
b₁ is non-empty-addLoopStr-yielding

proof end;

end;

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 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 b₁ being MultOps of REAL , carr G st
( len b₁ = len (carr G) & ( for j being Element of dom (carr G) holds b₁ . j = the Mult of (G . j) ) )

proof end;

uniqueness
for b₁, b₂ being MultOps of REAL , carr G st len b₁ = len (carr G) & ( for j being Element of dom (carr G) holds b₁ . j = the Mult of (G . j) ) & len b₂ = len (carr G) & ( for j being Element of dom (carr G) holds b₂ . j = the Mult of (G . j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem PRVECT_2:def 4 :
canceled;

:: deftheorem PRVECT_2:def 5 :
canceled;

:: deftheorem PRVECT_2:def 6 :
canceled;

:: deftheorem PRVECT_2:def 7 :
canceled;

:: deftheorem Def8 defines multop PRVECT_2:def 8 :
for G being RealLinearSpace-Sequence
for b₂ being MultOps of REAL , carr G holds
( b₂ = multop G iff ( len b₂ = len (carr G) & ( for j being Element of dom (carr G) holds b₂ . 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 b₁ being FinSequence st
( not b₁ is empty & b₁ 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 b₁ being FinSequence st b₁ is RealNormSpace-yielding holds
b₁ 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 b₁ being Element of REAL (len G) st
( len b₁ = len G & ( for j being Element of dom G holds b₁ . j = the normF of (G . j) . (x . j) ) )

proof end;

uniqueness
for b₁, b₂ being Element of REAL (len G) st len b₁ = len G & ( for j being Element of dom G holds b₁ . j = the normF of (G . j) . (x . j) ) & len b₂ = len G & ( for j being Element of dom G holds b₂ . j = the normF of (G . j) . (x . j) ) holds
b₁ = b₂

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 b₃ being Element of REAL (len G) holds
( b₃ = normsequence (G,x) iff ( len b₃ = len G & ( for j being Element of dom G holds b₃ . 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 b₁ being Function of (product (carr G)),REAL st
for x being Element of product (carr G) holds b₁ . x = |.(normsequence (G,x)).|

proof end;

uniqueness
for b₁, b₂ being Function of (product (carr G)),REAL st ( for x being Element of product (carr G) holds b₁ . x = |.(normsequence (G,x)).| ) & ( for x being Element of product (carr G) holds b₂ . x = |.(normsequence (G,x)).| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines productnorm PRVECT_2:def 12 :
for G being RealNormSpace-Sequence
for b₂ being Function of (product (carr G)),REAL holds
( b₂ = productnorm G iff for x being Element of product (carr G) holds b₂ . 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 b₁ being non empty strict NORMSTR st
( RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = product G & the normF of b₁ = productnorm G )

proof end;

uniqueness
for b₁, b₂ being non empty strict NORMSTR st RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = product G & the normF of b₁ = productnorm G & RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = product G & the normF of b₂ = productnorm G holds
b₁ = b₂ ;

end;

:: deftheorem Def13 defines product PRVECT_2:def 13 :
for G being RealNormSpace-Sequence
for b₂ being non empty strict NORMSTR holds
( b₂ = product G iff ( RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = product G & the normF of b₂ = 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 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 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;