Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Linear Combinations in Real Linear Space

by
Wojciech A. Trybulec

MML identifier: RLVECT_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, FINSEQ_1, RLVECT_1, RELAT_1, FINSEQ_4, ARYTM_1, FUNCT_2,
BOOLE, FINSET_1, SEQ_1, RLSUB_1, CARD_1, QC_LANG1, BINOP_1, RLVECT_2;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0,
FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1,
REAL_1, RLSUB_1, FRAENKEL, NAT_1, BINOP_1, FINSEQ_4, CARD_1, PRE_TOPC;
constructors REAL_1, RLSUB_1, DOMAIN_1, FRAENKEL, NAT_1, BINOP_1, FINSEQ_4,
PRE_TOPC, XREAL_0, MEMBERED, XBOOLE_0;
clusters RLVECT_1, RLSUB_1, RELSET_1, STRUCT_0, FINSET_1, PRE_TOPC, ARYTM_3,
FUNCT_2, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

scheme LambdaSep1{D, R() -> non empty set, A() -> Element of D(),
B() -> Element of R(), F(set) -> Element of R()}:
ex f being Function of D(),R() st
f.A() = B() & for x being Element of D() st x <> A() holds f.x = F(x);

scheme LambdaSep2{D, R() -> non empty set, A1, A2() -> Element of D(),
B1, B2() -> Element of R(), F(set) -> Element of R()}:
ex f being Function of D(),R() st
f.A1() = B1() & f.A2() = B2() &
for x being Element of D() st x <> A1() & x <> A2() holds f.x = F(x)
provided
A1() <> A2();

reserve X,Y,x,y,y1,y2 for set,
p for FinSequence,
i,j,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 the carrier 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;

canceled 2;

theorem :: RLVECT_2:3
for S being non empty 1-sorted,v being Element of S
holds vector(S,v) = v;

theorem :: RLVECT_2:4
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
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:5
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:6
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 st k in dom F holds G.k = - F/.k) holds
Sum(G) = - Sum(F);

theorem :: RLVECT_2:7
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
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:8
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
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:9
for V being Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
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 1-sorted;
cluster empty finite Subset of V;
end;

definition let V be 1-sorted; let S,T be finite Subset of V;
redefine func S \/ T -> finite Subset of V;
func S /\ T -> finite Subset of V;
func S \ T -> finite Subset of V;
func S \+\ T -> finite Subset of V;
end;

definition let V be non empty LoopStr,
T be finite Subset of V;
assume V is Abelian add-associative right_zeroed;
canceled 2;

func Sum(T) -> Element of V means
:: RLVECT_2:def 4
ex F be FinSequence of the carrier of V st
rng F = T & F is one-to-one & it = Sum(F);
end;

definition let V be non empty 1-sorted;
cluster non empty finite Subset of V;
end;

definition let V be non empty 1-sorted; let v be Element of V;
redefine func {v} -> finite Subset of V;
end;

definition let V be non empty 1-sorted;
let v1,v2 be Element of V;
redefine func {v1,v2} -> finite Subset of V;
end;

definition let V be non empty 1-sorted;
let v1,v2,v3 be Element of V;
redefine func {v1,v2,v3} -> finite Subset of V;
end;

canceled 4;

theorem :: RLVECT_2:14
for V be Abelian add-associative right_zeroed (non empty LoopStr) holds
Sum({}V) = 0.V;

theorem :: RLVECT_2:15
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v be Element of V holds
Sum{v} = v;

theorem :: RLVECT_2:16
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
v1,v2 be Element of V holds
v1 <> v2 implies Sum{v1,v2} = v1 + v2;

theorem :: RLVECT_2:17
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
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:18
for V be Abelian add-associative right_zeroed (non empty LoopStr),
S,T be finite Subset of V holds
T misses S implies Sum(T \/ S) = Sum(T) + Sum(S);

theorem :: RLVECT_2:19
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
S,T be finite Subset of V holds
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S);

theorem :: RLVECT_2:20
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
S,T be finite Subset of V holds
Sum(T /\ S) = Sum(T) + Sum(S) - Sum(T \/ S);

theorem :: RLVECT_2:21
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
S,T be finite Subset of V holds
Sum(T \ S) = Sum(T \/ S) - Sum(S);

theorem :: RLVECT_2:22
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
S,T be finite Subset of V holds
Sum(T \ S) = Sum(T) - Sum(T /\ S);

theorem :: RLVECT_2:23
for V be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr),
S,T be finite Subset of V holds
Sum(T \+\ S) = Sum(T \/ S) - Sum(T /\ S);

theorem :: RLVECT_2:24
for V be Abelian add-associative right_zeroed (non empty LoopStr),
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 5
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;

definition let V be non empty LoopStr, L be Linear_Combination of V;
func Carrier(L) -> finite Subset of V equals
:: RLVECT_2:def 6
{v where v is Element of V : L.v <> 0};
end;

canceled 3;

theorem :: RLVECT_2:28
for V be non empty LoopStr, 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 LoopStr;
func ZeroLC(V) -> Linear_Combination of V means
:: RLVECT_2:def 7
Carrier (it) = {};
end;

canceled;

theorem :: RLVECT_2:30
for V be non empty LoopStr, v be Element of V holds
ZeroLC(V).v = 0;

definition let V be non empty LoopStr; let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means
:: RLVECT_2:def 8
Carrier (it) c= A;
end;

reserve l,l1,l2 for Linear_Combination of A;

canceled 2;

theorem :: RLVECT_2:33
A c= B implies l is Linear_Combination of B;

theorem :: RLVECT_2:34
ZeroLC(V) is Linear_Combination of A;

theorem :: RLVECT_2:35
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 9
len it = len F &
for i st i in dom it holds it.i = f.(F/.i) * F/.i;
end;

canceled 4;

theorem :: RLVECT_2:40
i in dom F & v = F.i implies (f (#) F).i = f.v * v;

theorem :: RLVECT_2:41
f (#) <*>(the carrier of V) = <*>(the carrier of V);

theorem :: RLVECT_2:42
f (#) <* v *> = <* f.v * v *>;

theorem :: RLVECT_2:43
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;

theorem :: RLVECT_2:44
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 10
ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;

canceled 2;

theorem :: RLVECT_2:47
A <> {} & A is lineary-closed iff for l holds Sum(l) in A;

theorem :: RLVECT_2:48
Sum(ZeroLC(V)) = 0.V;

theorem :: RLVECT_2:49
for l being Linear_Combination of {}(the carrier of V) holds
Sum(l) = 0.V;

theorem :: RLVECT_2:50
for l being Linear_Combination of {v} holds
Sum(l) = l.v * v;

theorem :: RLVECT_2:51
v1 <> v2 implies
for l being Linear_Combination of {v1,v2} holds
Sum(l) = l.v1 * v1 + l.v2 * v2;

theorem :: RLVECT_2:52
Carrier(L) = {} implies Sum(L) = 0.V;

theorem :: RLVECT_2:53
Carrier(L) = {v} implies Sum(L) = L.v * v;

theorem :: RLVECT_2:54
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2;

definition let V be non empty LoopStr; let L1,L2 be Linear_Combination of V;
redefine pred L1 = L2 means
:: RLVECT_2:def 11
for v being Element of V holds L1.v = L2.v;
end;

definition let V be non empty LoopStr; let L1,L2 be Linear_Combination of V;
func L1 + L2 -> Linear_Combination of V means
:: RLVECT_2:def 12
for v being Element of V holds it.v = L1.v + L2.v;
end;

canceled 3;

theorem :: RLVECT_2:58
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: RLVECT_2:59
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 + L2 is Linear_Combination of A;

theorem :: RLVECT_2:60
for V be non empty LoopStr, L1,L2 be Linear_Combination of V holds
L1 + L2 = L2 + L1;

theorem :: RLVECT_2:61
L1 + (L2 + L3) = L1 + L2 + L3;

theorem :: RLVECT_2:62
L + ZeroLC(V) = L & ZeroLC(V) + L = L;

definition let V,a; let L;
func a * L -> Linear_Combination of V means
:: RLVECT_2:def 13
for v holds it.v = a * L.v;
end;

canceled 2;

theorem :: RLVECT_2:65
a <> 0 implies Carrier(a * L) = Carrier(L);

theorem :: RLVECT_2:66
0 * L = ZeroLC(V);

theorem :: RLVECT_2:67
L is Linear_Combination of A implies a * L is Linear_Combination of A;

theorem :: RLVECT_2:68
(a + b) * L = a * L + b * L;

theorem :: RLVECT_2:69
a * (L1 + L2) = a * L1 + a * L2;

theorem :: RLVECT_2:70
a * (b * L) = (a * b) * L;

theorem :: RLVECT_2:71
1 * L = L;

definition let V,L;
func - L -> Linear_Combination of V equals
:: RLVECT_2:def 14
(- 1) * L;
end;

canceled;

theorem :: RLVECT_2:73
(- L).v = - L.v;

theorem :: RLVECT_2:74
L1 + L2 = ZeroLC(V) implies L2 = - L1;

theorem :: RLVECT_2:75
Carrier(- L) = Carrier(L);

theorem :: RLVECT_2:76
L is Linear_Combination of A implies - L is Linear_Combination of A;

theorem :: RLVECT_2:77
- (- L) = L;

definition let V; let L1,L2;
func L1 - L2 -> Linear_Combination of V equals
:: RLVECT_2:def 15
L1 + (- L2);
end;

canceled;

theorem :: RLVECT_2:79
(L1 - L2).v = L1.v - L2.v;

theorem :: RLVECT_2:80
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: RLVECT_2:81
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A;

theorem :: RLVECT_2:82
L - L = ZeroLC(V);

definition let V;
func LinComb(V) -> set means
:: RLVECT_2:def 16
x in it iff x is Linear_Combination of V;
end;

definition 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 17
e;
end;

definition let V; let L;
func @L -> Element of LinComb(V) equals
:: RLVECT_2:def 18
L;
end;

definition let V;
func LCAdd(V) -> BinOp of LinComb(V) means
:: RLVECT_2:def 19
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 20
for a,e holds it.[a,e] = a * @e;
end;

definition let V;
func LC_RLSpace(V) -> RealLinearSpace equals
:: RLVECT_2:def 21
RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #);
end;

definition let V;
cluster LC_RLSpace(V) -> strict non empty;
end;

canceled 9;

theorem :: RLVECT_2:92
the carrier of LC_RLSpace(V) = LinComb(V);

theorem :: RLVECT_2:93
the Zero of LC_RLSpace(V) = ZeroLC(V);

theorem :: RLVECT_2:94

theorem :: RLVECT_2:95
the Mult of LC_RLSpace(V) = LCMult(V);

theorem :: RLVECT_2:96
vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = L1 + L2;

theorem :: RLVECT_2:97
a * vector(LC_RLSpace(V),L) = a * L;

theorem :: RLVECT_2:98
- vector(LC_RLSpace(V),L) = - L;

theorem :: RLVECT_2:99
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 22
the carrier of it = {l : not contradiction};
end;

canceled 3;

theorem :: RLVECT_2:103
k < n implies n - 1 is Nat;

canceled 3;

theorem :: RLVECT_2:107
X is finite & Y is finite implies X \+\ Y is finite;

theorem :: RLVECT_2:108
for f being Function st
f " X = f " Y & X c= rng f & Y c= rng f holds X = Y;
```