:: PRVECT_2 semantic presentation
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 ) )
proof
let s, t be Real_Sequence; ::_thesis: 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 ) )
let g be real number ; ::_thesis: ( ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) implies ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) ) )
assume A1: for n being Element of NAT holds t . n = abs ((s . n) - g) ; ::_thesis: ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )
hereby ::_thesis: ( t is convergent & lim t = 0 implies ( s is convergent & lim s = g ) )
assume A2: ( s is convergent & lim s = g ) ; ::_thesis: ( t is convergent & lim t = 0 )
A3: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((t_._m)_-_0)_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r by A2, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((t_._m)_-_0)_<_r
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((t . m) - 0) < r )
assume n <= m ; ::_thesis: abs ((t . m) - 0) < r
then abs (abs ((s . m) - g)) < r by A4;
hence abs ((t . m) - 0) < r by A1; ::_thesis: verum
end;
hence for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r ; ::_thesis: verum
end;
hence t is convergent by SEQ_2:def_6; ::_thesis: lim t = 0
hence lim t = 0 by A3, SEQ_2:def_7; ::_thesis: verum
end;
assume A5: ( t is convergent & lim t = 0 ) ; ::_thesis: ( s is convergent & lim s = g )
A6: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((s_._m)_-_g)_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r
then consider n being Element of NAT such that
A7: for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r by A5, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((s_._m)_-_g)_<_r
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s . m) - g) < r )
assume n <= m ; ::_thesis: abs ((s . m) - g) < r
then abs ((t . m) - 0) < r by A7;
then abs (abs ((s . m) - g)) < r by A1;
hence abs ((s . m) - g) < r ; ::_thesis: verum
end;
hence for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r ; ::_thesis: verum
end;
hence s is convergent by SEQ_2:def_6; ::_thesis: lim s = g
hence lim s = g by A6, SEQ_2:def_7; ::_thesis: verum
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
let x, y be FinSequence of REAL ; ::_thesis: ( len x = len y & ( for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i & x . i <= y . i ) ) implies |.x.| <= |.y.| )
assume that
A1: len x = len y and
A2: for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i & x . i <= y . i ) ; ::_thesis: |.x.| <= |.y.|
A3: for i being Nat st i in Seg (len x) holds
(sqr x) . i <= (sqr y) . i
proof
let i be Nat; ::_thesis: ( i in Seg (len x) implies (sqr x) . i <= (sqr y) . i )
assume i in Seg (len x) ; ::_thesis: (sqr x) . i <= (sqr y) . i
then A4: ( 0 <= x . i & x . i <= y . i ) by A2;
( (x . i) ^2 = (sqr x) . i & (y . i) ^2 = (sqr y) . i ) by VALUED_1:11;
hence (sqr x) . i <= (sqr y) . i by A4, SQUARE_1:15; ::_thesis: verum
end;
( Seg (len (sqr y)) = dom (sqr y) & dom (sqr y) = dom y ) by FINSEQ_1:def_3, VALUED_1:11;
then A5: len (sqr y) = len y by FINSEQ_1:def_3;
( Seg (len (sqr x)) = dom (sqr x) & dom (sqr x) = dom x ) by FINSEQ_1:def_3, VALUED_1:11;
then A6: len (sqr x) = len x by FINSEQ_1:def_3;
A7: 0 <= Sum (sqr x) by RVSUM_1:86;
( sqr x is Element of (len (sqr x)) -tuples_on REAL & sqr y is Element of (len (sqr y)) -tuples_on REAL ) by FINSEQ_2:92;
hence |.x.| <= |.y.| by A1, A3, A6, A5, A7, RVSUM_1:82, SQUARE_1:26; ::_thesis: verum
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
let F be FinSequence of REAL ; ::_thesis: ( ( for i being Element of NAT st i in dom F holds
F . i = 0 ) implies Sum F = 0 )
set i = len F;
set R1 = (len F) |-> 0;
reconsider R2 = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: Seg (len F) = dom F by FINSEQ_1:def_3;
assume A2: for i being Element of NAT st i in dom F holds
0 = F . i ; ::_thesis: Sum F = 0
A3: for j being Nat st j in Seg (len F) holds
((len F) |-> 0) . j = R2 . j by A2, A1;
len ((len F) |-> 0) = len F by CARD_1:def_7;
then dom ((len F) |-> 0) = dom R2 by FINSEQ_3:29;
then (len F) |-> 0 = R2 by A1, A3, FINSEQ_1:13;
hence Sum F = 0 by RVSUM_1:81; ::_thesis: verum
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
deffunc H1( set ) -> Element of bool [:[:X,(f . $1):],(f . $1):] = pr2 (X,(f . $1));
consider g being Function such that
A1: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
take g ; ::_thesis: ( dom g = dom f & ( for i being set st i in dom f holds
g . i is Function of [:X,(f . i):],(f . i) ) )
thus dom g = dom f by A1; ::_thesis: for i being set st i in dom f holds
g . i is Function of [:X,(f . i):],(f . i)
let i be set ; ::_thesis: ( i in dom f implies g . i is Function of [:X,(f . i):],(f . i) )
assume i in dom f ; ::_thesis: g . i is Function of [:X,(f . i):],(f . i)
then g . i = pr2 (X,(f . i)) by A1;
hence g . i is Function of [:X,(f . i):],(f . i) ; ::_thesis: verum
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
let f be MultOps of X,F; ::_thesis: f is FinSequence-like
( dom F = dom f & dom F = Seg (len F) ) by Def1, FINSEQ_1:def_3;
hence f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
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
let X be set ; ::_thesis: 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) ) ) )
let F be Domain-Sequence; ::_thesis: 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) ) ) )
let p be FinSequence; ::_thesis: ( 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) ) ) )
( dom p = dom F iff len p = len F ) by FINSEQ_3:29;
hence ( 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) ) ) ) by Def1; ::_thesis: verum
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 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
proof
let X be non empty set ; ::_thesis: 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
let F be Domain-Sequence; ::_thesis: 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
let f, g be Function of [:X,(product F):],(product F); ::_thesis: ( ( 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 ) implies f = g )
assume A1: 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 ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_X
for_d_being_Element_of_product_F_holds_f_._(x,d)_=_g_._(x,d)
let x be Element of X; ::_thesis: for d being Element of product F holds f . (x,d) = g . (x,d)
let d be Element of product F; ::_thesis: f . (x,d) = g . (x,d)
A2: ( dom (f . (x,d)) = dom F & dom (g . (x,d)) = dom F ) by CARD_3:9;
for v being set st v in dom F holds
(f . (x,d)) . v = (g . (x,d)) . v by A1;
hence f . (x,d) = g . (x,d) by A2, FUNCT_1:2; ::_thesis: verum
end;
hence f = g by BINOP_1:2; ::_thesis: verum
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
defpred S1[ Element of X, Element of product F, Element of product F] means for i being Element of dom F holds $3 . i = (p . i) . ($1,($2 . i));
A1: for x being Element of X
for d being Element of product F ex z being Element of product F st S1[x,d,z]
proof
let x be Element of X; ::_thesis: for d being Element of product F ex z being Element of product F st S1[x,d,z]
let d be Element of product F; ::_thesis: ex z being Element of product F st S1[x,d,z]
defpred S2[ set , set ] means ex i being Element of dom F st
( $1 = i & $2 = (p . i) . (x,(d . i)) );
A2: for w being set st w in dom F holds
ex z being set st S2[w,z]
proof
let w be set ; ::_thesis: ( w in dom F implies ex z being set st S2[w,z] )
assume w in dom F ; ::_thesis: ex z being set st S2[w,z]
then reconsider i = w as Element of dom F ;
take (p . i) . (x,(d . i)) ; ::_thesis: S2[w,(p . i) . (x,(d . i))]
thus S2[w,(p . i) . (x,(d . i))] ; ::_thesis: verum
end;
consider z being Function such that
A3: ( dom z = dom F & ( for w being set st w in dom F holds
S2[w,z . w] ) ) from CLASSES1:sch_1(A2);
now__::_thesis:_for_w_being_set_st_w_in_dom_F_holds_
z_._w_in_F_._w
let w be set ; ::_thesis: ( w in dom F implies z . w in F . w )
assume w in dom F ; ::_thesis: z . w in F . w
then ex i being Element of dom F st
( w = i & z . w = (p . i) . (x,(d . i)) ) by A3;
hence z . w in F . w ; ::_thesis: verum
end;
then reconsider z9 = z as Element of product F by A3, CARD_3:9;
take z9 ; ::_thesis: S1[x,d,z9]
let i be Element of dom F; ::_thesis: z9 . i = (p . i) . (x,(d . i))
ex j being Element of dom F st
( j = i & z . i = (p . j) . (x,(d . j)) ) by A3;
hence z9 . i = (p . i) . (x,(d . i)) ; ::_thesis: verum
end;
thus ex P being Function of [:X,(product F):],(product F) st
for x being Element of X
for d being Element of product F holds S1[x,d,P . (x,d)] from BINOP_1:sch_3(A1); ::_thesis: verum
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
let P, Q be Function of [:X,(product F):],(product F); ::_thesis: ( ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (P . (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 (Q . (x,d)) . i = (p . i) . (x,(d . i)) ) implies P = Q )
assume that
A4: for x being Element of X
for f being Element of product F
for i being Element of dom F holds (P . (x,f)) . i = (p . i) . (x,(f . i)) and
A5: for x being Element of X
for f being Element of product F
for i being Element of dom F holds (Q . (x,f)) . i = (p . i) . (x,(f . i)) ; ::_thesis: P = Q
now__::_thesis:_for_x_being_Element_of_X
for_f_being_Element_of_product_F
for_i_being_Element_of_dom_F_holds_(P_._(x,f))_._i_=_(Q_._(x,f))_._i
let x be Element of X; ::_thesis: for f being Element of product F
for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . i
let f be Element of product F; ::_thesis: for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . i
let i be Element of dom F; ::_thesis: (P . (x,f)) . i = (Q . (x,f)) . i
(P . (x,f)) . i = (p . i) . (x,(f . i)) by A4;
hence (P . (x,f)) . i = (Q . (x,f)) . i by A5; ::_thesis: verum
end;
hence P = Q by Th5; ::_thesis: verum
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;
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 & b1 is RealLinearSpace-yielding )
proof
set S = the RealLinearSpace;
take <* the RealLinearSpace*> ; ::_thesis: ( not <* the RealLinearSpace*> is empty & <* the RealLinearSpace*> is RealLinearSpace-yielding )
thus not <* the RealLinearSpace*> is empty ; ::_thesis: <* the RealLinearSpace*> is RealLinearSpace-yielding
let x be set ; :: according to PRVECT_2:def_3 ::_thesis: ( x in rng <* the RealLinearSpace*> implies x is RealLinearSpace )
assume that
A1: x in rng <* the RealLinearSpace*> and
A2: x is not RealLinearSpace ; ::_thesis: contradiction
x in { the RealLinearSpace} by A1, FINSEQ_1:38;
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
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 funcG . j -> RealLinearSpace;
coherence
G . j is RealLinearSpace
proof
G . j in rng G by FUNCT_1:def_3;
hence G . j is RealLinearSpace by Def3; ::_thesis: verum
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
defpred S1[ set , set ] means ex j9 being Element of dom G st
( j9 = $1 & $2 = the carrier of (G . j9) );
A1: for j being Nat st j in Seg (len G) holds
ex x being set st S1[j,x]
proof
let j be Nat; ::_thesis: ( j in Seg (len G) implies ex x being set st S1[j,x] )
assume j in Seg (len G) ; ::_thesis: ex x being set st S1[j,x]
then reconsider j9 = j as Element of dom G by FINSEQ_1:def_3;
take the carrier of (G . j9) ; ::_thesis: S1[j, the carrier of (G . j9)]
thus S1[j, the carrier of (G . j9)] ; ::_thesis: verum
end;
consider p being FinSequence such that
A2: ( dom p = Seg (len G) & ( for j being Nat st j in Seg (len G) holds
S1[j,p . j] ) ) from FINSEQ_1:sch_1(A1);
now__::_thesis:_not_{}_in_rng_p
assume {} in rng p ; ::_thesis: contradiction
then consider x being set such that
A3: x in dom p and
A4: {} = p . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3;
ex x9 being Element of dom G st
( x9 = x & p . x = the carrier of (G . x9) ) by A2, A3;
hence contradiction by A4; ::_thesis: verum
end;
then reconsider q = p as Domain-Sequence by A2, RELAT_1:def_9;
take q ; ::_thesis: ( len q = len G & ( for j being Element of dom G holds q . j = the carrier of (G . j) ) )
thus len q = len G by A2, FINSEQ_1:def_3; ::_thesis: for j being Element of dom G holds q . j = the carrier of (G . j)
let j be Element of dom G; ::_thesis: q . j = the carrier of (G . j)
reconsider k = j as Element of NAT ;
dom G = Seg (len G) by FINSEQ_1:def_3;
then ex n being Element of dom G st
( n = k & q . k = the carrier of (G . n) ) by A2;
hence q . j = the carrier of (G . j) ; ::_thesis: verum
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
let f, h be Domain-Sequence; ::_thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the carrier of (G . j) ) & len h = len G & ( for j being Element of dom G holds h . j = the carrier of (G . j) ) implies f = h )
assume that
A5: len f = len G and
A6: for j being Element of dom G holds f . j = the carrier of (G . j) and
A7: len h = len G and
A8: for j being Element of dom G holds h . j = the carrier of (G . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_f9_holds_
f9_._j_=_h9_._j
let j be Nat; ::_thesis: ( j in dom f9 implies f9 . j = h9 . j )
assume j in dom f9 ; ::_thesis: f9 . j = h9 . j
then reconsider j9 = j as Element of dom G by A5, FINSEQ_3:29;
f9 . j = the carrier of (G . j9) by A6;
hence f9 . j = h9 . j by A8; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A5, A7, A9, FINSEQ_1:13; ::_thesis: verum
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 funcG . j -> RealLinearSpace;
coherence
G . j is RealLinearSpace
proof
( dom G = Seg (len G) & Seg (len (carr G)) = dom (carr G) ) by FINSEQ_1:def_3;
then reconsider j9 = j as Element of dom G by Def4;
G . j9 is RealLinearSpace ;
hence G . j is RealLinearSpace ; ::_thesis: verum
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
deffunc H1( Element of dom (carr G)) -> Element of bool [:[: the carrier of (G . $1), the carrier of (G . $1):], the carrier of (G . $1):] = the addF of (G . $1);
consider p being non empty FinSequence such that
A1: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_j_being_Element_of_dom_(carr_G)_holds_p_._j_is_BinOp_of_((carr_G)_._j)
let j be Element of dom (carr G); ::_thesis: p . j is BinOp of ((carr G) . j)
len G = len (carr G) by Def4;
then reconsider k = j as Element of dom G by FINSEQ_3:29;
( p . j = the addF of (G . j) & the carrier of (G . k) = (carr G) . k ) by A1, Def4;
hence p . j is BinOp of ((carr G) . j) ; ::_thesis: verum
end;
then reconsider p9 = p as BinOps of carr G by A1, PRVECT_1:11;
take p9 ; ::_thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the addF of (G . j) ) )
thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the addF of (G . j) ) ) by A1; ::_thesis: verum
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
let f, h be BinOps of carr G; ::_thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = the addF of (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = the addF of (G . j) ) implies f = h )
assume that
A2: len f = len (carr G) and
A3: for j being Element of dom (carr G) holds f . j = the addF of (G . j) and
A4: len h = len (carr G) and
A5: for j being Element of dom (carr G) holds h . j = the addF of (G . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f9_._i_=_h9_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f9 . i = h9 . i )
assume i in dom f9 ; ::_thesis: f9 . i = h9 . i
then reconsider i9 = i as Element of dom (carr G) by A2, FINSEQ_3:29;
f9 . i = the addF of (G . i9) by A3;
hence f9 . i = h9 . i by A5; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A2, A4, A6, FINSEQ_1:13; ::_thesis: verum
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
deffunc H1( Element of dom (carr G)) -> Element of bool [: the carrier of (G . $1), the carrier of (G . $1):] = comp (G . $1);
consider p being non empty FinSequence such that
A7: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_j_being_Element_of_dom_(carr_G)_holds_p_._j_is_UnOp_of_((carr_G)_._j)
let j be Element of dom (carr G); ::_thesis: p . j is UnOp of ((carr G) . j)
len G = len (carr G) by Def4;
then reconsider k = j as Element of dom G by FINSEQ_3:29;
( p . j = comp (G . j) & the carrier of (G . k) = (carr G) . k ) by A7, Def4;
hence p . j is UnOp of ((carr G) . j) ; ::_thesis: verum
end;
then reconsider p9 = p as UnOps of carr G by A7, PRVECT_1:12;
take p9 ; ::_thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) )
thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) ) by A7; ::_thesis: verum
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
let f, h be UnOps of carr G; ::_thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = comp (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = comp (G . j) ) implies f = h )
assume that
A8: len f = len (carr G) and
A9: for j being Element of dom (carr G) holds f . j = comp (G . j) and
A10: len h = len (carr G) and
A11: for j being Element of dom (carr G) holds h . j = comp (G . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f_._i_=_h_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f . i = h . i )
assume i in dom f9 ; ::_thesis: f . i = h . i
then reconsider i9 = i as Element of dom (carr G) by A8, FINSEQ_3:29;
f . i = comp (G . i9) by A9;
hence f . i = h . i by A11; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A8, A10, A12, FINSEQ_1:13; ::_thesis: verum
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
deffunc H1( Element of dom (carr G)) -> Element of the carrier of (G . $1) = the ZeroF of (G . $1);
consider p being non empty FinSequence such that
A13: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1();
A14: dom (carr G) = Seg (len (carr G)) by FINSEQ_1:def_3;
A15: dom G = Seg (len G) by FINSEQ_1:def_3;
A16: now__::_thesis:_for_i_being_set_st_i_in_dom_(carr_G)_holds_
p_._i_in_(carr_G)_._i
let i be set ; ::_thesis: ( i in dom (carr G) implies p . i in (carr G) . i )
assume i in dom (carr G) ; ::_thesis: p . i in (carr G) . i
then reconsider x = i as Element of dom (carr G) ;
reconsider x9 = x as Element of dom G by A15, A14, Def4;
( p . x = the ZeroF of (G . x) & (carr G) . x9 = the carrier of (G . x9) ) by A13, Def4;
hence p . i in (carr G) . i ; ::_thesis: verum
end;
dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider t = p as Element of product (carr G) by A13, A14, A16, CARD_3:9;
take t ; ::_thesis: for j being Element of dom (carr G) holds t . j = the ZeroF of (G . j)
thus for j being Element of dom (carr G) holds t . j = the ZeroF of (G . j) by A13; ::_thesis: verum
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
let f, h be Element of product (carr G); ::_thesis: ( ( for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) ) & ( for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ) implies f = h )
assume that
A17: for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) and
A18: for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as Function ;
A19: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_
f9_._x_=_h9_._x
let x be set ; ::_thesis: ( x in dom (carr G) implies f9 . x = h9 . x )
assume x in dom (carr G) ; ::_thesis: f9 . x = h9 . x
then reconsider i = x as Element of dom (carr G) ;
thus f9 . x = the ZeroF of (G . i) by A17
.= h9 . x by A18 ; ::_thesis: verum
end;
( dom f9 = dom (carr G) & dom h9 = dom (carr G) ) by CARD_3:9;
hence f = h by A19, FUNCT_1:2; ::_thesis: verum
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
deffunc H1( Element of dom (carr G)) -> Element of bool [:[:REAL, the carrier of (G . $1):], the carrier of (G . $1):] = the Mult of (G . $1);
consider p being non empty FinSequence such that
A20: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_ai_being_set_st_ai_in_dom_(carr_G)_holds_
p_._ai_is_Function_of_[:REAL,((carr_G)_._ai):],((carr_G)_._ai)
let ai be set ; ::_thesis: ( ai in dom (carr G) implies p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) )
assume ai in dom (carr G) ; ::_thesis: p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai)
then reconsider i = ai as Element of dom (carr G) ;
len G = len (carr G) by Def4;
then reconsider j = i as Element of dom G by FINSEQ_3:29;
( p . i = the Mult of (G . i) & the carrier of (G . j) = (carr G) . j ) by A20, Def4;
hence p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) ; ::_thesis: verum
end;
then reconsider p9 = p as MultOps of REAL , carr G by A20, Th4;
take p9 ; ::_thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the Mult of (G . j) ) )
thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the Mult of (G . j) ) ) by A20; ::_thesis: verum
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
let f, h be MultOps of REAL , carr G; ::_thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = the Mult of (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ) implies f = h )
assume that
A21: len f = len (carr G) and
A22: for j being Element of dom (carr G) holds f . j = the Mult of (G . j) and
A23: len h = len (carr G) and
A24: for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A25: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f9_._i_=_h9_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f9 . i = h9 . i )
assume i in dom f9 ; ::_thesis: f9 . i = h9 . i
then reconsider i9 = i as Element of dom (carr G) by A21, FINSEQ_3:29;
f9 . i = the Mult of (G . i9) by A22;
hence f9 . i = h9 . i by A24; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A21, A23, A25, FINSEQ_1:13; ::_thesis: verum
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 )
proof
deffunc H1( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
let LS be non empty addLoopStr ; ::_thesis: ( the addF of LS is commutative & the addF of LS is associative implies ( LS is Abelian & LS is add-associative ) )
assume that
A1: H1(LS) is commutative and
A2: H1(LS) is associative ; ::_thesis: ( LS is Abelian & LS is add-associative )
for x, y being Element of LS holds x + y = y + x by A1, BINOP_1:def_2;
hence LS is Abelian by RLVECT_1:def_2; ::_thesis: LS is add-associative
for x, y, z being Element of LS holds (x + y) + z = x + (y + z) by A2, BINOP_1:def_3;
hence LS is add-associative by RLVECT_1:def_3; ::_thesis: verum
end;
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
proof
let LS be non empty addLoopStr ; ::_thesis: ( the ZeroF of LS is_a_unity_wrt the addF of LS implies LS is right_zeroed )
assume A1: the ZeroF of LS is_a_unity_wrt the addF of LS ; ::_thesis: LS is right_zeroed
let x be Element of LS; :: according to RLVECT_1:def_4 ::_thesis: x + (0. LS) = x
thus x + (0. LS) = x by A1, BINOP_1:3; ::_thesis: verum
end;
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
let G be RealLinearSpace-Sequence; ::_thesis: 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 ) )
let v1, w1 be Element of product (carr G); ::_thesis: 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 ) )
let i be Element of dom (carr G); ::_thesis: ( ([:(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 ) )
([:(addop G):] . (v1,w1)) . i = ((addop G) . i) . ((v1 . i),(w1 . i)) by PRVECT_1:def_8;
hence ( ([:(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 ) ) by Def5; ::_thesis: verum
end;
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)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:(multop G):] . (r,v)) . i = r * vi ) )
proof
let G be RealLinearSpace-Sequence; ::_thesis: 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)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:(multop G):] . (r,v)) . i = r * vi ) )
let r be Real; ::_thesis: 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 ) )
let v be Element of product (carr G); ::_thesis: 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 ) )
let i be Element of dom (carr G); ::_thesis: ( ([:(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 ) )
([:(multop G):] . (r,v)) . i = ((multop G) . i) . (r,(v . i)) by Def2;
hence ( ([:(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 ) ) by Def8; ::_thesis: verum
end;
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
deffunc H1( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
let G be RealLinearSpace-Sequence; ::_thesis: ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ;
dom G = Seg (len G) by FINSEQ_1:def_3;
then dom G = Seg (len (carr G)) by Def4;
then A1: dom G = dom (carr G) by FINSEQ_1:def_3;
now__::_thesis:_for_a1,_b1_being_real_number_
for_v,_w_being_VECTOR_of_GS_holds_
(_a1_*_(v_+_w)_=_(a1_*_v)_+_(a1_*_w)_&_(a1_+_b1)_*_v_=_(a1_*_v)_+_(b1_*_v)_&_(a1_*_b1)_*_v_=_a1_*_(b1_*_v)_&_1_*_v_=_v_)
let a1, b1 be real number ; ::_thesis: for v, w being VECTOR of GS holds
( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
reconsider a = a1, b = b1 as Real by XREAL_0:def_1;
let v, w be VECTOR of GS; ::_thesis: ( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
reconsider v1 = v, w1 = w as Element of product (carr G) ;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_
([:(multop_G):]_._(1,v1))_._x_=_v1_._x
let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . (1,v1)) . x = v1 . x )
assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . (1,v1)) . x = v1 . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . (1,v1)) . x = 1 * vi by Lm4;
hence ([:(multop G):] . (1,v1)) . x = v1 . x by RLVECT_1:def_8; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_
([:(multop_G):]_._((a_+_b),v1))_._x_=_([:(addop_G):]_._(([:(multop_G):]_._(a,v1)),([:(multop_G):]_._(b,v1))))_._x
let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x )
assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . ((a + b),v1)) . i = (a + b) * vi by Lm4
.= (a * vi) + (b * vi) by RLVECT_1:def_6
.= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(b * vi)) by Lm4
.= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(([:(multop G):] . (b,v1)) . i)) by Lm4 ;
hence ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x by Lm3; ::_thesis: verum
end;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_
([:(multop_G):]_._(a,([:(addop_G):]_._(v1,w1))))_._x_=_([:(addop_G):]_._(([:(multop_G):]_._(a,v1)),([:(multop_G):]_._(a,w1))))_._x
let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x )
assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i, wi = w1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . i = the Mult of (G . i) . (a,(([:(addop G):] . (v1,w1)) . i)) by Lm4
.= a * (vi + wi) by Lm3
.= (a * vi) + (a * wi) by RLVECT_1:def_5
.= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(a * wi)) by Lm4
.= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(([:(multop G):] . (a,w1)) . i)) by Lm4 ;
hence ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x by Lm3; ::_thesis: verum
end;
( dom ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) = dom (carr G) & dom ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) = dom (carr G) ) by CARD_3:9;
hence a1 * (v + w) = (a1 * v) + (a1 * w) by A4, FUNCT_1:2; ::_thesis: ( (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
A5: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_
([:(multop_G):]_._((a_*_b),v1))_._x_=_([:(multop_G):]_._(a,([:(multop_G):]_._(b,v1))))_._x
let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x )
assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . ((a * b),v1)) . i = (a * b) * vi by Lm4
.= a * (b * vi) by RLVECT_1:def_7
.= the Mult of (G . i) . (a,(([:(multop G):] . (b,v1)) . i)) by Lm4 ;
hence ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x by Lm4; ::_thesis: verum
end;
( dom ([:(multop G):] . ((a + b),v1)) = dom (carr G) & dom ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) = dom (carr G) ) by CARD_3:9;
hence (a1 + b1) * v = (a1 * v) + (b1 * v) by A3, FUNCT_1:2; ::_thesis: ( (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
( dom ([:(multop G):] . ((a * b),v1)) = dom (carr G) & dom ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) = dom (carr G) ) by CARD_3:9;
hence (a1 * b1) * v = a1 * (b1 * v) by A5, FUNCT_1:2; ::_thesis: 1 * v = v
( dom ([:(multop G):] . (1,v1)) = dom (carr G) & dom v1 = dom (carr G) ) by CARD_3:9;
hence 1 * v = v by A2, FUNCT_1:2; ::_thesis: verum
end;
hence ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) by RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum
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
deffunc H1( addLoopStr ) -> Element of the carrier of G = the ZeroF of G;
reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ;
deffunc H2( 1-sorted ) -> set = the carrier of G;
deffunc H3( addLoopStr ) -> Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:] = the addF of G;
A1: now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(carr_G)_._i_=_H2(G_._i)
let i be Element of dom (carr G); ::_thesis: (carr G) . i = H2(G . i)
dom G = Seg (len G) by FINSEQ_1:def_3
.= Seg (len (carr G)) by Def4
.= dom (carr G) by FINSEQ_1:def_3 ;
hence (carr G) . i = H2(G . i) by Def4; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_associative
let i be Element of dom (carr G); ::_thesis: (addop G) . i is associative
( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by A1, Def5;
hence (addop G) . i is associative by FVSUM_1:2; ::_thesis: verum
end;
then A2: [:(addop G):] is associative by PRVECT_1:18;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(zeros_G)_._i_is_a_unity_wrt_(addop_G)_._i
let i be Element of dom (carr G); ::_thesis: (zeros G) . i is_a_unity_wrt (addop G) . i
A3: (zeros G) . i = 0. (G . i) by Def7;
( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by A1, Def5;
hence (zeros G) . i is_a_unity_wrt (addop G) . i by A3, PRVECT_1:1; ::_thesis: verum
end;
then A4: zeros G is_a_unity_wrt [:(addop G):] by PRVECT_1:19;
A5: GS is right_complementable
proof
let x be Element of GS; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider y = (Frege (complop G)) . x as Element of GS by FUNCT_2:5;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. GS
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_
(_(complop_G)_._i_is_an_inverseOp_wrt_(addop_G)_._i_&_(addop_G)_._i_is_having_a_unity_)
let i be Element of dom (carr G); ::_thesis: ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity )
0. (G . i) = H1(G . i) ;
then A6: H1(G . i) is_a_unity_wrt H3(G . i) by PRVECT_1:1;
A7: (complop G) . i = comp (G . i) by Def6;
( (carr G) . i = H2(G . i) & (addop G) . i = H3(G . i) ) by A1, Def5;
hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, A7, PRVECT_1:2, SETWISEO:def_2; ::_thesis: verum
end;
then Frege (complop G) is_an_inverseOp_wrt [:(addop G):] by PRVECT_1:20;
then [:(addop G):] . (x,y) = the_unity_wrt [:(addop G):] by FINSEQOP:def_1;
hence x + y = 0. GS by A4, BINOP_1:def_8; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_commutative
let i be Element of dom (carr G); ::_thesis: (addop G) . i is commutative
( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by A1, Def5;
hence (addop G) . i is commutative by FVSUM_1:1; ::_thesis: verum
end;
then [:(addop G):] is commutative by PRVECT_1:17;
hence ( 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 ) by A2, A4, A5, Lm1, Lm2, Lm5; ::_thesis: verum
end;
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 & b1 is RealNormSpace-yielding )
proof
set A = the RealNormSpace;
take <* the RealNormSpace*> ; ::_thesis: ( not <* the RealNormSpace*> is empty & <* the RealNormSpace*> is RealNormSpace-yielding )
thus not <* the RealNormSpace*> is empty ; ::_thesis: <* the RealNormSpace*> is RealNormSpace-yielding
let x be set ; :: according to PRVECT_2:def_10 ::_thesis: ( x in rng <* the RealNormSpace*> implies x is RealNormSpace )
assume that
A1: x in rng <* the RealNormSpace*> and
A2: x is not RealNormSpace ; ::_thesis: contradiction
x in { the RealNormSpace} by A1, FINSEQ_1:38;
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
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 funcG . j -> RealNormSpace;
coherence
G . j is RealNormSpace
proof
G . j in rng G by FUNCT_1:def_3;
hence G . j is RealNormSpace by Def10; ::_thesis: verum
end;
end;
Lm6: for g being RealNormSpace-yielding FinSequence holds g is RealLinearSpace-yielding
proof
let g be RealNormSpace-yielding FinSequence; ::_thesis: g is RealLinearSpace-yielding
for x being set st x in rng g holds
x is RealLinearSpace by Def10;
hence g is RealLinearSpace-yielding by Def3; ::_thesis: verum
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 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 & ( 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
deffunc H1( Element of dom G) -> Element of REAL = the normF of (G . $1) . (x . $1);
consider f being Function of (dom G),REAL such that
A1: for j being Element of dom G holds f . j = H1(j) from FUNCT_2:sch_4();
A2: rng f c= REAL ;
dom f = dom G by FUNCT_2:def_1;
then A3: dom f = Seg (len G) by FINSEQ_1:def_3;
then f is FinSequence by FINSEQ_1:def_2;
then reconsider f = f as FinSequence of REAL by A2, FINSEQ_1:def_4;
A4: f in REAL * by FINSEQ_1:def_11;
len f = len G by A3, FINSEQ_1:def_3;
then f in (len G) -tuples_on REAL by A4;
then reconsider f = f as Element of REAL (len G) ;
take f ; ::_thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) ) )
thus len f = len G by CARD_1:def_7; ::_thesis: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j)
let j be Element of dom G; ::_thesis: f . j = the normF of (G . j) . (x . j)
thus f . j = the normF of (G . j) . (x . j) by A1; ::_thesis: verum
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
let f, g be Element of REAL (len G); ::_thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) ) & len g = len G & ( for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ) implies f = g )
assume that
len f = len G and
A5: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) and
len g = len G and
A6: for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ; ::_thesis: f = g
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(len_G)_holds_
f_._j_=_g_._j
let j be Nat; ::_thesis: ( j in Seg (len G) implies f . j = g . j )
assume j in Seg (len G) ; ::_thesis: f . j = g . j
then reconsider j1 = j as Element of dom G by FINSEQ_1:def_3;
f . j = the normF of (G . j1) . (x . j1) by A5;
hence f . j = g . j by A6; ::_thesis: verum
end;
hence f = g by FINSEQ_2:119; ::_thesis: verum
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
deffunc H1( Element of product (carr G)) -> Element of REAL = |.(normsequence (G,$1)).|;
consider f being Function of (product (carr G)),REAL such that
A1: for x being Element of product (carr G) holds f . x = H1(x) from FUNCT_2:sch_4();
take f ; ::_thesis: for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).|
let x be Element of product (carr G); ::_thesis: f . x = |.(normsequence (G,x)).|
thus f . x = |.(normsequence (G,x)).| by A1; ::_thesis: verum
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
let f, g be Function of (product (carr G)),REAL; ::_thesis: ( ( for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).| ) & ( for x being Element of product (carr G) holds g . x = |.(normsequence (G,x)).| ) implies f = g )
assume that
A2: for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).| and
A3: for x being Element of product (carr G) holds g . x = |.(normsequence (G,x)).| ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_product_(carr_G)_holds_f_._x_=_g_._x
let x be Element of product (carr G); ::_thesis: f . x = g . x
f . x = |.(normsequence (G,x)).| by A2;
hence f . x = g . x by A3; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
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
reconsider G0 = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) as non empty strict NORMSTR ;
take G0 ; ::_thesis: ( RLSStruct(# the carrier of G0, the ZeroF of G0, the addF of G0, the Mult of G0 #) = product G & the normF of G0 = productnorm G )
thus ( RLSStruct(# the carrier of G0, the ZeroF of G0, the addF of G0, the Mult of G0 #) = product G & the normF of G0 = productnorm G ) ; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #)
RLSStruct(# the carrier of (product G), the ZeroF of (product G), the addF of (product G), the Mult of (product G) #) = product G by Def13;
hence product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Def13; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: for x being VECTOR of (product G)
for y being Element of product (carr G) st x = y holds
||.x.|| = |.(normsequence (G,y)).|
let x be VECTOR of (product G); ::_thesis: for y being Element of product (carr G) st x = y holds
||.x.|| = |.(normsequence (G,y)).|
let y be Element of product (carr G); ::_thesis: ( x = y implies ||.x.|| = |.(normsequence (G,y)).| )
assume A1: x = y ; ::_thesis: ||.x.|| = |.(normsequence (G,y)).|
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
hence ||.x.|| = |.(normsequence (G,y)).| by A1, Def12; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: 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
let x, y, z be Element of product (carr G); ::_thesis: 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
let i be Element of NAT ; ::_thesis: ( i in dom x & z = [:(addop G):] . (x,y) implies (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i )
assume that
A1: i in dom x and
A2: z = [:(addop G):] . (x,y) ; ::_thesis: (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i
reconsider i0 = i as Element of dom (carr G) by A1, CARD_3:9;
A3: z . i0 = ((addop G) . i0) . ((x . i0),(y . i0)) by A2, PRVECT_1:def_8;
dom G = Seg (len G) by FINSEQ_1:def_3
.= Seg (len (carr G)) by Def4
.= dom (carr G) by FINSEQ_1:def_3 ;
then reconsider i0 = i as Element of dom G by A1, CARD_3:9;
( dom x = dom (carr G) & (carr G) . i0 = the carrier of (G . i0) ) by Def4, CARD_3:9;
then reconsider xi0 = x . i0, yi0 = y . i0, zi0 = z . i0 as Element of (G . i0) by A1, CARD_3:9;
||.zi0.|| = ||.(xi0 + yi0).|| by A3, Def5;
then A4: ||.zi0.|| <= ||.xi0.|| + ||.yi0.|| by NORMSP_1:def_1;
A5: ((normsequence (G,x)) . i0) + ((normsequence (G,y)) . i0) = ((normsequence (G,x)) + (normsequence (G,y))) . i0 by RVSUM_1:11;
( the normF of (G . i0) . yi0 = (normsequence (G,y)) . i0 & the normF of (G . i0) . zi0 = (normsequence (G,z)) . i0 ) by Def11;
hence (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i by A4, A5, Def11; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: 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
let x be Element of product (carr G); ::_thesis: for i being Element of NAT st i in dom x holds
0 <= (normsequence (G,x)) . i
let i be Element of NAT ; ::_thesis: ( i in dom x implies 0 <= (normsequence (G,x)) . i )
assume A1: i in dom x ; ::_thesis: 0 <= (normsequence (G,x)) . i
dom G = Seg (len G) by FINSEQ_1:def_3
.= Seg (len (carr G)) by Def4
.= dom (carr G) by FINSEQ_1:def_3 ;
then reconsider i0 = i as Element of dom G by A1, CARD_3:9;
( dom x = dom (carr G) & (carr G) . i0 = the carrier of (G . i0) ) by Def4, CARD_3:9;
then reconsider xi0 = x . i0 as Element of (G . i0) by A1, CARD_3:9;
0 <= ||.xi0.|| by NORMSP_1:4;
hence 0 <= (normsequence (G,x)) . i by Def11; ::_thesis: verum
end;
Lm7: for G being RealNormSpace-Sequence holds
( product G is reflexive & product G is discerning & product G is RealNormSpace-like )
proof
let G be RealNormSpace-Sequence; ::_thesis: ( product G is reflexive & product G is discerning & product G is RealNormSpace-like )
A1: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
A2: len G = len (carr G) by Def4;
reconsider n = len G as Element of NAT ;
thus product G is reflexive ::_thesis: ( product G is discerning & product G is RealNormSpace-like )
proof
reconsider z = 0. (product G) as Element of product (carr G) by A1;
A3: for i being Element of dom (carr G) holds (normsequence (G,z)) . i = 0
proof
let i be Element of dom (carr G); ::_thesis: (normsequence (G,z)) . i = 0
reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29;
(carr G) . i0 = the carrier of (G . i0) by Def4;
then reconsider zi0 = z . i0 as Element of (G . i0) by CARD_3:9;
z . i = 0. (G . i) by A1, Def7;
then ||.zi0.|| = 0 ;
hence (normsequence (G,z)) . i = 0 by Def11; ::_thesis: verum
end;
for i being Element of NAT st i in dom (sqr (normsequence (G,z))) holds
(sqr (normsequence (G,z))) . i = 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom (sqr (normsequence (G,z))) implies (sqr (normsequence (G,z))) . i = 0 )
assume A4: i in dom (sqr (normsequence (G,z))) ; ::_thesis: (sqr (normsequence (G,z))) . i = 0
len (normsequence (G,z)) = len G by Def11;
then A5: dom (normsequence (G,z)) = dom G by FINSEQ_3:29;
dom (carr G) = dom G by A2, FINSEQ_3:29;
then dom (sqr (normsequence (G,z))) = dom (carr G) by A5, VALUED_1:11;
then ((normsequence (G,z)) . i) ^2 = 0 ^2 by A3, A4;
hence (sqr (normsequence (G,z))) . i = 0 by VALUED_1:11; ::_thesis: verum
end;
then |.(normsequence (G,z)).| = 0 by Th3, SQUARE_1:17;
hence ||.(0. (product G)).|| = 0 by Th7; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
thus product G is discerning ::_thesis: product G is RealNormSpace-like
proof
let x be Point of (product G); :: according to NORMSP_0:def_5 ::_thesis: ( not ||.x.|| = 0 or x = 0. (product G) )
reconsider z = x as Element of product (carr G) by A1;
assume A6: ||.x.|| = 0 ; ::_thesis: x = 0. (product G)
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_z_._i_=_the_ZeroF_of_(G_._i)
let i be Element of dom (carr G); ::_thesis: z . i = the ZeroF of (G . i)
reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29;
(carr G) . i0 = the carrier of (G . i0) by Def4;
then reconsider zzi0 = z . i0 as Element of (G . i0) by CARD_3:9;
||.x.|| = |.(normsequence (G,z)).| by Th7;
then normsequence (G,z) = 0* n by A6, EUCLID:8;
then (normsequence (G,z)) . i = 0 ;
then ||.zzi0.|| = 0 by Def11;
then z . i = 0. (G . i) by NORMSP_0:def_5;
hence z . i = the ZeroF of (G . i) ; ::_thesis: verum
end;
hence x = 0. (product G) by A1, Def7; ::_thesis: verum
end;
let x, y be Point of (product G); :: according to NORMSP_1:def_1 ::_thesis: for b1 being Element of REAL holds
( ||.(b1 * x).|| = (abs b1) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider z = x as Element of product (carr G) by A1;
reconsider xx = x, yy = y as Element of product (carr G) by A1;
reconsider ax = a * x as Element of product (carr G) by A1;
A7: ( ||.y.|| = |.(normsequence (G,yy)).| & |.((normsequence (G,xx)) + (normsequence (G,yy))).| <= |.(normsequence (G,xx)).| + |.(normsequence (G,yy)).| ) by Th7, EUCLID:12;
A8: len (normsequence (G,ax)) = n by CARD_1:def_7;
then A9: dom (normsequence (G,ax)) = Seg n by FINSEQ_1:def_3;
A10: for i being Nat st i in dom (normsequence (G,ax)) holds
(normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i
proof
let i be Nat; ::_thesis: ( i in dom (normsequence (G,ax)) implies (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i )
assume i in dom (normsequence (G,ax)) ; ::_thesis: (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i
then reconsider i0 = i as Element of dom G by A9, FINSEQ_1:def_3;
reconsider i1 = i0 as Element of dom (carr G) by A2, FINSEQ_3:29;
( (carr G) . i0 = the carrier of (G . i0) & dom (carr G) = dom G ) by A2, Def4, FINSEQ_3:29;
then reconsider axi0 = ax . i0, zi0 = z . i0 as Element of (G . i0) by CARD_3:9;
([:(multop G):] . (a,z)) . i1 = ((multop G) . i1) . (a,zi0) by Def2;
then axi0 = a * zi0 by A1, Def8;
then ||.axi0.|| = (abs a) * ||.zi0.|| by NORMSP_1:def_1;
then ||.axi0.|| = (abs a) * ((normsequence (G,z)) . i0) by Def11;
then ||.axi0.|| = ((abs a) * (normsequence (G,z))) . i0 by RVSUM_1:44;
hence (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i by Def11; ::_thesis: verum
end;
len ((abs a) * (normsequence (G,z))) = n by CARD_1:def_7;
then |.(normsequence (G,ax)).| = |.((abs a) * (normsequence (G,z))).| by A8, A10, FINSEQ_2:9;
then A11: |.(normsequence (G,ax)).| = (abs (abs a)) * |.(normsequence (G,z)).| by EUCLID:11;
reconsider z = x + y as Element of product (carr G) by A1;
A12: for i being Element of NAT st i in Seg n holds
( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i )
proof
A13: dom xx = dom (carr G) by CARD_3:9;
A14: ( Seg n = dom G & dom (carr G) = dom G ) by A2, FINSEQ_1:def_3, FINSEQ_3:29;
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) )
assume A15: i in Seg n ; ::_thesis: ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i )
i in dom z by A15, A14, CARD_3:9;
hence ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) by A1, A15, A14, A13, Th8, Th9; ::_thesis: verum
end;
A16: len (normsequence (G,z)) = n by Def11;
then len (normsequence (G,z)) = len ((normsequence (G,xx)) + (normsequence (G,yy))) by CARD_1:def_7;
then A17: |.(normsequence (G,z)).| <= |.((normsequence (G,xx)) + (normsequence (G,yy))).| by A16, A12, Th2;
( ||.(x + y).|| = |.(normsequence (G,z)).| & ||.x.|| = |.(normsequence (G,xx)).| ) by Th7;
hence ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by A11, A17, A7, Th7, XXREAL_0:2; ::_thesis: verum
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
reconsider G1 = G as RealLinearSpace-Sequence ;
A1: RLSStruct(# the carrier of (product G), the ZeroF of (product G), the addF of (product G), the Mult of (product G) #) = product G by Def13;
A2: now__::_thesis:_for_v_being_VECTOR_of_(product_G)_holds_1_*_v_=_v
let v be VECTOR of (product G); ::_thesis: 1 * v = v
reconsider v1 = v as VECTOR of (product G1) by A1;
1 * v = 1 * v1 by A1;
hence 1 * v = v by RLVECT_1:def_8; ::_thesis: verum
end;
A3: product G is right_complementable
proof
let v be VECTOR of (product G); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v1 = v as VECTOR of (product G1) by A1;
reconsider w = - v1 as VECTOR of (product G) by A1;
take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (product G)
v + w = v1 - v1 by A1;
then v + w = 0. (product G1) by RLVECT_1:15;
hence v + w = 0. (product G) by A1; ::_thesis: verum
end;
A4: now__::_thesis:_for_a_being_real_number_
for_v,_w_being_VECTOR_of_(product_G)_holds_a_*_(v_+_w)_=_(a_*_v)_+_(a_*_w)
let a be real number ; ::_thesis: for v, w being VECTOR of (product G) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (product G); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as VECTOR of (product G1) by A1;
a * (v + w) = a * (v1 + w1) by A1;
then a * (v + w) = (a * v1) + (a * w1) by RLVECT_1:def_5;
hence a * (v + w) = (a * v) + (a * w) by A1; ::_thesis: verum
end;
A5: now__::_thesis:_for_a,_b_being_real_number_
for_v_being_VECTOR_of_(product_G)_holds_(a_*_b)_*_v_=_a_*_(b_*_v)
let a, b be real number ; ::_thesis: for v being VECTOR of (product G) holds (a * b) * v = a * (b * v)
let v be VECTOR of (product G); ::_thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as VECTOR of (product G1) by A1;
(a * b) * v = (a * b) * v1 by A1;
then (a * b) * v = a * (b * v1) by RLVECT_1:def_7;
hence (a * b) * v = a * (b * v) by A1; ::_thesis: verum
end;
A6: now__::_thesis:_for_a,_b_being_real_number_
for_v_being_VECTOR_of_(product_G)_holds_(a_+_b)_*_v_=_(a_*_v)_+_(b_*_v)
let a, b be real number ; ::_thesis: for v being VECTOR of (product G) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (product G); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as VECTOR of (product G1) by A1;
(a + b) * v = (a + b) * v1 by A1;
then (a + b) * v = (a * v1) + (b * v1) by RLVECT_1:def_6;
hence (a + b) * v = (a * v) + (b * v) by A1; ::_thesis: verum
end;
A7: product G is add-associative
proof
let v, w, x be VECTOR of (product G); :: according to RLVECT_1:def_3 ::_thesis: (v + w) + x = v + (w + x)
reconsider v1 = v, w1 = w, x1 = x as VECTOR of (product G1) by A1;
(v + w) + x = (v1 + w1) + x1 by A1;
then (v + w) + x = v1 + (w1 + x1) by RLVECT_1:def_3;
hence (v + w) + x = v + (w + x) by A1; ::_thesis: verum
end;
A8: product G is Abelian
proof
let v, w be VECTOR of (product G); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider v1 = v, w1 = w as VECTOR of (product G1) by A1;
v + w = v1 + w1 by A1;
then v + w = w1 + v1 ;
hence v + w = w + v by A1; ::_thesis: verum
end;
product G is right_zeroed
proof
let v be VECTOR of (product G); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (product G)) = v
reconsider v1 = v as VECTOR of (product G1) by A1;
v + (0. (product G)) = v1 + (0. (product G1)) by A1;
hence v + (0. (product G)) = v by RLVECT_1:def_4; ::_thesis: verum
end;
hence ( 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 ) by A8, A7, A3, A4, A6, A5, A2, Lm7, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: 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.||
let i be Element of dom G; ::_thesis: 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.||
let x be Point of (product G); ::_thesis: for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <= ||.x.||
let y be Element of product (carr G); ::_thesis: for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <= ||.x.||
let xi be Point of (G . i); ::_thesis: ( y = x & xi = y . i implies ||.xi.|| <= ||.x.|| )
reconsider n = len G as Element of NAT ;
assume that
A1: y = x and
A2: xi = y . i ; ::_thesis: ||.xi.|| <= ||.x.||
A3: ((normsequence (G,y)) . i) ^2 = (sqr (normsequence (G,y))) . i by VALUED_1:11;
A4: for i being Element of NAT st i in Seg n holds
0 <= (sqr (normsequence (G,y))) . i
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies 0 <= (sqr (normsequence (G,y))) . i )
assume i in Seg n ; ::_thesis: 0 <= (sqr (normsequence (G,y))) . i
((normsequence (G,y)) . i) ^2 >= 0 by XREAL_1:63;
hence 0 <= (sqr (normsequence (G,y))) . i by VALUED_1:11; ::_thesis: verum
end;
dom G = Seg n by FINSEQ_1:def_3;
then A5: ( 0 <= ((normsequence (G,y)) . i) ^2 & (sqr (normsequence (G,y))) . i <= Sum (sqr (normsequence (G,y))) ) by A4, REAL_NS1:7, XREAL_1:63;
||.xi.|| = (normsequence (G,y)) . i by A2, Def11;
then sqrt ((sqr (normsequence (G,y))) . i) = (normsequence (G,y)) . i by A3, NORMSP_1:4, SQUARE_1:22;
then A6: ||.xi.|| = sqrt ((sqr (normsequence (G,y))) . i) by A2, Def11;
||.x.|| = |.(normsequence (G,y)).| by A1, Th7;
hence ||.xi.|| <= ||.x.|| by A3, A5, A6, SQUARE_1:26; ::_thesis: verum
end;
Lm8: 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
let RNS be RealNormSpace; ::_thesis: 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 ) )
let S be sequence of RNS; ::_thesis: for g being Point of RNS holds
( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
let g be Point of RNS; ::_thesis: ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
now__::_thesis:_(_||.(S_-_g).||_is_convergent_&_lim_||.(S_-_g).||_=_0_implies_(_S_is_convergent_&_lim_S_=_g_)_)
assume A1: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ; ::_thesis: ( S is convergent & lim S = g )
A2: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((S_._m)_-_g).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r )
reconsider p = r as real number ;
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
abs ((||.(S - g).|| . m) - 0) < p by A1, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((S_._m)_-_g).||_<_p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((S . m) - g).|| < p )
assume n <= m ; ::_thesis: ||.((S . m) - g).|| < p
then abs ((||.(S - g).|| . m) - 0) < p by A3;
then abs ||.((S - g) . m).|| < p by NORMSP_0:def_4;
then A4: abs ||.((S . m) - g).|| < p by NORMSP_1:def_4;
0 <= ||.((S . m) - g).|| by NORMSP_1:4;
hence ||.((S . m) - g).|| < p by A4, ABSVALUE:def_1; ::_thesis: verum
end;
hence for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r ; ::_thesis: verum
end;
hence S is convergent by NORMSP_1:def_6; ::_thesis: lim S = g
hence lim S = g by A2, NORMSP_1:def_7; ::_thesis: verum
end;
hence ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) by NORMSP_1:24; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: 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).||
let i be Element of dom G; ::_thesis: 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).||
let x, y be Point of (product G); ::_thesis: 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).||
let xi, yi be Point of (G . i); ::_thesis: 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).||
let zx, zy be Element of product (carr G); ::_thesis: ( xi = zx . i & zx = x & yi = zy . i & zy = y implies ||.(yi - xi).|| <= ||.(y - x).|| )
assume that
A1: xi = zx . i and
A2: zx = x and
A3: yi = zy . i and
A4: zy = y ; ::_thesis: ||.(yi - xi).|| <= ||.(y - x).||
reconsider zyi = zy . i, zxi = zx . i as Element of (G . i) by A1, A3;
A5: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
then reconsider mzx = - x as Element of product (carr G) ;
len G = len (carr G) by Def4;
then A6: dom G = dom (carr G) by FINSEQ_3:29;
- x = (- 1) * x by RLVECT_1:16;
then A7: mzx . i = (- 1) * zxi by A2, A5, A6, Lm4;
then reconsider mzxi = mzx . i as Element of (G . i) ;
reconsider zyMm = y - x as Element of product (carr G) by A5;
zyMm . i = zyi + mzxi by A4, A5, A6, Lm3;
then zyMm . i = zyi + (- zxi) by A7, RLVECT_1:16;
hence ||.(yi - xi).|| <= ||.(y - x).|| by A1, A3, Th10; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: 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 ) ) )
let seq be sequence of (product G); ::_thesis: 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 ) ) )
let x0 be Point of (product G); ::_thesis: 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 ) ) )
let y0 be Element of product (carr G); ::_thesis: ( x0 = y0 & seq is convergent & lim seq = x0 implies 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 ) ) ) )
assume that
A1: x0 = y0 and
A2: ( seq is convergent & lim seq = x0 ) ; ::_thesis: 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 ) ) )
let i be Element of dom G; ::_thesis: 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 ) ) )
defpred S1[ Element of NAT , Element of (G . i)] means ex seqm being Element of product (carr G) st
( seqm = seq . $1 & $2 = seqm . i );
len G = len (carr G) by Def4;
then A3: dom G = dom (carr G) by FINSEQ_3:29;
then y0 . i in (carr G) . i by CARD_3:9;
then reconsider x0i = y0 . i as Point of (G . i) by Def4;
A4: for x being Element of NAT ex y being Element of (G . i) st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of (G . i) st S1[x,y]
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
then consider seqm being Element of product (carr G) such that
A5: seqm = seq . x ;
take seqm . i ; ::_thesis: ( seqm . i is Element of (G . i) & S1[x,seqm . i] )
(carr G) . i = the carrier of (G . i) by Def4;
hence ( seqm . i is Element of (G . i) & S1[x,seqm . i] ) by A3, A5, CARD_3:9; ::_thesis: verum
end;
ex f being Function of NAT, the carrier of (G . i) st
for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A4);
then consider seqi being sequence of (G . i) such that
A6: for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ;
take seqi ; ::_thesis: ( 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 ) ) )
A7: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r )
assume r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r
then consider k being Element of NAT such that
A8: for n being Element of NAT st k <= n holds
||.((seq . n) - x0).|| < r by A2, NORMSP_1:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
||.((seqi_._n)_-_x0i).||_<_r
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((seqi . n) - x0i).|| < r )
assume n >= k ; ::_thesis: ||.((seqi . n) - x0i).|| < r
then A9: ||.((seq . n) - x0).|| < r by A8;
ex seqn being Element of product (carr G) st
( seqn = seq . n & seqi . n = seqn . i ) by A6;
then ||.((seqi . n) - x0i).|| <= ||.((seq . n) - x0).|| by A1, Th11;
hence ||.((seqi . n) - x0i).|| < r by A9, XXREAL_0:2; ::_thesis: verum
end;
hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r ; ::_thesis: verum
end;
then seqi is convergent by NORMSP_1:def_6;
hence ( 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 ) ) ) by A6, A7, NORMSP_1:def_7; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: 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 )
let seq be sequence of (product G); ::_thesis: 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 )
let x0 be Point of (product G); ::_thesis: 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 )
let y0 be Element of product (carr G); ::_thesis: ( 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 ) ) ) ) implies ( seq is convergent & lim seq = x0 ) )
assume that
A1: x0 = y0 and
A2: 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 ) ) ) ; ::_thesis: ( seq is convergent & lim seq = x0 )
defpred S1[ Element of dom G, set ] means ex rseqi being Real_Sequence ex seqi being sequence of (G . $1) st
( rseqi = $2 & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . $1 ) ) );
A3: for i being Element of dom G ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi]
proof
let i be Element of dom G; ::_thesis: ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi]
consider seqi being sequence of (G . i) such that
A4: seqi is convergent and
y0 . i = lim seqi and
A5: for m being Element of NAT ex Sm being Element of product (carr G) st
( Sm = seq . m & seqi . m = Sm . i ) by A2;
set rseqi = ||.(seqi - (lim seqi)).||;
A6: ||.(seqi - (lim seqi)).|| is Element of Funcs (NAT,REAL) by FUNCT_2:8;
( ||.(seqi - (lim seqi)).|| is convergent & lim ||.(seqi - (lim seqi)).|| = 0 ) by A4, Lm8;
hence ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi] by A4, A5, A6; ::_thesis: verum
end;
consider yyseq being Function of (dom G),(Funcs (NAT,REAL)) such that
A7: for i being Element of dom G holds S1[i,yyseq . i] from FUNCT_2:sch_3(A3);
reconsider I = len G as Element of NAT ;
defpred S2[ Element of NAT , Element of REAL I] means for i being Element of dom G holds (yyseq . i) . $1 = $2 . i;
A8: for k being Element of NAT ex yseqk being Element of REAL I st S2[k,yseqk]
proof
let k be Element of NAT ; ::_thesis: ex yseqk being Element of REAL I st S2[k,yseqk]
defpred S3[ set , set ] means ex i being Element of dom G st
( i = $1 & $2 = (yyseq . i) . k );
A9: for k being Nat st k in Seg I holds
ex x being set st S3[k,x]
proof
let j be Nat; ::_thesis: ( j in Seg I implies ex x being set st S3[j,x] )
assume j in Seg I ; ::_thesis: ex x being set st S3[j,x]
then reconsider i = j as Element of dom G by FINSEQ_1:def_3;
take (yyseq . i) . k ; ::_thesis: S3[j,(yyseq . i) . k]
thus S3[j,(yyseq . i) . k] ; ::_thesis: verum
end;
consider yseqk being FinSequence such that
A10: ( dom yseqk = Seg I & ( for j being Nat st j in Seg I holds
S3[j,yseqk . j] ) ) from FINSEQ_1:sch_1(A9);
now__::_thesis:_for_j_being_Nat_st_j_in_dom_yseqk_holds_
yseqk_._j_in_REAL
let j be Nat; ::_thesis: ( j in dom yseqk implies yseqk . j in REAL )
assume j in dom yseqk ; ::_thesis: yseqk . j in REAL
then consider i being Element of dom G such that
i = j and
A11: yseqk . j = (yyseq . i) . k by A10;
yyseq . i is Function of NAT,REAL by FUNCT_2:66;
hence yseqk . j in REAL by A11, FUNCT_2:5; ::_thesis: verum
end;
then reconsider yyy = yseqk as FinSequence of REAL by FINSEQ_2:12;
yyy is Element of (len yyy) -tuples_on REAL by FINSEQ_2:92;
then reconsider yseqk = yseqk as Element of REAL I by A10, FINSEQ_1:def_3;
now__::_thesis:_for_j_being_Element_of_dom_G_holds_yseqk_._j_=_(yyseq_._j)_._k
let j be Element of dom G; ::_thesis: yseqk . j = (yyseq . j) . k
j in dom G ;
then j in Seg I by FINSEQ_1:def_3;
then ex i being Element of dom G st
( i = j & yseqk . j = (yyseq . i) . k ) by A10;
hence yseqk . j = (yyseq . j) . k ; ::_thesis: verum
end;
hence ex yseqk being Element of REAL I st S2[k,yseqk] ; ::_thesis: verum
end;
consider yseq being Function of NAT,(REAL I) such that
A12: for k being Element of NAT holds S2[k,yseq . k] from FUNCT_2:sch_3(A8);
A13: now__::_thesis:_for_i0_being_Element_of_NAT_st_i0_in_Seg_I_holds_
ex_i_being_Element_of_dom_G_ex_rseqi_being_Real_Sequence_ex_seqi_being_sequence_of_(G_._i)_st_
(_(_for_k_being_Element_of_NAT_holds_rseqi_._k_=_(yseq_._k)_._i0_)_&_i_=_i0_&_seqi_is_convergent_&_rseqi_is_convergent_&_lim_rseqi_=_(0*_I)_._i_&_rseqi_=_||.(seqi_-_(lim_seqi)).||_&_(_for_m_being_Element_of_NAT_ex_seqm_being_Element_of_product_(carr_G)_st_
(_seqm_=_seq_._m_&_seqi_._m_=_seqm_._i_)_)_)
let i0 be Element of NAT ; ::_thesis: ( i0 in Seg I implies ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) )
assume i0 in Seg I ; ::_thesis: ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
then reconsider i = i0 as Element of dom G by FINSEQ_1:def_3;
take i = i; ::_thesis: ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
consider rseqi being Real_Sequence, seqi being sequence of (G . i) such that
A14: ( rseqi = yyseq . i & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) by A7;
take rseqi = rseqi; ::_thesis: ex seqi being sequence of (G . i) st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
take seqi = seqi; ::_thesis: ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
thus ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) by A12, A14; ::_thesis: verum
end;
the carrier of (REAL-NS I) = REAL I by REAL_NS1:def_4;
then reconsider xseq = yseq as sequence of (REAL-NS I) ;
xseq = yseq ;
then consider xseq being sequence of (REAL-NS I), yseq being Function of NAT,(REAL I) such that
A15: xseq = yseq and
A16: for i0 being Element of NAT st i0 in Seg I holds
ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) by A13;
A17: for i being Element of NAT st i in Seg I holds
ex rseqi being Real_Sequence st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i ) & rseqi is convergent & (0* I) . i = lim rseqi )
proof
let i0 be Element of NAT ; ::_thesis: ( i0 in Seg I implies ex rseqi being Real_Sequence st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) )
assume i0 in Seg I ; ::_thesis: ex rseqi being Real_Sequence st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi )
then ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) by A16;
hence ex rseqi being Real_Sequence st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) ; ::_thesis: verum
end;
A18: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
||.(xseq_-_(0._(REAL-NS_I))).||_._x_=_||.(seq_-_x0).||_._x
let x be set ; ::_thesis: ( x in NAT implies ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x )
assume x in NAT ; ::_thesis: ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x
then reconsider i = x as Element of NAT ;
reconsider seqimx0 = (seq . i) - x0 as Element of product (carr G) by A18;
A19: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(normsequence_(G,seqimx0))_holds_
(normsequence_(G,seqimx0))_._k_=_(yseq_._i)_._k
reconsider mx0 = - x0 as Element of product (carr G) by A18;
let k be Nat; ::_thesis: ( k in dom (normsequence (G,seqimx0)) implies (normsequence (G,seqimx0)) . k = (yseq . i) . k )
assume A20: k in dom (normsequence (G,seqimx0)) ; ::_thesis: (normsequence (G,seqimx0)) . k = (yseq . i) . k
A21: len G = len (normsequence (G,seqimx0)) by Def11;
then reconsider k0 = k as Element of dom G by A20, FINSEQ_3:29;
k in Seg I by A20, A21, FINSEQ_1:def_3;
then consider k1 being Element of dom G, rseqk1i being Real_Sequence, seqk1i being sequence of (G . k1) such that
A22: for j being Element of NAT holds rseqk1i . j = (yseq . j) . k and
A23: k1 = k and
seqk1i is convergent and
rseqk1i is convergent and
lim rseqk1i = (0* I) . k1 and
A24: rseqk1i = ||.(seqk1i - (lim seqk1i)).|| and
A25: for m being Element of NAT ex seqk1m being Element of product (carr G) st
( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) by A16;
consider seqk0 being sequence of (G . k0) such that
seqk0 is convergent and
A26: y0 . k0 = lim seqk0 and
A27: for m being Element of NAT ex seqm0 being Element of product (carr G) st
( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) by A2;
A28: ex seqm0 being Element of product (carr G) st
( seqm0 = seq . i & seqk0 . i = seqm0 . k0 ) by A27;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
seqk1i_._x_=_seqk0_._x
let x be set ; ::_thesis: ( x in NAT implies seqk1i . x = seqk0 . x )
assume x in NAT ; ::_thesis: seqk1i . x = seqk0 . x
then reconsider m = x as Element of NAT ;
( ex seqk1m being Element of product (carr G) st
( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) & ex seqm0 being Element of product (carr G) st
( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) ) by A27, A25;
hence seqk1i . x = seqk0 . x by A23; ::_thesis: verum
end;
then A29: seqk1i = seqk0 by A23, FUNCT_2:12;
len G = len (carr G) by Def4;
then A30: dom G = dom (carr G) by FINSEQ_3:29;
- x0 = (- 1) * x0 by RLVECT_1:16;
then mx0 . k0 = (- 1) * (lim seqk0) by A1, A18, A26, A30, Lm4;
then - (lim seqk0) = mx0 . k0 by RLVECT_1:16;
then A31: seqimx0 . k0 = (seqk0 . i) - (lim seqk0) by A18, A28, A30, Lm3;
thus (normsequence (G,seqimx0)) . k = the normF of (G . k0) . (seqimx0 . k0) by Def11
.= ||.((seqk0 - (lim seqk0)) . i).|| by A31, NORMSP_1:def_4
.= ||.(seqk1i - (lim seqk1i)).|| . i by A23, A29, NORMSP_0:def_4
.= (yseq . i) . k by A22, A24 ; ::_thesis: verum
end;
len (yseq . i) = I by CARD_1:def_7;
then len (yseq . i) = len (normsequence (G,seqimx0)) by Def11;
then dom (yseq . i) = dom (normsequence (G,seqimx0)) by FINSEQ_3:29;
then A32: yseq . i = normsequence (G,seqimx0) by A19, FINSEQ_1:13;
thus ||.(xseq - (0. (REAL-NS I))).|| . x = ||.((xseq - (0. (REAL-NS I))) . i).|| by NORMSP_0:def_4
.= ||.((xseq . i) - (0. (REAL-NS I))).|| by NORMSP_1:def_4
.= ||.(xseq . i).|| by RLVECT_1:13
.= |.(yseq . i).| by A15, REAL_NS1:1
.= ||.((seq . i) - x0).|| by A32, Th7
.= ||.((seq - x0) . i).|| by NORMSP_1:def_4
.= ||.(seq - x0).|| . x by NORMSP_0:def_4 ; ::_thesis: verum
end;
then A33: ||.(xseq - (0. (REAL-NS I))).|| = ||.(seq - x0).|| by FUNCT_2:12;
0* I = 0. (REAL-NS I) by REAL_NS1:def_4;
then ( xseq is convergent & lim xseq = 0. (REAL-NS I) ) by A15, A17, REAL_NS1:11;
then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by A33, Lm8;
hence ( seq is convergent & lim seq = x0 ) by Lm8; ::_thesis: verum
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
let G be RealNormSpace-Sequence; ::_thesis: ( ( for i being Element of dom G holds G . i is complete ) implies product G is complete )
assume A1: for i being Element of dom G holds G . i is complete ; ::_thesis: product G is complete
reconsider I = len G as Element of NAT ;
A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
for seq being sequence of (product G) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let seq be sequence of (product G); ::_thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
defpred S1[ Nat, set ] means ex i being Element of dom G st
( i = $1 & ex seqi being sequence of (G . i) st
( seqi is convergent & $2 = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) );
assume A3: seq is Cauchy_sequence_by_Norm ; ::_thesis: seq is convergent
A4: for k being Nat st k in Seg I holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg I implies ex x being set st S1[k,x] )
assume k in Seg I ; ::_thesis: ex x being set st S1[k,x]
then reconsider i = k as Element of dom G by FINSEQ_1:def_3;
defpred S2[ Element of NAT , Element of (G . i)] means ex seqm being Element of product (carr G) st
( seqm = seq . $1 & $2 = seqm . i );
A5: for x being Element of NAT ex y being Element of (G . i) st S2[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of (G . i) st S2[x,y]
consider seqm being Element of product (carr G) such that
A6: seqm = seq . x by A2;
len G = len (carr G) by Def4;
then A7: dom G = dom (carr G) by FINSEQ_3:29;
take seqm . i ; ::_thesis: ( seqm . i is Element of (G . i) & S2[x,seqm . i] )
(carr G) . i = the carrier of (G . i) by Def4;
hence ( seqm . i is Element of (G . i) & S2[x,seqm . i] ) by A6, A7, CARD_3:9; ::_thesis: verum
end;
ex f being Function of NAT, the carrier of (G . i) st
for x being Element of NAT holds S2[x,f . x] from FUNCT_2:sch_3(A5);
then consider seqi being sequence of (G . i) such that
A8: for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ;
take lim seqi ; ::_thesis: S1[k, lim seqi]
now__::_thesis:_for_r1_being_Real_st_r1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seqi_._n)_-_(seqi_._m)).||_<_r1
let r1 be Real; ::_thesis: ( r1 > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1 )
assume A9: r1 > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1
reconsider r = r1 as Element of REAL ;
consider k being Element of NAT such that
A10: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A3, A9, RSSPACE3:8;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seqi_._n)_-_(seqi_._m)).||_<_r1
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seqi . n) - (seqi . m)).|| < r1 )
assume ( n >= k & m >= k ) ; ::_thesis: ||.((seqi . n) - (seqi . m)).|| < r1
then A11: ||.((seq . n) - (seq . m)).|| < r by A10;
( ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) & ex seqn being Element of product (carr G) st
( seqn = seq . n & seqi . n = seqn . i ) ) by A8;
then ||.((seqi . n) - (seqi . m)).|| <= ||.((seq . n) - (seq . m)).|| by Th11;
hence ||.((seqi . n) - (seqi . m)).|| < r1 by A11, XXREAL_0:2; ::_thesis: verum
end;
hence ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1 ; ::_thesis: verum
end;
then A12: seqi is Cauchy_sequence_by_Norm by RSSPACE3:8;
G . i is complete by A1;
then seqi is convergent by A12, LOPBAN_1:def_15;
hence S1[k, lim seqi] by A8; ::_thesis: verum
end;
consider yy0 being FinSequence such that
A13: ( dom yy0 = Seg I & ( for j being Nat st j in Seg I holds
S1[j,yy0 . j] ) ) from FINSEQ_1:sch_1(A4);
A14: len yy0 = I by A13, FINSEQ_1:def_3;
then A15: len yy0 = len (carr G) by Def4;
A16: now__::_thesis:_for_i_being_set_st_i_in_dom_(carr_G)_holds_
yy0_._i_in_(carr_G)_._i
let i be set ; ::_thesis: ( i in dom (carr G) implies yy0 . i in (carr G) . i )
assume i in dom (carr G) ; ::_thesis: yy0 . i in (carr G) . i
then reconsider x = i as Element of dom (carr G) ;
reconsider x = x as Element of dom G by A14, A15, FINSEQ_3:29;
reconsider j = x as Element of NAT ;
j in dom G ;
then j in Seg I by FINSEQ_1:def_3;
then ex i0 being Element of dom G st
( i0 = j & ex seqi being sequence of (G . i0) st
( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i0 ) ) ) ) by A13;
then yy0 . x in the carrier of (G . x) ;
hence yy0 . i in (carr G) . i by Def4; ::_thesis: verum
end;
( dom (carr G) = Seg (len (carr G)) & len G = len (carr G) ) by Def4, FINSEQ_1:def_3;
then reconsider y0 = yy0 as Element of product (carr G) by A13, A16, CARD_3:9;
A17: now__::_thesis:_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_)_)_)
let i be Element of dom G; ::_thesis: 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 ) ) )
reconsider j = i as Element of NAT ;
i in dom G ;
then i in Seg I by FINSEQ_1:def_3;
then consider i0 being Element of dom G such that
A18: i0 = j and
A19: ex seqi being sequence of (G . i0) st
( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A13;
consider seqi being sequence of (G . i0) such that
A20: ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A19;
reconsider seqi = seqi as sequence of (G . i) by A18;
take seqi = seqi; ::_thesis: ( 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 ) ) )
thus ( 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 ) ) ) by A18, A20; ::_thesis: verum
end;
reconsider x0 = y0 as Point of (product G) by A2;
x0 = y0 ;
hence seq is convergent by A17, Th13; ::_thesis: verum
end;
hence product G is complete by LOPBAN_1:def_15; ::_thesis: verum
end;