:: 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 ) )

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.|

( 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

F . i = 0 ) holds

Sum F = 0

proof end;

definition

let f be Function;

let X be set ;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for i being set st i in dom f holds

b_{1} . i is Function of [:X,(f . i):],(f . i) ) )

end;
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 ( dom it = dom f & ( for i being set st i in dom f holds

it . i is Function of [:X,(f . i):],(f . i) ) );

ex b

( dom b

b

proof end;

:: deftheorem Def1 defines MultOps PRVECT_2:def 1 :

for f being Function

for X being set

for b_{3} being Function holds

( b_{3} is MultOps of X,f iff ( dom b_{3} = dom f & ( for i being set st i in dom f holds

b_{3} . i is Function of [:X,(f . i):],(f . i) ) ) );

for f being Function

for X being set

for b

( b

b

registration

let F be Domain-Sequence;

let X be set ;

coherence

for b_{1} being MultOps of X,F holds b_{1} is FinSequence-like

end;
let X be set ;

coherence

for b

proof 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) ) ) )

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

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

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;

ex b_{1} 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_{1} . (x,d)) . i = (p . i) . (x,(d . i))

for b_{1}, b_{2} 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_{1} . (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_{2} . (x,d)) . i = (p . i) . (x,(d . i)) ) holds

b_{1} = b_{2}

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

ex b

for x being Element of X

for d being Element of product F

for i being Element of dom F holds (b

proof end;

uniqueness for b

for d being Element of product F

for i being Element of dom F holds (b

for d being Element of product F

for i being Element of dom F holds (b

b

proof 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_{4} being Function of [:X,(product F):],(product F) holds

( b_{4} = [:p:] iff for x being Element of X

for d being Element of product F

for i being Element of dom F holds (b_{4} . (x,d)) . i = (p . i) . (x,(d . i)) );

for F being Domain-Sequence

for X being non empty set

for p being MultOps of X,F

for b

( b

for d being Element of product F

for i being Element of dom F holds (b

definition

let R be Relation;

end;
attr R is RealLinearSpace-yielding means :Def3: :: PRVECT_2:def 3

for S being set st S in rng R holds

S is RealLinearSpace;

for S being set st S in rng R holds

S is RealLinearSpace;

:: 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 );

for R being Relation holds

( R is RealLinearSpace-yielding iff for S being set st S in rng R holds

S is RealLinearSpace );

registration

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is RealLinearSpace-yielding )
end;

cluster Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like countable RealLinearSpace-yielding for set ;

existence ex b

( not b

proof 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

end;
let j be Element of dom G;

:: original: .

redefine func G . j -> RealLinearSpace;

coherence

G . j is RealLinearSpace

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is RealLinearSpace-yielding holds

b_{1} is non-empty-addLoopStr-yielding

end;
for b

b

proof 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

end;
let j be Element of dom (carr G);

:: original: .

redefine func G . j -> RealLinearSpace;

coherence

G . j is RealLinearSpace

proof end;

definition

let G be RealLinearSpace-Sequence;

ex b_{1} being MultOps of REAL , carr G st

( len b_{1} = len (carr G) & ( for j being Element of dom (carr G) holds b_{1} . j = the Mult of (G . j) ) )

for b_{1}, b_{2} being MultOps of REAL , carr G st len b_{1} = len (carr G) & ( for j being Element of dom (carr G) holds b_{1} . j = the Mult of (G . j) ) & len b_{2} = len (carr G) & ( for j being Element of dom (carr G) holds b_{2} . j = the Mult of (G . j) ) holds

b_{1} = b_{2}

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 ( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = the Mult of (G . j) ) );

ex b

( len b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines multop PRVECT_2:def 8 :

for G being RealLinearSpace-Sequence

for b_{2} being MultOps of REAL , carr G holds

( b_{2} = multop G iff ( len b_{2} = len (carr G) & ( for j being Element of dom (carr G) holds b_{2} . j = the Mult of (G . j) ) ) );

for G being RealLinearSpace-Sequence

for b

( b

definition

let G be RealLinearSpace-Sequence;

RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) is non empty strict RLSStruct ;

end;
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):] #);

RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) is non empty strict RLSStruct ;

:: 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):] #);

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;

( 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 )

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

definition

let R be Relation;

end;
attr R is RealNormSpace-yielding means :Def10: :: PRVECT_2:def 10

for x being set st x in rng R holds

x is RealNormSpace;

for x being set st x in rng R holds

x is RealNormSpace;

:: 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 );

for R being Relation holds

( R is RealNormSpace-yielding iff for x being set st x in rng R holds

x is RealNormSpace );

registration

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is RealNormSpace-yielding )
end;

cluster Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like countable RealNormSpace-yielding for set ;

existence ex b

( not b

proof 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

end;
let j be Element of dom G;

:: original: .

redefine func G . j -> RealNormSpace;

coherence

G . j is RealNormSpace

proof end;

registration

for b_{1} being FinSequence st b_{1} is RealNormSpace-yielding holds

b_{1} is RealLinearSpace-yielding
;

end;

cluster Relation-like Function-like FinSequence-like RealNormSpace-yielding -> RealLinearSpace-yielding for set ;

coherence for b

b

definition

let G be RealNormSpace-Sequence;

let x be Element of product (carr G);

ex b_{1} being Element of REAL (len G) st

( len b_{1} = len G & ( for j being Element of dom G holds b_{1} . j = the normF of (G . j) . (x . j) ) )

for b_{1}, b_{2} being Element of REAL (len G) st len b_{1} = len G & ( for j being Element of dom G holds b_{1} . j = the normF of (G . j) . (x . j) ) & len b_{2} = len G & ( for j being Element of dom G holds b_{2} . j = the normF of (G . j) . (x . j) ) holds

b_{1} = b_{2}

end;
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 ( len it = len G & ( for j being Element of dom G holds it . j = the normF of (G . j) . (x . j) ) );

ex b

( len b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines normsequence PRVECT_2:def 11 :

for G being RealNormSpace-Sequence

for x being Element of product (carr G)

for b_{3} being Element of REAL (len G) holds

( b_{3} = normsequence (G,x) iff ( len b_{3} = len G & ( for j being Element of dom G holds b_{3} . j = the normF of (G . j) . (x . j) ) ) );

for G being RealNormSpace-Sequence

for x being Element of product (carr G)

for b

( b

definition

let G be RealNormSpace-Sequence;

ex b_{1} being Function of (product (carr G)),REAL st

for x being Element of product (carr G) holds b_{1} . x = |.(normsequence (G,x)).|

for b_{1}, b_{2} being Function of (product (carr G)),REAL st ( for x being Element of product (carr G) holds b_{1} . x = |.(normsequence (G,x)).| ) & ( for x being Element of product (carr G) holds b_{2} . x = |.(normsequence (G,x)).| ) holds

b_{1} = b_{2}

end;
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 for x being Element of product (carr G) holds it . x = |.(normsequence (G,x)).|;

ex b

for x being Element of product (carr G) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines productnorm PRVECT_2:def 12 :

for G being RealNormSpace-Sequence

for b_{2} being Function of (product (carr G)),REAL holds

( b_{2} = productnorm G iff for x being Element of product (carr G) holds b_{2} . x = |.(normsequence (G,x)).| );

for G being RealNormSpace-Sequence

for b

( b

definition

let G be RealNormSpace-Sequence;

ex b_{1} being non empty strict NORMSTR st

( RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = product G & the normF of b_{1} = productnorm G )

for b_{1}, b_{2} being non empty strict NORMSTR st RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = product G & the normF of b_{1} = productnorm G & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = product G & the normF of b_{2} = productnorm G holds

b_{1} = b_{2}
;

end;
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 ( 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 );

ex b

( RLSStruct(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def13 defines product PRVECT_2:def 13 :

for G being RealNormSpace-Sequence

for b_{2} being non empty strict NORMSTR holds

( b_{2} = product G iff ( RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = product G & the normF of b_{2} = productnorm G ) );

for G being RealNormSpace-Sequence

for b

( b

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)).|

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

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

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;

( 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 )

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

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.||

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).||

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 ) ) )

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 )

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

product G is complete

proof end;