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

reconsider z0 = 0 as Real ;

deffunc H₁( object ) -> Element of REAL = In (0,REAL);

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)

proof end;

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)

proof end;

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)

proof end;

definition

let V be RealLinearSpace;
let i be Integer;
let L be Linear_Combination of V;

func i * 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 b₁ being Linear_Combination of V st
for v being VECTOR of V holds b₁ . v = i * (L . v)

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of V st ( for v being VECTOR of V holds b₁ . v = i * (L . v) ) & ( for v being VECTOR of V holds b₂ . v = i * (L . v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines * RLVECT_X:def 1 :
for V being RealLinearSpace
for i being Integer
for L, b₄ being Linear_Combination of V holds
( b₄ = i * L iff for v being VECTOR of V holds b₄ . 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;

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th7: :: RLVECT_X:7

for V being RealLinearSpace holds rng (ZeroLC V) c= INT

proof end;

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)

proof end;

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

proof end;

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

proof end;

theorem Th11: :: RLVECT_X:11

for V being RealLinearSpace
for A being Subset of V holds 0. V in Z_Lin A

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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 )

proof end;

theorem :: RLVECT_X:17

for V being RealLinearSpace
for v being VECTOR of V holds v in Z_Lin {v}

proof end;

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

proof end;

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

proof end;

theorem :: RLVECT_X:20

for V being RealLinearSpace
for w1, w2 being VECTOR of V holds w1 in Z_Lin {w1,w2}

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 b₁ being FinSequence st
( b₁ is n -element & b₁ is D -valued )

proof end;

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;

proof end;

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 b₂ -element FinSequence of RS : ex a being INT -valued len b₂ -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 b₂ -element FinSequence of RS ex a being INT -valued len b₂ -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) )

proof end;

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 Integer st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th31: :: RLVECT_X:31

for RS being RealLinearSpace
for f being FinSequence of RS holds rng f c= Z_Lin f

proof end;

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

proof end;

theorem :: RLVECT_X:33

for RS being RealLinearSpace
for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f

proof end;

theorem Th34: :: RLVECT_X:34

for V being RealLinearSpace
for A being Subset of V holds Lin (Z_Lin A) = Lin A

proof end;

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

proof end;

theorem :: RLVECT_X:36

for V being RealLinearSpace
for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A

proof end;

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

proof end;