:: Formalization of Integral Linear Space
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

reconsider z0 = 0 as Real ;

deffunc H1( set ) ->  Element of NAT = 0 ;

theorem :: RLVECT_X:1
for X being RealLinearSpace
for R1, R2 being FinSequence of X st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
proofend;

theorem :: RLVECT_X:2
for X being RealLinearSpace
for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds
Sum R3 = (Sum R1) - (Sum R2)
proofend;

theorem Th3: :: RLVECT_X:3
for X being RealLinearSpace
for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
proofend;

begin

definition
let V be RealLinearSpace;
let i be Integer;
let L be Linear_Combination of V;
funci * L ->  Linear_Combination of V means :Def1: :: RLVECT_X:def 1
 for v being VECTOR of V holds it . v = i * (L . v);
existence
 ex b1 being Linear_Combination of V st
for v being VECTOR of V holds b1 . v = i * (L . v)
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st ( for v being VECTOR of V holds b1 . v = i * (L . v) ) & ( for v being VECTOR of V holds b2 . v = i * (L . v) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines * RLVECT_X:def_1_:_
 for V being RealLinearSpace
for i being Integer
for L, b4 being Linear_Combination of V holds
( b4 = i * L iff for v being VECTOR of V holds b4 . v = i * (L . v) );

definition
let V be RealLinearSpace;
let A be Subset of V;
func Z_Lin A ->  Subset of V equals :: RLVECT_X:def 2
 {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  ;
correctness
coherence
{  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  is Subset of V;
proofend;
end;

:: deftheorem  defines Z_Lin RLVECT_X:def_2_:_
 for V being RealLinearSpace
for A being Subset of V holds Z_Lin A =  {  (Sum l) where l is Linear_Combination of A : rng l c= INT  }  ;

theorem Th4: :: RLVECT_X:4
for a being Real
for i being Integer
for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l
proofend;

theorem Th5: :: RLVECT_X:5
for V being RealLinearSpace
for A being Subset of V
for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds
rng (l1 + l2) c= INT
proofend;

theorem Th6: :: RLVECT_X:6
for i being Integer
for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
proofend;

theorem Th7: :: RLVECT_X:7
for V being RealLinearSpace holds rng (ZeroLC V) c= INT
proofend;

theorem Th8: :: RLVECT_X:8
for V being RealLinearSpace
for A being Subset of V holds Z_Lin A c= the carrier of (Lin A)
proofend;

theorem Th9: :: RLVECT_X:9
for V being RealLinearSpace
for v, u being VECTOR of V
for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A
proofend;

theorem Th10: :: RLVECT_X:10
for i being Integer
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
proofend;

theorem Th11: :: RLVECT_X:11
for V being RealLinearSpace
for A being Subset of V holds 0. V in Z_Lin A
proofend;

theorem Th12: :: RLVECT_X:12
for x being set
for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Z_Lin A
proofend;

theorem Th13: :: RLVECT_X:13
for V being RealLinearSpace
for A, B being Subset of V st A c= B holds
Z_Lin A c= Z_Lin B
proofend;

theorem :: RLVECT_X:14
for V being RealLinearSpace
for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)
proofend;

theorem :: RLVECT_X:15
for V being RealLinearSpace
for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)
proofend;

theorem Th16: :: RLVECT_X:16
for x being set
for V being RealLinearSpace
for v being VECTOR of V holds
( x in Z_Lin {v} iff ex a being Integer st x = a * v )
proofend;

theorem :: RLVECT_X:17
for V being RealLinearSpace
for v being VECTOR of V holds v in Z_Lin {v}
proofend;

theorem :: RLVECT_X:18
for x being set
for V being RealLinearSpace
for v, w being VECTOR of V holds
( x in v + (Z_Lin {w}) iff ex a being Integer st x = v + (a * w) )
proofend;

theorem Th19: :: RLVECT_X:19
for x being set
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
proofend;

theorem :: RLVECT_X:20
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2}
proofend;

theorem :: RLVECT_X:21
for x being set
for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
proofend;

theorem Th22: :: RLVECT_X:22
for x being set
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Z_Lin {v1,v2,v3} iff ex a, b, c being Integer st x = ((a * v1) + (b * v2)) + (c * v3) )
proofend;

theorem :: RLVECT_X:23
for V being RealLinearSpace
for w1, w2, w3 being VECTOR of V holds
( w1 in Z_Lin {w1,w2,w3} & w2 in Z_Lin {w1,w2,w3} & w3 in Z_Lin {w1,w2,w3} )
proofend;

theorem :: RLVECT_X:24
for x being set
for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2,w3}) iff ex a, b, c being Integer st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
proofend;

Lm1:  for RS being RealLinearSpace
for X being Subset of RS
for g1, h1 being FinSequence of RS
for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X
proofend;

Lm2:  for V being RealLinearSpace
for A being Subset of V
for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
proofend;

theorem :: RLVECT_X:25
for V being RealLinearSpace
for A being Subset of V
for x being set holds
( x in Z_Lin A iff ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) ) by Lm1, Lm2;

registration
let D be non empty set ;
let n be Nat;
cluster Relation-like NAT -defined D -valued Function-like finite n -element FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st
( b1 is n -element & b1 is D -valued )
proofend;
end;

definition
let RS be RealLinearSpace;
let f be FinSequence of RS;
func Z_Lin f ->  Subset of RS equals :: RLVECT_X:def 3
 {  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  ;
correctness
coherence
{  (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  is Subset of RS;
proofend;
end;

:: deftheorem  defines Z_Lin RLVECT_X:def_3_:_
 for RS being RealLinearSpace
for f being FinSequence of RS holds Z_Lin f =  {  (Sum g) where g is len b2 -element FinSequence of RS : ex a being INT -valued len b2 -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i)  }  ;

theorem Th26: :: RLVECT_X:26
for RS being RealLinearSpace
for f being FinSequence of RS
for x being set holds
( x in Z_Lin f iff ex g being len b2 -element FinSequence of RS ex a being INT -valued len b2 -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) )
proofend;

theorem Th27: :: RLVECT_X:27
for RS being RealLinearSpace
for f being FinSequence of RS
for x, y being Element of RS
for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f
proofend;

theorem Th28: :: RLVECT_X:28
for RS being RealLinearSpace
for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds
Sum f = 0. RS
proofend;

theorem Th29: :: RLVECT_X:29
for RS being RealLinearSpace
for f being FinSequence of RS
for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
proofend;

theorem Th30: :: RLVECT_X:30
for RS being RealLinearSpace
for f being FinSequence of RS
for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
proofend;

theorem Th31: :: RLVECT_X:31
for RS being RealLinearSpace
for f being FinSequence of RS holds rng f c= Z_Lin f
proofend;

theorem Th32: :: RLVECT_X:32
for RS being RealLinearSpace
for f being non empty FinSequence of RS
for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
proofend;

theorem :: RLVECT_X:33
for RS being RealLinearSpace
for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f
proofend;

theorem Th34: :: RLVECT_X:34
for V being RealLinearSpace
for A being Subset of V holds Lin (Z_Lin A) = Lin A
proofend;

theorem Th35: :: RLVECT_X:35
for V being RealLinearSpace
for A being Subset of V
for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
x in Z_Lin A
proofend;

theorem :: RLVECT_X:36
for V being RealLinearSpace
for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A
proofend;

theorem :: RLVECT_X:37
for V being RealLinearSpace
for A, B being Subset of V st Z_Lin A = Z_Lin B holds
Lin A = Lin B
proofend;