:: Linear Combinations in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2016 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, FINSEQ_1, SUBSET_1, RLVECT_1, REAL_1, STRUCT_0, FUNCT_1,
XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4,
XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1,
FUNCOP_1, VALUED_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, RLVECT_2,
LATTICES, VECTSP_1, PRE_POLY, FUNCT_7;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1,
RELSET_1, PRE_POLY, PARTFUN1, FUNCT_2, FUNCOP_1, DOMAIN_1, VALUED_1,
FINSEQ_4, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REAL_1,
RLSUB_1, NAT_1, BINOP_1, XXREAL_0;
constructors PARTFUN1, BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1,
FINSEQ_4, RLSUB_1, VALUED_1, RELSET_1, VECTSP_1, PRE_POLY, RLVECT_1,
NUMBERS, GROUP_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, RLSUB_1, VALUED_1, VALUED_0, MEMBERED,
FINSEQ_1, CARD_1, VECTSP_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve x,y,y1,y2 for set,
p for FinSequence,
i,k,l,n for Nat,
V for RealLinearSpace,
u,v,v1,v2,v3,w for VECTOR of V,
a,b for Real,
F,G,H1,H2 for FinSequence of V,
A,B for Subset of V,
f for Function of the carrier of V, REAL;
definition
let S be 1-sorted;
let x;
assume
x in S;
func vector(S,x) -> Element of S equals
:: RLVECT_2:def 1
x;
end;
theorem :: RLVECT_2:1
for S being non empty 1-sorted,v being Element of S holds vector(S,v) = v;
theorem :: RLVECT_2:2
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, F,G,H being FinSequence of the
carrier of V st len F = len G & len F = len H & for k st k in dom F holds H.k =
F/.k + G/.k holds Sum(H) = Sum(F) + Sum(G);
theorem :: RLVECT_2:3
len F = len G & (for k st k in dom F holds G.k = a * F/.k) implies Sum
(G) = a * Sum(F);
theorem :: RLVECT_2:4
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, F,G being FinSequence of the
carrier of V st len F = len G & (for k st k in dom F holds G.k = - F/.k) holds
Sum(G) = - Sum(F);
theorem :: RLVECT_2:5
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, F,G,H being FinSequence of the carrier of V st len F =
len G & len F = len H & (for k st k in dom F holds H.k = F/.k - G/.k) holds Sum
(H) = Sum(F) - Sum(G);
theorem :: RLVECT_2:6
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, F,G being FinSequence of the
carrier of V for f being Permutation of dom F st len F = len G & (for i st i in
dom G holds G.i = F.(f.i)) holds Sum(F) = Sum(G);
theorem :: RLVECT_2:7
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, F,G being FinSequence of the carrier of V for f being
Permutation of dom F st G = F * f holds Sum(F) = Sum(G);
definition
let V be non empty addLoopStr, T be finite Subset of V;
assume
V is Abelian add-associative right_zeroed;
func Sum(T) -> Element of V means
:: RLVECT_2:def 2
ex F be FinSequence of the carrier of V st rng F = T & F is one-to-one &
it = Sum(F);
end;
theorem :: RLVECT_2:8
for V be Abelian add-associative right_zeroed non empty
addLoopStr holds Sum({}V) = 0.V;
theorem :: RLVECT_2:9
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v be Element of V holds Sum{v} = v;
theorem :: RLVECT_2:10
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v1,v2 be Element of V holds v1 <> v2 implies Sum{v1,v2}
= v1 + v2;
theorem :: RLVECT_2:11
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v1,v2,v3 be Element of V holds v1 <> v2 & v2 <> v3 & v1
<> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3;
theorem :: RLVECT_2:12
for V be Abelian add-associative right_zeroed non empty
addLoopStr, S,T be finite Subset of V holds T misses S implies Sum(T \/ S) =
Sum(T) + Sum(S);
theorem :: RLVECT_2:13
for V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, S,T be finite Subset of V holds
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S);
theorem :: RLVECT_2:14
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, S,T be finite Subset of V holds Sum(T /\ S) = Sum(T) +
Sum(S) - Sum(T \/ S);
theorem :: RLVECT_2:15
for V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, S,T be finite Subset of V holds
Sum(T \ S) = Sum(T \/ S) - Sum(S);
theorem :: RLVECT_2:16
for V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, S,T be finite Subset of V holds
Sum(T \ S) = Sum(T) - Sum(T /\ S);
theorem :: RLVECT_2:17
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, S,T be finite Subset of V holds Sum(T \+\ S) = Sum(T \/
S) - Sum(T /\ S);
theorem :: RLVECT_2:18
for V be Abelian add-associative right_zeroed non empty addLoopStr,
S,T be finite Subset of V holds Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T);
definition
let V be non empty ZeroStr;
mode Linear_Combination of V -> Element of Funcs(the carrier of V, REAL)
means
:: RLVECT_2:def 3
ex T being finite Subset of V st for v being Element of V st not v in T
holds it.v = 0;
end;
reserve K,L,L1,L2,L3 for Linear_Combination of V;
notation
let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
synonym Carrier L for support L;
end;
definition
let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
redefine func Carrier(L) -> Subset of V equals
:: RLVECT_2:def 4
{v where v is Element of V : L.v <> 0};
end;
registration
let V be non empty addLoopStr, L be Linear_Combination of V;
cluster Carrier(L) -> finite;
end;
theorem :: RLVECT_2:19
for V be non empty addLoopStr, L be Linear_Combination of V, v be
Element of V holds L.v = 0 iff not v in Carrier(L);
definition
let V be non empty addLoopStr;
func ZeroLC(V) -> Linear_Combination of V means
:: RLVECT_2:def 5
Carrier (it) = {};
end;
theorem :: RLVECT_2:20
for V be non empty addLoopStr, v be Element of V holds ZeroLC(V) .v = 0;
definition
let V be non empty addLoopStr;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means
:: RLVECT_2:def 6
Carrier (it) c= A;
end;
reserve l,l1,l2 for Linear_Combination of A;
theorem :: RLVECT_2:21
A c= B implies l is Linear_Combination of B;
theorem :: RLVECT_2:22
ZeroLC(V) is Linear_Combination of A;
theorem :: RLVECT_2:23
for l being Linear_Combination of {}the carrier of V holds l = ZeroLC(V);
definition
let V;
let F;
let f;
func f (#) F -> FinSequence of the carrier of V means
:: RLVECT_2:def 7
len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
end;
theorem :: RLVECT_2:24
i in dom F & v = F.i implies (f (#) F).i = f.v * v;
theorem :: RLVECT_2:25
f (#) <*>(the carrier of V) = <*>(the carrier of V);
theorem :: RLVECT_2:26
f (#) <* v *> = <* f.v * v *>;
theorem :: RLVECT_2:27
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;
theorem :: RLVECT_2:28
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>;
definition
let V;
let L;
func Sum(L) -> Element of V means
:: RLVECT_2:def 8
ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;
theorem :: RLVECT_2:29
A <> {} & A is linearly-closed iff for l holds Sum(l) in A;
theorem :: RLVECT_2:30
Sum(ZeroLC(V)) = 0.V;
theorem :: RLVECT_2:31
for l being Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V;
theorem :: RLVECT_2:32
for l being Linear_Combination of {v} holds Sum(l) = l.v * v;
theorem :: RLVECT_2:33
v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
Sum(l) = l.v1 * v1 + l.v2 * v2;
theorem :: RLVECT_2:34
Carrier(L) = {} implies Sum(L) = 0.V;
theorem :: RLVECT_2:35
Carrier(L) = {v} implies Sum(L) = L.v * v;
theorem :: RLVECT_2:36
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2;
definition
let V be non empty addLoopStr;
let L1,L2 be Linear_Combination of V;
redefine pred L1 = L2 means
:: RLVECT_2:def 9
for v being Element of V holds L1.v = L2.v;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be Linear_Combination of V;
redefine func L1 + L2 -> Linear_Combination of V means
:: RLVECT_2:def 10
for v being Element of V holds it.v = L1.v + L2.v;
end;
theorem :: RLVECT_2:37
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);
theorem :: RLVECT_2:38
L1 is Linear_Combination of A & L2 is Linear_Combination of A
implies L1 + L2 is Linear_Combination of A;
theorem :: RLVECT_2:39
for V be non empty addLoopStr, L1,L2 be Linear_Combination of V holds
L1 + L2 = L2 + L1;
theorem :: RLVECT_2:40
L1 + (L2 + L3) = L1 + L2 + L3;
theorem :: RLVECT_2:41
L + ZeroLC(V) = L & ZeroLC(V) + L = L;
definition
let V;
let a be Real;
let L;
func a * L -> Linear_Combination of V means
:: RLVECT_2:def 11
for v holds it.v = a * L.v;
end;
theorem :: RLVECT_2:42
a <> 0 implies Carrier(a * L) = Carrier(L);
theorem :: RLVECT_2:43
0 * L = ZeroLC(V);
theorem :: RLVECT_2:44
L is Linear_Combination of A implies a * L is Linear_Combination of A;
theorem :: RLVECT_2:45
(a + b) * L = a * L + b * L;
theorem :: RLVECT_2:46
a * (L1 + L2) = a * L1 + a * L2;
theorem :: RLVECT_2:47
a * (b * L) = (a * b) * L;
theorem :: RLVECT_2:48
1 * L = L;
definition
let V,L;
func - L -> Linear_Combination of V equals
:: RLVECT_2:def 12
(- 1) * L;
end;
theorem :: RLVECT_2:49
(- L).v = - L.v;
theorem :: RLVECT_2:50
L1 + L2 = ZeroLC(V) implies L2 = - L1;
theorem :: RLVECT_2:51
Carrier(- L) = Carrier(L);
theorem :: RLVECT_2:52
L is Linear_Combination of A implies - L is Linear_Combination of A;
theorem :: RLVECT_2:53
- (- L) = L;
definition
let V;
let L1,L2;
func L1 - L2 -> Linear_Combination of V equals
:: RLVECT_2:def 13
L1 + (- L2);
end;
theorem :: RLVECT_2:54
(L1 - L2).v = L1.v - L2.v;
theorem :: RLVECT_2:55
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);
theorem :: RLVECT_2:56
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A;
theorem :: RLVECT_2:57
L - L = ZeroLC(V);
definition
let V;
func LinComb(V) -> set means
:: RLVECT_2:def 14
x in it iff x is Linear_Combination of V;
end;
registration
let V;
cluster LinComb(V) -> non empty;
end;
reserve e,e1,e2 for Element of LinComb(V);
definition
let V;
let e;
func @e -> Linear_Combination of V equals
:: RLVECT_2:def 15
e;
end;
definition
let V;
let L;
func @L -> Element of LinComb(V) equals
:: RLVECT_2:def 16
L;
end;
definition
let V;
func LCAdd(V) -> BinOp of LinComb(V) means
:: RLVECT_2:def 17
for e1,e2 holds it.(e1,e2 ) = @e1 + @e2;
end;
definition
let V;
func LCMult(V) -> Function of [:REAL,LinComb(V):], LinComb(V) means
:: RLVECT_2:def 18
for a,e holds it.[a,e] = a * @e;
end;
definition
let V;
func LC_RLSpace V -> RLSStruct equals
:: RLVECT_2:def 19
RLSStruct (# LinComb(V), @ZeroLC(V),
LCAdd(V), LCMult(V) #);
end;
registration
let V;
cluster LC_RLSpace V -> strict non empty;
end;
registration
let V;
cluster LC_RLSpace V -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;
theorem :: RLVECT_2:58
the carrier of LC_RLSpace(V) = LinComb(V);
theorem :: RLVECT_2:59
0.LC_RLSpace(V) = ZeroLC(V);
theorem :: RLVECT_2:60
the addF of LC_RLSpace(V) = LCAdd(V);
theorem :: RLVECT_2:61
the Mult of LC_RLSpace(V) = LCMult(V);
theorem :: RLVECT_2:62
vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = L1 + L2;
theorem :: RLVECT_2:63
a * vector(LC_RLSpace(V),L) = a * L;
theorem :: RLVECT_2:64
- vector(LC_RLSpace(V),L) = - L;
theorem :: RLVECT_2:65
vector(LC_RLSpace(V),L1) - vector(LC_RLSpace(V),L2) = L1 - L2;
definition
let V;
let A;
func LC_RLSpace(A) -> strict Subspace of LC_RLSpace(V) means
:: RLVECT_2:def 20
the carrier of it = the set of all l ;
end;
reserve x,y for set,
k,n for Nat;
theorem :: RLVECT_2:66
for R being add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr,
a being
Element of R for V being Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over R, 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 = a * v holds Sum(F) = a * Sum(G);
theorem :: RLVECT_2:67
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, F,G being FinSequence of V
st len F = len G & for k st k in dom F holds G.k = a * F/.k holds Sum(G) =
a * Sum(F);
theorem :: RLVECT_2:68
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr for V being
Abelian add-associative right_zeroed right_complementable non empty ModuleStr
over R, F,G,H being FinSequence of V st len F = len G & len F =
len H & for k st k in dom F holds H.k = F/.k - G/.k holds Sum(H) = Sum(F) - Sum
(G);
theorem :: RLVECT_2:69
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R holds a * Sum(<*>(the carrier of V)) =
0.V;
theorem :: RLVECT_2:70
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
a being Element of R
for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, v,u being Element of V holds a * Sum
<* v,u *> = a * v + a * u;
theorem :: RLVECT_2:71
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, v,u,w being Element of V holds a *
Sum<* v,u,w *> = a * v + a * u + a * w;