:: by Wojciech A. Trybulec

::

:: Received July 24, 1989

:: Copyright (c) 1990-2018 Association of Mizar Users

definition

attr c_{1} is strict ;

struct RLSStruct -> addLoopStr ;

aggr RLSStruct(# carrier, ZeroF, addF, Mult #) -> RLSStruct ;

sel Mult c_{1} -> Function of [:REAL, the carrier of c_{1}:], the carrier of c_{1};

end;
struct RLSStruct -> addLoopStr ;

aggr RLSStruct(# carrier, ZeroF, addF, Mult #) -> RLSStruct ;

sel Mult c

definition

let V be non empty RLSStruct ;

let v be VECTOR of V;

let a be Real;

coherence

the Mult of V . (a,v) is Element of V

end;
let v be VECTOR of V;

let a be Real;

coherence

the Mult of V . (a,v) is Element of V

proof end;

:: deftheorem defines * RLVECT_1:def 1 :

for V being non empty RLSStruct

for v being VECTOR of V

for a being Real holds a * v = the Mult of V . (a,v);

for V being non empty RLSStruct

for v being VECTOR of V

for a being Real holds a * v = the Mult of V . (a,v);

:: Definitional theorems of zero element, addition, multiplication.

theorem :: RLVECT_1:2

registration

let ZS be non empty set ;

let O be Element of ZS;

let F be BinOp of ZS;

let G be Function of [:REAL,ZS:],ZS;

coherence

not RLSStruct(# ZS,O,F,G #) is empty ;

end;
let O be Element of ZS;

let F be BinOp of ZS;

let G be Function of [:REAL,ZS:],ZS;

coherence

not RLSStruct(# ZS,O,F,G #) is empty ;

definition

let IT be addMagma ;

end;
attr IT is add-associative means :Def3: :: RLVECT_1:def 3

for u, v, w being Element of IT holds (u + v) + w = u + (v + w);

for u, v, w being Element of IT holds (u + v) + w = u + (v + w);

:: deftheorem Def2 defines Abelian RLVECT_1:def 2 :

for IT being addMagma holds

( IT is Abelian iff for v, w being Element of IT holds v + w = w + v );

for IT being addMagma holds

( IT is Abelian iff for v, w being Element of IT holds v + w = w + v );

:: deftheorem Def3 defines add-associative RLVECT_1:def 3 :

for IT being addMagma holds

( IT is add-associative iff for u, v, w being Element of IT holds (u + v) + w = u + (v + w) );

for IT being addMagma holds

( IT is add-associative iff for u, v, w being Element of IT holds (u + v) + w = u + (v + w) );

definition

let IT be addLoopStr ;

end;
attr IT is right_zeroed means :Def4: :: RLVECT_1:def 4

for v being Element of IT holds v + (0. IT) = v;

for v being Element of IT holds v + (0. IT) = v;

:: deftheorem Def4 defines right_zeroed RLVECT_1:def 4 :

for IT being addLoopStr holds

( IT is right_zeroed iff for v being Element of IT holds v + (0. IT) = v );

for IT being addLoopStr holds

( IT is right_zeroed iff for v being Element of IT holds v + (0. IT) = v );

definition

let IT be non empty RLSStruct ;

end;
attr IT is vector-distributive means :Def5: :: RLVECT_1:def 5

for a being Real

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);

for a being Real

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);

attr IT is scalar-distributive means :Def6: :: RLVECT_1:def 6

for a, b being Real

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);

for a, b being Real

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);

attr IT is scalar-associative means :Def7: :: RLVECT_1:def 7

for a, b being Real

for v being VECTOR of IT holds (a * b) * v = a * (b * v);

for a, b being Real

for v being VECTOR of IT holds (a * b) * v = a * (b * v);

:: deftheorem Def5 defines vector-distributive RLVECT_1:def 5 :

for IT being non empty RLSStruct holds

( IT is vector-distributive iff for a being Real

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

for IT being non empty RLSStruct holds

( IT is vector-distributive iff for a being Real

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

:: deftheorem Def6 defines scalar-distributive RLVECT_1:def 6 :

for IT being non empty RLSStruct holds

( IT is scalar-distributive iff for a, b being Real

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

for IT being non empty RLSStruct holds

( IT is scalar-distributive iff for a, b being Real

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

:: deftheorem Def7 defines scalar-associative RLVECT_1:def 7 :

for IT being non empty RLSStruct holds

( IT is scalar-associative iff for a, b being Real

for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

for IT being non empty RLSStruct holds

( IT is scalar-associative iff for a, b being Real

for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

:: deftheorem Def8 defines scalar-unital RLVECT_1:def 8 :

for IT being non empty RLSStruct holds

( IT is scalar-unital iff for v being VECTOR of IT holds 1 * v = v );

for IT being non empty RLSStruct holds

( IT is scalar-unital iff for v being VECTOR of IT holds 1 * v = v );

definition

RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #) is strict RLSStruct ;

end;

func Trivial-RLSStruct -> strict RLSStruct equals :: RLVECT_1:def 9

RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #);

coherence RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #);

RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #) is strict RLSStruct ;

:: deftheorem defines Trivial-RLSStruct RLVECT_1:def 9 :

Trivial-RLSStruct = RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #);

Trivial-RLSStruct = RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #);

registration
end;

registration

existence

ex b_{1} being addMagma st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

existence

ex b_{1} being addLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

ex b_{1} being non empty RLSStruct st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is scalar-distributive & b_{1} is vector-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital )
end;

cluster non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital for RLSStruct ;

existence ex b

( b

proof end;

definition

mode RealLinearSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;

end;
definition

let V be Abelian addMagma ;

let v, w be Element of V;

:: original: +

redefine func v + w -> Element of the carrier of V;

commutativity

for v, w being Element of V holds v + w = w + v by Def2;

end;
let v, w be Element of V;

:: original: +

redefine func v + w -> Element of the carrier of V;

commutativity

for v, w being Element of V holds v + w = w + v by Def2;

Lm1: for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V st v + w = 0. V holds

w + v = 0. V

proof end;

theorem Th3: :: RLVECT_1:3

for V being right_complementable add-associative right_zeroed addLoopStr holds V is right_add-cancelable

proof end;

theorem Th4: :: RLVECT_1:4

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds

( v + (0. V) = v & (0. V) + v = v )

for v being Element of V holds

( v + (0. V) = v & (0. V) + v = v )

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed addLoopStr ;

let v1 be zero Element of V;

let v2 be Element of V;

reducibility

v1 + v2 = v2

v2 + v1 = v2

end;
let v1 be zero Element of V;

let v2 be Element of V;

reducibility

v1 + v2 = v2

proof end;

reducibility v2 + v1 = v2

proof end;

:: Definitions of reverse element to the vector and of

:: subtraction of vectors.

:: subtraction of vectors.

definition

let V be non empty addLoopStr ;

let v be Element of V;

assume A1: ( V is add-associative & V is right_zeroed & V is right_complementable ) ;

compatibility

for b_{1} being Element of the carrier of V holds

( b_{1} = - v iff v + b_{1} = 0. V )

end;
let v be Element of V;

assume A1: ( V is add-associative & V is right_zeroed & V is right_complementable ) ;

compatibility

for b

( b

proof end;

:: deftheorem Def10 defines - RLVECT_1:def 10 :

for V being non empty addLoopStr

for v being Element of V st V is add-associative & V is right_zeroed & V is right_complementable holds

for b_{3} being Element of the carrier of V holds

( b_{3} = - v iff v + b_{3} = 0. V );

for V being non empty addLoopStr

for v being Element of V st V is add-associative & V is right_zeroed & V is right_complementable holds

for b

( b

Lm2: for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u being Element of V ex w being Element of V st v + w = u

proof end;

definition

let V be addLoopStr ;

let v, w be Element of V;

correctness

compatibility

for b_{1} being Element of the carrier of V holds

( b_{1} = v - w iff b_{1} = v + (- w) );

;

end;
let v, w be Element of V;

correctness

compatibility

for b

( b

;

:: deftheorem defines - RLVECT_1:def 11 :

for V being addLoopStr

for v, w being Element of V holds v - w = v + (- w);

for V being addLoopStr

for v, w being Element of V holds v - w = v + (- w);

:: Definitional theorems of reverse element and substraction.

theorem Th5: :: RLVECT_1:5

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds

( v + (- v) = 0. V & (- v) + v = 0. V )

for v being Element of V holds

( v + (- v) = 0. V & (- v) + v = 0. V )

proof end;

theorem Th6: :: RLVECT_1:6

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V st v + w = 0. V holds

v = - w

for v, w being Element of V st v + w = 0. V holds

v = - w

proof end;

theorem :: RLVECT_1:7

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u being Element of V ex w being Element of V st v + w = u by Lm2;

for v, u being Element of V ex w being Element of V st v + w = u by Lm2;

theorem Th8: :: RLVECT_1:8

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for w, u, v1, v2 being Element of V st ( w + v1 = w + v2 or v1 + w = v2 + w ) holds

v1 = v2

for w, u, v1, v2 being Element of V st ( w + v1 = w + v2 or v1 + w = v2 + w ) holds

v1 = v2

proof end;

theorem :: RLVECT_1:9

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V st ( v + w = v or w + v = v ) holds

w = 0. V

for v, w being Element of V st ( v + w = v or w + v = v ) holds

w = 0. V

proof end;

theorem Th10: :: RLVECT_1:10

for a being Real

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for v being Element of V st ( a = 0 or v = 0. V ) holds

a * v = 0. V

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for v being Element of V st ( a = 0 or v = 0. V ) holds

a * v = 0. V

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct ;

let v be zero Element of V;

let r be Real;

reducibility

r * v = v

end;
let v be zero Element of V;

let r be Real;

reducibility

r * v = v

proof end;

theorem Th11: :: RLVECT_1:11

for a being Real

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds

( not a * v = 0. V or a = 0 or v = 0. V )

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds

( not a * v = 0. V or a = 0 or v = 0. V )

proof end;

theorem Th12: :: RLVECT_1:12

for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0. V) = 0. V

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed addLoopStr ;

let v be zero Element of V;

reducibility

- v = v

end;
let v be zero Element of V;

reducibility

- v = v

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed addLoopStr ;

let v1 be Element of V;

let v2 be zero Element of V;

reducibility

v1 - v2 = v1 ;

end;
let v1 be Element of V;

let v2 be zero Element of V;

reducibility

v1 - v2 = v1 ;

theorem :: RLVECT_1:13

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds v - (0. V) = v ;

for v being Element of V holds v - (0. V) = v ;

theorem :: RLVECT_1:14

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds (0. V) - v = - v ;

for v being Element of V holds (0. V) - v = - v ;

theorem :: RLVECT_1:15

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds v - v = 0. V by Def10;

for v being Element of V holds v - v = 0. V by Def10;

theorem Th16: :: RLVECT_1:16

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for v being Element of V holds - v = (- 1) * v

for v being Element of V holds - v = (- 1) * v

proof end;

registration

let V be non empty right_complementable add-associative right_zeroed addLoopStr ;

let v be Element of V;

reducibility

- (- v) = v

end;
let v be Element of V;

reducibility

- (- v) = v

proof end;

theorem :: RLVECT_1:17

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds - (- v) = v ;

for v being Element of V holds - (- v) = v ;

theorem Th18: :: RLVECT_1:18

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V st - v = - w holds

v = w

for v, w being Element of V st - v = - w holds

v = w

proof end;

theorem Th19: :: RLVECT_1:19

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V st v = - v holds

v = 0. V

for v being Element of V st v = - v holds

v = 0. V

proof end;

theorem :: RLVECT_1:20

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V st v + v = 0. V holds

v = 0. V

for v being Element of V st v + v = 0. V holds

v = 0. V

proof end;

theorem Th21: :: RLVECT_1:21

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V st v - w = 0. V holds

v = w

for v, w being Element of V st v - w = 0. V holds

v = w

proof end;

theorem :: RLVECT_1:22

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for u, v being Element of V ex w being Element of V st v - w = u

for u, v being Element of V ex w being Element of V st v - w = u

proof end;

theorem :: RLVECT_1:23

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for w, v1, v2 being Element of V st w - v1 = w - v2 holds

v1 = v2

for w, v1, v2 being Element of V st w - v1 = w - v2 holds

v1 = v2

proof end;

theorem Th24: :: RLVECT_1:24

for a being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds a * (- v) = (- a) * v

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds a * (- v) = (- a) * v

proof end;

theorem Th25: :: RLVECT_1:25

for a being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds a * (- v) = - (a * v)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds a * (- v) = - (a * v)

proof end;

theorem :: RLVECT_1:26

for a being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds (- a) * (- v) = a * v

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds (- a) * (- v) = a * v

proof end;

Lm3: for V being non empty right_complementable add-associative right_zeroed addLoopStr

for u, w being Element of V holds - (u + w) = (- w) + (- u)

proof end;

theorem Th27: :: RLVECT_1:27

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds v - (u + w) = (v - w) - u

for v, u, w being Element of V holds v - (u + w) = (v - w) - u

proof end;

theorem :: RLVECT_1:28

for V being non empty add-associative addLoopStr

for v, u, w being Element of V holds (v + u) - w = v + (u - w) by Def3;

for v, u, w being Element of V holds (v + u) - w = v + (u - w) by Def3;

theorem :: RLVECT_1:29

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds v - (u - w) = (v - u) + w

for v, u, w being Element of V holds v - (u - w) = (v - u) + w

proof end;

theorem Th30: :: RLVECT_1:30

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds - (v + w) = (- w) - v

for v, w being Element of V holds - (v + w) = (- w) - v

proof end;

theorem :: RLVECT_1:31

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds - (v + w) = (- w) + (- v) by Lm3;

for v, w being Element of V holds - (v + w) = (- w) + (- v) by Lm3;

theorem :: RLVECT_1:32

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, w being Element of V holds (- v) - w = (- w) - v

for v, w being Element of V holds (- v) - w = (- w) - v

proof end;

theorem :: RLVECT_1:33

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds - (v - w) = w + (- v)

for v, w being Element of V holds - (v - w) = w + (- v)

proof end;

theorem Th34: :: RLVECT_1:34

for a being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v, w being Element of V holds a * (v - w) = (a * v) - (a * w)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v, w being Element of V holds a * (v - w) = (a * v) - (a * w)

proof end;

theorem Th35: :: RLVECT_1:35

for a, b being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds (a - b) * v = (a * v) - (b * v)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds (a - b) * v = (a * v) - (b * v)

proof end;

theorem :: RLVECT_1:36

for a being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v, w being Element of V st a <> 0 & a * v = a * w holds

v = w

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v, w being Element of V st a <> 0 & a * v = a * w holds

v = w

proof end;

theorem :: RLVECT_1:37

for a, b being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V st v <> 0. V & a * v = b * v holds

a = b

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V st v <> 0. V & a * v = b * v holds

a = b

proof end;

definition

let V be non empty addLoopStr ;

let F be the carrier of V -valued FinSequence;

ex b_{1} being Element of V ex f being sequence of V st

( b_{1} = f . (len F) & f . 0 = 0. V & ( for j being Nat

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) )

for b_{1}, b_{2} being Element of V st ex f being sequence of V st

( b_{1} = f . (len F) & f . 0 = 0. V & ( for j being Nat

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) & ex f being sequence of V st

( b_{2} = f . (len F) & f . 0 = 0. V & ( for j being Nat

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) holds

b_{1} = b_{2}

end;
let F be the carrier of V -valued FinSequence;

func Sum F -> Element of V means :Def12: :: RLVECT_1:def 12

ex f being sequence of V st

( it = f . (len F) & f . 0 = 0. V & ( for j being Nat

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) );

existence ex f being sequence of V st

( it = f . (len F) & f . 0 = 0. V & ( for j being Nat

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) );

ex b

( b

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) )

proof end;

uniqueness for b

( b

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) & ex f being sequence of V st

( b

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) holds

b

proof end;

:: deftheorem Def12 defines Sum RLVECT_1:def 12 :

for V being non empty addLoopStr

for F being the carrier of b_{1} -valued FinSequence

for b_{3} being Element of V holds

( b_{3} = Sum F iff ex f being sequence of V st

( b_{3} = f . (len F) & f . 0 = 0. V & ( for j being Nat

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) );

for V being non empty addLoopStr

for F being the carrier of b

for b

( b

( b

for v being Element of V st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) );

Lm4: for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V

proof end;

Lm5: for V being non empty addLoopStr

for F being FinSequence-like PartFunc of NAT,V st len F = 0 holds

Sum F = 0. V

proof end;

theorem Th38: :: RLVECT_1:38

for V being non empty addLoopStr

for v being Element of V

for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds

Sum F = (Sum G) + v

for v being Element of V

for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds

Sum F = (Sum G) + v

proof end;

theorem :: RLVECT_1:39

for a being Real

for V being RealLinearSpace

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being VECTOR of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

for V being RealLinearSpace

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being VECTOR of V st k in dom F & v = G . k holds

F . k = a * v ) holds

Sum F = a * (Sum G)

proof end;

theorem :: RLVECT_1:40

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = - v ) holds

Sum F = - (Sum G)

for F, G being FinSequence of V st len F = len G & ( for k being Nat

for v being Element of V st k in dom F & v = G . k holds

F . k = - v ) holds

Sum F = - (Sum G)

proof end;

theorem Th41: :: RLVECT_1:41

for V being non empty add-associative right_zeroed addLoopStr

for F, G being FinSequence of V holds Sum (F ^ G) = (Sum F) + (Sum G)

for F, G being FinSequence of V holds Sum (F ^ G) = (Sum F) + (Sum G)

proof end;

Lm6: for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds Sum <*v*> = v

proof end;

theorem :: RLVECT_1:42

for V being non empty Abelian add-associative right_zeroed addLoopStr

for F, G being FinSequence of V st rng F = rng G & F is one-to-one & G is one-to-one holds

Sum F = Sum G

for F, G being FinSequence of V st rng F = rng G & F is one-to-one & G is one-to-one holds

Sum F = Sum G

proof end;

theorem :: RLVECT_1:43

theorem :: RLVECT_1:44

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds Sum <*v*> = v by Lm6;

for v being Element of V holds Sum <*v*> = v by Lm6;

theorem Th45: :: RLVECT_1:45

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u being Element of V holds Sum <*v,u*> = v + u

for v, u being Element of V holds Sum <*v,u*> = v + u

proof end;

theorem Th46: :: RLVECT_1:46

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*v,u,w*> = (v + u) + w

for v, u, w being Element of V holds Sum <*v,u,w*> = (v + u) + w

proof end;

theorem :: RLVECT_1:47

theorem :: RLVECT_1:48

for V being RealLinearSpace

for a being Real

for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

for a being Real

for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

proof end;

theorem :: RLVECT_1:49

for V being RealLinearSpace

for a being Real

for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

for a being Real

for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

proof end;

theorem :: RLVECT_1:50

for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V

proof end;

theorem :: RLVECT_1:51

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds - (Sum <*v*>) = - v by Lm6;

for v being Element of V holds - (Sum <*v*>) = - v by Lm6;

theorem :: RLVECT_1:52

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u

for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u

proof end;

theorem :: RLVECT_1:53

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w

for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w

proof end;

theorem Th54: :: RLVECT_1:54

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, w being Element of V holds Sum <*v,w*> = Sum <*w,v*>

for v, w being Element of V holds Sum <*v,w*> = Sum <*w,v*>

proof end;

theorem :: RLVECT_1:55

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)

for v, w being Element of V holds Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)

proof end;

::$CT

theorem :: RLVECT_1:57

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds

( Sum <*(0. V),v*> = v & Sum <*v,(0. V)*> = v )

for v being Element of V holds

( Sum <*(0. V),v*> = v & Sum <*v,(0. V)*> = v )

proof end;

theorem :: RLVECT_1:58

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds

( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )

for v being Element of V holds

( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )

proof end;

theorem :: RLVECT_1:59

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds Sum <*v,(- w)*> = v - w by Th45;

for v, w being Element of V holds Sum <*v,(- w)*> = v - w by Th45;

theorem Th59: :: RLVECT_1:60

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds Sum <*(- v),(- w)*> = - (w + v)

for v, w being Element of V holds Sum <*(- v),(- w)*> = - (w + v)

proof end;

theorem :: RLVECT_1:63

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>)

for v, u, w being Element of V holds Sum <*u,v,w*> = ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>)

proof end;

theorem :: RLVECT_1:64

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,v*>) + w

for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,v*>) + w

proof end;

theorem :: RLVECT_1:65

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*v,w*>) + u

for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*v,w*>) + u

proof end;

theorem Th65: :: RLVECT_1:66

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,w*>) + v

for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,w*>) + v

proof end;

theorem Th66: :: RLVECT_1:67

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*u,w,v*>

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*u,w,v*>

proof end;

theorem Th67: :: RLVECT_1:68

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,u,w*>

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,u,w*>

proof end;

theorem Th68: :: RLVECT_1:69

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,w,u*>

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,w,u*>

proof end;

theorem :: RLVECT_1:70

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*w,v,u*>

for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*w,v,u*>

proof end;

::$CT

theorem :: RLVECT_1:72

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds

( Sum <*(0. V),(0. V),v*> = v & Sum <*(0. V),v,(0. V)*> = v & Sum <*v,(0. V),(0. V)*> = v )

for v being Element of V holds

( Sum <*(0. V),(0. V),v*> = v & Sum <*(0. V),v,(0. V)*> = v & Sum <*v,(0. V),(0. V)*> = v )

proof end;

theorem :: RLVECT_1:73

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, u being Element of V holds

( Sum <*(0. V),u,v*> = u + v & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )

for v, u being Element of V holds

( Sum <*(0. V),u,v*> = u + v & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )

proof end;

theorem :: RLVECT_1:75

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of V st len F = 0 holds

Sum F = 0. V by Lm5;

for F being FinSequence of V st len F = 0 holds

Sum F = 0. V by Lm5;

theorem :: RLVECT_1:76

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of V st len F = 1 holds

Sum F = F . 1

for F being FinSequence of V st len F = 1 holds

Sum F = F . 1

proof end;

theorem :: RLVECT_1:77

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of V

for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds

Sum F = v1 + v2

for F being FinSequence of V

for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds

Sum F = v1 + v2

proof end;

theorem :: RLVECT_1:78

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of V

for v, v1, v2 being Element of V st len F = 3 & v1 = F . 1 & v2 = F . 2 & v = F . 3 holds

Sum F = (v1 + v2) + v

for F being FinSequence of V

for v, v1, v2 being Element of V st len F = 3 & v1 = F . 1 & v2 = F . 2 & v = F . 3 holds

Sum F = (v1 + v2) + v

proof end;

:: deftheorem defines zeroed RLVECT_1:def 13 :

for L being non empty addLoopStr holds

( L is zeroed iff for a being Element of L holds

( a + (0. L) = a & (0. L) + a = a ) );

for L being non empty addLoopStr holds

( L is zeroed iff for a being Element of L holds

( a + (0. L) = a & (0. L) + a = a ) );

registration
end;

registration

coherence

for b_{1} being non empty addLoopStr st b_{1} is Abelian & b_{1} is right_zeroed holds

b_{1} is zeroed

for b_{1} being non empty addLoopStr st b_{1} is Abelian & b_{1} is right_complementable holds

b_{1} is left_complementable

end;
for b

b

proof end;

coherence for b

b

proof end;

:: missing, 2009.02.14, A.T.

theorem :: RLVECT_1:79

for a being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds (- a) * v = - (a * v)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for v being Element of V holds (- a) * v = - (a * v)

proof end;

theorem :: RLVECT_1:80

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V

proof end;

theorem :: RLVECT_1:81

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u

for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u

proof end;

theorem :: RLVECT_1:82

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w

for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w

proof end;

theorem :: RLVECT_1:83

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v being Element of V holds

( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )

for v being Element of V holds

( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )

proof end;

theorem :: RLVECT_1:84

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, w being Element of V holds

( Sum <*v,(- w)*> = v - w & Sum <*(- w),v*> = v - w )

for v, w being Element of V holds

( Sum <*v,(- w)*> = v - w & Sum <*(- w),v*> = v - w )

proof end;

theorem :: RLVECT_1:85

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for v, w being Element of V holds

( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )

for v, w being Element of V holds

( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )

proof end;