:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received August 17, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

reconsider z0 = 0 as Real ;

deffunc H

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)

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)

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)

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;

ex b_{1} being Linear_Combination of V st

for v being VECTOR of V holds b_{1} . v = i * (L . v)

for b_{1}, b_{2} being Linear_Combination of V st ( for v being VECTOR of V holds b_{1} . v = i * (L . v) ) & ( for v being VECTOR of V holds b_{2} . v = i * (L . v) ) holds

b_{1} = b_{2}

end;
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 for v being VECTOR of V holds it . v = i * (L . v);

ex b

for v being VECTOR of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines * RLVECT_X:def 1 :

for V being RealLinearSpace

for i being Integer

for L, b_{4} being Linear_Combination of V holds

( b_{4} = i * L iff for v being VECTOR of V holds b_{4} . v = i * (L . v) );

for V being RealLinearSpace

for i being Integer

for L, b

( b

definition

let V be RealLinearSpace;

let A be Subset of V;

coherence

{ (Sum l) where l is Linear_Combination of A : rng l c= INT } is Subset of V;

end;
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 { (Sum l) where l is Linear_Combination of A : rng l c= INT } ;

coherence

{ (Sum l) where l is Linear_Combination of A : rng l c= INT } is Subset of V;

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

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

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

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

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

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

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

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 )

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

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

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

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

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

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

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;

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;

ex b_{1} being FinSequence st

( b_{1} is n -element & b_{1} is D -valued )

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

( b

proof end;

definition

let RS be RealLinearSpace;

let f be FinSequence of RS;

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;

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

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;

:: 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_{2} -element FinSequence of RS : ex a being INT -valued len b_{2} -element FinSequence st

for i being Nat st i in Seg (len f) holds

g /. i = (a . i) * (f /. i) } ;

for RS being RealLinearSpace

for f being FinSequence of RS holds Z_Lin f = { (Sum g) where g is len b

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_{2} -element FinSequence of RS ex a being INT -valued len b_{2} -element FinSequence st

( x = Sum g & ( for i being Nat st i in Seg (len f) holds

g /. i = (a . i) * (f /. i) ) ) )

for f being FinSequence of RS

for x being set holds

( x in Z_Lin f iff ex g being len b

( 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

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

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

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

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

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

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;