:: RSSPACE semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
func the_set_of_RealSequences -> non empty set means :Def1: :: RSSPACE:def 1
for x being set holds
( x in it iff x is Real_Sequence );
existence
ex b1 being non empty set st
for x being set holds
( x in b1 iff x is Real_Sequence )
proof end;
uniqueness
for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff x is Real_Sequence ) ) & ( for x being set holds
( x in b2 iff x is Real_Sequence ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def 1 :
for b1 being non empty set holds
( b1 = the_set_of_RealSequences iff for x being set holds
( x in b1 iff x is Real_Sequence ) );

definition
let a be set ;
assume A1: a in the_set_of_RealSequences ;
func seq_id a -> Real_Sequence equals :Def2: :: RSSPACE:def 2
a;
coherence
a is Real_Sequence
by A1, Def1;
end;

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
for a being set st a in the_set_of_RealSequences holds
seq_id a = a;

definition
let a be set ;
assume A1: a in REAL ;
func R_id a -> Real equals :Def3: :: RSSPACE:def 3
a;
coherence
a is Real
by A1;
end;

:: deftheorem Def3 defines R_id RSSPACE:def 3 :
for a being set st a in REAL holds
R_id a = a;

theorem Th1: :: RSSPACE:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex ADD being BinOp of the_set_of_RealSequences st
( ( for a, b being Element of the_set_of_RealSequences holds ADD . a,b = (seq_id a) + (seq_id b) ) & ADD is commutative & ADD is associative )
proof end;

theorem Th2: :: RSSPACE:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex f being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
f . [r,x] = (R_id r) (#) (seq_id x)
proof end;

definition
func l_add -> BinOp of the_set_of_RealSequences means :Def4: :: RSSPACE:def 4
for a, b being Element of the_set_of_RealSequences holds it . a,b = (seq_id a) + (seq_id b);
existence
ex b1 being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds b1 . a,b = (seq_id a) + (seq_id b)
by Th1;
uniqueness
for b1, b2 being BinOp of the_set_of_RealSequences st ( for a, b being Element of the_set_of_RealSequences holds b1 . a,b = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_RealSequences holds b2 . a,b = (seq_id a) + (seq_id b) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines l_add RSSPACE:def 4 :
for b1 being BinOp of the_set_of_RealSequences holds
( b1 = l_add iff for a, b being Element of the_set_of_RealSequences holds b1 . a,b = (seq_id a) + (seq_id b) );

definition
func l_mult -> Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences means :Def5: :: RSSPACE:def 5
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
it . [r,x] = (R_id r) (#) (seq_id x);
existence
ex b1 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . [r,x] = (R_id r) (#) (seq_id x)
by Th2;
uniqueness
for b1, b2 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . [r,x] = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b2 . [r,x] = (R_id r) (#) (seq_id x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines l_mult RSSPACE:def 5 :
for b1 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences holds
( b1 = l_mult iff for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . [r,x] = (R_id r) (#) (seq_id x) );

definition
func Zeroseq -> Element of the_set_of_RealSequences means :Def6: :: RSSPACE:def 6
for n being Nat holds (seq_id it) . n = 0;
existence
ex b1 being Element of the_set_of_RealSequences st
for n being Nat holds (seq_id b1) . n = 0
proof end;
uniqueness
for b1, b2 being Element of the_set_of_RealSequences st ( for n being Nat holds (seq_id b1) . n = 0 ) & ( for n being Nat holds (seq_id b2) . n = 0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :
for b1 being Element of the_set_of_RealSequences holds
( b1 = Zeroseq iff for n being Nat holds (seq_id b1) . n = 0 );

theorem Th3: :: RSSPACE:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real_Sequence holds seq_id x = x
proof end;

theorem Th4: :: RSSPACE:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds v + w = (seq_id v) + (seq_id w)
proof end;

theorem Th5: :: RSSPACE:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds r * v = r (#) (seq_id v)
proof end;

registration
cluster RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) -> Abelian ;
coherence
RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) is Abelian
proof end;
end;

Lm1: for u, v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds u + v = v + u
;

theorem Th6: :: RSSPACE:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for u, v, w being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds (u + v) + w = u + (v + w)
proof end;

theorem Th7: :: RSSPACE:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds v + (0. RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #)) = v
proof end;

theorem Th8: :: RSSPACE:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) ex w being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #)
proof end;

theorem Th9: :: RSSPACE:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds a * (v + w) = (a * v) + (a * w)
proof end;

theorem Th10: :: RSSPACE:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds (a + b) * v = (a * v) + (b * v)
proof end;

theorem Th11: :: RSSPACE:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds (a * b) * v = a * (b * v)
proof end;

theorem Th12: :: RSSPACE:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds 1 * v = v
proof end;

definition
func Linear_Space_of_RealSequences -> RealLinearSpace equals :: RSSPACE:def 7
RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #);
correctness
coherence
RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) is RealLinearSpace
;
by Lm1, Th6, Th7, Th8, Th9, Th10, Th11, Th12, RLVECT_1:7;
end;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :
Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #);

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Add_ X1,X -> BinOp of X1 equals :Def8: :: RSSPACE:def 8
the add of X || X1;
correctness
coherence
the add of X || X1 is BinOp of X1
;
proof end;
end;

:: deftheorem Def8 defines Add_ RSSPACE:def 8 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is lineary-closed & not X1 is empty holds
Add_ X1,X = the add of X || X1;

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Mult_ X1,X -> Function of [:REAL ,X1:],X1 equals :Def9: :: RSSPACE:def 9
the Mult of X | [:REAL ,X1:];
correctness
coherence
the Mult of X | [:REAL ,X1:] is Function of [:REAL ,X1:],X1
;
proof end;
end;

:: deftheorem Def9 defines Mult_ RSSPACE:def 9 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is lineary-closed & not X1 is empty holds
Mult_ X1,X = the Mult of X | [:REAL ,X1:];

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Zero_ X1,X -> Element of X1 equals :Def10: :: RSSPACE:def 10
0. X;
correctness
coherence
0. X is Element of X1
;
proof end;
end;

:: deftheorem Def10 defines Zero_ RSSPACE:def 10 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is lineary-closed & not X1 is empty holds
Zero_ X1,X = 0. X;

theorem Th13: :: RSSPACE:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for V1 being Subset of V st V1 is lineary-closed & not V1 is empty holds
RLSStruct(# V1,(Zero_ V1,V),(Add_ V1,V),(Mult_ V1,V) #) is Subspace of V
proof end;

definition
func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences means :Def11: :: RSSPACE:def 11
for x being set holds
( x in it iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) );
existence
ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines the_set_of_l2RealSequences RSSPACE:def 11 :
for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_l2RealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) );

registration
cluster the_set_of_l2RealSequences -> non empty lineary-closed ;
coherence
( the_set_of_l2RealSequences is lineary-closed & not the_set_of_l2RealSequences is empty )
proof end;
end;

theorem :: RSSPACE:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RSSPACE:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
RLSStruct(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences by Th13;

theorem Th16: :: RSSPACE:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
RLSStruct(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ) #) is RealLinearSpace by Th13;

theorem :: RSSPACE:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of Linear_Space_of_RealSequences = the_set_of_RealSequences & ( for x being set holds
( x is VECTOR of Linear_Space_of_RealSequences iff x is Real_Sequence ) ) & ( for u being VECTOR of Linear_Space_of_RealSequences holds u = seq_id u ) & ( for u, v being VECTOR of Linear_Space_of_RealSequences holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of Linear_Space_of_RealSequences holds r * u = r (#) (seq_id u) ) ) by Def1, Def2, Th4, Th5;

theorem Th18: :: RSSPACE:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex f being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
f . [x,y] = Sum ((seq_id x) (#) (seq_id y))
proof end;

definition
func l_scalar -> Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL means :: RSSPACE:def 12
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
it . [x,y] = Sum ((seq_id x) (#) (seq_id y));
existence
ex b1 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . [x,y] = Sum ((seq_id x) (#) (seq_id y))
by Th18;
uniqueness
for b1, b2 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . [x,y] = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b2 . [x,y] = Sum ((seq_id x) (#) (seq_id y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines l_scalar RSSPACE:def 12 :
for b1 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL holds
( b1 = l_scalar iff for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . [x,y] = Sum ((seq_id x) (#) (seq_id y)) );

registration
cluster UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #) -> non empty ;
coherence
not UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #) is empty
;
end;

definition
func l2_Space -> non empty UNITSTR equals :: RSSPACE:def 13
UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #);
coherence
UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #) is non empty UNITSTR
;
end;

:: deftheorem defines l2_Space RSSPACE:def 13 :
l2_Space = UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #);

theorem Th19: :: RSSPACE:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being UNITSTR st RLSStruct(# the carrier of l,the Zero of l,the add of l,the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace
proof end;

theorem :: RSSPACE:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq is summable & Sum rseq = 0 )
proof end;

theorem :: RSSPACE:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for rseq being Real_Sequence st ( for n being Nat holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 holds
for n being Nat holds rseq . n = 0
proof end;

registration
cluster l2_Space -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence
( l2_Space is Abelian & l2_Space is add-associative & l2_Space is right_zeroed & l2_Space is right_complementable & l2_Space is RealLinearSpace-like )
by Th16, Th19;
end;