:: Vectors in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1,
ZFMISC_1, XBOOLE_0, RELAT_1, REAL_1, ARYTM_3, SUPINF_2, FUNCT_5, MCART_1,
ARYTM_1, CARD_1, FINSEQ_1, ORDINAL4, CARD_3, TARSKI, XXREAL_0, FUNCOP_1,
NAT_1, VALUED_0, RLVECT_1, PARTFUN1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1,
FUNCOP_1, REAL_1, FINSEQ_1, NAT_1, FUNCT_3, FUNCT_5, FINSEQ_4, STRUCT_0,
ALGSTR_0;
constructors BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, FINSEQ_1, FUNCT_3,
FUNCT_5, ALGSTR_0, REALSET1, RELSET_1, FINSEQ_4, VALUED_0, XREAL_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, RELAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, TARSKI, STRUCT_0, ALGSTR_0;
equalities RELAT_1, ALGSTR_0;
expansions FUNCT_1, STRUCT_0;
theorems FUNCT_1, NAT_1, TARSKI, RELAT_1, STRUCT_0, XBOOLE_0, XBOOLE_1,
FINSEQ_1, XCMPLX_0, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, ALGSTR_0,
FINSEQ_3, XREAL_0;
schemes FINSEQ_1, FUNCT_2, NAT_1;
begin
definition
struct (addLoopStr) RLSStruct (# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier,
Mult -> Function of [:REAL, the carrier :], the carrier #);
end;
registration
cluster non empty for RLSStruct;
existence
proof
set ZS = the non empty set,O = the Element of ZS,F = the BinOp of ZS,G =the
Function of [:REAL,ZS:],ZS;
take RLSStruct(#ZS,O,F,G#);
thus the carrier of RLSStruct(#ZS,O,F,G#) is non empty;
end;
end;
reserve V for non empty RLSStruct;
reserve x,y,y1 for set;
definition
let V be RLSStruct;
mode VECTOR of V is Element of V;
end;
theorem
for V being non empty 1-sorted, v being Element of V holds v in V;
:: Definitons of functions on the Elements of the carrier of
:: Real Linear Space structure, i.e. zero element, addition of two
:: elements, and multiplication of the element by a real number.
reserve v for VECTOR of V;
reserve a,b for Real;
definition
let V,v;
let a be Real;
func a * v -> Element of V equals
(the Mult of V).(a,v);
coherence
proof
reconsider a as Element of REAL by XREAL_0:def 1;
(the Mult of V).(a,v) is Element of V;
hence thesis;
end;
end;
:: Definitional theorems of zero element, addition, multiplication.
theorem
for V being non empty addMagma, v,w being Element of V holds
v + w = (the addF of V).(v,w);
registration
let ZS be non empty set, O be Element of ZS, F be BinOp of ZS, G be Function
of [:REAL,ZS:],ZS;
cluster RLSStruct (# ZS,O,F,G #) -> non empty;
coherence;
end;
definition
let IT be addMagma;
attr IT is Abelian means
:Def2:
for v,w being Element of IT holds v + w = w + v;
attr IT is add-associative means
:Def3:
for u,v,w being Element of IT holds (u + v) + w = u + (v + w);
end;
definition
let IT be addLoopStr;
attr IT is right_zeroed means
:Def4: for v being Element of IT holds v + 0.IT = v;
end;
definition
let IT be non empty RLSStruct;
attr IT is vector-distributive means
:Def5: for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w;
attr IT is scalar-distributive means
:Def6: for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v;
attr IT is scalar-associative means
:Def7: for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attr IT is scalar-unital means
:Def8: for v being VECTOR of IT holds 1 * v = v;
end;
definition
func Trivial-RLSStruct -> strict RLSStruct equals
RLSStruct(#{0},op0,op2,pr2(REAL,{0})#);
coherence;
end;
registration
cluster Trivial-RLSStruct -> 1-element;
coherence;
end;
registration
cluster strict Abelian add-associative non empty for addMagma;
existence
proof
take S = Trivial-addMagma;
thus S is strict;
thus S is Abelian
by STRUCT_0:def 10;
thus S is add-associative
by STRUCT_0:def 10;
thus thesis;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
non empty for addLoopStr;
existence
proof
take S = Trivial-addLoopStr;
thus S is strict;
thus S is Abelian
by STRUCT_0:def 10;
thus S is add-associative
by STRUCT_0:def 10;
thus S is right_zeroed
by STRUCT_0:def 10;
thus thesis;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative scalar-unital
for non empty RLSStruct;
existence
proof
take S = Trivial-RLSStruct;
thus S is strict;
thus S is Abelian
by STRUCT_0:def 10;
thus S is add-associative
by STRUCT_0:def 10;
thus S is right_zeroed
by STRUCT_0:def 10;
thus S is right_complementable
proof
let x be Element of S;
take x;
thus thesis by STRUCT_0:def 10;
end;
thus for a,b for v being VECTOR of S holds (a + b) * v = a * v + b * v by
STRUCT_0:def 10;
thus for a for v,w being VECTOR of S holds a * (v + w) = a * v + a * w by
STRUCT_0:def 10;
thus for a,b for v being VECTOR of S holds (a * b) * v = a * (b * v) by
STRUCT_0:def 10;
thus for v being VECTOR of S holds 1 * v = v by STRUCT_0:def 10;
end;
end;
definition
mode RealLinearSpace is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty RLSStruct;
end;
definition
let V be Abelian addMagma, v,w be Element of V;
redefine func v + w; :: redefines + (ALGSTR_0, definition)
commutativity by Def2;
end;
:: Axioms of real linear space.
Lm1: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, v,w being Element of V st v + w = 0.V holds w + v = 0.V
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,w be Element of V;
assume
A1: v + w = 0.V;
consider u being Element of V such that
A2: w + u = 0.V by ALGSTR_0:def 11;
w + v = w + (v + (w + u)) by A2,Def4
.= w + (v + w + u) by Def3
.= w + (v + w) + u by Def3
.= w + u by A1,Def4;
hence thesis by A2;
end;
theorem Th3:
for V being add-associative right_zeroed right_complementable
addLoopStr holds V is right_add-cancelable
proof
let V being add-associative right_zeroed right_complementable addLoopStr;
let v being Element of V;
consider v1 being Element of V such that
A1: v + v1 = 0.V by ALGSTR_0:def 11;
let u, w be Element of V;
assume
A2: u + v = w + v;
thus u = u + 0.V by Def4
.= u + v + v1 by A1,Def3
.= w + 0.V by A1,A2,Def3
.= w by Def4;
end;
theorem Th4:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds v + 0.V = v & 0.V + v = v
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v be Element of V;
consider w being Element of V such that
A1: v + w = 0.V by ALGSTR_0:def 11;
thus
A2: v + 0.V = v by Def4;
w + v = 0.V by A1,Lm1;
hence thesis by A2,A1,Def3;
end;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v1 be zero Element of V;
let v2 be Element of V;
reduce v1 + v2 to v2;
reducibility
proof
v1 = 0.V by STRUCT_0:def 12;
hence thesis by Th4;
end;
reduce v2 + v1 to v2;
reducibility
proof
v1 = 0.V by STRUCT_0:def 12;
hence thesis by Th4;
end;
end;
:: Definitions of reverse element to the vector and of
:: subtraction of vectors.
definition
let V be non empty addLoopStr;
let v be Element of V;
assume
A1: V is add-associative right_zeroed right_complementable;
redefine func - v means :: redefines - (ALGSTR_0, definition)
:Def10:
v + it = 0.V;
compatibility
proof
let IT be Element of V;
consider v1 being Element of V such that
A2: v + v1 = 0.V by A1,ALGSTR_0:def 11;
A3: V is right_add-cancelable by A1,Th3;
A4: v is left_complementable
proof
take v1;
v1 + v + v1 = v1 + 0.V by A1,A2
.= 0.V + v1 by A1;
hence thesis by A3,ALGSTR_0:def 4;
end;
v + -v + v = v + (-v + v) by A1
.= v + 0.V by A3,A4,ALGSTR_0:def 13
.= 0.V + v by A1;
hence IT = -v implies v + IT = 0.V by A3,ALGSTR_0:def 4;
assume
A5: v + IT = 0.V;
thus IT = 0.V + IT by A1
.= -v + v + IT by A3,A4,ALGSTR_0:def 13
.= -v + 0.V by A1,A5
.= -v by A1;
end;
end;
Lm2: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, v,u being Element of V ex w being Element of V st v + w = u
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,u be Element of V;
take w = (- v) + u;
thus v + w = (v + (- v)) + u by Def3
.= 0.V + u by Def10
.= u;
end;
definition
let V be addLoopStr;
let v,w be Element of V;
redefine func v - w equals :: redefines - (ALGSTR_0, definition)
v + (- w);
correctness;
end;
:: Definitional theorems of reverse element and substraction.
theorem Th5:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds v + -v = 0.V & -v + v = 0.V
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v be Element of V;
thus v + -v = 0.V by Def10;
hence thesis by Lm1;
end;
theorem Th6:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds v + w = 0.V implies v = - w
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,w be Element of V;
assume v + w = 0.V;
then w + v = 0.V by Lm1;
hence thesis by Def10;
end;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,u being Element of V ex w being Element of V st v + w = u
by Lm2;
theorem Th8:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, w,u,v1,v2 being Element of V st
w + v1 = w + v2 or v1 + w = v2 + w holds v1 = v2
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let w,u,v1,v2 be Element of V;
A1: now
assume
A2: v1 + w = v2 + w;
thus v1 = v1 + 0.V
.= v1 + (w + -w) by Th5
.= v1 + w + -w by Def3
.= v2 + (w + -w) by A2,Def3
.= v2 + 0.V by Th5
.= v2;
end;
now
assume
A3: w + v1 = w + v2;
thus v1 = 0.V + v1
.= -w + w + v1 by Th5
.= -w + (w + v1) by Def3
.= -w + w + v2 by A3,Def3
.= 0.V + v2 by Th5
.= v2;
end;
hence thesis by A1;
end;
theorem
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
v + w = v or w + v = v implies w = 0.V
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,w be Element of V;
assume v + w = v or w + v = v;
then v + w = v + 0.V or w + v = 0.V + v;
hence thesis by Th8;
end;
theorem Th10:
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-unital vector-distributive non empty RLSStruct,
v being Element of V holds
a = 0 or v = 0.V implies a * v = 0.V
proof
let V be add-associative right_zeroed right_complementable
scalar-distributive scalar-unital vector-distributive non empty RLSStruct,
v be Element of V;
assume a = 0 or v = 0.V;
then per cases;
suppose
A1: a = 0;
v + 0 * v = 1 * v + 0 * v by Def8
.= (1 + 0) * v by Def6
.= v + 0.V by Def8;
hence thesis by A1,Th8;
end;
suppose
A2: v = 0.V;
a * 0.V + a * 0.V = a * (0.V + 0.V) by Def5
.= a * 0.V + 0.V;
hence thesis by A2,Th8;
end;
end;
registration
let V be add-associative right_zeroed right_complementable
scalar-distributive scalar-unital vector-distributive non empty RLSStruct;
let v be zero Element of V;
let r be Real;
reduce r * v to v;
reducibility
proof
v = 0.V by STRUCT_0:def 12;
hence thesis by Th10;
end;
end;
theorem Th11:
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
a * v = 0.V implies a = 0 or v = 0.V
proof
let V be add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
assume that
A1: a * v = 0.V and
A2: a <> 0;
thus v = 1 * v by Def8
.= (a" * a) * v by A2,XCMPLX_0:def 7
.= a" * 0.V by A1,Def7
.= 0.V;
end;
theorem Th12:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr holds - 0.V = 0.V
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
thus 0.V = 0.V + (- 0.V) by Def10
.= - 0.V;
end;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v be zero Element of V;
reduce - v to v;
reducibility
proof
v = 0.V by STRUCT_0:def 12;
hence thesis by Th12;
end;
end;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v1 be Element of V;
let v2 be zero Element of V;
reduce v1 - v2 to v1;
reducibility;
end;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds v - 0.V = v;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds 0.V - v = - v;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds v - v = 0.V by Def10;
theorem Th16:
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital vector-distributive non empty RLSStruct,
v being Element of V holds
- v = (- 1) * v
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital vector-distributive non empty RLSStruct,
v be Element of V;
v + (- 1) * v = 1 * v + (- 1) * v by Def8
.= (1 + (- 1)) * v by Def6
.= 0.V by Th10;
hence (- v) = (- v) + (v + (- 1) * v)
.= ((- v) + v) + (- 1) * v by Def3
.= 0.V + (- 1) * v by Def10
.= (- 1) * v;
end;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v be Element of V;
reduce --v to v;
reducibility
proof
v + -v = 0.V by Def10;
hence thesis by Th6;
end;
end;
theorem
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds --v = v;
theorem Th18:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds - v = - w implies v = w
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,w be Element of V;
assume - v = - w;
hence v = - (- w)
.= w;
end;
theorem Th19:
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
v = - v implies v = 0.V
proof
let V be add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
assume v = - v;
then 0.V = v + v by Def10
.= 1 * v + v by Def8
.= 1 * v + 1 * v by Def8
.= (1 + 1) * v by Def6
.= 2 * v;
hence thesis by Th11;
end;
theorem
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
v + v = 0.V implies v = 0.V
proof
let V be add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
assume v + v = 0.V;
then v = - v by Def10;
hence thesis by Th19;
end;
theorem Th21:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds v - w = 0.V implies v = w
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,w be Element of V;
assume v - w = 0.V;
then - v = - w by Def10;
hence thesis by Th18;
end;
theorem
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, u,v being Element of V
ex w being Element of V st v - w = u
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let u,v be Element of V;
consider w being Element of V such that
A1: v + w = u by Lm2;
take - w;
thus thesis by A1;
end;
theorem
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, w,v1,v2 being Element of V st
w - v1 = w - v2 holds v1 = v2
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let w,v1,v2 be Element of V;
assume w - v1 = w - v2;
then - v1 = - v2 by Th8;
hence thesis by Th18;
end;
theorem Th24:
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
a * (- v) = (- a) * v
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
thus a * (- v) = a * ((- 1) * v) by Th16
.= (a *(- 1)) * v by Def7
.= (- a) * v;
end;
theorem Th25:
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
a * (- v) = - (a * v)
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
thus a * (- v) = (- (1 * a)) * v by Th24
.= ((- 1) * a) * v
.= (- 1) * (a * v) by Def7
.= - (a * v) by Th16;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
(- a) * (- v) = a * v
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
thus (- a) * (- v) = (- (- a)) * v by Th24
.= a * v;
end;
Lm3: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, u,w being Element of V holds - (u + w) = -w + -u
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, u,w be Element of V;
u + w + (-w + -u) = u + (w + (-w + -u)) by Def3
.= u + (w + -w + -u) by Def3
.= u + (0.V + -u) by Def10
.= 0.V by Def10;
hence thesis by Def10;
end;
theorem Th27:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
v - (u + w) = (v - w) - u
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,u,w be Element of V;
thus v - (u + w) = v + (-w + -u) by Lm3
.= (v - w) - u by Def3;
end;
theorem
for V being add-associative non empty addLoopStr,
v,u,w being Element of V holds (v + u) - w = v + (u - w) by Def3;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds v - (u - w) = (v -u) + w
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
let v,u,w be Element of V;
thus v - (u - w) = v - (u + - w) .= (v - u) - - w by Th27
.= (v - u) + w;
end;
theorem Th30:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds - (v + w) = (- w) - v
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,w be Element of V;
thus - (v + w) = 0.V - (v + w)
.= (0.V - w) - v by Th27
.= (- w) - v;
end;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,w being Element of V holds - (v + w) = -w + -v by Lm3;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds (- v) - w = (- w) - v
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
let v,w be Element of V;
thus (- v) - w = - (w + v) by Th30
.= (- w) - v by Th30;
end;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,w being Element of V holds - (v - w) = w + (- v)
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr;
let v,w be Element of V;
thus - (v - w) = --w + -v by Lm3
.= w + -v;
end;
theorem Th34:
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v,w being Element of V holds
a * (v - w) = a * v - a * w
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v,w be Element of V;
thus a * (v - w) = a * v + a * (- w) by Def5
.= a * v - a * w by Th25;
end;
theorem Th35:
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
(a - b) * v = a * v - b * v
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
thus (a - b) * v = (a + (- b)) * v .= a * v + (- b) * v by Def6
.= a * v + b * (- v) by Th24
.= a * v - b * v by Th25;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v,w being Element of V holds
a <> 0 & a * v = a * w implies v = w
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v,w be Element of V;
assume that
A1: a <> 0 and
A2: a * v = a * w;
0.V = a * v - a * w by A2,Def10
.= a * (v - w) by Th34;
then v - w = 0.V by A1,Th11;
hence thesis by Th21;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
v <> 0.V & a * v = b * v implies a = b
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
assume that
A1: v <> 0.V and
A2: a * v = b * v;
0.V = a * v - b * v by A2,Def10
.= (a - b) * v by Th35;
then (- b) + a = 0 by A1,Th11;
hence thesis;
end;
:: Definition of the sum of the finite sequence of vectors.
reserve V for non empty addLoopStr;
reserve F for FinSequence-like PartFunc of NAT,V;
reserve f,f9,g for sequence of V;
reserve v,u for Element of V;
reserve j,k,n for Nat;
definition
let V; let F be (the carrier of V)-valued FinSequence;
func Sum(F) -> Element of V means
:Def12:
ex f st it = f.(len F) & f.0 = 0.V
& for j being Nat,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v;
existence
proof
defpred P[set] means
for F being (the carrier of V)-valued FinSequence
st len F = $1 ex u st ex f st u = f.(len F) & f.0 = 0.V &
for j,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n;
assume
A2: for F being (the carrier of V)-valued FinSequence
st len F = n ex u st ex f st u = f.(len F) & f.0 = 0.V &
for j,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v;
let F be (the carrier of V)-valued FinSequence;
A3: rng F c= the carrier of V by RELAT_1:def 19;
then reconsider F1 = F as FinSequence of V by FINSEQ_1:def 4;
reconsider G = F1 | Seg(n) as FinSequence of V by FINSEQ_1:18;
assume
A4: len F = n + 1;
then dom F = Seg(n + 1) by FINSEQ_1:def 3;
then n + 1 in dom F by FINSEQ_1:4;
then F.(n + 1) in rng F by FUNCT_1:def 3;
then reconsider u1 = F.(n + 1) as Element of V by A3;
A5: n < n + 1 by NAT_1:13;
then consider u,f such that
u = f.(len G) and
A6: f.0 = 0.V and
A7: for j,v st j < len G & v = G.(j + 1) holds f.(j + 1) = f.j + v
by A2,A4,FINSEQ_1:17;
defpred P[set,set] means for j st $1 = j holds (j < n + 1 implies $2 = f
.$1) & (n + 1 <= j implies for u st u = F.(n + 1) holds $2 = f.(len G) + u);
A8: for k being Element of NAT qua non empty set ex v being Element of
V st P[k,v]
proof
let k be Element of NAT qua non empty set;
reconsider i = k as Element of NAT;
A9: now
assume
A10: n + 1 <= i;
take v = f.(len G) + u1;
let j;
assume k = j;
hence j < n + 1 implies v = f.k by A10;
assume n + 1 <= j;
let u2 be Element of V;
assume u2 = F.(n + 1);
hence v = f.(len G) + u2;
end;
now
assume
A11: i < n + 1;
take v = f.k;
let j such that
A12: k = j;
thus j < n + 1 implies v = f.k;
thus n + 1 <= j implies for u st u = F.(n + 1) holds v = f.(len G) +
u by A11,A12;
end;
hence thesis by A9;
end;
consider f9 being sequence of the carrier of V such that
A13: for k being Element of NAT holds P[k,f9.k] from FUNCT_2:sch 3(A8);
A14: for k being Nat holds P[k,f9.k]
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A13;
end;
take z = f9.(n + 1);
take f99 = f9;
thus z = f99.(len F) by A4;
thus f99.0 = 0.V by A6,A14;
let j,v;
assume that
A15: j < len F and
A16: v = F.(j + 1);
A17: len G = n by A4,A5,FINSEQ_1:17;
A18: now
assume
A19: j = n;
then f99.(j + 1) = f.j + v by A17,A14,A16;
hence f99.(j + 1) = f99.j + v by A5,A14,A19;
end;
A20: now
assume
A21: j < n;
then
A22: j + 1 < n + 1 by XREAL_1:6;
1 <= 1 + j & j + 1 <= n by A21,NAT_1:11,13;
then j + 1 in Seg n by FINSEQ_1:1;
then
A23: v = G.(j + 1) by A16,FUNCT_1:49;
j < len G by A4,A5,A21,FINSEQ_1:17;
then
A24: f.(j + 1) = f.j + v by A7,A23;
j < n + 1 by A21,NAT_1:13;
then f.(j + 1) = f9.j + v by A14,A24;
hence f99.(j + 1) = f99.j + v by A14,A22;
end;
j <= n by A4,A15,NAT_1:13;
hence f99.(j + 1) = f99.j + v by A20,A18,XXREAL_0:1;
end;
A25: P[0]
proof
reconsider f = NAT --> 0.V as sequence of the carrier of V;
let F be (the carrier of V)-valued FinSequence;
assume
A26: len F = 0;
take u = f.(len F);
take f9 = f;
thus u = f9.(len F) & f9.0 = 0.V by FUNCOP_1:7;
let j;
thus for v st j < len F & v = F.(j + 1) holds f9.(j + 1) = f9.j + v by
A26;
end;
for n holds P[n] from NAT_1:sch 2(A25,A1);
hence thesis;
end;
uniqueness
proof
let v1,v2 be Element of V;
given f such that
A27: v1 = f.(len F) and
A28: f.0 = 0.V and
A29: for j,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v;
given f9 such that
A30: v2 = f9.(len F) and
A31: f9.0 = 0.V and
A32: for j,v st j < len F & v = F.(j + 1) holds f9.(j + 1) = f9.j + v;
defpred P[Nat] means $1 <= len F implies f.$1 = f9.$1;
now
A33: rng F c= the carrier of V by RELAT_1:def 19;
let k;
assume
A34: k <= len F implies f.k = f9.k;
assume
A35: k + 1 <= len F;
1 <= k + 1 & dom F = Seg(len F) by FINSEQ_1:def 3,NAT_1:11;
then k + 1 in dom F by A35,FINSEQ_1:1;
then F.(k + 1) in rng F by FUNCT_1:def 3;
then reconsider u1 = F.(k + 1) as Element of V by A33;
A36: k < len F by A35,NAT_1:13;
then f.(k + 1) = f.k + u1 by A29;
hence f.(k + 1) = f9.(k + 1) by A32,A34,A36;
end;
then
A37: for k st P[k] holds P[k+1];
A38: P[0] by A28,A31;
for k holds P[k] from NAT_1:sch 2(A38,A37);
hence thesis by A27,A30;
end;
end;
Lm4: Sum(<*>(the carrier of V)) = 0.V
proof
set S = <*>(the carrier of V);
ex f st Sum(S) = f.(len S) & f.0 = 0.V & for j,v st j < len S & v = S.(j
+ 1) holds f.(j + 1) = f.j + v by Def12;
hence thesis;
end;
Lm5: len F = 0 implies Sum(F) = 0.V
proof
assume len F = 0;
then F = <*>(the carrier of V);
hence thesis by Lm4;
end;
theorem Th38:
for F,G being FinSequence of V holds
len F = len G + 1 & G = F | (dom G) & v = F.(len F) implies
Sum(F) = Sum(G) + v
proof
let F,G be FinSequence of V;
assume that
A1: len F = len G + 1 and
A2: G = F | (dom G) and
A3: v = F.(len F);
consider g such that
A4: Sum(G) = g.(len G) and
A5: g.0 = 0.V and
A6: for j,v st j < len G & v = G.(j + 1) holds g.(j + 1) = g.j + v by Def12;
consider f such that
A7: Sum(F) = f.(len F) and
A8: f.0 = 0.V and
A9: for j,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v by Def12;
defpred P[Nat] means
for H being FinSequence of V holds len H = $1 & H = F | (Seg $1) &
len H <= len G implies f.(len H) = g.(len H);
now
let k;
assume
A10: for H be FinSequence of V st len H = k & H = F | (Seg k) & len H <= len G
holds f.(len H) = g.(len H);
let H be FinSequence of V;
assume that
A11: len H = k + 1 and
A12: H = F | (Seg (k + 1)) and
A13: len H <= len G;
1 <= k + 1 & k + 1 <= len F by A1,A11,A13,NAT_1:12;
then k + 1 in dom F by FINSEQ_3:25;
then reconsider v = F.(k + 1) as Element of V by FUNCT_1:102;
1 <= k + 1 by NAT_1:12;
then k + 1 in Seg(len G) by A11,A13,FINSEQ_1:1;
then k + 1 in dom G by FINSEQ_1:def 3;
then
A14: v = G.(k + 1) by A2,FUNCT_1:47;
reconsider H1 = H as FinSequence of V;
reconsider p = H1 | (Seg k) as FinSequence of V by FINSEQ_1:18;
A15: k <= len H by A11,NAT_1:12;
then Seg k c= Seg(k + 1) by A11,FINSEQ_1:5;
then
A16: p = F | (Seg k) by A12,FUNCT_1:51;
k < k + 1 by XREAL_1:29;
then k < len G by A11,A13,XXREAL_0:2;
then
A17: g.(k + 1) = g.k + v by A6,A14;
A18: len G < len F by A1,XREAL_1:29;
k <= len G by A13,A15,XXREAL_0:2;
then k < len F by A18,XXREAL_0:2;
then
A19: f.(k + 1) = f.k + v by A9;
len p = k by A15,FINSEQ_1:17;
hence f.(len H) = g.(len H) by A10,A11,A13,A15,A16,A19,A17,XXREAL_0:2;
end;
then
A20: for k st P[k] holds P[k+1];
A21: dom G = Seg len G by FINSEQ_1:def 3;
A22: P[0] by A8,A5;
for k holds P[k] from NAT_1:sch 2(A22,A20);
then f.(len G) = g.(len G) by A2,A21;
hence thesis by A1,A3,A7,A9,A4,XREAL_1:29;
end;
reserve V for RealLinearSpace;
reserve v for VECTOR of V;
reserve F,G,H,I for FinSequence of V;
theorem
len F = len G & (for k,v st k in dom F & v = G.k holds F.k = a * v)
implies Sum(F) = a * Sum(G)
proof
defpred P[set] means for H,I st len H = len I & len H = $1 & (for k,v st k
in Seg len H & v = I.k holds H.k = a * v) holds Sum(H) = a * Sum(I);
A1: dom F = Seg len F by FINSEQ_1:def 3;
now
let n;
assume
A2: for H,I st len H = len I & len H = n & for k,v st k in Seg len H &
v = I.k holds H.k = a * v holds Sum(H) = a * Sum(I);
let H,I;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k,v st k in Seg len H & v = I.k holds H.k = a * v;
reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of the carrier
of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then
A7: len q = n by A3,A4,FINSEQ_1:17;
A8: len p = n by A4,A6,FINSEQ_1:17;
A9: now
len p <= len H by A4,A6,FINSEQ_1:17;
then
A10: Seg len p c= Seg len H by FINSEQ_1:5;
A11: dom p = Seg n by A4,A6,FINSEQ_1:17;
let k,v;
assume that
A12: k in Seg len p and
A13: v = q.k;
dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
then I.k = q.k by A8,A12,FUNCT_1:47;
then H.k = a * v by A5,A12,A13,A10;
hence p.k = a * v by A8,A12,A11,FUNCT_1:47;
end;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom H & n + 1 in dom I by A3,A4,FINSEQ_3:25;
then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as VECTOR of V by FUNCT_1:102
;
A14: v1 = a * v2 by A4,A5,FINSEQ_1:4;
A15: dom q = Seg len q by FINSEQ_1:def 3;
dom p = Seg len p by FINSEQ_1:def 3;
hence Sum(H) = Sum(p) + v1 by A4,A8,Th38
.= a * Sum(q) + a * v2 by A2,A8,A7,A9,A14
.= a * (Sum(q) + v2) by Def5
.= a * Sum(I) by A3,A4,A7,A15,Th38;
end;
then
A16: for n st P[n] holds P[n+1];
now
let H,I;
assume that
A17: len H = len I and
A18: len H = 0 and
for k,v st k in Seg len H & v = I.k holds H.k = a * v;
Sum(H) = 0.V by A18,Lm5;
hence Sum(H) = a * Sum(I) by A17,A18,Lm5,Th10;
end;
then
A19: P[0];
for n holds P[n] from NAT_1:sch 2(A19,A16);
hence thesis by A1;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, F,G being FinSequence of V st len F = len G &
(for k for v being Element of V st k in dom F & v = G.k holds F.k = - v)
holds Sum(F) = - Sum(G)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, F,G be FinSequence of V;
defpred P[set] means for H,I being FinSequence of V st len H
= len I & len H = $1 & (for k for v being Element of V st k in Seg len H & v =
I.k holds H.k = - v) holds Sum(H) = - Sum(I);
A1: dom F = Seg len F by FINSEQ_1:def 3;
now
let n;
assume
A2: for H,I being FinSequence of V st len H = len I &
len H = n & for k for v being Element of V st k in Seg len H & v = I.k holds H.
k = - v holds Sum(H) = - Sum(I);
let H,I be FinSequence of V;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k for v being Element of V st k in Seg(len H) & v = I.k holds
H.k = - v;
reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of the carrier
of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then
A7: len q = n by A3,A4,FINSEQ_1:17;
A8: len p = n by A4,A6,FINSEQ_1:17;
A9: now
len p <= len H by A4,A6,FINSEQ_1:17;
then
A10: Seg(len p) c= Seg(len H) by FINSEQ_1:5;
A11: dom p = Seg n by A4,A6,FINSEQ_1:17;
let k;
let v be Element of V;
assume that
A12: k in Seg(len p) and
A13: v = q.k;
dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
then I.k = q.k by A8,A12,FUNCT_1:47;
then H.k = - v by A5,A12,A13,A10;
hence p.k = - v by A8,A12,A11,FUNCT_1:47;
end;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom H & n + 1 in dom I by A3,A4,FINSEQ_3:25;
then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as Element of V by
FUNCT_1:102;
A14: v1 = - v2 by A4,A5,FINSEQ_1:4;
A15: dom q = Seg len q by FINSEQ_1:def 3;
dom p = Seg len p by FINSEQ_1:def 3;
hence Sum(H) = Sum(p) + v1 by A4,A8,Th38
.= - Sum(q) + - v2 by A2,A8,A7,A9,A14
.= - (Sum(q) + v2) by Lm3
.= - Sum(I) by A3,A4,A7,A15,Th38;
end;
then
A16: for n st P[n] holds P[n+1];
now
let H,I be FinSequence of V;
assume that
A17: len H = len I & len H = 0 and
for k for v being Element of V st k in Seg len H & v = I.k holds H.k = - v;
Sum(H) = 0.V & Sum(I) = 0.V by A17,Lm5;
hence Sum(H) = - Sum(I);
end;
then
A18: P[0];
for n holds P[n] from NAT_1:sch 2(A18,A16);
hence thesis by A1;
end;
theorem Th41:
for V being add-associative right_zeroed non empty addLoopStr,
F,G being FinSequence of V holds Sum(F ^ G) = Sum(F) + Sum(G)
proof
let V be add-associative right_zeroed non empty addLoopStr, F,G be
FinSequence of V;
defpred P[set] means for G be FinSequence of V st len G = $1
holds Sum(F ^ G) = Sum(F) + Sum(G);
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: for G being FinSequence of V st len G = k holds Sum
(F ^ G) = Sum(F) + Sum(G);
let H be FinSequence of V;
reconsider p = H | (Seg k) as FinSequence of V by FINSEQ_1:18;
A3: rng H c= the carrier of V by FINSEQ_1:def 4;
assume
A4: len H = k + 1;
then
A5: dom H = Seg(k + 1) by FINSEQ_1:def 3;
then
A6: k + 1 in dom H by FINSEQ_1:4;
then H.(k + 1) in rng H by FUNCT_1:def 3;
then reconsider v = H.(k + 1) as Element of V by A3;
A7: k <= k + 1 by NAT_1:12;
A8: now
let n be Nat;
assume n in dom p;
then n in Seg k by A4,A7,FINSEQ_1:17;
hence p.n = H.n by FUNCT_1:49;
end;
A9: dom p = Seg len p by FINSEQ_1:def 3;
A10: Seg(len(F ^ p)) = Seg(len F + len p) by FINSEQ_1:22;
A11: dom(F ^ H) = Seg len(F ^ H) by FINSEQ_1:def 3
.= Seg(len F + len H) by FINSEQ_1:22;
A12: dom(F ^ p) = Seg len(F ^ p) by FINSEQ_1:def 3;
dom p = Seg k by A4,A7,FINSEQ_1:17;
then
A13: dom p c= dom H by A5,A7,FINSEQ_1:5;
A14: now
let x be object;
assume
A15: x in dom(F ^ p);
then reconsider n = x as Element of NAT;
A16: now
assume not n in dom F;
then
A17: not n in Seg(len F) by FINSEQ_1:def 3;
A18: 1 <= n by A12,A15,FINSEQ_1:1;
then len F <= n by A17,FINSEQ_1:1;
then consider j being Nat such that
A19: n = len F + j by NAT_1:10;
A20: now
assume not j <= k;
then
A21: len F + k < n by A19,XREAL_1:6;
n <= len F + len p by A12,A10,A15,FINSEQ_1:1;
hence contradiction by A4,A7,A21,FINSEQ_1:17;
end;
now
assume not 1 <= j;
then j = 0 by NAT_1:14;
hence contradiction by A17,A18,A19,FINSEQ_1:1;
end;
then j in Seg k by A20,FINSEQ_1:1;
then
A22: j in dom p by A4,A7,FINSEQ_1:17;
then (F ^ p).n = p.j & (F ^ H).n = H.j by A13,A19,FINSEQ_1:def 7;
hence (F ^ p).x = (F ^ H).x by A8,A22;
end;
now
assume
A23: n in dom F;
then (F ^ p).n = F.n by FINSEQ_1:def 7;
hence (F ^ p).x = (F ^ H).x by A23,FINSEQ_1:def 7;
end;
hence (F ^ p).x = (F ^ H).x by A16;
end;
A24: len p = k by A4,A7,FINSEQ_1:17;
then len F + len p <= len F + len H by A4,A7,XREAL_1:7;
then Seg len(F ^ p) c= dom(F ^ H) by A11,A10,FINSEQ_1:5;
then dom(F ^ p) = dom(F ^ H) /\ Seg(len(F ^ p)) by A12,XBOOLE_1:28;
then
A25: F ^ p = (F ^ H) | (Seg len (F ^ p)) by A14,FUNCT_1:46
.= (F ^ H) | (dom (F ^ p)) by FINSEQ_1:def 3;
A26: now
let n be Nat;
assume n in dom<* v *>;
then n in {1} by FINSEQ_1:2,38;
then n = 1 by TARSKI:def 1;
hence H.(len p + n) = <* v *>.n by A24;
end;
dom H = Seg(len p + len<* v *>) by A5,A24,FINSEQ_1:39;
then H = p ^ <* v *> by A8,A26,FINSEQ_1:def 7;
then F ^ H = (F ^ p) ^ <* v *> by FINSEQ_1:32;
then len(F ^ H) = len(F ^ p) + len<* v *> by FINSEQ_1:22;
then
A27: len(F ^ H) = len(F ^ p) + 1 by FINSEQ_1:39;
v = (F ^ H).(len F + len H) by A4,A6,FINSEQ_1:def 7
.= (F ^ H).(len(F ^ H)) by FINSEQ_1:22;
hence Sum(F ^ H) = Sum(F ^ p) + v by A27,A25,Th38
.= (Sum(F) + Sum(p)) + v by A2,A24
.= Sum(F) + (Sum(p) + v) by Def3
.= Sum(F) + Sum(H) by A4,A24,A9,Th38;
end;
A28: P[0]
proof
let G be FinSequence of V;
assume len G = 0;
then G = <*>(the carrier of V);
then F ^ G = F & Sum(G) = 0.V by Lm4,FINSEQ_1:34;
hence thesis by Def4;
end;
for k holds P[k] from NAT_1:sch 2(A28,A1);
then len G = len G implies thesis;
hence thesis;
end;
reserve V for add-associative right_zeroed right_complementable non empty
addLoopStr;
reserve F for FinSequence of V;
reserve v,v1,v2,u,w for Element of V;
reserve j,k for Nat;
Lm6: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, v being Element of V holds Sum<* v *> = v
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v be Element of V;
set S = <* v *>;
consider f being sequence of the carrier of V such that
A1: Sum(S) = f.(len S) and
A2: f.0 = 0.V & for j for v being Element of V st j < len S & v = S.(j +
1) holds f.(j + 1) = f.j + v by Def12;
0 < 1;
then consider j such that
A3: j < len S;
A4: len S = 1 by FINSEQ_1:39;
then
A5: S.(j + 1) = S.(0 + 1) by A3,NAT_1:14
.= v;
j = 0 by A4,A3,NAT_1:14;
then f.1 = 0.V + v by A2,A5
.= v;
hence thesis by A1,FINSEQ_1:39;
end;
theorem
for V being Abelian add-associative right_zeroed non empty addLoopStr,
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
let V be Abelian add-associative right_zeroed non empty addLoopStr, F,G be
FinSequence of V;
defpred P[set] means for H,I being FinSequence of V st len H
= $1 & rng H = rng I & H is one-to-one & I is one-to-one holds Sum(H) = Sum (I)
;
A1: len F = len F;
now
let k;
assume
A2: for H,I being FinSequence of V st len H = k & rng
H = rng I & H is one-to-one & I is one-to-one holds Sum(H) = Sum(I);
let H,I be FinSequence of V;
assume that
A3: len H = k + 1 and
A4: rng H = rng I and
A5: H is one-to-one and
A6: I is one-to-one;
k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A7: k + 1 in dom H by A3,FINSEQ_1:def 3;
then H.(k + 1) in rng I by A4,FUNCT_1:def 3;
then consider x being object such that
A8: x in dom I and
A9: H.(k + 1) = I.x by FUNCT_1:def 3;
reconsider v = H.(k + 1) as Element of V by A7,FUNCT_1:102;
reconsider n = x as Element of NAT by A8;
A10: len H = len I by A4,A5,A6,FINSEQ_1:48;
then
A11: x in Seg(k + 1) by A3,A8,FINSEQ_1:def 3;
then
A12: n <= k + 1 by FINSEQ_1:1;
then consider m2 being Nat such that
A13: n + m2 = k + 1 by NAT_1:10;
defpred P[Nat,object] means $2 = I.(n + $1);
reconsider m2 as Element of NAT by ORDINAL1:def 12;
A14: for j be Nat st j in Seg m2 ex x being object st P[j,x];
consider q2 being FinSequence such that
A15: dom q2 = Seg m2 and
A16: for k be Nat st k in Seg m2 holds P[k,q2.k] from FINSEQ_1:sch 1 (
A14);
A17: rng q2 c= the carrier of V
proof
let x be object;
assume x in rng q2;
then consider y being object such that
A18: y in dom q2 and
A19: x = q2.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A18;
1 <= y by A15,A18,FINSEQ_1:1;
then
A20: 1 <= n + y by NAT_1:12;
y <= m2 by A15,A18,FINSEQ_1:1;
then n + y <= len I by A3,A10,A13,XREAL_1:7;
then n + y in dom I by A20,FINSEQ_3:25;
then reconsider xx = I.(n + y) as Element of V by FUNCT_1:102;
xx in the carrier of V;
hence thesis by A15,A16,A18,A19;
end;
reconsider p = H | (Seg k) as FinSequence of V by FINSEQ_1:18;
A21: p is one-to-one by A5,FUNCT_1:52;
Seg k = Seg(k + 1) \ {k + 1} by FINSEQ_1:10;
then
A22: H .: (Seg k) = H .: Seg(k + 1) \ Im(H,k + 1) by A5,FUNCT_1:64;
A23: 1 <= n by A11,FINSEQ_1:1;
then consider m1 being Nat such that
A24: 1 + m1 = n by NAT_1:10;
reconsider q1 = I | (Seg m1) as FinSequence of V by FINSEQ_1:18;
reconsider q2 as FinSequence of V by A17,FINSEQ_1:def 4;
m1 <= n by A24,NAT_1:11;
then
A25: m1 <= k + 1 by A12,XXREAL_0:2;
then
A26: len q1 = m1 by A3,A10,FINSEQ_1:17;
A27: now
let j be Nat;
assume
A28: j in dom q2;
len(q1 ^ <* v *>) = m1 + len<* v *> by A26,FINSEQ_1:22
.= n by A24,FINSEQ_1:39;
hence I.(len(q1 ^ <* v *>) + j) = q2.j by A15,A16,A28;
end;
set q = q1 ^ q2;
A29: m1 < n by A24,XREAL_1:29;
A30: {v} misses rng q
proof
set y = the Element of {v} /\ rng q;
assume not thesis;
then
A31: {v} /\ rng q <> {} by XBOOLE_0:def 7;
then
A32: y in {v} by XBOOLE_0:def 4;
A33: now
assume y in rng q1;
then consider y1 being object such that
A34: y1 in dom q1 and
A35: y = q1.y1 by FUNCT_1:def 3;
A36: y1 in Seg m1 by A3,A10,A25,A34,FINSEQ_1:17;
reconsider y1 as Element of NAT by A34;
y1 <= m1 by A36,FINSEQ_1:1;
then
A37: y1 <= k + 1 by A25,XXREAL_0:2;
1 <= y1 by A36,FINSEQ_1:1;
then y1 in Seg(k + 1) by A37,FINSEQ_1:1;
then
A38: y1 in dom I by A3,A10,FINSEQ_1:def 3;
q1.y1 = I.y1 by A34,FUNCT_1:47;
then
A39: I.y1 = I.n by A9,A32,A35,TARSKI:def 1;
y1 <> n by A29,A36,FINSEQ_1:1;
hence contradiction by A6,A8,A38,A39;
end;
A40: y = I.n by A9,A32,TARSKI:def 1;
A41: now
assume y in rng q2;
then consider y1 being object such that
A42: y1 in dom q2 and
A43: y = q2.y1 by FUNCT_1:def 3;
reconsider y1 as Element of NAT by A42;
y1 <= m2 by A15,A42,FINSEQ_1:1;
then
A44: n + y1 <= k + 1 by A13,XREAL_1:7;
1 <= n + y1 by A23,NAT_1:12;
then n + y1 in Seg(k + 1) by A44,FINSEQ_1:1;
then
A45: n + y1 in dom I by A3,A10,FINSEQ_1:def 3;
I.n = I.(n + y1) by A15,A16,A40,A42,A43;
then
A46: n = n + y1 by A6,A8,A45;
y1 <> 0 by A15,A42,FINSEQ_1:1;
hence contradiction by A46;
end;
y in rng q by A31,XBOOLE_0:def 4;
then y in rng q1 \/ rng q2 by FINSEQ_1:31;
hence thesis by A33,A41,XBOOLE_0:def 3;
end;
A47: q is one-to-one
proof
let y1,y2 be object;
assume that
A48: y1 in dom q & y2 in dom q and
A49: q.y1 = q.y2;
reconsider x1 = y1, x2 = y2 as Element of NAT by A48;
A50: now
given j1 being Nat such that
A51: j1 in dom q2 and
A52: x1 = len q1 + j1;
A53: q2.j1 = I.(n + j1) by A15,A16,A51;
j1 <= m2 by A15,A51,FINSEQ_1:1;
then
A54: n + j1 <= k + 1 by A13,XREAL_1:7;
1 <= n + j1 by A23,NAT_1:12;
then n + j1 in Seg(k + 1) by A54,FINSEQ_1:1;
then
A55: n + j1 in dom I by A3,A10,FINSEQ_1:def 3;
given j2 being Nat such that
A56: j2 in dom q2 and
A57: x2 = len q1 + j2;
A58: q2.j2 = I.(n + j2) by A15,A16,A56;
j2 <= m2 by A15,A56,FINSEQ_1:1;
then
A59: n + j2 <= k + 1 by A13,XREAL_1:7;
1 <= n + j2 by A23,NAT_1:12;
then n + j2 in Seg(k + 1) by A59,FINSEQ_1:1;
then
A60: n + j2 in dom I by A3,A10,FINSEQ_1:def 3;
q2.j1 = q.(m1 + j2) by A26,A49,A51,A52,A57,FINSEQ_1:def 7
.= q2.j2 by A26,A56,FINSEQ_1:def 7;
then n + j1 = n + j2 by A6,A53,A58,A55,A60;
hence thesis by A52,A57;
end;
A61: now
assume
A62: x2 in dom q1;
then q1.x2 = I.x2 by FUNCT_1:47;
then
A63: q.x2 = I.x2 by A62,FINSEQ_1:def 7;
A64: x2 in Seg m1 by A3,A10,A25,A62,FINSEQ_1:17;
then
A65: 1 <= x2 by FINSEQ_1:1;
A66: x2 <= m1 by A64,FINSEQ_1:1;
then x2 <= k + 1 by A25,XXREAL_0:2;
then x2 in Seg(k + 1) by A65,FINSEQ_1:1;
then
A67: x2 in dom I by A3,A10,FINSEQ_1:def 3;
given j be Nat such that
A68: j in dom q2 and
A69: x1 = len q1 + j;
q2.j = I.(n + j) by A15,A16,A68;
then
A70: I.x2 = I.(n + j) by A49,A68,A69,A63,FINSEQ_1:def 7;
j <= m2 by A15,A68,FINSEQ_1:1;
then
A71: n + j <= k + 1 by A13,XREAL_1:7;
1 <= n + j by A23,NAT_1:12;
then n + j in Seg(k + 1) by A71,FINSEQ_1:1;
then
A72: n + j in dom I by A3,A10,FINSEQ_1:def 3;
A73: n <= n + j by NAT_1:12;
x2 < n by A29,A66,XXREAL_0:2;
hence thesis by A6,A70,A67,A72,A73;
end;
A74: now
assume
A75: x1 in dom q1;
then q1.x1 = I.x1 by FUNCT_1:47;
then
A76: q.x1 = I.x1 by A75,FINSEQ_1:def 7;
A77: x1 in Seg m1 by A3,A10,A25,A75,FINSEQ_1:17;
then
A78: 1 <= x1 by FINSEQ_1:1;
A79: x1 <= m1 by A77,FINSEQ_1:1;
then x1 <= k + 1 by A25,XXREAL_0:2;
then x1 in Seg(k + 1) by A78,FINSEQ_1:1;
then
A80: x1 in dom I by A3,A10,FINSEQ_1:def 3;
given j be Nat such that
A81: j in dom q2 and
A82: x2 = len q1 + j;
q2.j = I.(n + j) by A15,A16,A81;
then
A83: I.x1 = I.(n + j) by A49,A81,A82,A76,FINSEQ_1:def 7;
j <= m2 by A15,A81,FINSEQ_1:1;
then
A84: n + j <= k + 1 by A13,XREAL_1:7;
1 <= n + j by A23,NAT_1:12;
then n + j in Seg(k + 1) by A84,FINSEQ_1:1;
then
A85: n + j in dom I by A3,A10,FINSEQ_1:def 3;
A86: n <= n + j by NAT_1:12;
x1 < n by A29,A79,XXREAL_0:2;
hence thesis by A6,A83,A80,A85,A86;
end;
A87: q1 is one-to-one by A6,FUNCT_1:52;
now
assume
A88: x1 in dom q1 & x2 in dom q1;
then q1.x1 = q.x1 & q1.x2 = q.x2 by FINSEQ_1:def 7;
hence thesis by A49,A87,A88;
end;
hence thesis by A48,A74,A61,A50,FINSEQ_1:25;
end;
k <= k + 1 by NAT_1:12;
then
A89: len p = k by A3,FINSEQ_1:17;
A90: now
let k be Nat;
assume k in dom<* v *>;
then k in Seg 1 by FINSEQ_1:38;
then k = 1 by FINSEQ_1:2,TARSKI:def 1;
hence H.(len p + k) = <* v *>.k by A89;
end;
A91: now
let j be Nat;
assume
A92: j in dom(q1 ^ <* v *>);
A93: now
assume j in Seg m1;
then
A94: j in dom q1 by A3,A10,A25,FINSEQ_1:17;
then q1.j = I.j by FUNCT_1:47;
hence I.j = (q1 ^ <* v *>).j by A94,FINSEQ_1:def 7;
end;
A95: now
1 in Seg 1 & len<* v *> = 1 by FINSEQ_1:1,39;
then 1 in dom <* v *> by FINSEQ_1:def 3;
then
A96: (q1 ^ <* v *>).(len q1 + 1) = <* v *>.1 by FINSEQ_1:def 7;
assume j in {n};
then j = n by TARSKI:def 1;
hence (q1 ^ <* v *>).j = I.j by A9,A24,A26,A96;
end;
len(q1 ^ <* v *>) = m1 + len <* v *> by A26,FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40;
then j in Seg(m1 + 1) by A92,FINSEQ_1:def 3;
then j in Seg m1 \/ {n} by A24,FINSEQ_1:9;
hence I.j = (q1 ^ <* v *>).j by A93,A95,XBOOLE_0:def 3;
end;
len q2 = m2 by A15,FINSEQ_1:def 3;
then len(q1 ^ <* v *>) + len q2 = len q1 + len<* v *> + m2 by FINSEQ_1:22
.= k + 1 by A24,A13,A26,FINSEQ_1:40;
then dom I = Seg(len(q1 ^ <* v *>) + len q2) by A3,A10,FINSEQ_1:def 3;
then
A97: I = q1 ^ <* v *> ^ q2 by A91,A27,FINSEQ_1:def 7;
then rng I = rng(q1 ^ <* v *>) \/ rng q2 by FINSEQ_1:31
.= rng <* v *> \/ rng q1 \/ rng q2 by FINSEQ_1:31
.= {v} \/ rng q1 \/ rng q2 by FINSEQ_1:39
.= {v} \/ (rng q1 \/ rng q2) by XBOOLE_1:4
.= {v} \/ rng q by FINSEQ_1:31;
then
A98: rng q = rng I \ {v} by A30,XBOOLE_1:88;
A99: Seg(k + 1) = dom H by A3,FINSEQ_1:def 3;
then rng p = H .: (Seg k) & rng H = H .: (Seg(k + 1)) by RELAT_1:113,115;
then
A100: rng p = rng q by A4,A98,A99,A22,FINSEQ_1:4,FUNCT_1:59;
len<* v *> = 1 & for k be Nat st k in dom p holds H.k=p.k by FINSEQ_1:39
,FUNCT_1:47;
then H = p ^ <* v *> by A89,A99,A90,FINSEQ_1:def 7;
then
A101: Sum(H) = Sum(p) + Sum<* v *> by Th41;
Sum(I) = Sum(q1 ^ <* v *>) + Sum(q2) by A97,Th41
.= (Sum(q1) + Sum<* v *>) + Sum(q2) by Th41
.= Sum<* v *> + (Sum(q1) + Sum(q2)) by Def3
.= Sum(q) + Sum<* v *> by Th41;
hence Sum(H) = Sum(I) by A2,A89,A100,A21,A47,A101;
end;
then
A102: for k st P[k] holds P[k+1];
now
let H,I be FinSequence of V;
assume that
A103: len H = 0 and
A104: rng H = rng I and
H is one-to-one and
I is one-to-one;
H = {} by A103;
then I = {} by A104;
then
A105: len I = 0;
Sum(H) = 0.V by A103,Lm5;
hence Sum(H) = Sum(I) by A105,Lm5;
end;
then
A106: P[0];
for k holds P[k] from NAT_1:sch 2(A106,A102);
hence thesis by A1;
end;
theorem
for V being non empty addLoopStr holds Sum(<*>(the carrier of V)) = 0.V
by Lm4;
theorem
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds Sum<* v *> = v by Lm6;
theorem Th45:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,u being Element of V holds Sum<* v,u *> = v + u
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,u be Element of V;
<* v,u *> = <* v *> ^ <* u *> by FINSEQ_1:def 9;
hence Sum<* v,u *> = Sum<* v *> + Sum<* u *> by Th41
.= v + Sum<* u *> by Lm6
.= v + u by Lm6;
end;
theorem Th46:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
Sum<* v,u,w *> = v + u + w
proof
let V be add-associative right_zeroed right_complementable non empty
addLoopStr, v,u,w be Element of V;
<* v,u,w *> = <* v,u *> ^ <* w *> by FINSEQ_1:43;
hence Sum<* v,u,w *> = Sum<* v,u *> + Sum<* w *> by Th41
.= Sum<* v,u *> + w by Lm6
.= v + u + w by Th45;
end;
theorem
for V being RealLinearSpace, a being Real holds
a * Sum(<*>(the carrier of V)) = 0.V by Lm4,Th10;
theorem
for V being RealLinearSpace, a being Real, v,u being VECTOR of V holds
a * Sum<* v,u *> = a * v + a * u
proof
let V be RealLinearSpace, a be Real, v,u be VECTOR of V;
thus a * Sum<* v,u *> = a * (v + u) by Th45
.= a * v + a * u by Def5;
end;
theorem
for V being RealLinearSpace, a being Real, v,u,w being VECTOR of V
holds a * Sum<* v,u,w *> = a * v + a * u + a * w
proof
let V be RealLinearSpace, a be Real, v,u,w be VECTOR of V;
thus a * Sum<* v,u,w *> = a * (v + u + w) by Th46
.= a * (v + u) + a * w by Def5
.= a * v + a * u + a * w by Def5;
end;
theorem
- Sum(<*>(the carrier of V)) = 0.V
proof
thus - Sum(<*>(the carrier of V)) = - 0.V by Lm4
.= 0.V;
end;
theorem
- Sum<* v *> = - v by Lm6;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u being Element of V holds - Sum<* v,u *> = (- v) - u
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u be Element of V;
thus - Sum<* v,u *> = - (v + u) by Th45
.= (- v) - u by Th30;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
- Sum<* v,u,w *> = ((- v) - u) - w
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus - Sum<* v,u,w *> = - (v + u + w) by Th46
.= (- (v + u)) - w by Th30
.= ((- v) - u) - w by Th30;
end;
theorem Th54:
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
Sum<* v,w *> = Sum<* w,v*>
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,w be Element of V;
thus Sum<* v,w *> = v + w by Th45
.= Sum<* w,v *> by Th45;
end;
theorem
Sum<* v,w *> = Sum<* v *> + Sum<* w *>
proof
thus Sum<* v,w *> = v + w by Th45
.= Sum<* v *> + w by Lm6
.= Sum<* v *> + Sum<* w *> by Lm6;
end;
::$CT
theorem
Sum<* 0.V,v *> = v & Sum<* v,0.V *> = v
proof
thus Sum<* 0.V,v *> = 0.V + v by Th45
.= v;
thus Sum<* v,0.V *> = v + 0.V by Th45
.= v;
end;
theorem
Sum<* v,- v *> = 0.V & Sum<* - v,v *> = 0.V
proof
A1: v + - v = 0.V by Def10;
hence Sum<* v,- v *> = 0.V by Th45;
- v + v = 0.V by A1,Lm1;
hence thesis by Th45;
end;
theorem
Sum<* v,- w *> = v - w by Th45;
theorem Th59:
Sum<* - v,- w *> = - (w + v)
proof
thus Sum<* - v,- w *> = (- v) + (- w) by Th45
.= - (w + v) by Lm3;
end;
theorem Th60:
for V being RealLinearSpace, v being VECTOR of V holds Sum<* v,v *> = 2 * v
proof
let V be RealLinearSpace, v be VECTOR of V;
thus Sum<* v,v *> = v + v by Th45
.= 1 * v + v by Def8
.= 1 * v + 1 * v by Def8
.= (1 + 1) * v by Def6
.= 2 * v;
end;
theorem
for V being RealLinearSpace, v being VECTOR of V holds
Sum<* - v,- v*> = (- 2) * v
proof
let V be RealLinearSpace, v be VECTOR of V;
thus Sum<* - v,- v *> = - (v + v) by Th59
.= - Sum<* v,v *> by Th45
.= - (2 * v) by Th60
.= (- 1) * (2 * v) by Th16
.= ((- 1) * 2) * v by Def7
.= (- 2) * v;
end;
theorem
Sum<* u,v,w *> = Sum<* u *> + Sum<* v *> + Sum<* w *>
proof
thus Sum<* u,v,w *> = u + v + w by Th46
.= Sum<* u *> + v + w by Lm6
.= Sum<* u *> + v + Sum<* w *> by Lm6
.= Sum<* u *> + Sum<* v *> + Sum<* w *> by Lm6;
end;
theorem
Sum<* u,v,w *> = Sum<* u,v *> + w
proof
thus Sum<* u,v,w *> = u + v + w by Th46
.= Sum<* u,v *> + w by Th45;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
Sum<* u,v,w *> = Sum<* v,w *> + u
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus Sum<* u,v,w *> = u + v + w by Th46
.= u + (v + w) by Def3
.= Sum<* v,w *> + u by Th45;
end;
theorem Th65:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* u,w *> + v
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus Sum<* u,v,w *> = u + v + w by Th46
.= u + w + v by Def3
.= Sum<* u,w *> + v by Th45;
end;
theorem Th66:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* u,w,v *>
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus Sum<* u,v,w *> = u + v + w by Th46
.= u + w + v by Def3
.= Sum<* u,w,v *> by Th46;
end;
theorem Th67:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* v,u,w *>
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus Sum<* u,v,w *> = u + v + w by Th46
.= Sum<* v,u,w *> by Th46;
end;
theorem Th68:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* v,w,u *>
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus Sum<* u,v,w *> = Sum<* v,u,w *> by Th67
.= Sum<* v,w,u *> by Th66;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
Sum<* u,v,w *> = Sum<* w,v,u *>
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus Sum<* u,v,w *> = Sum<* w,u,v *> by Th68
.= Sum<* w,v,u *> by Th66;
end;
::$CT
theorem
Sum<* 0.V,0.V,v *> = v & Sum<* 0.V,v,0.V *> = v & Sum<* v,0.V,0.V *> = v
proof
thus Sum<* 0.V,0.V,v *> = 0.V + 0.V + v by Th46
.= v;
thus Sum<* 0.V,v,0.V *> = 0.V + v + 0.V by Th46
.= v;
thus Sum<* v,0.V,0.V *> = v + 0.V by Th46
.= v;
end;
theorem
Sum<*0.V,u,v*> = u + v & Sum<*u,v,0.V*> = u + v & Sum<*u,0.V,v*> = u + v
proof
thus Sum<* 0.V,u,v *> = 0.V + u + v by Th46
.= u + v;
thus Sum<* u,v,0.V *> = u + v + 0.V by Th46
.= u + v;
thus Sum<* u,0.V,v *> = u + 0.V + v by Th46
.= u + v;
end;
theorem
for V being RealLinearSpace, v being VECTOR of V holds Sum<* v,v,v *> = 3 * v
proof
let V be RealLinearSpace, v be VECTOR of V;
thus Sum<* v,v,v *> = Sum<* v,v *> + v by Th65
.= 2 * v + v by Th60
.= 2 * v + 1 * v by Def8
.= (2 + 1) * v by Def6
.= 3 * v;
end;
theorem
len F = 0 implies Sum(F) = 0.V by Lm5;
theorem
len F = 1 implies Sum(F) = F.1
proof
assume
A1: len F = 1;
then dom F = {1} by FINSEQ_1:2,def 3;
then 1 in dom F by TARSKI:def 1;
then
A2: F.1 in rng F by FUNCT_1:def 3;
rng F c= the carrier of V by FINSEQ_1:def 4;
then reconsider v = F.1 as Element of V by A2;
F = <* v *> by A1,FINSEQ_1:40;
hence thesis by Lm6;
end;
theorem
len F = 2 & v1 = F.1 & v2 = F.2 implies Sum(F) = v1 + v2
proof
assume len F = 2 & v1 = F.1 & v2 = F.2;
then F = <* v1,v2 *> by FINSEQ_1:44;
hence thesis by Th45;
end;
theorem
len F = 3 & v1 = F.1 & v2 = F.2 & v = F.3 implies Sum(F) = v1 + v2 + v
proof
assume len F = 3 & v1 = F.1 & v2 = F.2 & v = F.3;
then F = <* v1,v2,v *> by FINSEQ_1:45;
hence thesis by Th46;
end;
begin :: from REALSET2, 2007.02.24, A.T
definition
let L be non empty addLoopStr;
attr L is zeroed means
for a being Element of L holds a+0.L = a & 0.L+a = a;
end;
registration
cluster zeroed -> right_zeroed for non empty addLoopStr;
coherence;
end;
registration
cluster Abelian right_zeroed -> zeroed for non empty addLoopStr;
coherence
proof
let L be non empty addLoopStr;
assume
A1: L is Abelian right_zeroed;
let a be Element of L;
thus a+0.L = a by A1;
hence thesis by A1;
end;
cluster Abelian right_complementable -> left_complementable for non empty
addLoopStr;
coherence
proof
let L be non empty addLoopStr;
assume
A2: L is Abelian right_complementable;
let a be Element of L;
consider w being Element of L such that
A3: a+w = 0.L by A2,ALGSTR_0:def 11;
take w;
thus thesis by A2,A3;
end;
end;
:: missing, 2009.02.14, A.T.
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
(- a) * v = - a * v
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v be Element of V;
thus (- a) * v = a * (- v) by Th24
.= - a * v by Th25;
end;
begin :: VECTSP_3
reserve x,y for set,
k,n for Element of NAT;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr holds - Sum(<*>(the carrier of V)) = 0.V
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
thus - Sum(<*>(the carrier of V)) = - 0.V by Lm4
.= 0.V;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u being Element of V holds - Sum<* v,u *> = (- v) - u
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u be Element of V;
thus - Sum<* v,u *> = - (v + u) by Th45
.= (- v) - u by Th30;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
- Sum<* v,u,w *> = ((- v) - u) - w
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,u,w be Element of V;
thus - Sum<* v,u,w *> = - (v + u + w) by Th46
.= (- (v + u)) - w by Th30
.= ((- v) - u) - w by Th30;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds
Sum<* v,- v *> = 0.V & Sum<*- v,v *> = 0.V
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v be Element of V;
thus Sum<* v,- v *> = v + (- v) by Th45
.= 0.V by Th5;
hence thesis by Th54;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
Sum<* v,- w *> = v - w & Sum<* - w,v *> = v - w
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,w be Element of V;
thus Sum<* v,- w *> = v - w by Th45;
hence thesis by Th54;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
Sum<* - v,- w *> = - (v + w) & Sum<* - w,- v *> = - (v + w)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v,w be Element of V;
thus Sum<* - v,- w *> = (- v) + (- w) by Th45
.= - (v + w) by Lm3;
hence thesis by Th54;
end;