Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Wojciech A. Trybulec
- Received July 24, 1989
- MML identifier: RLVECT_1
- [
Mizar article,
MML identifier index
]
environ
vocabulary BINOP_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_1, BOOLE, RLVECT_1,
ANPROJ_1, ORDINAL2, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS,
XCMPLX_0, XREAL_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, REAL_1,
FINSEQ_1, NAT_1, STRUCT_0;
constructors DOMAIN_1, BINOP_1, REAL_1, FINSEQ_1, NAT_1, STRUCT_0, XREAL_0,
MEMBERED, XBOOLE_0, ORDINAL2;
clusters RELSET_1, FINSEQ_1, STRUCT_0, XREAL_0, SUBSET_1, NAT_1, MEMBERED,
ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS, ARYTM_3, XCMPLX_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
definition
struct (ZeroStr) LoopStr (# carrier -> set,
add -> BinOp of the carrier,
Zero -> Element of the carrier #);
end;
definition
struct (LoopStr) RLSStruct (# carrier -> set,
Zero -> Element of the carrier,
add -> BinOp of the carrier,
Mult -> Function of [:REAL, the carrier:], the carrier
#);
end;
definition
cluster non empty RLSStruct;
end;
reserve V for non empty RLSStruct;
reserve x,y,y1,y2 for set;
definition let V be RLSStruct;
mode VECTOR of V is Element of V;
end;
definition let V be 1-sorted; let x;
pred x in V means
:: RLVECT_1:def 1
x in the carrier of V;
end;
canceled 2;
theorem :: RLVECT_1:3
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.
::
definition let V be ZeroStr;
func 0.V -> Element of V equals
:: RLVECT_1:def 2
the Zero of V;
end;
reserve v for VECTOR of V;
reserve a,b for Real;
definition
cluster strict non empty LoopStr;
end;
definition let V be non empty LoopStr, v,w be Element of V;
func v + w -> Element of V equals
:: RLVECT_1:def 3
(the add of V).[v,w];
end;
definition let V; let v; let a;
func a * v -> Element of V equals
:: RLVECT_1:def 4
(the Mult of V).[a,v];
end;
::
:: Definitional theorems of zero element, addition, multiplication.
::
canceled;
theorem :: RLVECT_1:5
for V being non empty LoopStr, v,w being Element of V
holds v + w = (the add of V).(v,w);
definition 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;
end;
definition let IT be non empty LoopStr;
attr IT is Abelian means
:: RLVECT_1:def 5
for v,w being Element of IT holds v + w = w + v;
attr IT is add-associative means
:: RLVECT_1:def 6
for u,v,w being Element of IT
holds (u + v) + w = u + (v + w);
attr IT is right_zeroed means
:: RLVECT_1:def 7
for v being Element of IT holds v + 0.IT = v;
attr IT is right_complementable means
:: RLVECT_1:def 8
for v being Element of IT
ex w being Element of IT st v + w = 0.IT;
end;
definition let IT be non empty RLSStruct;
attr IT is RealLinearSpace-like means
:: RLVECT_1:def 9
(for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w) &
(for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v) &
(for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v)) &
(for v being VECTOR of IT holds 1 * v = v);
end;
definition
cluster strict Abelian add-associative right_zeroed right_complementable
(non empty LoopStr);
end;
definition
cluster non empty strict Abelian add-associative right_zeroed
right_complementable RealLinearSpace-like (non empty RLSStruct);
end;
definition
mode RealLinearSpace is Abelian add-associative right_zeroed
right_complementable RealLinearSpace-like (non empty RLSStruct);
end;
definition let V be Abelian (non empty LoopStr),
v,w be Element of V;
redefine func v + w;
commutativity;
end;
canceled;
theorem :: RLVECT_1:7
(for v,w being VECTOR of V holds v + w = w + v) &
(for u,v,w being VECTOR of V holds (u + v) + w = u + (v + w)) &
(for v being VECTOR of V holds v + 0.V = v) &
(for v being VECTOR of V
ex w being VECTOR of V st v + w = 0.V) &
(for a for v,w being VECTOR of V holds a * (v + w) = a * v + a * w) &
(for a,b for v being VECTOR of V holds (a + b) * v = a * v + b * v) &
(for a,b for v being VECTOR of V holds (a * b) * v = a * (b * v)) &
(for v being VECTOR of V holds 1 * v = v)
implies V is RealLinearSpace;
::
:: Axioms of real linear space.
::
reserve V for RealLinearSpace;
reserve v,w for VECTOR of V;
canceled 2;
theorem :: RLVECT_1:10
for V being add-associative
right_zeroed right_complementable (non empty LoopStr),
v being Element of V
holds v + 0.V = v & 0.V + v = v;
::
:: Definitions of reverse element to the vector and of
:: subtraction of vectors.
::
definition let V be non empty LoopStr;
let v be Element of V;
assume V is add-associative right_zeroed right_complementable;
func - v -> Element of V means
:: RLVECT_1:def 10
v + it = 0.V;
end;
definition let V be non empty LoopStr;
let v,w be Element of V;
func v - w -> Element of V equals
:: RLVECT_1:def 11
v + (- w);
end;
::
:: Definitional theorems of reverse element and substraction.
::
canceled 5;
theorem :: RLVECT_1:16
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v being Element of V
holds v + -v = 0.V & -v + v = 0.V;
canceled 2;
theorem :: RLVECT_1:19
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds v + w = 0.V implies v = - w;
theorem :: RLVECT_1:20
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,u being Element of V
ex w being Element of V st v + w = u;
theorem :: RLVECT_1:21
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
w,u,v1,v2 being Element of V
st w + v1 = w + v2 or v1 + w = v2 + w holds v1 = v2;
theorem :: RLVECT_1:22
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds v + w = v or w + v = v implies w = 0.V;
theorem :: RLVECT_1:23
a = 0 or v = 0.V implies a * v = 0.V;
theorem :: RLVECT_1:24
a * v = 0.V implies a = 0 or v = 0.V;
theorem :: RLVECT_1:25
for V being add-associative
right_zeroed right_complementable (non empty LoopStr)
holds - 0.V = 0.V;
theorem :: RLVECT_1:26
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v being Element of V
holds v - 0.V = v;
theorem :: RLVECT_1:27
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v being Element of V
holds 0.V - v = - v;
theorem :: RLVECT_1:28
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v being Element of V
holds v - v = 0.V;
theorem :: RLVECT_1:29
- v = (- 1) * v;
theorem :: RLVECT_1:30
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v being Element of V
holds - (- v) = v;
theorem :: RLVECT_1:31
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds - v = - w implies v = w;
canceled;
theorem :: RLVECT_1:33
v = - v implies v = 0.V;
theorem :: RLVECT_1:34
v + v = 0.V implies v = 0.V;
theorem :: RLVECT_1:35
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds v - w = 0.V implies v = w;
theorem :: RLVECT_1:36
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
u,v being Element of V
ex w being Element of V st v - w = u;
theorem :: RLVECT_1:37
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
w,v1,v2 being Element of V
st w - v1 = w - v2 holds v1 = v2;
theorem :: RLVECT_1:38
a * (- v) = (- a) * v;
theorem :: RLVECT_1:39
a * (- v) = - (a * v);
theorem :: RLVECT_1:40
(- a) * (- v) = a * v;
theorem :: RLVECT_1:41
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,u,w being Element of V
holds v - (u + w) = (v - w) - u;
theorem :: RLVECT_1:42
for V being add-associative (non empty LoopStr),
v,u,w being Element of V
holds (v + u) - w = v + (u - w);
theorem :: RLVECT_1:43
for V being Abelian add-associative right_zeroed
right_complementable (non empty LoopStr),
v,u,w being Element of V
holds v - (u - w) = (v -u) + w;
theorem :: RLVECT_1:44
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds - (v + w) = (- w) - v;
theorem :: RLVECT_1:45
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds - (v + w) = -w + -v;
theorem :: RLVECT_1:46
for V being Abelian add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds (- v) - w = (- w) - v;
theorem :: RLVECT_1:47
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,w being Element of V
holds - (v - w) = w + (- v);
theorem :: RLVECT_1:48
a * (v - w) = a * v - a * w;
theorem :: RLVECT_1:49
(a - b) * v = a * v - b * v;
theorem :: RLVECT_1:50
a <> 0 & a * v = a * w implies v = w;
theorem :: RLVECT_1:51
v <> 0.V & a * v = b * v implies a = b;
::
:: Definition of the sum of the finite sequence of vectors.
::
definition let V be non empty 1-sorted; let v,u be Element of V;
redefine func <* v,u *> -> FinSequence of the carrier of V;
end;
definition let V be non empty 1-sorted;
let v,u,w be Element of V;
redefine func <* v,u,w *> -> FinSequence of the carrier of V;
end;
reserve V for non empty LoopStr;
reserve F,G,H for FinSequence of the carrier of V;
reserve f,f',g for Function of NAT, the carrier of V;
reserve v,u for Element of V;
reserve j,k,n for Nat;
definition let V; let F;
func Sum(F) -> Element of V means
:: RLVECT_1:def 12
ex f st it = 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;
end;
canceled 2;
theorem :: RLVECT_1:54
k in Seg n & len F = n implies F.k is Element of V;
theorem :: RLVECT_1:55
len F = len G + 1 & G = F | (dom G) & v = F.(len F) implies
Sum(F) = Sum(G) + v;
reserve V for RealLinearSpace;
reserve v for VECTOR of V;
reserve F,G,H,I for FinSequence of the carrier of V;
theorem :: RLVECT_1:56
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);
theorem :: RLVECT_1:57
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
F,G being FinSequence of the carrier 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);
theorem :: RLVECT_1:58
for V being add-associative right_zeroed (non empty LoopStr),
F,G being FinSequence of the carrier of V
holds Sum(F ^ G) = Sum(F) + Sum(G);
reserve V for add-associative right_zeroed
right_complementable (non empty LoopStr);
reserve F for FinSequence of the carrier of V;
reserve v,v1,v2,u,w for Element of V;
reserve i,j,k,n for Nat;
reserve p,q for FinSequence;
theorem :: RLVECT_1:59
for V being Abelian add-associative right_zeroed (non empty LoopStr),
F,G being FinSequence of the carrier of V st
rng F = rng G & F is one-to-one & G is one-to-one
holds Sum(F) = Sum(G);
theorem :: RLVECT_1:60
for V being non empty LoopStr holds
Sum(<*>(the carrier of V)) = 0.V;
theorem :: RLVECT_1:61
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v being Element of V
holds Sum<* v *> = v;
theorem :: RLVECT_1:62
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,u being Element of V
holds Sum<* v,u *> = v + u;
theorem :: RLVECT_1:63
for V being add-associative right_zeroed
right_complementable (non empty LoopStr),
v,u,w being Element of V
holds Sum<* v,u,w *> = v + u + w;
theorem :: RLVECT_1:64
for V being RealLinearSpace, a being Real
holds a * Sum(<*>(the carrier of V)) = 0.V;
canceled;
theorem :: RLVECT_1:66
for V being RealLinearSpace, a being Real,
v,u being VECTOR of V
holds a * Sum<* v,u *> = a * v + a * u;
theorem :: RLVECT_1:67
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;
theorem :: RLVECT_1:68
- Sum(<*>(the carrier of V)) = 0.V;
theorem :: RLVECT_1:69
- Sum<* v *> = - v;
theorem :: RLVECT_1:70
for V being Abelian add-associative right_zeroed
right_complementable (non empty LoopStr),
v,u being Element of V
holds - Sum<* v,u *> = (- v) - u;
theorem :: RLVECT_1:71
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds - Sum<* v,u,w *> = ((- v) - u) - w;
theorem :: RLVECT_1:72
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,w being Element of V
holds Sum<* v,w *> = Sum<* w,v *>;
theorem :: RLVECT_1:73
Sum<* v,w *> = Sum<* v *> + Sum<* w *>;
theorem :: RLVECT_1:74
Sum<* 0.V,0.V *> = 0.V;
theorem :: RLVECT_1:75
Sum<* 0.V,v *> = v & Sum<* v,0.V *> = v;
theorem :: RLVECT_1:76
Sum<* v,- v *> = 0.V & Sum<* - v,v *> = 0.V;
theorem :: RLVECT_1:77
Sum<* v,- w *> = v - w;
theorem :: RLVECT_1:78
Sum<* - v,- w *> = - (w + v);
theorem :: RLVECT_1:79
for V being RealLinearSpace, v being VECTOR of V
holds Sum<* v,v *> = 2 * v;
theorem :: RLVECT_1:80
for V being RealLinearSpace, v being VECTOR of V
holds Sum<* - v,- v *> = (- 2) * v;
theorem :: RLVECT_1:81
Sum<* u,v,w *> = Sum<* u *> + Sum<* v *> + Sum<* w *>;
theorem :: RLVECT_1:82
Sum<* u,v,w *> = Sum<* u,v *> + w;
theorem :: RLVECT_1:83
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds Sum<* u,v,w *> = Sum<* v,w *> + u;
theorem :: RLVECT_1:84
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds Sum<* u,v,w *> = Sum<* u,w *> + v;
theorem :: RLVECT_1:85
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds Sum<* u,v,w *> = Sum<* u,w,v *>;
theorem :: RLVECT_1:86
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds Sum<* u,v,w *> = Sum<* v,u,w *>;
theorem :: RLVECT_1:87
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds Sum<* u,v,w *> = Sum<* v,w,u *>;
canceled;
theorem :: RLVECT_1:89
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v,u,w being Element of V
holds Sum<* u,v,w *> = Sum<* w,v,u *>;
theorem :: RLVECT_1:90
Sum<* 0.V,0.V,0.V *> = 0.V;
theorem :: RLVECT_1:91
Sum<* 0.V,0.V,v *> = v & Sum<* 0.V,v,0.V *> = v & Sum<* v,0.V,0.V *> = v;
theorem :: RLVECT_1:92
Sum<* 0.V,u,v *> = u + v & Sum<* u,v,0.V *> = u + v & Sum<* u,0.V,v *> = u +
v;
theorem :: RLVECT_1:93
for V being RealLinearSpace, v being VECTOR of V
holds Sum<* v,v,v *> = 3 * v;
theorem :: RLVECT_1:94
len F = 0 implies Sum(F) = 0.V;
theorem :: RLVECT_1:95
len F = 1 implies Sum(F) = F.1;
theorem :: RLVECT_1:96
len F = 2 & v1 = F.1 & v2 = F.2 implies Sum(F) = v1 + v2;
theorem :: RLVECT_1:97
len F = 3 & v1 = F.1 & v2 = F.2 & v = F.3 implies Sum(F) = v1 + v2 + v;
::
:: Auxiliary theorems.
::
definition
let R be non empty ZeroStr,
a be Element of R;
attr a is non-zero means
:: RLVECT_1:def 13
a <> 0.R;
end;
reserve j, k, n for natural number;
theorem :: RLVECT_1:98
j < 1 implies j = 0;
theorem :: RLVECT_1:99
1 <= k iff k <> 0;
canceled 2;
theorem :: RLVECT_1:102
k <> 0 implies n < n + k;
theorem :: RLVECT_1:103
k < k + n iff 1 <= n;
theorem :: RLVECT_1:104
Seg k = Seg(k + 1) \ {k + 1};
theorem :: RLVECT_1:105
p = (p ^ q) | (dom p);
theorem :: RLVECT_1:106
rng p = rng q & p is one-to-one & q is one-to-one implies
len p = len q;
Back to top