:: Linear Combinations in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: 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, FUNCSDOM, VECTSP_2, VECTSP_1, FINSEQ_1, NAT_1, SUBSET_1,
FUNCT_1, FINSET_1, ARYTM_3, RELAT_1, CARD_3, XXREAL_0, TARSKI, CARD_1,
STRUCT_0, SUPINF_2, PARTFUN1, XBOOLE_0, ORDINAL4, ARYTM_1, RLVECT_2,
FUNCT_2, FUNCOP_1, VALUED_1, GROUP_1, RLSUB_1, FINSEQ_4, RLVECT_3,
RMOD_2;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FINSET_1, FINSEQ_1, ORDINAL1,
NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, CARD_1, DOMAIN_1,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_4, VECTSP_2,
RMOD_2, RMOD_3, FUNCOP_1, XXREAL_0;
constructors PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, FINSEQ_4,
RLVECT_2, RMOD_2, RMOD_3, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0,
STRUCT_0, VECTSP_1, ORDINAL1, FINSEQ_1, VECTSP_2, RMOD_2, CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions FUNCT_1, TARSKI, RMOD_2, XBOOLE_0;
equalities RMOD_2, XBOOLE_0, RELAT_1;
expansions FUNCT_1, TARSKI, RMOD_2, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4,
FUNCT_1, FUNCT_2, RLVECT_1, RLVECT_2, TARSKI, VECTSP_1, VECTSP_2,
ZFMISC_1, RMOD_2, NAT_1, RELAT_1, XBOOLE_0, XBOOLE_1, RLSUB_2, XCMPLX_1,
GROUP_1, FUNCOP_1, XREAL_1, PARTFUN1, STRUCT_0, RMOD_3;
schemes FINSEQ_1, FUNCT_2, NAT_1;
begin
reserve R for Ring,
V for RightMod of R,
a,b for Scalar of R,
x,y for set,
p,q ,r for FinSequence,
i,k for Nat,
u,v,v1,v2,v3,w for Vector of V,
F,G,H for FinSequence of V,
A,B for Subset of V,
f for Function of V, R,
S,T for finite Subset of V;
Lm1: len F = len G + 1 & G = F | (Seg len G) & v = F.(len F) implies Sum(F) =
Sum(G) + v
proof
len F = len G + 1 & G = F | (dom G) & v = F.(len F) implies Sum(F) = Sum
(G) + v by RLVECT_1:38;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th1:
len F = len G & (for k,v st k in dom F & v = G.k holds F.k = v *
a) implies Sum(F) = Sum(G) * a
proof
defpred P[Nat] means for H,I be FinSequence of V st len H = len I & len H =
$1 & (for k,v st k in dom H & v = I.k holds H.k = v * a) holds Sum(H) = Sum(I)
* a;
now
let n be Nat;
assume
A1: for H,I be FinSequence of V st len H = len I & len H = n & for k,
v st k in dom H & v = I.k holds H.k = v * a holds Sum(H) = Sum(I) * a;
let H,I be FinSequence of V;
assume that
A2: len H = len I and
A3: len H = n + 1 and
A4: for k,v st k in dom H & v = I.k holds H.k = v * a;
reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of V by
FINSEQ_1:18;
A5: n <= n + 1 by NAT_1:12;
then
A6: len p = n by A3,FINSEQ_1:17;
A7: len q = n by A2,A3,A5,FINSEQ_1:17;
A8: now
len p <= len H by A3,A5,FINSEQ_1:17;
then
A9: dom p c= dom H by FINSEQ_3:30;
let k,v;
assume that
A10: k in dom p and
A11: v = q.k;
dom p = dom q by A6,A7,FINSEQ_3:29;
then I.k = q.k by A10,FUNCT_1:47;
then H.k = v * a by A4,A10,A11,A9;
hence p.k = v * a by A10,FUNCT_1:47;
end;
A12: n + 1 in Seg(n + 1) by FINSEQ_1:4;
then n + 1 in dom H & n + 1 in dom I by A2,A3,FINSEQ_1:def 3;
then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as Vector of V by FINSEQ_2:11
;
n + 1 in dom H by A3,A12,FINSEQ_1:def 3;
then
A13: v1 = v2 * a by A4;
thus Sum(H) = Sum(p) + v1 by A3,A6,Lm1
.= Sum(q) * a + v2 * a by A1,A6,A7,A8,A13
.= (Sum(q) + v2) * a by VECTSP_2:def 9
.= Sum(I) * a by A2,A3,A7,Lm1;
end;
then
A14: for i be Nat st P[i] holds P[i+1];
now
let H,I be FinSequence of V;
assume that
A15: len H = len I and
A16: len H = 0 and
for k,v st k in dom H & v = I.k holds H.k = v * a;
H = <*>(the carrier of V) by A16;
then
A17: Sum(H) = 0.V by RLVECT_1:43;
I = <*>(the carrier of V) by A15,A16;
then Sum(I) = 0.V by RLVECT_1:43;
hence Sum(H) = Sum(I) * a by A17,VECTSP_2:32;
end;
then
A18: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A18,A14);
hence thesis;
end;
Lm2: len F = len G & (for k st k in dom F holds G.k = F/.k * a) implies Sum(G)
= Sum(F) * a
proof
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = F/.k * a;
now
let k,v;
assume that
A3: k in dom G and
A4: v = F.k;
A5: k in dom F by A1,A3,FINSEQ_3:29;
then v = F/.k by A4,PARTFUN1:def 6;
hence G.k = v * a by A2,A5;
end;
hence thesis by A1,Th1;
end;
theorem
Sum(<*>(the carrier of V)) * a = 0.V
proof
thus Sum(<*>(the carrier of V)) * a = 0.V * a by RLVECT_1:43
.= 0.V by VECTSP_2:32;
end;
theorem
Sum<* v,u *> * a = v * a + u * a
proof
thus Sum<* v,u *> * a = (v + u) * a by RLVECT_1:45
.= v * a + u * a by VECTSP_2:def 9;
end;
theorem
Sum<* v,u,w *> * a = v * a + u * a + w * a
proof
thus Sum<* v,u,w *> * a = (v + u + w) * a by RLVECT_1:46
.= (v + u) * a + w * a by VECTSP_2:def 9
.= v * a + u * a + w * a by VECTSP_2:def 9;
end;
definition
let R, V, T;
func Sum(T) -> Vector of V means
:Def1:
ex F st rng F = T & F is one-to-one & it = Sum(F);
existence
proof
consider p such that
A1: rng p = T and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of V by A1,FINSEQ_1:def 4;
take Sum(p);
take p;
thus thesis by A1,A2;
end;
uniqueness by RLVECT_1:42;
end;
theorem Th5:
Sum({}V) = 0.V
proof
Sum(<*>(the carrier of V)) = 0.V by RLVECT_1:43;
hence thesis by Def1,RELAT_1:38;
end;
theorem
Sum{v} = v
proof
A1: Sum<* v *> = v by RLVECT_1:44;
rng<* v *> = {v} & <* v *> is one-to-one by FINSEQ_1:39,FINSEQ_3:93;
hence thesis by A1,Def1;
end;
theorem
v1 <> v2 implies Sum{v1,v2} = v1 + v2
proof
assume v1 <> v2;
then
A1: <* v1,v2 *> is one-to-one by FINSEQ_3:94;
rng<* v1,v2 *> = {v1,v2} & Sum<* v1,v2 *> = v1 + v2 by FINSEQ_2:127
,RLVECT_1:45;
hence thesis by A1,Def1;
end;
theorem
v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3
proof
assume v1 <> v2 & v2 <> v3 & v1 <> v3;
then
A1: <* v1,v2,v3 *> is one-to-one by FINSEQ_3:95;
rng<* v1,v2,v3 *> = {v1,v2,v3} & Sum<* v1,v2,v3 *> = v1 + v2 + v3 by
FINSEQ_2:128,RLVECT_1:46;
hence thesis by A1,Def1;
end;
theorem Th9:
T misses S implies Sum(T \/ S) = Sum(T) + Sum(S)
proof
consider F such that
A1: rng F = T \/ S and
A2: F is one-to-one & Sum(T \/ S) = Sum(F) by Def1;
consider G such that
A3: rng G = T and
A4: G is one-to-one and
A5: Sum(T) = Sum(G) by Def1;
consider H such that
A6: rng H = S and
A7: H is one-to-one and
A8: Sum(S) = Sum(H) by Def1;
set I = G ^ H;
assume T misses S;
then
A9: I is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
rng I = rng F by A1,A3,A6,FINSEQ_1:31;
hence Sum(T \/ S) = Sum(I) by A2,A9,RLVECT_1:42
.= Sum(T) + Sum(S) by A5,A8,RLVECT_1:41;
end;
theorem Th10:
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S)
proof
set A = S \ T;
set B = T \ S;
set Z = A \/ B;
set I = T /\ S;
A1: A \/ I = S by XBOOLE_1:51;
A2: B \/ I = T by XBOOLE_1:51;
A3: Z = T \+\ S;
then Z \/ I = T \/ S by XBOOLE_1:93;
then Sum(T \/ S) + Sum(I) = Sum(Z) + Sum(I) + Sum(I) by A3,Th9,XBOOLE_1:103
.= Sum(A) + Sum(B) + Sum(I) + Sum(I) by Th9,XBOOLE_1:82
.= Sum(A) + (Sum(I) + Sum(B)) + Sum(I) by RLVECT_1:def 3
.= (Sum(A) + Sum(I)) + (Sum(B) + Sum(I)) by RLVECT_1:def 3
.= Sum(S) + (Sum(B) + Sum(I)) by A1,Th9,XBOOLE_1:89
.= Sum(T) + Sum(S) by A2,Th9,XBOOLE_1:89;
hence thesis by RLSUB_2:61;
end;
theorem
Sum(T /\ S) = Sum(T) + Sum(S) - Sum(T \/ S)
proof
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S) by Th10;
then Sum(T) + Sum(S) = Sum(T /\ S) + Sum(T \/ S) by RLSUB_2:61;
hence thesis by RLSUB_2:61;
end;
theorem Th12:
Sum(T \ S) = Sum(T \/ S) - Sum(S)
proof
(T \ S) misses S by XBOOLE_1:79;
then
A1: (T \ S) /\ S = {}V;
(T \ S) \/ S = T \/ S by XBOOLE_1:39;
then Sum(T \/ S) = Sum(T \ S) + Sum(S) - Sum((T \ S) /\ S) by Th10;
then Sum(T \/ S) = Sum(T \ S) + Sum(S) - 0.V by A1,Th5
.= Sum(T \ S) + Sum(S) by VECTSP_1:18;
hence thesis by RLSUB_2:61;
end;
theorem Th13:
Sum(T \ S) = Sum(T) - Sum(T /\ S)
proof
T \ (T /\ S) = T \ S by XBOOLE_1:47;
then Sum(T \ S) = Sum(T \/ (T /\ S)) - Sum(T /\ S) by Th12;
hence thesis by XBOOLE_1:22;
end;
theorem
Sum(T \+\ S) = Sum(T \/ S) - Sum(T /\ S)
proof
T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101;
hence Sum(T \+\ S) = Sum(T \/ S) - Sum((T \/ S) /\ (T /\ S)) by Th13
.= Sum(T \/ S) - Sum((T \/ S) /\ T /\ S) by XBOOLE_1:16
.= Sum(T \/ S) - Sum(T /\ S) by XBOOLE_1:21;
end;
theorem
Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T) by Th9,XBOOLE_1:82;
definition
let R, V;
mode Linear_Combination of V -> Element of Funcs(the carrier of V, the
carrier of R) means
:Def2:
ex T st for v st not v in T holds it.v = 0.R;
existence
proof
{}V = {};
then reconsider P = {} as finite Subset of V;
reconsider f = (the carrier of V) --> 0.R as Function of V, R;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
take f;
take P;
thus thesis by FUNCOP_1:7;
end;
end;
reserve L,L1,L2,L3 for Linear_Combination of V;
definition
let R, V, L;
func Carrier(L) -> finite Subset of V equals
{v : L.v <> 0.R};
coherence
proof
set A = {v : L.v <> 0.R};
consider T such that
A1: for v st not v in T holds L.v = 0.R by Def2;
A c= T
proof
let x be object;
assume x in A;
then ex v st x = v & L.v <> 0.R;
hence thesis by A1;
end;
hence thesis by XBOOLE_1:1;
end;
end;
theorem
x in Carrier(L) iff ex v st x = v & L.v <> 0.R;
theorem
L.v = 0.R iff not v in Carrier(L)
proof
thus L.v = 0.R implies not v in Carrier(L)
proof
assume
A1: L.v = 0.R;
assume not thesis;
then ex u st u = v & L.u <> 0.R;
hence thesis by A1;
end;
assume not v in Carrier(L);
hence thesis;
end;
definition
let R, V;
func ZeroLC(V) -> Linear_Combination of V means
:Def4:
Carrier(it) = {};
existence
proof
reconsider f = (the carrier of V) --> 0.R as Function of V, R;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
f is Linear_Combination of V
proof
reconsider T = {}V as finite empty Subset of V;
take T;
thus thesis by FUNCOP_1:7;
end;
then reconsider f as Linear_Combination of V;
take f;
set C = {v : f.v <> 0.R};
now
set x = the Element of C;
assume C <> {};
then x in C;
then ex v st x = v & f.v <> 0.R;
hence contradiction by FUNCOP_1:7;
end;
hence thesis;
end;
uniqueness
proof
let L,L9 be Linear_Combination of V;
assume that
A1: Carrier(L) = {} and
A2: Carrier(L9) = {};
now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Element of V;
A3: now
assume L9.v <> 0.R;
then v in {u : L9.u <> 0.R};
hence contradiction by A2;
end;
now
assume L.v <> 0.R;
then v in {u : L.u <> 0.R};
hence contradiction by A1;
end;
hence L.x = L9.x by A3;
end;
hence L = L9 by FUNCT_2:12;
end;
end;
theorem Th18:
ZeroLC(V).v = 0.R
proof
Carrier(ZeroLC(V)) = {} & not v in {} by Def4;
hence thesis;
end;
definition
let R, V, A;
mode Linear_Combination of A -> Linear_Combination of V means
:Def5:
Carrier (it) c= A;
existence
proof
take L = ZeroLC(V);
Carrier(L) = {} by Def4;
hence thesis;
end;
end;
reserve l for Linear_Combination of A;
theorem Th19:
A c= B implies l is Linear_Combination of B
proof
assume
A1: A c= B;
Carrier(l) c= A by Def5;
then Carrier(l) c= B by A1;
hence thesis by Def5;
end;
theorem Th20:
ZeroLC(V) is Linear_Combination of A
proof
Carrier(ZeroLC(V)) = {} & {} c= A by Def4;
hence thesis by Def5;
end;
theorem Th21:
for l being Linear_Combination of {}(the carrier of V) holds l = ZeroLC(V)
proof
let l be Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by Def5;
then Carrier(l) = {};
hence thesis by Def4;
end;
theorem
L is Linear_Combination of Carrier(L) by Def5;
definition
let R, V, F, f;
func f (#) F -> FinSequence of V means
:Def6:
len it = len F & for i being
Nat st i in dom it holds it.i = (F/.i) * f.(F/.i);
existence
proof
deffunc Q(Nat) = (F/.$1)*f.(F/.$1);
consider G being FinSequence such that
A1: len G = len F and
A2: for n be Nat st n in dom G holds G.n = Q(n) from FINSEQ_1:sch 2;
rng G c= the carrier of V
proof
let x be object;
assume x in rng G;
then consider y be object such that
A3: y in dom G and
A4: G.y = x by FUNCT_1:def 3;
y in Seg(len F) by A1,A3,FINSEQ_1:def 3;
then reconsider y as Element of NAT;
G.y = (F/.y) * f.(F/.y) by A2,A3;
hence thesis by A4;
end;
then reconsider G as FinSequence of V by FINSEQ_1:def 4;
take G;
thus thesis by A1,A2;
end;
uniqueness
proof
let H1,H2 be FinSequence of V;
assume that
A5: len H1 = len F and
A6: for i st i in dom H1 holds H1.i = (F/.i) * f.(F/.i) and
A7: len H2 = len F and
A8: for i st i in dom H2 holds H2.i = (F/.i) * f.(F/.i);
now
let k be Nat;
assume 1 <= k & k <= len H1;
then
A9: k in Seg(len H1) by FINSEQ_1:1;
then k in dom H1 by FINSEQ_1:def 3;
then
A10: H1.k = (F/.k) * f.(F/.k) by A6;
k in dom H2 by A5,A7,A9,FINSEQ_1:def 3;
hence H1.k = H2.k by A8,A10;
end;
hence thesis by A5,A7,FINSEQ_1:14;
end;
end;
theorem Th23:
i in dom F & v = F.i implies (f (#) F).i = v * f.v
proof
assume that
A1: i in dom F and
A2: v = F.i;
A3: F/.i = F.i by A1,PARTFUN1:def 6;
len(f (#) F) = len F by Def6;
then i in dom(f (#) F) by A1,FINSEQ_3:29;
hence thesis by A2,A3,Def6;
end;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def6
.= 0;
hence thesis;
end;
theorem Th25:
f (#) <* v *> = <* v * f.v *>
proof
A1: 1 in {1} by TARSKI:def 1;
A2: len(f (#) <* v *>) = len<* v *> by Def6
.= 1 by FINSEQ_1:40;
then dom(f (#) <* v *>) = {1} by FINSEQ_1:2,def 3;
then (f (#) <* v *>).1 = (<* v *>/.1) * f.(<* v *>/.1) by A1,Def6
.= v * f.(<* v *>/.1) by FINSEQ_4:16
.= v * f.v by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th26:
f (#) <* v1,v2 *> = <* v1 * f.v1, v2 * f.v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def6
.= 2 by FINSEQ_1:44;
then
A2: dom(f (#) <* v1,v2 *>) = {1,2} by FINSEQ_1:2,def 3;
2 in {1,2} by TARSKI:def 2;
then
A3: (f (#) <* v1,v2 *>).2 = (<* v1,v2 *>/.2) * f.(<* v1,v2 *>/.2) by A2,Def6
.= v2 * f.(<* v1,v2 *>/.2) by FINSEQ_4:17
.= v2 * f.v2 by FINSEQ_4:17;
1 in {1,2} by TARSKI:def 2;
then (f (#) <* v1,v2 *>).1 = (<* v1,v2 *>/.1) * f.(<* v1,v2 *>/.1) by A2,Def6
.= v1 * f.(<* v1,v2 *>/.1) by FINSEQ_4:17
.= v1 * f.v1 by FINSEQ_4:17;
hence thesis by A1,A3,FINSEQ_1:44;
end;
theorem
f (#) <* v1,v2,v3 *> = <* v1 * f.v1, v2 * f.v2, v3 * f.v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def6
.= 3 by FINSEQ_1:45;
then
A2: dom(f (#) <* v1,v2,v3 *>) = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
3 in {1,2,3} by ENUMSET1:def 1;
then
A3: (f (#) <* v1,v2,v3 *>).3 = (<* v1,v2,v3 *>/.3) * f.(<* v1,v2,v3 *>/.3)
by A2,Def6
.= v3 * f.(<* v1,v2,v3 *>/.3) by FINSEQ_4:18
.= v3 * f.v3 by FINSEQ_4:18;
2 in {1,2,3} by ENUMSET1:def 1;
then
A4: (f (#) <* v1,v2,v3 *>).2 = (<* v1,v2,v3 *>/.2) * f.(<* v1,v2,v3 *>/.2)
by A2,Def6
.= v2 * f.(<* v1,v2,v3 *>/.2) by FINSEQ_4:18
.= v2 * f.v2 by FINSEQ_4:18;
1 in {1,2,3} by ENUMSET1:def 1;
then (f (#) <* v1,v2,v3 *>).1 = (<* v1,v2,v3 *>/.1) * f.(<* v1,v2,v3 *>/.1)
by A2,Def6
.= v1 * f.(<* v1,v2,v3 *>/.1) by FINSEQ_4:18
.= v1 * f.v1 by FINSEQ_4:18;
hence thesis by A1,A4,A3,FINSEQ_1:45;
end;
theorem Th28:
f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len F = len(f (#) F) by Def6;
A2: len H = len(f (#) F) + len(f (#) G) by FINSEQ_1:22
.= len F + len(f (#) G) by Def6
.= len F + len G by Def6
.= len I by FINSEQ_1:22;
A3: len G = len(f (#) G) by Def6;
now
let k be Nat;
assume
A4: k in dom H;
now
per cases by A4,FINSEQ_1:25;
suppose
A5: k in dom(f (#) F);
then
A6: k in dom F by A1,FINSEQ_3:29;
then
A7: k in dom(F ^ G) by FINSEQ_3:22;
A8: F/.k = F.k by A6,PARTFUN1:def 6
.= (F ^ G).k by A6,FINSEQ_1:def 7
.= (F ^ G)/.k by A7,PARTFUN1:def 6;
thus H.k = (f (#) F).k by A5,FINSEQ_1:def 7
.= (I/.k) * f.(I/.k) by A5,A8,Def6;
end;
suppose
A9: ex n be Nat st n in dom(f (#) G) & k = len(f (#) F) + n;
A10: k in dom I by A2,A4,FINSEQ_3:29;
consider n be Nat such that
A11: n in dom(f (#) G) and
A12: k = len(f (#) F) + n by A9;
A13: n in dom G by A3,A11,FINSEQ_3:29;
then
A14: G/.n = G.n by PARTFUN1:def 6
.= (F ^ G).k by A1,A12,A13,FINSEQ_1:def 7
.= (F ^ G)/.k by A10,PARTFUN1:def 6;
thus H.k = (f (#) G).n by A11,A12,FINSEQ_1:def 7
.= (I/.k) * f.(I/.k) by A11,A14,Def6;
end;
end;
hence H.k = (I/.k) * f.(I/.k);
end;
hence thesis by A2,Def6;
end;
definition
let R, V, L;
func Sum(L) -> Vector of V means
:Def7:
ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
existence
proof
consider F being FinSequence such that
A1: rng F = Carrier(L) and
A2: F is one-to-one by FINSEQ_4:58;
reconsider F as FinSequence of V by A1,FINSEQ_1:def 4;
take Sum(L (#) F);
take F;
thus F is one-to-one & rng F = Carrier(L) by A1,A2;
thus thesis;
end;
uniqueness
proof
let v1,v2;
given F1 being FinSequence of V such that
A3: F1 is one-to-one and
A4: rng F1 = Carrier(L) and
A5: v1 = Sum(L (#) F1);
given F2 being FinSequence of V such that
A6: F2 is one-to-one and
A7: rng F2 = Carrier(L) and
A8: v2 = Sum(L (#) F2);
defpred P[object,object] means {$2} = F1 " {F2.$1};
A9: len F1 = len F2 by A3,A4,A6,A7,FINSEQ_1:48;
A10: dom F1 = Seg(len F1) by FINSEQ_1:def 3;
A11: dom F2 = Seg(len F2) by FINSEQ_1:def 3;
A12: for x being object st x in dom F1
ex y being object st y in dom F1 & P[x,y]
proof
let x be object;
assume x in dom F1;
then F2.x in rng F1 by A4,A7,A9,A10,A11,FUNCT_1:def 3;
then consider y being object such that
A13: F1 " {F2.x} = {y} by A3,FUNCT_1:74;
take y;
y in F1 " {F2.x} by A13,TARSKI:def 1;
hence y in dom F1 by FUNCT_1:def 7;
thus thesis by A13;
end;
consider f being Function of dom F1, dom F1 such that
A14: for x being object st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A15: rng f = dom F1
proof
thus rng f c= dom F1 by RELAT_1:def 19;
let y be object;
assume
A16: y in dom F1;
then F1.y in rng F2 by A4,A7,FUNCT_1:def 3;
then consider x being object such that
A17: x in dom F2 and
A18: F2.x = F1.y by FUNCT_1:def 3;
F1 " {F2.x} = F1 " Im(F1,y) by A16,A18,FUNCT_1:59;
then F1 " {F2.x} c= {y} by A3,FUNCT_1:82;
then {f.x} c= {y} by A9,A10,A11,A14,A17;
then
A19: f.x = y by ZFMISC_1:18;
x in dom f by A9,A10,A11,A17,FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:def 3;
end;
set G1 = L (#) F1;
A20: len G1 = len F1 by Def6;
A21: dom F1 = {} implies dom F1 = {};
A22: f is one-to-one
proof
let y1,y2 be object;
assume that
A23: y1 in dom f and
A24: y2 in dom f and
A25: f.y1 = f.y2;
A26: y2 in dom F1 by A21,A24,FUNCT_2:def 1;
then
A27: F1 " {F2.y2} = {f.y2} by A14;
A28: y1 in dom F1 by A21,A23,FUNCT_2:def 1;
then F2.y1 in rng F1 by A4,A7,A9,A10,A11,FUNCT_1:def 3;
then
A29: {F2.y1} c= rng F1 by ZFMISC_1:31;
F2.y2 in rng F1 by A4,A7,A9,A10,A11,A26,FUNCT_1:def 3;
then
A30: {F2.y2} c= rng F1 by ZFMISC_1:31;
F1 " {F2.y1} = {f.y1} by A14,A28;
then {F2.y1} = {F2.y2} by A25,A27,A29,A30,FUNCT_1:91;
then
A31: F2.y1 = F2.y2 by ZFMISC_1:3;
y1 in dom F2 & y2 in dom F2 by A9,A10,A11,A21,A23,A24,FUNCT_2:def 1;
hence thesis by A6,A31;
end;
set G2 = L (#) F2;
A32: dom G2 = Seg(len G2) by FINSEQ_1:def 3;
reconsider f as Permutation of dom F1 by A15,A22,FUNCT_2:57;
dom F1 = Seg len F1 & dom G1 = Seg len G1 by FINSEQ_1:def 3;
then reconsider f as Permutation of dom G1 by A20;
A33: len G2 = len F2 by Def6;
A34: dom(G1) = Seg(len G1) by FINSEQ_1:def 3;
now
let i be Nat;
assume
A35: i in dom G2;
then
A36: G2.i = (F2/.i) * L.(F2/.i) & F2.i = F2/.i by A33,A11,A32,Def6,
PARTFUN1:def 6;
i in dom F2 by A33,A35,FINSEQ_3:29;
then reconsider u = F2.i as Vector of V by FINSEQ_2:11;
i in dom f by A9,A20,A33,A34,A32,A35,FUNCT_2:def 1;
then
A37: f.i in dom F1 by A15,FUNCT_1:def 3;
then reconsider m = f.i as Element of NAT by A10;
reconsider v = F1.m as Vector of V by A37,FINSEQ_2:11;
{F1.(f.i)} = Im(F1,f.i) by A37,FUNCT_1:59
.= F1 .: (F1 " {F2.i}) by A9,A33,A10,A32,A14,A35;
then
A38: u = v by FUNCT_1:75,ZFMISC_1:18;
F1.m = F1/.m by A37,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A20,A10,A34,A37,A38,A36,Def6;
end;
hence thesis by A3,A4,A5,A6,A7,A8,A20,A33,FINSEQ_1:48,RLVECT_2:6;
end;
end;
Lm3: Sum(ZeroLC(V)) = 0.V
proof
consider F such that
F is one-to-one and
A1: rng F = Carrier(ZeroLC(V)) and
A2: Sum(ZeroLC(V)) = Sum(ZeroLC(V) (#) F) by Def7;
Carrier(ZeroLC(V)) = {} by Def4;
then F = {} by A1,RELAT_1:41;
then len F = 0;
then len(ZeroLC(V) (#) F) = 0 by Def6;
hence thesis by A2,RLVECT_1:75;
end;
theorem Th29:
0.R <> 1_R implies (A <> {} & A is linearly-closed iff for l
holds Sum l in A)
proof
assume
A1: 0.R <> 1_R;
thus A <> {} & A is linearly-closed implies for l holds Sum(l) in A
proof
defpred P[Nat] means for l st card(Carrier(l)) = $1 holds Sum (l) in A;
assume that
A2: A <> {} and
A3: A is linearly-closed;
now
let l;
assume card(Carrier(l)) = 0;
then Carrier(l) = {};
then l = ZeroLC(V) by Def4;
then Sum(l) = 0.V by Lm3;
hence Sum(l) in A by A2,A3,RMOD_2:1;
end;
then
A4: P[0];
now
let k be Nat;
assume
A5: for l st card Carrier l = k holds Sum(l) in A;
let l;
deffunc Q(Element of V) = l.$1;
consider F such that
A6: F is one-to-one and
A7: rng F = Carrier(l) and
A8: Sum(l) = Sum(l (#) F) by Def7;
reconsider G = F | Seg k as FinSequence of V by FINSEQ_1:18;
assume
A9: card Carrier l = k + 1;
then
A10: len F = k + 1 by A6,A7,FINSEQ_4:62;
then
A11: len(l (#) F) = k + 1 by Def6;
A12: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A13: k + 1 in dom F by A10,FINSEQ_1:def 3;
k + 1 in dom F by A10,A12,FINSEQ_1:def 3;
then reconsider v = F.(k + 1) as Vector of V by FINSEQ_2:11;
consider f being Function of V, R such that
A14: f.v = 0.R and
A15: for u being Element of V st u <> v holds f.u = Q(u) from
FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
A16: v in Carrier(l) by A7,A13,FUNCT_1:def 3;
now
let u;
assume
A17: not u in Carrier(l);
hence f.u = l.u by A16,A15
.= 0.R by A17;
end;
then reconsider f as Linear_Combination of V by Def2;
A18: A \ {v} c= A by XBOOLE_1:36;
A19: Carrier(l) c= A by Def5;
then
A20: v * l.v in A by A3,A16;
A21: Carrier(f) = Carrier(l) \ {v}
proof
thus Carrier(f) c= Carrier(l) \ {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A22: u = x and
A23: f.u <> 0.R;
f.u = l.u by A14,A15,A23;
then
A24: x in Carrier(l) by A22,A23;
not x in {v} by A14,A22,A23,TARSKI:def 1;
hence thesis by A24,XBOOLE_0:def 5;
end;
let x be object;
assume
A25: x in Carrier(l) \ {v};
then x in Carrier(l) by XBOOLE_0:def 5;
then consider u such that
A26: x = u and
A27: l.u <> 0.R;
not x in {v} by A25,XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then l.u = f.u by A15,A26;
hence thesis by A26,A27;
end;
then Carrier(f) c= A \ {v} by A19,XBOOLE_1:33;
then Carrier(f) c= A by A18;
then reconsider f as Linear_Combination of A by Def5;
A28: len G = k by A10,FINSEQ_3:53;
then
A29: len (f (#) G) = k by Def6;
A30: rng G = Carrier(f)
proof
thus rng G c= Carrier f
proof
let x be object;
assume x in rng G;
then consider y being object such that
A31: y in dom G and
A32: G.y = x by FUNCT_1:def 3;
reconsider y as Nat by A31,FINSEQ_3:23;
A33: dom G c= dom F & G.y = F.y by A31,FUNCT_1:47,RELAT_1:60;
now
assume x = v;
then
A34: k + 1 = y by A6,A13,A31,A32,A33;
y <= k by A28,A31,FINSEQ_3:25;
hence contradiction by A34,XREAL_1:29;
end;
then
A35: not x in {v} by TARSKI:def 1;
x in rng F by A31,A32,A33,FUNCT_1:def 3;
hence thesis by A7,A21,A35,XBOOLE_0:def 5;
end;
let x be object;
assume
A36: x in Carrier(f);
then x in rng F by A7,A21,XBOOLE_0:def 5;
then consider y being object such that
A37: y in dom F and
A38: F.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A37,FINSEQ_3:23;
now
assume not y in Seg k;
then y in dom F \ Seg k by A37,XBOOLE_0:def 5;
then y in Seg(k + 1) \ Seg k by A10,FINSEQ_1:def 3;
then y in {k + 1} by FINSEQ_3:15;
then y = k + 1 by TARSKI:def 1;
then not v in {v} by A21,A36,A38,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then y in dom F /\ Seg k by A37,XBOOLE_0:def 4;
then
A39: y in dom G by RELAT_1:61;
then G.y = F.y by FUNCT_1:47;
hence thesis by A38,A39,FUNCT_1:def 3;
end;
Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
.= dom(f (#) G) by A29,FINSEQ_1:def 3;
then
A40: dom(f (#) G) = dom(l (#) F) /\ Seg k by A11,FINSEQ_1:def 3;
now
let x be object;
A41: rng F c= the carrier of V by FINSEQ_1:def 4;
assume
A42: x in dom(f (#) G);
then reconsider n = x as Nat by FINSEQ_3:23;
n in dom(l (#) F) by A40,A42,XBOOLE_0:def 4;
then
A43: n in dom F by A10,A11,FINSEQ_3:29;
then F.n in rng F by FUNCT_1:def 3;
then reconsider w = F.n as Vector of V by A41;
A44: n in dom G by A28,A29,A42,FINSEQ_3:29;
then
A45: G.n in rng G by FUNCT_1:def 3;
rng G c= the carrier of V by FINSEQ_1:def 4;
then reconsider u = G.n as Vector of V by A45;
not u in {v} by A21,A30,A45,XBOOLE_0:def 5;
then
A46: u <> v by TARSKI:def 1;
A47: (f (#) G).n = u * f.u by A44,Th23
.= u * l.u by A15,A46;
w = u by A44,FUNCT_1:47;
hence (f (#) G).x = (l (#) F).x by A47,A43,Th23;
end;
then f (#) G = (l (#) F) | Seg k by A40,FUNCT_1:46;
then
A48: f (#) G = (l (#) F) | dom (f (#) G) by A29,FINSEQ_1:def 3;
v in rng F by A13,FUNCT_1:def 3;
then {v} c= Carrier(l) by A7,ZFMISC_1:31;
then card(Carrier(f)) = k + 1 - card{v} by A9,A21,CARD_2:44
.= k + 1 - 1 by CARD_1:30
.= k by XCMPLX_1:26;
then
A49: Sum(f) in A by A5;
G is one-to-one by A6,FUNCT_1:52;
then
A50: Sum(f (#) G) = Sum(f) by A30,Def7;
(l (#) F).(len F) = v * l.v by A10,A13,Th23;
then Sum(l (#) F) = Sum (f (#) G) + v * l.v by A10,A11,A29,A48,
RLVECT_1:38;
hence Sum(l) in A by A3,A8,A20,A50,A49;
end;
then
A51: for k be Nat st P[k] holds P[k+1];
let l;
A52: card Carrier l = card Carrier l;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A51);
hence thesis by A52;
end;
assume
A53: for l holds Sum(l) in A;
hence A <> {};
ZeroLC(V) is Linear_Combination of A & Sum(ZeroLC(V)) = 0.V by Lm3,Th20;
then
A54: 0.V in A by A53;
A55: for a,v st v in A holds v * a in A
proof
let a,v;
assume
A56: v in A;
now
per cases;
suppose
a = 0.R;
hence thesis by A54,VECTSP_2:32;
end;
suppose
A57: a <> 0.R;
deffunc F(Element of V)=0.R;
consider f such that
A58: f.v = a and
A59: for u being Element of V st u <> v holds f.u = F(u) from
FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R)
by FUNCT_2:8;
now
let u;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0.R by A59;
end;
then reconsider f as Linear_Combination of V by Def2;
A60: Carrier(f) = {v}
proof
thus Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A61: x = u and
A62: f.u <> 0.R;
u = v by A59,A62;
hence thesis by A61,TARSKI:def 1;
end;
let x be object;
assume x in {v};
then x = v by TARSKI:def 1;
hence thesis by A57,A58;
end;
{v} c= A by A56,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by A60,Def5;
consider F such that
A63: F is one-to-one & rng F = Carrier(f) and
A64: Sum(f (#) F) = Sum(f) by Def7;
F = <* v *> by A60,A63,FINSEQ_3:97;
then f (#) F = <* v * f.v *> by Th25;
then Sum(f) = v * a by A58,A64,RLVECT_1:44;
hence thesis by A53;
end;
end;
hence thesis;
end;
thus for v,u st v in A & u in A holds v + u in A
proof
let v,u;
assume that
A65: v in A and
A66: u in A;
now
per cases;
suppose
u = v;
then v + u = v * 1_R + v by VECTSP_2:def 9
.= v * 1_R + v * 1_R by VECTSP_2:def 9
.= v * (1_R + 1_R) by VECTSP_2:def 9;
hence thesis by A55,A65;
end;
suppose
A67: v <> u;
deffunc F(Element of V)=0.R;
consider f such that
A68: f.v = 1_R & f.u = 1_R and
A69: for w being Element of V st w <> v & w <> u holds f.w = F(w)
from FUNCT_2:sch 7(A67);
reconsider f as Element of Funcs(the carrier of V, the carrier of R)
by FUNCT_2:8;
now
let w;
assume not w in {v,u};
then w <> v & w <> u by TARSKI:def 2;
hence f.w = 0.R by A69;
end;
then reconsider f as Linear_Combination of V by Def2;
A70: Carrier(f) = {v,u}
proof
thus Carrier(f) c= {v,u}
proof
let x be object;
assume x in Carrier(f);
then ex w st x = w & f.w <> 0.R;
then x = v or x = u by A69;
hence thesis by TARSKI:def 2;
end;
let x be object;
assume x in {v,u};
then x = v or x = u by TARSKI:def 2;
hence thesis by A1,A68;
end;
then
A71: Carrier(f) c= A by A65,A66,ZFMISC_1:32;
A72: u * 1_R = u & v * 1_R = v by VECTSP_2:def 9;
reconsider f as Linear_Combination of A by A71,Def5;
consider F such that
A73: F is one-to-one & rng F = Carrier(f) and
A74: Sum(f (#) F) = Sum(f) by Def7;
F = <* v,u *> or F = <* u,v *> by A67,A70,A73,FINSEQ_3:99;
then f (#) F = <* v * 1_R, u * 1_R *> or f (#) F = <* u * 1_R, v *
1_R *> by A68,Th26;
then Sum(f) = v + u by A74,A72,RLVECT_1:45;
hence thesis by A53;
end;
end;
hence thesis;
end;
thus thesis by A55;
end;
theorem
Sum(ZeroLC(V)) = 0.V by Lm3;
theorem Th31:
for l being Linear_Combination of {}(the carrier of V) holds Sum (l) = 0.V
proof
let l be Linear_Combination of {}(the carrier of V);
l = ZeroLC(V) by Th21;
hence thesis by Lm3;
end;
theorem Th32:
for l being Linear_Combination of {v} holds Sum(l) = v * l.v
proof
let l be Linear_Combination of {v};
A1: Carrier(l) c= {v} by Def5;
now
per cases by A1,ZFMISC_1:33;
suppose
Carrier(l) = {};
then
A2: l = ZeroLC(V) by Def4;
hence Sum(l) = 0.V by Lm3
.= v * 0.R by VECTSP_2:32
.= v * l.v by A2,Th18;
end;
suppose
Carrier(l) = {v};
then consider F such that
A3: F is one-to-one & rng F = {v} and
A4: Sum(l) = Sum(l (#) F) by Def7;
F = <* v *> by A3,FINSEQ_3:97;
then l (#) F = <* v * l.v *> by Th25;
hence thesis by A4,RLVECT_1:44;
end;
end;
hence thesis;
end;
theorem Th33:
v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
Sum (l) = v1 * l.v1 + v2 * l.v2
proof
assume
A1: v1 <> v2;
let l be Linear_Combination of {v1,v2};
A2: Carrier(l) c= {v1,v2} by Def5;
now
per cases by A2,ZFMISC_1:36;
suppose
Carrier(l) = {};
then
A3: l = ZeroLC(V) by Def4;
hence Sum(l) = 0.V by Lm3
.= 0.V + 0.V by RLVECT_1:def 4
.= v1 * 0.R + 0.V by VECTSP_2:32
.= v1 * 0.R + v2 * 0.R by VECTSP_2:32
.= v1 * l.v1 + v2 * 0.R by A3,Th18
.= v1 * l.v1 + v2 * l.v2 by A3,Th18;
end;
suppose
A4: Carrier(l) = {v1};
then reconsider L = l as Linear_Combination of {v1} by Def5;
A5: not v2 in Carrier(l) by A1,A4,TARSKI:def 1;
thus Sum(l) = Sum(L) .= v1 * l.v1 by Th32
.= v1 * l.v1 + 0.V by RLVECT_1:def 4
.= v1 * l.v1 + v2 * 0.R by VECTSP_2:32
.= v1 * l.v1 + v2 * l.v2 by A5;
end;
suppose
A6: Carrier(l) = {v2};
then reconsider L = l as Linear_Combination of {v2} by Def5;
A7: not v1 in Carrier(l) by A1,A6,TARSKI:def 1;
thus Sum(l) = Sum(L) .= v2 * l.v2 by Th32
.= 0.V + v2 * l.v2 by RLVECT_1:def 4
.= v1 * 0.R + v2 * l.v2 by VECTSP_2:32
.= v1 * l.v1 + v2 * l.v2 by A7;
end;
suppose
Carrier(l) = {v1,v2};
then consider F such that
A8: F is one-to-one & rng F = {v1,v2} and
A9: Sum(l) = Sum(l (#) F) by Def7;
F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A8,FINSEQ_3:99;
then l (#) F = <* v1 * l.v1, v2 * l.v2 *> or l (#) F = <* v2 * l.v2, v1
* l.v1 *> by Th26;
hence thesis by A9,RLVECT_1:45;
end;
end;
hence thesis;
end;
theorem
Carrier(L) = {} implies Sum(L) = 0.V
proof
assume Carrier(L) = {};
then L = ZeroLC(V) by Def4;
hence thesis by Lm3;
end;
theorem Th35:
Carrier(L) = {v} implies Sum(L) = v * L.v
proof
assume Carrier(L) = {v};
then L is Linear_Combination of {v} by Def5;
hence thesis by Th32;
end;
theorem
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = v1 * L.v1 + v2 * L.v2
proof
assume that
A1: Carrier(L) = {v1,v2} and
A2: v1 <> v2;
L is Linear_Combination of {v1,v2} by A1,Def5;
hence thesis by A2,Th33;
end;
definition
let R, V, L1, L2;
redefine pred L1 = L2 means :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for v holds L1.v = L2.v;
compatibility by FUNCT_2:63;
end;
definition
let R, V, L1, L2;
func L1 + L2 -> Linear_Combination of V means
:Def9:
for v holds it.v = L1. v + L2.v;
existence
proof
deffunc F(Element of V)=L1.$1 + L2.$1;
consider f being Function of V, R such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of V,the carrier of R) by
FUNCT_2:8;
now
let v;
assume
A2: not v in (Carrier(L1) \/ Carrier(L2));
then not v in Carrier(L2) by XBOOLE_0:def 3;
then
A3: L2.v = 0.R;
not v in Carrier(L1) by A2,XBOOLE_0:def 3;
then L1.v = 0.R;
hence f.v = 0.R + 0.R by A1,A3
.= 0.R by RLVECT_1:4;
end;
then reconsider f as Linear_Combination of V by Def2;
take f;
let v;
thus thesis by A1;
end;
uniqueness
proof
let M,N be Linear_Combination of V;
assume
A4: for v holds M.v = L1.v + L2.v;
assume
A5: for v holds N.v = L1.v + L2.v;
let v;
thus M.v = L1.v + L2.v by A4
.= N.v by A5;
end;
end;
theorem Th37:
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2)
proof
let x be object;
assume x in Carrier(L1 + L2);
then consider u such that
A1: x = u and
A2: (L1 + L2).u <> 0.R;
(L1 + L2).u = L1.u + L2.u by Def9;
then L1.u <> 0.R or L2.u <> 0.R by A2,RLVECT_1:4;
then x in {v1 : L1.v1 <> 0.R} or x in {v2 : L2.v2 <> 0.R} by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th38:
L1 is Linear_Combination of A & L2 is Linear_Combination of A
implies L1 + L2 is Linear_Combination of A
proof
assume L1 is Linear_Combination of A & L2 is Linear_Combination of A;
then Carrier(L1) c= A & Carrier(L2) c= A by Def5;
then
A1: Carrier(L1) \/ Carrier(L2) c= A by XBOOLE_1:8;
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by Th37;
hence Carrier(L1 + L2) c= A by A1;
end;
theorem Th39:
for R being comRing for V being RightMod of R for L1, L2 being
Linear_Combination of V holds L1 + L2 = L2 + L1
proof
let R be comRing;
let V be RightMod of R;
let L1, L2 be Linear_Combination of V;
let v be Vector of V;
thus (L1 + L2).v = L2.v + L1.v by Def9
.= (L2 + L1).v by Def9;
end;
theorem
L1 + (L2 + L3) = L1 + L2 + L3
proof
let v;
thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def9
.= L1.v + (L2.v + L3.v) by Def9
.= L1.v + L2.v + L3.v by RLVECT_1:def 3
.= (L1 + L2).v + L3.v by Def9
.= (L1 + L2 + L3).v by Def9;
end;
theorem
for R being comRing for V being RightMod of R for L being
Linear_Combination of V holds L + ZeroLC(V) = L & ZeroLC(V) + L = L
proof
let R be comRing;
let V be RightMod of R;
let L be Linear_Combination of V;
thus L + ZeroLC(V) = L
proof
let v be Vector of V;
thus (L + ZeroLC(V)).v = L.v + ZeroLC(V).v by Def9
.= L.v + 0.R by Th18
.= L.v by RLVECT_1:4;
end;
hence thesis by Th39;
end;
definition
let R, V, a, L;
func L * a -> Linear_Combination of V means
:Def10:
for v holds it.v = L.v * a;
existence
proof
deffunc F(Element of V)=L.$1 * a;
consider f being Function of V, R such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of V,the carrier of R) by
FUNCT_2:8;
now
let v;
assume not v in Carrier(L);
then L.v = 0.R;
hence f.v = 0.R * a by A1
.= 0.R;
end;
then reconsider f as Linear_Combination of V by Def2;
take f;
let v;
thus thesis by A1;
end;
uniqueness
proof
let L1,L2;
assume
A2: for v holds L1.v = L.v * a;
assume
A3: for v holds L2.v = L.v * a;
let v;
thus L1.v = L.v * a by A2
.= L2.v by A3;
end;
end;
theorem Th42:
Carrier(L * a) c= Carrier(L)
proof
set T = {u : (L * a).u <> 0.R};
set S = {v : L.v <> 0.R};
T c= S
proof
let x be object;
assume x in T;
then consider u such that
A1: x = u and
A2: (L * a).u <> 0.R;
(L * a).u = L.u * a by Def10;
then L.u <> 0.R by A2;
hence thesis by A1;
end;
hence thesis;
end;
reserve RR for domRing;
reserve VV for RightMod of RR;
reserve LL for Linear_Combination of VV;
reserve aa for Scalar of RR;
reserve uu, vv for Vector of VV;
theorem Th43:
aa <> 0.RR implies Carrier(LL * aa) = Carrier(LL)
proof
set T = {uu : (LL * aa).uu <> 0.RR};
set S = {vv : LL.vv <> 0.RR};
assume
A1: aa <> 0.RR;
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider uu such that
A2: x = uu and
A3: (LL * aa).uu <> 0.RR;
(LL * aa).uu = LL.uu * aa by Def10;
then LL.uu <> 0.RR by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider vv such that
A4: x = vv and
A5: LL.vv <> 0.RR;
(LL * aa).vv = LL.vv * aa by Def10;
then (LL * aa).vv <> 0.RR by A1,A5,VECTSP_2:def 1;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th44:
L * 0.R = ZeroLC(V)
proof
let v;
thus (L * 0.R).v = L.v * 0.R by Def10
.= 0.R
.= ZeroLC(V).v by Th18;
end;
theorem Th45:
L is Linear_Combination of A implies L * a is Linear_Combination of A
proof
assume L is Linear_Combination of A;
then
A1: Carrier(L) c= A by Def5;
Carrier(L * a) c= Carrier(L) by Th42;
then Carrier(L * a) c= A by A1;
hence thesis by Def5;
end;
theorem
L * (a + b) = L * a + L * b
proof
let v;
thus (L * (a + b)).v = L.v * (a + b) by Def10
.= L.v * a + L.v * b by VECTSP_1:def 7
.= (L * a).v + L.v * b by Def10
.= (L * a).v + (L * b).v by Def10
.= ((L * a) + (L * b)).v by Def9;
end;
theorem
(L1 + L2) * a = L1 * a + L2 * a
proof
let v;
thus ((L1 + L2) * a).v = (L1 + L2).v * a by Def10
.= (L1.v + L2.v) * a by Def9
.= L1.v * a + L2.v * a by VECTSP_1:def 7
.= (L1 * a).v + L2.v * a by Def10
.= (L1 * a).v + (L2 * a). v by Def10
.= ((L1 * a) + (L2 * a)).v by Def9;
end;
theorem Th48:
(L * b) * a = L * (b * a)
proof
let v;
thus ((L * b) * a).v = (L * b).v * a by Def10
.= L.v * b * a by Def10
.= L.v * (b * a) by GROUP_1:def 3
.= (L * (b * a)).v by Def10;
end;
theorem
L * 1_R = L
proof
let v;
thus (L * 1_R).v = L.v * 1_R by Def10
.= L.v;
end;
definition
let R, V, L;
func - L -> Linear_Combination of V equals
L * (- 1_R);
correctness;
involutiveness
proof
let L, L9 be Linear_Combination of V;
assume
A1: L = L9 * (- 1_R);
let v;
thus L9.v = L9.v * (1_R)
.= L9.v * ((1_R) * (1_R))
.= L9.v * ((- 1_R) * (- 1_R)) by VECTSP_1:10
.= (L9 * ((- 1_R) * (- 1_R))).v by Def10
.= (L * (- 1_R)).v by A1,Th48;
end;
end;
theorem Th50:
(- L).v = - L.v
proof
thus (- L).v = L.v * (- 1_R) by Def10
.= - L.v by VECTSP_2:28;
end;
theorem
L1 + L2 = ZeroLC(V) implies L2 = - L1
proof
assume
A1: L1 + L2 = ZeroLC(V);
let v;
L1.v + L2.v = ZeroLC(V).v by A1,Def9
.= 0.R by Th18;
hence L2.v = - L1.v by RLVECT_1:6
.= (- L1).v by Th50;
end;
theorem Th52:
Carrier(- L) = Carrier(L)
proof
set a = -1_R;
Carrier(L * a) = Carrier(L)
proof
set S = {v : L.v <> 0.R};
set T = {u : (L * a).u <> 0.R};
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider u such that
A1: x = u and
A2: (L * a).u <> 0.R;
(L * a).u = L.u * a by Def10;
then L.u <> 0.R by A2;
hence thesis by A1;
end;
let x be object;
assume x in S;
then consider v such that
A3: x = v and
A4: L.v <> 0.R;
(L * a).v = L.v * a by Def10
.= -(L.v) by VECTSP_2:28;
then (L * a).v <> 0.R by A4,VECTSP_2:3;
hence thesis by A3;
end;
hence thesis;
end;
hence thesis;
end;
theorem
L is Linear_Combination of A implies - L is Linear_Combination of A by Th45;
definition
let R, V, L1, L2;
func L1 - L2 -> Linear_Combination of V equals
L1 + (- L2);
correctness;
end;
theorem Th54:
(L1 - L2).v = L1.v - L2.v
proof
thus (L1 - L2).v = L1.v + (- L2).v by Def9
.= L1.v + (- L2.v) by Th50
.= L1.v - L2.v by RLVECT_1:def 11;
end;
theorem
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2)
proof
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(- L2) by Th37;
hence thesis by Th52;
end;
theorem
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A
proof
assume that
A1: L1 is Linear_Combination of A and
A2: L2 is Linear_Combination of A;
- L2 is Linear_Combination of A by A2,Th45;
hence thesis by A1,Th38;
end;
theorem
L - L = ZeroLC(V)
proof
let v;
thus (L - L).v = L.v - L.v by Th54
.= 0.R by RLVECT_1:15
.= ZeroLC(V).v by Th18;
end;
theorem Th58:
Sum(L1 + L2) = Sum(L1) + Sum(L2)
proof
set A = Carrier(L1 + L2) \/ Carrier(L1) \/ Carrier(L2);
set C1 = A \ Carrier(L1);
consider p such that
A1: rng p = C1 and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of V by A1,FINSEQ_1:def 4;
A3: A = Carrier(L1) \/ (Carrier(L1 + L2) \/ Carrier(L2)) by XBOOLE_1:4;
set C3 = A \ Carrier(L1 + L2);
consider r such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of V by A4,FINSEQ_1:def 4;
A6: A = Carrier(L1 + L2) \/ (Carrier(L1) \/ Carrier(L2)) by XBOOLE_1:4;
set C2 = A \ Carrier(L2);
consider q such that
A7: rng q = C2 and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q as FinSequence of V by A7,FINSEQ_1:def 4;
consider F such that
A9: F is one-to-one and
A10: rng F = Carrier(L1 + L2) and
A11: Sum((L1 + L2) (#) F) = Sum(L1 + L2) by Def7;
set FF = F ^ r;
consider G such that
A12: G is one-to-one and
A13: rng G = Carrier(L1) and
A14: Sum(L1 (#) G) = Sum(L1) by Def7;
rng FF = rng F \/ rng r by FINSEQ_1:31;
then rng FF = Carrier(L1 + L2) \/ A by A10,A4,XBOOLE_1:39;
then
A15: rng FF = A by A6,XBOOLE_1:7,12;
set GG = G ^ p;
rng GG = rng G \/ rng p by FINSEQ_1:31;
then rng GG = Carrier(L1) \/ A by A13,A1,XBOOLE_1:39;
then
A16: rng GG = A by A3,XBOOLE_1:7,12;
rng F misses rng r
proof
set x = the Element of rng F /\ rng r;
assume not thesis;
then rng F /\ rng r <> {};
then x in Carrier(L1 + L2) & x in C3 by A10,A4,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A17: FF is one-to-one by A9,A5,FINSEQ_3:91;
rng G misses rng p
proof
set x = the Element of rng G /\ rng p;
assume not thesis;
then rng G /\ rng p <> {};
then x in Carrier(L1) & x in C1 by A13,A1,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A18: GG is one-to-one by A12,A2,FINSEQ_3:91;
then
A19: len GG = len FF by A17,A16,A15,FINSEQ_1:48;
deffunc Q(Nat)=FF <- (GG.$1);
consider P being FinSequence such that
A20: len P = len FF and
A21: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A22: dom P = Seg len FF by A20,FINSEQ_1:def 3;
A23: now
let x be object;
assume
A24: x in dom GG;
then reconsider n = x as Nat by FINSEQ_3:23;
GG.n in rng FF by A16,A15,A24,FUNCT_1:def 3;
then
A25: FF just_once_values GG.n by A17,FINSEQ_4:8;
n in Seg(len FF) by A19,A24,FINSEQ_1:def 3;
then FF.(P.n) = FF.(FF <- (GG.n)) by A21,A22
.= GG.n by A25,FINSEQ_4:def 3;
hence GG.x = FF.(P.x);
end;
A26: dom GG = dom FF by A19,FINSEQ_3:29;
A27: rng P c= dom FF
proof
let x be object;
assume x in rng P;
then consider y being object such that
A28: y in dom P and
A29: P.y = x by FUNCT_1:def 3;
reconsider y as Nat by A28,FINSEQ_3:23;
y in dom FF by A20,A28,FINSEQ_3:29;
then GG.y in rng FF by A16,A15,A26,FUNCT_1:def 3;
then
A30: FF just_once_values GG.y by A17,FINSEQ_4:8;
P.y = FF <- (GG.y) by A21,A28;
hence thesis by A29,A30,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom P & P.x in dom FF
proof
assume x in dom GG;
hence x in dom P by A19,A20,FINSEQ_3:29;
then P.x in rng P by FUNCT_1:def 3;
hence thesis by A27;
end;
assume that
A31: x in dom P and
P.x in dom FF;
x in Seg(len P) by A31,FINSEQ_1:def 3;
hence x in dom GG by A19,A20,FINSEQ_1:def 3;
end;
then
A32: GG = FF * P by A23,FUNCT_1:10;
dom FF c= rng P
proof
set f = FF" * GG;
let x be object;
assume
A33: x in dom FF;
dom(FF") = rng GG by A17,A16,A15,FUNCT_1:33;
then
A34: rng f = rng(FF") by RELAT_1:28
.= dom FF by A17,FUNCT_1:33;
f = FF " * FF * P by A32,RELAT_1:36
.= id(dom FF) * P by A17,FUNCT_1:39
.= P by A27,RELAT_1:53;
hence thesis by A33,A34;
end;
then
A35: dom FF = rng P by A27;
A36: len r = len((L1 + L2) (#) r) by Def6;
now
let k;
assume
A37: k in dom r;
then r/.k = r.k by PARTFUN1:def 6;
then r/.k in C3 by A4,A37,FUNCT_1:def 3;
then
A38: not r/.k in Carrier((L1 + L2)) by XBOOLE_0:def 5;
k in dom((L1 + L2) (#) r) by A36,A37,FINSEQ_3:29;
then ((L1 + L2) (#) r).k = (r/.k) * (L1 + L2).(r/.k) by Def6;
hence ((L1 + L2) (#) r).k = (r/.k) * 0.R by A38;
end;
then
A39: Sum((L1 + L2) (#) r) = Sum(r) * 0.R by A36,Lm2
.= 0.V by VECTSP_2:32;
A40: len p = len(L1 (#) p) by Def6;
now
let k;
assume
A41: k in dom p;
then p/.k = p.k by PARTFUN1:def 6;
then p/.k in C1 by A1,A41,FUNCT_1:def 3;
then
A42: not p/.k in Carrier(L1) by XBOOLE_0:def 5;
k in dom(L1 (#) p) by A40,A41,FINSEQ_3:29;
then (L1 (#) p).k = (p/.k) * L1.(p/.k) by Def6;
hence (L1 (#) p).k = (p/.k) * 0.R by A42;
end;
then
A43: Sum(L1 (#) p) = Sum(p) * 0.R by A40,Lm2
.= 0.V by VECTSP_2:32;
set f = (L1 + L2) (#) FF;
consider H such that
A44: H is one-to-one and
A45: rng H = Carrier(L2) and
A46: Sum(L2 (#) H) = Sum(L2) by Def7;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of rng H /\ rng q;
assume not thesis;
then rng H /\ rng q <> {};
then x in Carrier(L2) & x in C2 by A45,A7,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A47: HH is one-to-one by A44,A8,FINSEQ_3:91;
A48: len q = len(L2 (#) q) by Def6;
now
let k;
assume
A49: k in dom q;
then q/.k = q.k by PARTFUN1:def 6;
then q/.k in C2 by A7,A49,FUNCT_1:def 3;
then
A50: not q/.k in Carrier(L2) by XBOOLE_0:def 5;
k in dom(L2 (#) q) by A48,A49,FINSEQ_3:29;
then (L2 (#) q).k = (q/.k) * L2.(q/.k) by Def6;
hence (L2 (#) q).k = (q/.k) * 0.R by A50;
end;
then
A51: Sum(L2 (#) q) = Sum(q) * 0.R by A48,Lm2
.= 0.V by VECTSP_2:32;
set g = L1 (#) GG;
A52: len g = len GG by Def6;
then
A53: Seg len GG = dom g by FINSEQ_1:def 3;
rng HH = rng H \/ rng q by FINSEQ_1:31;
then rng HH = Carrier(L2) \/ A by A45,A7,XBOOLE_1:39;
then
A54: rng HH = A by XBOOLE_1:7,12;
then
A55: len GG = len HH by A47,A18,A16,FINSEQ_1:48;
deffunc Q(Nat)=HH <- (GG.$1);
consider R being FinSequence such that
A56: len R = len HH and
A57: for k be Nat st k in dom R holds R.k = Q(k) from FINSEQ_1:sch 2;
A58: dom R = Seg len HH by A56,FINSEQ_1:def 3;
A59: now
let x be object;
assume
A60: x in dom GG;
then reconsider n = x as Nat by FINSEQ_3:23;
GG.n in rng HH by A16,A54,A60,FUNCT_1:def 3;
then
A61: HH just_once_values GG.n by A47,FINSEQ_4:8;
n in Seg(len HH) by A55,A60,FINSEQ_1:def 3;
then HH.(R.n) = HH.(HH <- (GG.n)) by A57,A58
.= GG.n by A61,FINSEQ_4:def 3;
hence GG.x = HH.(R.x);
end;
A62: dom GG = dom HH by A55,FINSEQ_3:29;
A63: rng R c= dom HH
proof
let x be object;
assume x in rng R;
then consider y being object such that
A64: y in dom R and
A65: R.y = x by FUNCT_1:def 3;
reconsider y as Nat by A64,FINSEQ_3:23;
y in dom HH by A56,A64,FINSEQ_3:29;
then GG.y in rng HH by A16,A54,A62,FUNCT_1:def 3;
then
A66: HH just_once_values GG.y by A47,FINSEQ_4:8;
R.y = HH <- (GG.y) by A57,A64;
hence thesis by A65,A66,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom R & R.x in dom HH
proof
assume x in dom GG;
then x in Seg(len R) by A55,A56,FINSEQ_1:def 3;
hence x in dom R by FINSEQ_1:def 3;
then R.x in rng R by FUNCT_1:def 3;
hence thesis by A63;
end;
assume that
A67: x in dom R and
R.x in dom HH;
x in Seg(len R) by A67,FINSEQ_1:def 3;
hence x in dom GG by A55,A56,FINSEQ_1:def 3;
end;
then
A68: GG = HH * R by A59,FUNCT_1:10;
dom HH c= rng R
proof
set f = HH" * GG;
let x be object;
assume
A69: x in dom HH;
dom(HH") = rng GG by A47,A16,A54,FUNCT_1:33;
then
A70: rng f = rng(HH") by RELAT_1:28
.= dom HH by A47,FUNCT_1:33;
f = HH " * HH * R by A68,RELAT_1:36
.= id(dom HH) * R by A47,FUNCT_1:39
.= R by A63,RELAT_1:53;
hence thesis by A69,A70;
end;
then
A71: dom HH = rng R by A63;
A72: Sum(g) = Sum((L1 (#) G) ^ (L1 (#) p)) by Th28
.= Sum(L1 (#) G) + 0.V by A43,RLVECT_1:41
.= Sum(L1 (#) G) by RLVECT_1:def 4;
set h = L2 (#) HH;
A73: Sum(h) = Sum((L2 (#) H) ^ (L2 (#) q)) by Th28
.= Sum(L2 (#) H) + 0.V by A51,RLVECT_1:41
.= Sum(L2 (#) H) by RLVECT_1:def 4;
A74: Sum(f) = Sum(((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th28
.= Sum((L1 + L2) (#) F) + 0.V by A39,RLVECT_1:41
.= Sum((L1 + L2) (#) F) by RLVECT_1:def 4;
A75: dom P = dom FF by A20,FINSEQ_3:29;
then
A76: P is one-to-one by A35,FINSEQ_4:60;
A77: dom R = dom HH by A56,FINSEQ_3:29;
then
A78: R is one-to-one by A71,FINSEQ_4:60;
reconsider R as Function of dom HH, dom HH by A63,A77,FUNCT_2:2;
A79: len h = len HH by Def6;
then
A80: dom h = dom HH by FINSEQ_3:29;
then reconsider R as Function of dom h, dom h;
reconsider Hp = h * R as FinSequence of V by FINSEQ_2:47;
reconsider R as Permutation of dom h by A71,A78,A80,FUNCT_2:57;
A81: Hp = h * R;
then
A82: len Hp = len GG by A55,A79,FINSEQ_2:44;
reconsider P as Function of dom FF, dom FF by A27,A75,FUNCT_2:2;
A83: len f = len FF by Def6;
then
A84: dom f = dom FF by FINSEQ_3:29;
then reconsider P as Function of dom f, dom f;
reconsider Fp = f * P as FinSequence of V by FINSEQ_2:47;
reconsider P as Permutation of dom f by A35,A76,A84,FUNCT_2:57;
A85: Fp = f * P;
then
A86: Sum(Fp) = Sum(f) by RLVECT_2:7;
deffunc Q(Nat) = (g/.$1) + (Hp/.$1);
consider I being FinSequence such that
A87: len I = len GG and
A88: for k be Nat st k in dom I holds I.k = Q(k) from FINSEQ_1:sch 2;
A89: dom I = Seg len GG by A87,FINSEQ_1:def 3;
then
A90: for k be Nat st k in Seg(len GG) holds I.k = Q(k) by A88;
rng I c= the carrier of V
proof
let x be object;
assume x in rng I;
then consider y being object such that
A91: y in dom I and
A92: I.y = x by FUNCT_1:def 3;
reconsider y as Nat by A91,FINSEQ_3:23;
I.y = (g/.y) + (Hp/.y) by A88,A91;
hence thesis by A92;
end;
then reconsider I as FinSequence of V by FINSEQ_1:def 4;
A93: len Fp = len I by A19,A83,A85,A87,FINSEQ_2:44;
A94: now
let x be object;
assume
A95: x in Seg(len I);
then reconsider k = x as Element of NAT;
A96: x in dom HH by A55,A87,A95,FINSEQ_1:def 3;
then R.k in dom R by A71,A77,FUNCT_1:def 3;
then reconsider j = R.k as Nat by FINSEQ_3:23;
A97: x in dom GG by A87,A95,FINSEQ_1:def 3;
then
A98: HH.j = GG.k by A59
.= GG/.k by A97,PARTFUN1:def 6;
P.k in dom P by A26,A62,A35,A75,A96,FUNCT_1:def 3;
then reconsider l = P.k as Nat by FINSEQ_3:23;
set v = GG/.k;
A99: x in dom Fp by A93,A95,FINSEQ_1:def 3;
A100: FF.l = GG.k by A23,A97
.= GG/.k by A97,PARTFUN1:def 6;
P.k in dom FF by A26,A62,A35,A75,A96,FUNCT_1:def 3;
then
A101: f.l = v * (L1 + L2).v by A100,Th23
.= v * (L1.v + L2.v) by Def9
.= v * L1.v + v * L2.v by VECTSP_2:def 9;
A102: x in dom Hp by A87,A82,A95,FINSEQ_1:def 3;
then
A103: Hp/.k = (h * R).k by PARTFUN1:def 6
.= h.(R.k) by A102,FUNCT_1:12;
R.k in dom HH by A71,A77,A96,FUNCT_1:def 3;
then
A104: h.j = v * L2.v by A98,Th23;
A105: x in dom g by A87,A52,A95,FINSEQ_1:def 3;
then g/.k = g.k by PARTFUN1:def 6
.= v * L1.v by A105,Def6;
hence I.x = v * L1.v + v * L2.v by A87,A88,A89,A95,A103,A104
.= Fp.x by A99,A101,FUNCT_1:12;
end;
dom I = Seg(len I) & dom Fp = Seg(len I) by A93,FINSEQ_1:def 3;
then
A106: I = Fp by A94;
Sum(Hp) = Sum(h) by A81,RLVECT_2:7;
hence thesis by A11,A14,A46,A72,A73,A74,A86,A87,A90,A82,A52,A106,A53,
RLVECT_2:2;
end;
reserve R for domRing;
reserve V for RightMod of R;
reserve L,L1,L2 for Linear_Combination of V;
reserve a for Scalar of R;
theorem Th59:
Sum(L * a) = Sum(L) * a
proof
per cases;
suppose
A1: a <> 0.R;
set l = L * a;
A2: Carrier(l) = Carrier(L) by A1,Th43;
consider G being FinSequence of V such that
A3: G is one-to-one and
A4: rng G = Carrier(L) and
A5: Sum(L) = Sum(L (#) G) by Def7;
set g = L (#) G;
consider F being FinSequence of V such that
A6: F is one-to-one and
A7: rng F = Carrier(L * a) and
A8: Sum(L * a) = Sum((L * a) (#) F) by Def7;
A9: len G = len F by A1,A6,A7,A3,A4,Th43,FINSEQ_1:48;
set f = (L * a) (#) F;
deffunc Q(Nat)= F <- (G.$1);
consider P being FinSequence such that
A10: len P = len F and
A11: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A12: dom P = Seg len F by A10,FINSEQ_1:def 3;
A13: now
let x be object;
assume
A14: x in dom G;
then reconsider n = x as Nat by FINSEQ_3:23;
G.n in rng F by A7,A4,A2,A14,FUNCT_1:def 3;
then
A15: F just_once_values G.n by A6,FINSEQ_4:8;
n in Seg len F by A9,A14,FINSEQ_1:def 3;
then F.(P.n) = F.(F <- (G.n)) by A11,A12
.= G.n by A15,FINSEQ_4:def 3;
hence G.x = F.(P.x);
end;
A16: rng P c= dom F
proof
let x be object;
assume x in rng P;
then consider y being object such that
A17: y in dom P and
A18: P.y = x by FUNCT_1:def 3;
reconsider y as Nat by A17,FINSEQ_3:23;
y in dom G by A10,A9,A17,FINSEQ_3:29;
then G.y in rng F by A7,A4,A2,FUNCT_1:def 3;
then
A19: F just_once_values G.y by A6,FINSEQ_4:8;
P.y = F <- (G.y) by A11,A17;
hence thesis by A18,A19,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom G implies x in dom P & P.x in dom F
proof
assume x in dom G;
then x in Seg(len P) by A10,A9,FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3;
then P.x in rng P by FUNCT_1:def 3;
hence thesis by A16;
end;
assume that
A20: x in dom P and
P.x in dom F;
x in Seg(len P) by A20,FINSEQ_1:def 3;
hence x in dom G by A10,A9,FINSEQ_1:def 3;
end;
then
A21: G = F * P by A13,FUNCT_1:10;
dom F c= rng P
proof
set f = F" * G;
let x be object;
assume
A22: x in dom F;
dom(F") = rng G by A6,A7,A4,A2,FUNCT_1:33;
then
A23: rng f = rng(F") by RELAT_1:28
.= dom F by A6,FUNCT_1:33;
f = F " * F * P by A21,RELAT_1:36
.= id(dom F) * P by A6,FUNCT_1:39
.= P by A16,RELAT_1:53;
hence thesis by A22,A23;
end;
then
A24: dom F = rng P by A16;
A25: dom P = dom F by A10,FINSEQ_3:29;
then
A26: P is one-to-one by A24,FINSEQ_4:60;
reconsider P as Function of dom F, dom F by A16,A25,FUNCT_2:2;
A27: len f = len F by Def6;
then
A28: dom f = dom F by FINSEQ_3:29;
then reconsider P as Function of dom f, dom f;
reconsider Fp = f * P as FinSequence of V by FINSEQ_2:47;
reconsider P as Permutation of dom f by A24,A26,A28,FUNCT_2:57;
A29: Fp = f * P;
then
A30: len Fp = len f by FINSEQ_2:44;
then
A31: len Fp = len g by A9,A27,Def6;
A32: now
let k;
let v be Vector of V;
assume that
A33: k in dom Fp and
A34: v = g.k;
A35: k in Seg(len g) by A31,A33,FINSEQ_1:def 3;
then
A36: k in dom P by A10,A27,A30,A31,FINSEQ_1:def 3;
A37: k in dom G by A9,A27,A30,A31,A35,FINSEQ_1:def 3;
then G.k in rng G by FUNCT_1:def 3;
then F just_once_values G.k by A6,A7,A4,A2,FINSEQ_4:8;
then
A38: (F <- (G.k)) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G.k) as Nat by FINSEQ_3:23;
A39: G/.k = G.k by A37,PARTFUN1:def 6
.= F.(P.k) by A21,A36,FUNCT_1:13
.= F.i by A11,A12,A27,A30,A31,A35
.= F/.i by A38,PARTFUN1:def 6;
A40: k in dom g by A35,FINSEQ_1:def 3;
i in Seg(len f) by A27,A38,FINSEQ_1:def 3;
then
A41: i in dom f by FINSEQ_1:def 3;
thus Fp.k = f.(P.k) by A36,FUNCT_1:13
.= f.(F <- (G.k)) by A11,A12,A27,A30,A31,A35
.= (F/.i) * l.(F/.i) by A41,Def6
.= (F/.i) * (L.(F/.i) * a) by Def10
.= (F/.i) * L.(F/.i) * a by VECTSP_2:def 9
.= v * a by A34,A40,A39,Def6;
end;
Sum(Fp) = Sum(f) by A29,RLVECT_2:7;
hence thesis by A8,A5,A31,A32,Th1;
end;
suppose
A42: a = 0.R;
hence Sum(L * a) = Sum(ZeroLC(V)) by Th44
.= 0.V by Lm3
.= Sum(L) * a by A42,VECTSP_2:32;
end;
end;
theorem Th60:
Sum(- L) = - Sum(L)
proof
thus Sum(- L) = Sum(L) * (- 1_R) by Th59
.= - Sum(L) by VECTSP_2:32;
end;
theorem
Sum(L1 - L2) = Sum(L1) - Sum(L2)
proof
thus Sum(L1 - L2) = Sum(L1) + Sum(- L2) by Th58
.= Sum(L1) + (- Sum(L2)) by Th60
.= Sum(L1) - Sum(L2) by RLVECT_1:def 11;
end;
begin :: RMOD_5
reserve x for set;
reserve R for Ring;
reserve V for RightMod of R;
reserve v,v1,v2 for Vector of V;
reserve A,B for Subset of V;
definition
let R, V;
let IT be Subset of V;
attr IT is linearly-independent means
for l being Linear_Combination of IT st Sum(l) = 0.V holds Carrier(l) = {};
end;
notation
let R, V;
let IT be Subset of V;
antonym IT is linearly-dependent for IT is linearly-independent;
end;
theorem
A c= B & B is linearly-independent implies A is linearly-independent
proof
assume that
A1: A c= B and
A2: B is linearly-independent;
let l be Linear_Combination of A;
reconsider L = l as Linear_Combination of B by A1,Th19;
assume Sum(l) = 0.V;
then Carrier(L) = {} by A2;
hence thesis;
end;
theorem Th63:
0.R <> 1_R & A is linearly-independent implies not 0.V in A
proof
assume that
A1: 0.R <> 1_R and
A2: A is linearly-independent and
A3: 0.V in A;
deffunc F(Element of V)=0.R;
consider f being Function of the carrier of V, the carrier of R such that
A4: f.(0.V) = 1_R and
A5: for v being Element of V st v <> 0.V holds f.v = F(v) from FUNCT_2:
sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
ex T being finite Subset of V st for v st not v in T holds f.v = 0.R
proof
take T = {0.V};
let v;
assume not v in T;
then v <> 0.V by TARSKI:def 1;
hence thesis by A5;
end;
then reconsider f as Linear_Combination of V by Def2;
A6: Carrier(f) = {0.V}
proof
thus Carrier(f) c= {0.V}
proof
let x be object;
assume x in Carrier(f);
then consider v such that
A7: v = x and
A8: f.v <> 0.R;
v = 0.V by A5,A8;
hence thesis by A7,TARSKI:def 1;
end;
let x be object;
assume x in {0.V};
then x = 0.V by TARSKI:def 1;
hence thesis by A1,A4;
end;
then Carrier(f) c= A by A3,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by Def5;
Sum(f) = 0.V * f.(0.V) by A6,Th35
.= 0.V by VECTSP_2:32;
hence contradiction by A2,A6;
end;
theorem
{}(the carrier of V) is linearly-independent
proof
let l be Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by Def5;
hence thesis;
end;
theorem Th65:
0.R <> 1_R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V
proof
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
assume 0.R <> 1_R & {v1,v2} is linearly-independent;
hence thesis by A1,Th63;
end;
theorem
0.R <> 1_R implies {v,0.V} is linearly-dependent & {0.V,v} is
linearly-dependent by Th65;
reserve R for domRing;
reserve V for RightMod of R;
reserve v,u for Vector of V;
reserve A,B for Subset of V;
reserve l for Linear_Combination of A;
reserve f,g for Function of the carrier of V, the carrier of R;
definition
let R, V, A;
func Lin(A) -> strict Submodule of V means
:Def14:
the carrier of it = the set of all Sum( l) ;
existence
proof
set A1 = the set of all Sum(l) ;
reconsider l = ZeroLC(V) as Linear_Combination of A by Th20;
A1 c= the carrier of V
proof
let x be object;
assume x in A1;
then ex l st x = Sum(l);
hence thesis;
end;
then reconsider A1 as Subset of V;
A1: A1 is linearly-closed
proof
thus for v,u st v in A1 & u in A1 holds v + u in A1
proof
let v,u;
assume that
A2: v in A1 and
A3: u in A1;
consider l1 being Linear_Combination of A such that
A4: v = Sum(l1) by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum(l2) by A3;
reconsider f = l1 + l2 as Linear_Combination of A by Th38;
v + u = Sum(f) by A4,A5,Th58;
hence thesis;
end;
let a be Scalar of R,v;
assume v in A1;
then consider l such that
A6: v = Sum(l);
reconsider f = l * a as Linear_Combination of A by Th45;
v * a = Sum(f) by A6,Th59;
hence thesis;
end;
Sum(l) = 0.V by Lm3;
then 0.V in A1;
hence thesis by A1,RMOD_2:34;
end;
uniqueness by RMOD_2:29;
end;
theorem Th67:
x in Lin(A) iff ex l st x = Sum(l)
proof
thus x in Lin(A) implies ex l st x = Sum(l)
proof
assume x in Lin(A);
then x in the carrier of Lin(A) by STRUCT_0:def 5;
then x in the set of all Sum(l) by Def14;
hence thesis;
end;
given k being Linear_Combination of A such that
A1: x = Sum(k);
x in the set of all Sum(l) by A1;
then x in the carrier of Lin(A) by Def14;
hence thesis by STRUCT_0:def 5;
end;
theorem Th68:
x in A implies x in Lin(A)
proof
deffunc F(Element of V)=0.R;
assume
A1: x in A;
then reconsider v = x as Vector of V;
consider f being Function of the carrier of V, the carrier of R such that
A2: f.v = 1_R and
A3: for u st u <> v holds f.u = F(u) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
ex T being finite Subset of V st for u st not u in T holds f.u = 0.R
proof
take T = {v};
let u;
assume not u in T;
then u <> v by TARSKI:def 1;
hence thesis by A3;
end;
then reconsider f as Linear_Combination of V by Def2;
A4: Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A5: x = u and
A6: f.u <> 0.R;
u = v by A3,A6;
hence thesis by A5,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by Def5;
A7: Sum(f) = v * 1_R by A2,Th32
.= v by VECTSP_2:def 9;
{v} c= A by A1,ZFMISC_1:31;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by Def5;
Sum(f) = v by A7;
hence thesis by Th67;
end;
theorem
Lin({}(the carrier of V)) = (0).V
proof
set A = Lin({}(the carrier of V));
now
let v;
thus v in A implies v in (0).V
proof
assume v in A;
then
A1: v in the carrier of A by STRUCT_0:def 5;
the carrier of A = the set of all
Sum(l0) where l0 is Linear_Combination of {}(the
carrier of V) by Def14;
then
ex l0 being Linear_Combination of {}(the carrier of V) st v = Sum(l0
) by A1;
then v = 0.V by Th31;
hence thesis by RMOD_2:35;
end;
assume v in (0).V;
then v = 0.V by RMOD_2:35;
hence v in A by RMOD_2:17;
end;
hence thesis by RMOD_2:30;
end;
theorem
Lin(A) = (0).V implies A = {} or A = {0.V}
proof
assume that
A1: Lin(A) = (0).V and
A2: A <> {};
thus A c= {0.V}
proof
let x be object;
assume x in A;
then x in Lin(A) by Th68;
then x = 0.V by A1,RMOD_2:35;
hence thesis by TARSKI:def 1;
end;
set y = the Element of A;
let x be object;
assume x in {0.V};
then
A3: x = 0.V by TARSKI:def 1;
y in A & y in Lin(A) by A2,Th68;
hence thesis by A1,A3,RMOD_2:35;
end;
theorem Th71:
for W being strict Submodule of V st 0.R <> 1_R & A = the
carrier of W holds Lin(A) = W
proof
let W be strict Submodule of V;
assume that
A1: 0.R <> 1_R and
A2: A = the carrier of W;
now
let v;
thus v in Lin(A) implies v in W
proof
assume v in Lin(A);
then
A3: ex l st v = Sum(l) by Th67;
A is linearly-closed by A2,RMOD_2:33;
then v in the carrier of W by A1,A2,A3,Th29;
hence thesis by STRUCT_0:def 5;
end;
v in W iff v in the carrier of W by STRUCT_0:def 5;
hence v in W implies v in Lin(A) by A2,Th68;
end;
hence thesis by RMOD_2:30;
end;
theorem
for V being strict RightMod of R, A being Subset of V st 0.R <> 1_R &
A = the carrier of V holds Lin(A) = V
proof
let V be strict RightMod of R, A be Subset of V such that
A1: 0.R <> 1_R;
assume
A2: A = the carrier of V;
(Omega).V = V;
hence thesis by A1,A2,Th71;
end;
theorem Th73:
A c= B implies Lin(A) is Submodule of Lin(B)
proof
assume
A1: A c= B;
now
let v;
assume v in Lin(A);
then consider l such that
A2: v = Sum(l) by Th67;
reconsider l as Linear_Combination of B by A1,Th19;
Sum(l) = v by A2;
hence v in Lin(B) by Th67;
end;
hence thesis by RMOD_2:28;
end;
theorem
for V being strict RightMod of R, A,B being Subset of V st Lin(A) = V
& A c= B holds Lin(B) = V
proof
let V be strict RightMod of R, A,B be Subset of V;
assume Lin(A) = V & A c= B;
then V is Submodule of Lin(B) by Th73;
hence thesis by RMOD_2:25;
end;
theorem
Lin(A \/ B) = Lin(A) + Lin(B)
proof
now
deffunc G(object)=0.R;
let v;
assume v in Lin(A \/ B);
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) by Th67;
deffunc F(object)=l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred P[object] means $1 in C;
defpred C[object] means $1 in D;
now
let x;
assume x in the carrier of V;
then reconsider v = x as Vector of V;
f.v in the carrier of R;
hence x in C implies l.x in the carrier of R;
assume not x in C;
thus 0.R in the carrier of R;
end;
then
A2: for x being object st x in the carrier of V
holds (P[x] implies F(x) in the
carrier of R ) & (not P[x] implies G(x) in the carrier of R);
consider f being Function of the carrier of V, the carrier of R such that
A3: for x being object st x in the carrier of V
holds (P[x] implies f.x = F(x)) &
(not P[x] implies f.x = G(x)) from FUNCT_2:sch 5(A2);
reconsider C as finite Subset of V;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
for u holds not u in C implies f.u = 0.R by A3;
then reconsider f as Linear_Combination of V by Def2;
A4: Carrier(f) c= C
proof
let x be object;
assume x in Carrier(f);
then
A5: ex u st x = u & f.u <> 0.R;
assume not x in C;
hence thesis by A3,A5;
end;
C c= A by XBOOLE_1:17;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by Def5;
now
let x;
assume x in the carrier of V;
then reconsider v = x as Vector of V;
g.v in the carrier of R;
hence x in D implies l.x in the carrier of R;
assume not x in D;
thus 0.R in the carrier of R;
end;
then
A6: for x being object st x in the carrier of V
holds (C[x] implies F(x) in the
carrier of R) & (not C[x] implies G(x) in the carrier of R);
consider g being Function of the carrier of V, the carrier of R such that
A7: for x being object st x in the carrier of V
holds (C[x] implies g.x = F(x)) &
(not C[x] implies g.x = G(x)) from FUNCT_2:sch 5(A6);
reconsider D as finite Subset of V;
reconsider g as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
for u holds not u in D implies g.u = 0.R by A7;
then reconsider g as Linear_Combination of V by Def2;
A8: D c= B
proof
let x be object;
assume x in D;
then
A9: x in Carrier(l) & not x in A by XBOOLE_0:def 5;
Carrier(l) c= A \/ B by Def5;
hence thesis by A9,XBOOLE_0:def 3;
end;
Carrier(g) c= D
proof
let x be object;
assume x in Carrier(g);
then
A10: ex u st x = u & g.u <> 0.R;
assume not x in D;
hence thesis by A7,A10;
end;
then Carrier(g) c= B by A8;
then reconsider g as Linear_Combination of B by Def5;
l = f + g
proof
let v;
now
per cases;
suppose
A11: v in C;
A12: now
assume v in D;
then not v in A by XBOOLE_0:def 5;
hence contradiction by A11,XBOOLE_0:def 4;
end;
thus (f + g).v = f.v + g.v by Def9
.= l.v + g.v by A3,A11
.= l.v + 0.R by A7,A12
.= l.v by RLVECT_1:4;
end;
suppose
A13: not v in C;
now
per cases;
suppose
A14: v in Carrier(l);
A15: now
assume not v in D;
then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
hence contradiction by A13,A14,XBOOLE_0:def 4;
end;
thus (f + g). v = f.v + g.v by Def9
.= 0.R + g.v by A3,A13
.= g.v by RLVECT_1:4
.= l.v by A7,A15;
end;
suppose
A16: not v in Carrier(l);
then
A17: not v in D by XBOOLE_0:def 5;
A18: not v in C by A16,XBOOLE_0:def 4;
thus (f + g).v = f.v + g.v by Def9
.= 0.R + g.v by A3,A18
.= 0.R + 0.R by A7,A17
.= 0.R by RLVECT_1:4
.= l.v by A16;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A19: v = Sum(f) + Sum(g) by A1,Th58;
Sum(f) in Lin(A) & Sum(g) in Lin(B) by Th67;
hence v in Lin(A) + Lin(B) by A19,RMOD_3:1;
end;
then
A20: Lin(A \/ B) is Submodule of Lin(A) + Lin(B) by RMOD_2:28;
Lin(A) is Submodule of Lin(A \/ B) & Lin(B) is Submodule of Lin(A \/ B)
by Th73,XBOOLE_1:7;
then Lin(A) + Lin(B) is Submodule of Lin(A \/ B) by RMOD_3:35;
hence thesis by A20,RMOD_2:25;
end;
theorem
Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B)
proof
Lin(A /\ B) is Submodule of Lin(A) & Lin(A /\ B) is Submodule of Lin(B)
by Th73,XBOOLE_1:17;
hence thesis by RMOD_3:20;
end;