:: Quotient Module of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 7, 2012
:: Copyright (c) 2012 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, 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, INT_1,
ORDINAL1, RLVECT_2, ZMODUL01, ZMODUL02, FINSEQ_4, RLVECT_3, RMOD_2,
INT_3, VECTSP_1, VECTSP_2, LOPBAN_1, MESFUNC1, NEWTON, REALSET1, RSSPACE,
MONOID_0, SETFAM_1, VECTSP10, EC_PF_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FINSET_1,
CARD_1, NUMBERS, XXREAL_0, INT_1, INT_2, BINOP_2, REALSET1, FINSEQ_1,
VALUED_1, FINSEQ_4, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1,
VECTSP_2, RLVECT_2, INT_3, EC_PF_1, ZMODUL01;
constructors BINOP_2, FINSEQ_4, RELSET_1, RLVECT_2, ZMODUL01, REALSET1,
FUNCT_7, INT_3, NAT_D, GCD_1, VECTSP10, ALGSTR_1, BINOP_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, VALUED_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1,
ZMODUL01, XXREAL_0, ALGSTR_0, INT_3, VECTSP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, XBOOLE_0, RLVECT_1, RELAT_1, FUNCT_2, STRUCT_0, ALGSTR_0,
INT_3, VECTSP_1, REALSET1, ZMODUL01, BINOP_1, SUBSET_1, TARSKI;
theorems BINOP_1, CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, FUNCT_1, FUNCT_2, INT_1, NAT_1, RLSUB_2, RLVECT_1, TARSKI,
ZMODUL01, RLVECT_2, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
FUNCOP_1, XREAL_1, STRUCT_0, PARTFUN1, VALUED_1, INT_3, VECTSP_1,
ALGSTR_0, EULER_1, EULER_2, EC_PF_1;
schemes BINOP_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;
begin :: 1. Quotient module of Z-module and vector space
reserve x, y, y1, y2 for set;
reserve V for Z_Module;
reserve u, v, w for VECTOR of V;
reserve F, G, H, I for FinSequence of V;
reserve i, j, k, n for Element of NAT;
reserve f, f9, g for Function of NAT, the carrier of V;
definition
let V be Z_Module;
let a be integer number;
func a * V -> non empty Subset of V equals
{a * v where v is Element of V : not contradiction};
correctness
proof
set S = {a * v where v is Element of V : not contradiction};
P1:
now let x be set;
assume x in S;
then ex v be Element of V st x =a*v;
hence x in the carrier of V;
end;
a*(0.V) in S;
hence thesis by P1,TARSKI:def 3;
end;
end;
definition
let V be Z_Module;
let a be integer number;
func Zero_(a,V) -> Element of a*V equals
0.V;
correctness
proof
0.V = a*0.V by ZMODUL01:1;
then 0.V in a*V;
hence thesis;
end;
end;
definition
let V be Z_Module;
let a be integer number;
func Add_(a,V) -> Function of [:a*V,a*V :], a*V equals
(the addF of V) | [:a*V,a*V:];
correctness
proof
set adds = (the addF of V)| [:a*V,a*V:];
[:a*V,a*V:] c= [:the carrier of V,the carrier of V:]
by ZFMISC_1:96;
then
[:a*V,a*V:] c= dom(the addF of V) by FUNCT_2:def 1;
then
P2: dom adds = [:a*V,a*V:] by RELAT_1:62;
for z be set st z in [:a*V,a*V:] holds adds.z in a*V
proof
let z be set such that
P3:z in [:a*V,a*V:];
consider x,y be set such that
P4:(x in a*V) & y in a*V & z = [x,y] by P3,ZFMISC_1:def 2;
consider v be Element of V such that
P5: x =a*v by P4;
consider w be Element of V such that
P6: y =a*w by P4;
adds.z = a*v+a*w by P3,P4,P5,P6,FUNCT_1:49
.= a*(v+w) by ZMODUL01:def 2;
hence adds.z in a*V;
end;
hence thesis by P2,FUNCT_2:3;
end;
end;
definition
let V be Z_Module;
let a be integer number;
func Mult_(a,V) -> Function of [:INT,a*V :], a*V equals
(the Mult of V) | [:INT,a*V:];
correctness
proof
set scmult = (the Mult of V)| [:INT,a*V:];
[:INT,a*V:] c= [:INT,the carrier of V:] by ZFMISC_1:96;
then
[:INT,a*V:] c= dom(the Mult of V) by FUNCT_2:def 1;
then
P2: dom scmult = [:INT,a*V:] by RELAT_1:62;
for z be set st z in [:INT,a*V:] holds scmult.z in a*V
proof
let z be set such that
P3:z in [:INT,a*V:];
consider x,y be set such that
P4:x in INT & y in a*V & z = [x,y] by P3,ZFMISC_1:def 2;
reconsider i=x as Element of INT by P4;
consider v be Element of V such that
P5: y =a*v by P4;
scmult.z = i*(a*v) by P3,P4,P5,FUNCT_1:49
.= (i*a)*v by ZMODUL01:def 4
.= a*(i*v) by ZMODUL01:def 4;
hence scmult.z in a*V;
end;
hence thesis by P2,FUNCT_2:3;
end;
end;
definition
let V be Z_Module;
let a be integer number;
func a (*) V -> Submodule of V equals
Z_ModuleStruct (# a * V, Zero_(a,V), Add_(a,V), Mult_(a,V) #);
coherence
proof
set V1 = a*V;
set Z0 = Zero_(a,V);
set AV1 = Add_(a,V);
set MV1 = Mult_(a,V);
:: set W = Z_ModuleStruct(# V1, Z0, AV1, MV1 #);
Z0 = 0.V & AV1 = (the addF of V) ||V1
& MV1 = (the Mult of V) | [:INT,V1:];
hence thesis by ZMODUL01:40;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func CosetSet(V,W) -> non empty Subset-Family of V equals
{A where A is Coset of W: not contradiction};
correctness
proof
set C = {A where A is Coset of W: not contradiction};
A1: C c= bool the carrier of V
proof
let x be set;
assume x in C;
then ex A be Coset of W st A = x;
hence thesis;
end;
the carrier of W is Coset of W by ZMODUL01:83;
then the carrier of W in C;
hence thesis by A1;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func addCoset(V,W) -> BinOp of CosetSet(V,W) means
:DefaddCoset:
for A,B be Element of CosetSet(V,W)
for a,b be VECTOR of V st A = a + W & B = b + W holds
it.(A,B) = (a+b)+W;
existence
proof
defpred P[set,set,set] means for a,b be VECTOR of V
st $1 = a + W & $2 = b + W holds $3 = (a+b)+W;
set C = CosetSet(V,W);
A1:
now
let A,B be Element of C;
A in C;
then consider A1 be Coset of W such that
A2: A1=A;
consider a be VECTOR of V such that
A3: A1 = a+W by ZMODUL01:def 13;
B in C;
then consider B1 be Coset of W such that
A4: B1=B;
consider b be VECTOR of V such that
A5: B1 = b+W by ZMODUL01:def 13;
reconsider z = (a+b) + W as Coset of W by ZMODUL01:def 13;
z in C;
then reconsider z as Element of C;
take z;
thus P[A,B,z]
proof
let a1,b1 be VECTOR of V;
assume that
A6: A = a1 + W and
A7: B = b1 + W;
a1 in a+W by A2,A3,A6,ZMODUL01:58;
then consider w1 be VECTOR of V such that
A8: w1 in W and
A9: a1 = a+w1 by ZMODUL01:72;
b1 in b +W by A4,A5,A7,ZMODUL01:58;
then consider w2 be VECTOR of V such that
A10: w2 in W and
A11: b1 = b+w2 by ZMODUL01:72;
A12: w1+w2 in W by A8,A10,ZMODUL01:36;
a1+b1 = w1+ a + b+ w2 by A9,A11,RLVECT_1:def 3
.= w1+ (a + b)+ w2 by RLVECT_1:def 3
.= a + b+ (w1+ w2) by RLVECT_1:def 3;
then
A13: a1+b1 in (a+b)+W by A12;
a1+b1 in (a1+b1) +W by ZMODUL01:58;
hence thesis by A13,ZMODUL01:68;
end;
end;
consider f be Function of [:C,C:],C such that
A14: for A,B be Element of C holds P[A,B, f.(A,B)] from BINOP_1:sch 3(A1);
reconsider f as BinOp of C;
take f;
let A,B be Element of C;
let a,b be VECTOR of V;
assume A = a + W & B = b + W;
hence thesis by A14;
end;
uniqueness
proof
set C = CosetSet(V,W);
let f1,f2 be BinOp of CosetSet(V,W) such that
A15: for A,B be Element of CosetSet(V,W) for a,b be VECTOR of V st A =
a + W & B = b + W holds f1.(A,B) = (a+b) +W and
A16: for A,B be Element of CosetSet(V,W) for a,b be VECTOR of V st A =
a + W & B = b + W holds f2.(A,B) = (a+b) +W;
now
let A,B be Element of CosetSet(V,W);
A in C;
then consider A1 be Coset of W such that
A17: A1=A;
consider a be VECTOR of V such that
A18: A1 = a+W by ZMODUL01:def 13;
B in C;
then consider B1 be Coset of W such that
A19: B1=B;
consider b be VECTOR of V such that
A20: B1 = b+W by ZMODUL01:def 13;
thus f1.(A,B) = a+b + W by A15,A17,A19,A18,A20
.= f2.(A,B) by A16,A17,A19,A18,A20;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func zeroCoset(V,W) -> Element of CosetSet(V,W) equals
the carrier of W;
coherence
proof
the carrier of W = 0.V+W by ZMODUL01:59;
then the carrier of W is Coset of W by ZMODUL01:def 13;
then the carrier of W in CosetSet(V,W);
hence thesis;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func lmultCoset(V,W) -> Function of [:INT, CosetSet(V,W):],
CosetSet(V,W) means
:DeflmultCoset:
for z be Element of INT, A be Element of CosetSet(V,W)
for a be VECTOR of V st A = a+W holds it.(z,A) = z*a +W;
existence
proof
defpred P[Element of INT, set, set] means for a be VECTOR of V
st $2 = a + W holds $3 = $1*a+W;
set cF = INT;
set C = CosetSet(V,W);
A1:
now
let z be Element of INT;
let A be Element of C;
A in C;
then consider A1 be Coset of W such that
A2: A1=A;
consider a be VECTOR of V such that
A3: A1 = a+W by ZMODUL01:def 13;
reconsider c = z*a + W as Coset of W by ZMODUL01:def 13;
c in C;
then reconsider c as Element of C;
take c;
thus P[z, A, c]
proof
let a1 be VECTOR of V;
assume A = a1 + W;
then a1 in a+W by A2,A3,ZMODUL01:58;
then consider w1 be VECTOR of V such that
A4: w1 in W & a1 = a+w1 by ZMODUL01:72;
z*a1 = z*a+z*w1 & z*w1 in W by A4,ZMODUL01:def 2,ZMODUL01:37;
then
A5: z*a1 in z*a+W;
z*a1 in z*a1 +W by ZMODUL01:58;
hence thesis by A5,ZMODUL01:68;
end;
end;
consider f be Function of [:cF,C:],C such that
A6: for z be Element of INT for A be Element of C holds P[z,A, f.(z,A)]
from BINOP_1:sch 3(A1);
take f;
let z be Element of INT, A be Element of C, a be VECTOR of V;
assume A = a + W;
hence thesis by A6;
end;
uniqueness
proof
set cF = INT;
set C = CosetSet(V,W);
let f1,f2 be Function of [:cF, C:], C such that
A7: for z be Element of INT, A be Element of CosetSet(V,W) for a be
VECTOR of V st A = a + W holds f1.(z,A) = z*a + W and
A8: for z be Element of INT, A be Element of CosetSet(V,W) for a be
VECTOR of V st A = a + W holds f2.(z,A) = z*a + W;
set C = CosetSet(V,W);
now
let z be Element of INT;
let A be Element of CosetSet(V,W);
A in C;
then consider A1 be Coset of W such that
A9: A1=A;
consider a be VECTOR of V such that
A10: A1 = a+W by ZMODUL01:def 13;
thus f1.(z,A) = z*a + W by A7,A9,A10
.= f2.(z,A) by A8,A9,A10;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func Z_ModuleQuot(V,W) -> strict Z_Module means
:DefZModQuot:
the carrier of it = CosetSet(V,W) & the addF of it = addCoset(V,W) &
0.it = zeroCoset(V,W) & the Mult of it = lmultCoset(V,W);
existence
proof
set C = CosetSet(V,W), aC = addCoset(V,W), zC = zeroCoset(V,W), lC =
lmultCoset(V,W), A = Z_ModuleStruct (# C, zC, aC, lC #);
A1: A is right_zeroed
proof
let A1 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A2: A1=aa;
consider a be VECTOR of V such that
A3: aa = a+W by ZMODUL01:def 13;
0.A = 0.V + W by ZMODUL01:59;
hence A1 + 0.A = (a+0.V) +W by A2,A3,DefaddCoset
.= A1 by A2,A3,RLVECT_1:4;
end;
A4: A is right_complementable
proof
let A1 be Element of A;
A5: 0.A = 0.V + W by ZMODUL01:59;
A1 in C;
then consider aa be Coset of W such that
A6: A1=aa;
consider a be VECTOR of V such that
A7: aa = a+W by ZMODUL01:def 13;
set A2 = -a+ W;
A2 is Coset of W by ZMODUL01:def 13;
then A2 in C;
then reconsider A2 as Element of A;
take A2;
thus A1 + A2 = (a+-a) +W by A6,A7,DefaddCoset
.= 0.A by A5,RLVECT_1:5;
end;
A8:
now
let x,y be integer number;
let A1,A2 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A10: A1=aa;
A2 in C;
then consider bb be Coset of W such that
A11: A2=bb;
consider b be VECTOR of V such that
A12: bb = b+W by ZMODUL01:def 13;
B0: x is Element of INT by INT_1:def 2;
then
A13: lC.(x,A2) = x*A2 & lC.(x,A2) =x*b+W by A11,A12,DeflmultCoset;
consider a be VECTOR of V such that
A15: aa = a+W by ZMODUL01:def 13;
A16: aC.(A1,A2) =a+b+W by A10,A11,A15,A12,DefaddCoset;
A17: lC.(x,A1) =x*a+W by A10,A15,B0,DeflmultCoset;
thus x*(A1+A2) = x*(a+b) +W by A16,B0,DeflmultCoset
.= x*a+x*b +W by ZMODUL01:def 2
.= x*A1+x*A2 by A17,A13,DefaddCoset;
y is Element of INT by INT_1:def 2;
then
A18: lC.(y,A1) =y*a+W by A10,A15,DeflmultCoset;
thus (x+y)*A1 = (x+y)*a +W by A10,A15,DeflmultCoset
.= x*a + y*a + W by ZMODUL01:def 3
.= x*A1+y*A1 by A17,A18,DefaddCoset;
thus (x*y)*A1 = (x*y)*a +W by A10,A15,DeflmultCoset
.= x*(y*a) +W by ZMODUL01:def 4
.=x*(y*A1) by A18,B0,DeflmultCoset;
B2: 1 is Element of INT by INT_1:def 2;
thus (1)*A1 = (1)*a +W by A10,A15,B2,DeflmultCoset
.= A1 by A10,A15,ZMODUL01:def 5;
end;
A19: A is Abelian
proof
let A1,A2 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A20: A1=aa;
consider a be VECTOR of V such that
A21: aa = a+W by ZMODUL01:def 13;
A2 in C;
then consider bb be Coset of W such that
A22: A2=bb;
consider b be VECTOR of V such that
A23: bb = b+W by ZMODUL01:def 13;
thus A1+A2 = (a+b) +W by A20,A22,A21,A23,DefaddCoset
.= A2+A1 by A20,A22,A21,A23,DefaddCoset;
end;
A is add-associative
proof
let A1,A2,A3 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A24: A1=aa;
consider a be VECTOR of V such that
A25: aa = a+W by ZMODUL01:def 13;
A2 in C;
then consider bb be Coset of W such that
A26: A2=bb;
consider b be VECTOR of V such that
A27: bb = b+W by ZMODUL01:def 13;
A3 in C;
then consider cc be Coset of W such that
A28: A3=cc;
consider c be VECTOR of V such that
A29: cc = c+W by ZMODUL01:def 13;
A30: aC.(A2,A3) =b+c+W by A26,A28,A27,A29,DefaddCoset;
aC.(A1,A2) =a+b+W by A24,A26,A25,A27,DefaddCoset;
hence A1+A2 + A3 = a+b+c +W by A28,A29,DefaddCoset
.= a+(b+c) +W by RLVECT_1:def 3
.= A1+(A2+A3) by A24,A25,A30,DefaddCoset;
end;
then reconsider A as strict Z_Module
by A19,A1,A4,A8,ZMODUL01:def 2,def 3,def 4,def 5;
take A;
thus thesis;
end;
uniqueness;
end;
theorem ThQuot1:
for p be Integer, V be Z_Module, W be Submodule of V,
x be VECTOR of Z_ModuleQuot(V, W) st W = p (*) V
holds p * x = 0.Z_ModuleQuot(V, W)
proof
let p be Integer, V be Z_Module, W be Submodule of V,
x be VECTOR of Z_ModuleQuot(V, W) such that
A1: W = p (*) V;
A3: x is Element of CosetSet(V,W) by DefZModQuot;
then x in {A where A is Coset of W : not contradiction};
then consider xx be Coset of W such that
A4: xx = x;
consider v be VECTOR of V such that
A5: xx = v + W by ZMODUL01:def 13;
A6: p is Element of INT by INT_1:def 2;
p * v in the carrier of W by A1;
then A7: p * v in W by STRUCT_0:def 5;
thus p * x = lmultCoset(V,W).(p, x) by DefZModQuot
.= (p * v) + W by A3,A4,A5,A6,DeflmultCoset
.= zeroCoset(V,W) by A7,ZMODUL01:63
.= 0.Z_ModuleQuot(V, W) by DefZModQuot;
end;
theorem ThQuot2:
for p, i be Integer, V be Z_Module, W be Submodule of V,
x be VECTOR of Z_ModuleQuot(V, W)
st p <> 0 & W = p (*) V
holds i * x = (i mod p) * x
proof
let p, i be Integer, V be Z_Module, W be Submodule of V,
x be VECTOR of Z_ModuleQuot(V, W) such that
A0: p <> 0 and
A1: W = p (*) V;
consider j be Integer such that
A3: j = i div p;
thus i * x = (j*p + (i mod p)) * x by A0,A3,INT_1:59
.= (j*p) * x + (i mod p) * x by ZMODUL01:def 3
.= j * (p*x) + (i mod p) * x by ZMODUL01:def 4
.= 0.Z_ModuleQuot(V, W) + (i mod p) * x by A1,ThQuot1,ZMODUL01:1
.= (i mod p) * x by RLVECT_1:4;
end;
theorem
for p, q be Integer, V be Z_Module, W be Submodule of V,
v be VECTOR of V
st W = p (*) V & p > 1 & q > 1 & p,q are_relative_prime
holds q * v = 0.V implies v + W = 0.Z_ModuleQuot(V, W)
proof
let p, q be Integer, V be Z_Module, W be Submodule of V,
v be VECTOR of V such that
A1: W = p (*) V and
A4: p > 1 & q > 1 & p,q are_relative_prime;
v + W is Coset of W by ZMODUL01:def 13;
then v + W in CosetSet(V,W);
then reconsider x = v + W as VECTOR of Z_ModuleQuot(V, W) by DefZModQuot;
p in NAT & q in NAT by A4,INT_1:3;
then reconsider pp=p, qq=q as Nat;
consider i, j be Integer such that
A6: i*pp + j*qq = 1 by A4,EULER_1:10;
assume AS: q * v = 0.V;
AA: x is Element of CosetSet(V,W) by DefZModQuot;
A10: q is Element of INT by INT_1:def 2;
A11: q * x = lmultCoset(V,W).(q,x) by DefZModQuot
.= 0.V + W by AS,A10,AA,DeflmultCoset
.= zeroCoset(V,W) by ZMODUL01:59
.= 0.Z_ModuleQuot(V, W) by DefZModQuot;
(i*p + j*q) * x = (i*p) * x + (j*q) * x by ZMODUL01:def 3
.= (i*p) * x + j * (q*x) by ZMODUL01:def 4
.= (i*p) * x + 0.Z_ModuleQuot(V, W) by A11,ZMODUL01:1
.= (i*p) * x by RLVECT_1:4
.= i * (p*x) by ZMODUL01:def 4
.= 0.Z_ModuleQuot(V, W) by A1,ThQuot1,ZMODUL01:1;
hence 0.Z_ModuleQuot(V, W) = v + W by A6,ZMODUL01:def 5;
end;
definition
let p be Prime;
let V be Z_Module;
func Mult_Mod_pV(V,p) -> Function of
[:the carrier of GF(p), the carrier of Z_ModuleQuot(V,p(*)V):],
the carrier of Z_ModuleQuot(V,p(*)V) means
:DefMultModpV:
for a being Element of GF(p), i being Integer,
x being Element of Z_ModuleQuot(V,p(*)V) st a = i mod p
holds it.(a,x) = (i mod p) * x;
existence
proof
defpred P[Element of GF(p), Element of Z_ModuleQuot(V,p(*)V),
Element of Z_ModuleQuot(V,p(*)V)] means
for i be Integer st $1 = i mod p holds
$3 = (i mod p) * $2;
P1: for a being Element of GF(p)
for x being Element of Z_ModuleQuot(V,p(*)V)
ex z being Element of Z_ModuleQuot(V,p(*)V) st P[a,x,z]
proof
let a be Element of GF(p), x be Element of Z_ModuleQuot(V,p(*)V);
consider i be Nat such that
A1: a = i mod p by EC_PF_1:13;
reconsider i as Integer;
reconsider z = (i mod p) * x as Element of Z_ModuleQuot(V,p(*)V);
P[a,x,z] by A1;
hence thesis;
end;
consider f being Function of
[:the carrier of GF(p), the carrier of Z_ModuleQuot(V,p(*)V):],
the carrier of Z_ModuleQuot(V,p(*)V) such that
P2: for a being Element of GF(p)
for x being Element of Z_ModuleQuot(V,p(*)V) holds
P[a,x,f.(a,x)] from BINOP_1:sch 3(P1);
take f;
thus thesis by P2;
end;
uniqueness
proof
let f1, f2 be Function of
[:the carrier of GF(p), the carrier of Z_ModuleQuot(V,p(*)V):],
the carrier of Z_ModuleQuot(V,p(*)V);
assume
P1: for a being Element of GF(p), i being Integer,
x being Element of Z_ModuleQuot(V,p(*)V) st a = i mod p
holds f1.(a,x) = (i mod p) * x;
assume
P2: for a being Element of GF(p), i being Integer,
x being Element of Z_ModuleQuot(V,p(*)V) st a = i mod p
holds f2.(a,x) = (i mod p) * x;
let a, x be set;
assume A1: a in the carrier of GF(p) &
x in the carrier of Z_ModuleQuot(V,p(*)V);
then reconsider a0=a as Element of GF(p);
reconsider x0=x as Element of Z_ModuleQuot(V,p(*)V) by A1;
consider i be Nat such that
A2: a0 = i mod p by EC_PF_1:13;
reconsider i as Integer;
thus f1.(a,x) = (i mod p) * x0 by P1,A2
.= f2.(a,x) by P2,A2;
end;
end;
definition
let p be Prime, V be Z_Module;
func Z_MQ_VectSp(V,p) -> non empty strict VectSpStr over GF(p) equals
VectSpStr (# the carrier of Z_ModuleQuot(V,p(*)V),
the addF of Z_ModuleQuot(V,p(*)V), the ZeroF of Z_ModuleQuot(V,p(*)V),
Mult_Mod_pV(V,p) #);
coherence;
end;
registration
let p be Prime, V be Z_Module;
cluster Z_MQ_VectSp(V,p) -> scalar-distributive vector-distributive
scalar-associative scalar-unital add-associative right_zeroed
right_complementable Abelian;
coherence
proof set M = Z_MQ_VectSp(V,p);
set F = GF(p);
set AD = the addF of Z_ModuleQuot(V,p(*)V);
set ML = lmultCoset(V,p(*)V);
thus M is scalar-distributive
proof
let x, y be Element of F,v be Element of M;
consider i be Nat such that
A1: x = i mod p by EC_PF_1:13;
reconsider i as Integer;
consider j be Nat such that
A2: y = j mod p by EC_PF_1:13;
reconsider j as Integer;
reconsider v1=v as Element of Z_ModuleQuot(V,p(*)V);
A3: x+y = (i+j) mod p by A1,A2,EC_PF_1:15
.= ((i mod p) + (j mod p)) mod p by EULER_2:6;
X2: x * v = (i mod p)*v1 by DefMultModpV,A1;
X3: y * v = (j mod p)*v1 by DefMultModpV,A2;
(((i mod p) + (j mod p)) mod p)*v1
= ((i mod p) + (j mod p))*v1 by ThQuot2
.= (i mod p)*v1 + (j mod p)*v1 by ZMODUL01:def 3;
hence thesis by A3,X2,X3,DefMultModpV;
end;
thus M is vector-distributive
proof
let x be Element of F,v, w be Element of M;
consider i be Nat such that
A1: x = i mod p by EC_PF_1:13;
reconsider i as Integer;
reconsider v1=v,w1=w as Element of Z_ModuleQuot(V,p(*)V);
A4: x * w = (i mod p)*w1 by DefMultModpV,A1;
thus x * (v + w) =(i mod p)*(v1 + w1) by DefMultModpV,A1
.=(i mod p)*v1 + (i mod p)*w1 by ZMODUL01:def 2
.=(x * v) + (x * w) by A1,A4,DefMultModpV;
end;
thus M is scalar-associative
proof
let x, y be Element of F,v be Element of M;
consider i be Nat such that
A1: x = i mod p by EC_PF_1:13;
reconsider i as Integer;
consider j be Nat such that
A2: y = j mod p by EC_PF_1:13;
reconsider j as Integer;
reconsider v1=v as Element of Z_ModuleQuot(V,p(*)V);
A3: x*y = (i * j) mod p by A1,A2,EC_PF_1:18;
X3: y * v = (j mod p)*v1 by DefMultModpV,A2;
X4: x * (y * v) = (i mod p)*((j mod p)*v1) by A1,X3,DefMultModpV;
((i * j) mod p)*v1 = (i*j)*v1 by ThQuot2
.= i*(j*v1) by ZMODUL01:def 4
.= i*((j mod p)*v1) by ThQuot2
.= (i mod p)*((j mod p)*v1) by ThQuot2;
hence thesis by A3,X4,DefMultModpV;
end;
thus M is scalar-unital
proof
let v be Element of M;
reconsider v1=v as Element of Z_ModuleQuot(V,p(*)V);
consider i be Nat such that
A1: 1.F = i mod p by EC_PF_1:13;
reconsider i as Integer;
thus (1.F)*v = (i mod p)*v1 by DefMultModpV,A1
.= 1 * v1 by A1,EC_PF_1:12
.= v by ZMODUL01:def 5;
end;
thus M is add-associative
proof
let u, v, w be Element of M;
reconsider u1=u,v1=v,w1=w as Element of Z_ModuleQuot(V,p(*)V);
thus (u+v)+w =u1+v1+w1
.=u1+(v1+w1) by RLVECT_1:def 3
.=u+(v+w);
end;
thus M is right_zeroed
proof
let u be Element of M;
reconsider u1=u as Element of Z_ModuleQuot(V,p(*)V);
thus u+(0.M) =u1+ 0.(Z_ModuleQuot(V,p(*)V))
.=u by RLVECT_1:def 4;
end;
thus M is right_complementable
proof
let v be Element of M;
reconsider v1=v as Element of Z_ModuleQuot(V,p(*)V);
reconsider w =-v1 as Element of M;
take w;
thus v + w = v1+ -v1
.= 0.(Z_ModuleQuot(V,p(*)V)) by RLVECT_1:5
.= 0.M;
end;
let v, w be Element of M;
reconsider v1=v,w1=w as Element of Z_ModuleQuot(V,p(*)V);
thus v+w =v1+w1
.=w1+v1
.=w+v;
end;
end;
definition
let p be Prime, V be Z_Module, v be VECTOR of V;
func ZMtoMQV(V,p,v) -> Vector of Z_MQ_VectSp(V,p) equals
v + p(*)V;
correctness
proof
set vq = v + p(*)V;
vq is Coset of p(*)V by ZMODUL01:def 13;
then vq in {A where A is Coset of p(*)V : not contradiction};
then vq is Element of CosetSet(V,p(*)V);
hence thesis by DefZModQuot;
end;
end;
definition
let X be Z_Module;
func Mult_INT*(X) -> Function of
[:the carrier of INT.Ring,the carrier of X:], the carrier of X equals
the Mult of X;
correctness;
end;
definition
let X be Z_Module;
func modetrans(X) -> non empty strict VectSpStr over INT.Ring equals
VectSpStr (#the carrier of X, the addF of X, the ZeroF of X, Mult_INT*(X) #);
coherence;
end;
registration
let X be Z_Module;
cluster modetrans(X) -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
set X0 = the carrier of X;
set Z0 = the ZeroF of X;
set ADD = the addF of X;
set LMLT = Mult_INT*(X);
set XP = VectSpStr (# X0, ADD,Z0,LMLT #);
Q10: XP is vector-distributive
proof
let x be Scalar of INT.Ring;
let v,w be Element of XP;
reconsider x1=x as Integer;
reconsider v1=v, w1=w as Element of X;
thus x*(v+w)=x1*(v1+w1)
.= x1*v1+x1*w1 by ZMODUL01:def 2
.= x*v+x*w;
end;
Q11: XP is scalar-distributive
proof
let x,y be Scalar of INT.Ring;
let v be Element of XP;
reconsider x1=x, y1=y as Integer;
reconsider v1=v as Element of X;
thus (x+y)*v=(x1+y1)*v1
.=x1*v1+y1*v1 by ZMODUL01:def 3
.= x*v+y*v;
end;
Q12: XP is scalar-associative
proof
let x,y be Scalar of INT.Ring;
let v be Element of XP;
reconsider x1=x, y1=y as Integer;
reconsider v1=v as Element of X;
thus (x*y)*v =(x1*y1)*v1
.= x1*(y1*v1) by ZMODUL01:def 4
.= x*(y*v);
end;
Q13: XP is scalar-unital
proof
let v be Element of XP;
reconsider v1=v as Element of X;
thus (1.(INT.Ring))*v = 1*v1 by INT_3:13
.=v by ZMODUL01:def 5;
end;
Q2:
now let u,v,w be Element of XP;
reconsider u1=u, v1=v, w1=w as Element of X;
thus u+(v + w) = u1+(v1+w1)
.=(u1+v1)+w1 by RLVECT_1:def 3
.=(u+v)+w;
end;
Q3:
now let v be Element of XP;
reconsider v1=v as Element of X;
thus v + 0.XP = v1+0.X
.=v by RLVECT_1:def 4;
end;
Q4:
now let v be Element of XP;
reconsider v1=v as Element of X;
consider w1 be Element of X such that
A1: v1+w1= 0.X by ALGSTR_0:def 11;
reconsider w=w1 as Element of XP;
v + w = 0.XP by A1;
hence v is right_complementable by ALGSTR_0:def 11;
end;
now let v,w be Element of XP;
reconsider v1=v,w1=w as Element of X;
thus v + w = v1+w1
.=w1+v1
.=w+v;
end;
hence thesis
by Q10,Q11,Q12,Q13,Q2,Q3,Q4,ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4;
end;
end;
definition
let X be LeftMod of INT.Ring;
func Mult_INT*(X) -> Function of
[:INT,the carrier of X:], the carrier of X equals
the lmult of X;
coherence;
end;
definition
let X be LeftMod of INT.Ring;
func modetrans(X) -> non empty strict Z_ModuleStruct equals
Z_ModuleStruct (#the carrier of X,the ZeroF of X,
the addF of X,Mult_INT*(X) #);
correctness;
end;
registration
let X be LeftMod of INT.Ring;
cluster modetrans(X) -> Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital;
coherence
proof
set X0 = the carrier of X;
set Z0 = the ZeroF of X;
set ADD = the addF of X;
set VMLT = Mult_INT*(X);
set XQ = Z_ModuleStruct (# X0, Z0, ADD,VMLT #);
A1: for vd,wd be Element of X, v,w be Element of XQ st v = vd & w = wd
holds v + w = vd + wd;
XQ is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
proof
hereby let v,w be VECTOR of XQ;
reconsider vd = v, wd = w as Element of X;
thus v + w = wd + vd by A1
.= w + v;
end;
hereby let u,v,w be VECTOR of XQ;
reconsider ud = u, vd = v, wd = w as Element of X;
thus (u + v) + w = (ud + vd) + wd
.= ud + (vd + wd) by RLVECT_1:def 3
.= u + (v + w);
end;
hereby let v be VECTOR of XQ;
reconsider vd = v as Element of X;
thus v + 0.XQ = vd + 0.X
.= v by RLVECT_1:4;
end;
thus XQ is right_complementable
proof let v be VECTOR of XQ;
reconsider vd = v as Element of X;
consider wd being Element of X such that
A2: vd + wd = 0.X by ALGSTR_0:def 11;
reconsider w = wd as VECTOR of XQ;
take w;
thus v + w = 0.XQ by A2;
end;
hereby let a,b be integer number, v be VECTOR of XQ;
reconsider vd = v as Element of X;
reconsider ad=a as Scalar of INT.Ring by INT_1:def 2;
reconsider bd=b as Scalar of INT.Ring by INT_1:def 2;
thus (a + b) * v = (ad + bd) * vd
.= ad* vd + bd* vd by VECTSP_1:def 15
.= a * v + b * v;
end;
hereby let a be integer number, v,w be VECTOR of XQ;
reconsider ad=a as Element of INT.Ring by INT_1:def 2;
reconsider vd = v, wd = w as Element of X;
thus a * (v + w) =ad*(vd+wd)
.=ad*vd + ad*wd by VECTSP_1:def 14
.=a*v + a*w;
end;
hereby let a,b be integer number, v be VECTOR of XQ;
reconsider vd = v as Element of X;
reconsider ad=a as Scalar of INT.Ring by INT_1:def 2;
reconsider bd=b as Scalar of INT.Ring by INT_1:def 2;
thus (a * b) * v = (ad * bd) * vd
.=ad * (bd * vd) by VECTSP_1:def 16
.= a * (b * v);
end;
let v be VECTOR of XQ;
reconsider vd = v as Element of X;
thus 1 * v = 1.(INT.Ring) *vd by INT_3:13
.= v by VECTSP_1:def 17;
end;
hence thesis;
end;
end;
theorem
for X be Z_Module,
v,w be Element of X,
v1,w1 be Element of modetrans(X)
st v=v1 & w=w1 holds
v+w=v1+w1 & v-w = v1-w1
proof
let X be Z_Module,
v, w be Element of X,
v1, w1 be Element of modetrans(X);
assume AS: v=v1 & w=w1;
thus v+w=v1+w1 by AS;
P1: -w=(-1)*w by ZMODUL01:2
.=(-(1.(INT.Ring)))*w1 by AS,INT_3:13
.=-w1 by VECTSP_1:14;
thus v-w = v1-w1 by AS,P1;
end;
theorem
for X be Z_Module,
v be Element of X,
v1 be Element of modetrans(X),
a be Integer, a1 be Element of INT.Ring
st v=v1 & a=a1 holds a*v=a1*v1;
theorem
for X be LeftMod of INT.Ring,
v, w be Element of X,
v1, w1 be Element of modetrans(X)
st v=v1 & w=w1 holds
v+w=v1+w1 & v-w = v1-w1
proof
let X be LeftMod of INT.Ring,
v, w be Element of X,
v1, w1 be Element of modetrans(X);
assume AS: v=v1 & w=w1;
thus v+w=v1+w1 by AS;
P1: -w1=(-1)*w1 by ZMODUL01:2
.=(-(1.(INT.Ring)))*w by AS,INT_3:13
.=-w by VECTSP_1:14;
thus v-w = v1-w1 by AS,P1;
end;
theorem
for X be LeftMod of INT.Ring,
v be Element of X,
v1 be Element of modetrans(X),
a be Element of INT.Ring, a1 be Integer
st v=v1 & a=a1
holds a*v=a1*v1;
begin :: 2. Linear combination of Z-module
definition
let V be non empty ZeroStr;
mode Z_Linear_Combination of V -> Element of Funcs(the carrier of V, INT)
means
:RL2Def5:
ex T being finite Subset of V st for v being Element of V st not v
in T holds it.v = 0;
existence
proof
reconsider N0 = 0 as Element of INT by INT_1:def 2;
{}V = {};
then reconsider P = {} as finite Subset of V;
reconsider f = (the carrier of V) --> N0 as Function of the carrier of V,
INT;
reconsider f as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
take f;
take P;
thus thesis by FUNCOP_1:7;
end;
end;
reserve K,L,L1,L2,L3 for Z_Linear_Combination of V;
definition
let V be non empty addLoopStr, L be Z_Linear_Combination of V;
func Carrier(L) -> finite Subset of V equals
{v where v is Element of V : L.v <> 0};
coherence
proof
set A = {v where v is Element of V : L.v <> 0};
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds L.v = 0 by RL2Def5;
A c= T
proof
let x;
assume x in A;
then ex v being Element of V st x = v & L.v <> 0;
hence thesis by A1;
end;
hence thesis by XBOOLE_1:1;
end;
end;
theorem
for V be non empty addLoopStr, L be Z_Linear_Combination of V,
v be Element of V holds L.v = 0 iff not v in Carrier(L)
proof
let V be non empty addLoopStr,
L be Z_Linear_Combination of V, v be Element of V;
thus L.v = 0 implies not v in Carrier(L)
proof
assume
A1: L.v = 0;
assume not thesis;
then ex u be Element of V st u = v & L.u <> 0;
hence thesis by A1;
end;
assume not v in Carrier(L);
hence thesis;
end;
definition
let V be non empty addLoopStr;
func Z_ZeroLC(V) -> Z_Linear_Combination of V means
:RL2Def7:
Carrier (it) = {};
existence
proof
reconsider N0=0 as Element of INT by INT_1:def 2;
reconsider f = (the carrier of V) --> N0 as Function of the carrier of V,
INT;
reconsider f as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
f is Z_Linear_Combination of V
proof
reconsider T = {}V as empty finite Subset of V;
take T;
thus thesis by FUNCOP_1:7;
end;
then reconsider f as Z_Linear_Combination of V;
take f;
set C = {v where v is Element of V : f.v <> 0};
now
set x = the Element of C;
assume C <> {};
then x in C;
then ex v being Element of V st x = v & f.v <> 0;
hence contradiction by FUNCOP_1:7;
end;
hence thesis;
end;
uniqueness
proof
let L,L9 be Z_Linear_Combination of V;
assume that
A1: Carrier(L) = {} and
A2: Carrier(L9) = {};
now
let x;
assume x in the carrier of V;
then reconsider v = x as Element of V;
A3:
now
assume L9.v <> 0;
then v in {u where u is Element of V : L9.u <> 0};
hence contradiction by A2;
end;
now
assume L.v <> 0;
then v in {u where u is Element of V : L.u <> 0};
hence contradiction by A1;
end;
hence L.x = L9.x by A3;
end;
hence L = L9 by FUNCT_2:12;
end;
end;
theorem RL2Th30:
for V be non empty addLoopStr,
v be Element of V holds (Z_ZeroLC(V)).v = 0
proof
let V be non empty addLoopStr, v be Element of V;
Carrier (Z_ZeroLC(V)) = {} & not v in {} by RL2Def7;
hence thesis;
end;
definition
let V be non empty addLoopStr;
let A be Subset of V;
mode Z_Linear_Combination of A -> Z_Linear_Combination of V means
:RL2Def8:
Carrier (it) c= A;
existence
proof
take L = Z_ZeroLC(V);
Carrier (L) = {} by RL2Def7;
hence thesis by XBOOLE_1:2;
end;
end;
reserve a, b for Integer;
reserve G, H1, H2, F, F1, F2, F3 for FinSequence of V;
reserve A, B for Subset of V,
v1, v2, v3, u1, u2, u3 for VECTOR of V,
f for Function of the carrier of V, INT,
i for Element of NAT;
reserve l, l1, l2 for Z_Linear_Combination of A;
theorem RL2Th33:
A c= B implies l is Z_Linear_Combination of B
proof
assume A1: A c= B;
Carrier(l) c= A by RL2Def8;
then Carrier(l) c= B by A1,XBOOLE_1:1;
hence thesis by RL2Def8;
end;
theorem RL2Th34:
Z_ZeroLC(V) is Z_Linear_Combination of A
proof
Carrier(Z_ZeroLC(V)) = {} & {} c= A by RL2Def7,XBOOLE_1:2;
hence thesis by RL2Def8;
end;
theorem RL2Th35:
for l being Z_Linear_Combination of {}the carrier of V holds l = Z_ZeroLC(V)
proof
let l be Z_Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by RL2Def8;
then Carrier(l) = {};
hence thesis by RL2Def7;
end;
definition
let V, F, f;
func f (#) F -> FinSequence of V means :RL2Def9:
len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
existence
proof
deffunc Q(set)= f.(F/.$1) * 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;
assume x in rng G;
then consider y such that
A3: y in dom G and
A4: G.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A3;
G.y = f.(F/.y) * 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;
assume that
A5: len H1 = len F and
A6: for i st i in dom H1 holds H1.i = f.(F/.i) * F/.i and
A7: len H2 = len F and
A8: for i st i in dom H2 holds H2.i = f.(F/.i) * 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.(F/.k) * 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 RL2Th40:
i in dom F & v = F.i implies (f (#) F).i = f.v * 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 RL2Def9;
then i in dom(f (#) F) by A1,FINSEQ_3:29;
hence thesis by A2,A3,RL2Def9;
end;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by RL2Def9
.= 0;
hence thesis;
end;
theorem RL2Th42:
f (#) <* v *> = <* f.v * v *>
proof
A1: 1 in {1} by TARSKI:def 1;
A2: len(f (#) <* v *>) = len<* v *> by RL2Def9
.= 1 by FINSEQ_1:40;
then dom(f (#) <* v *>) = {1} by FINSEQ_1:2,def 3;
then (f (#) <* v *>).1 = f.(<* v *>/.1) * <* v *>/.1 by A1,RL2Def9
.= f.(<* v *>/.1) * v by FINSEQ_4:16
.= f.v * v by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem RL2Th43:
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by RL2Def9
.= 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 = f.(<* v1,v2 *>/.2) * <* v1,v2 *>/.2
by A2,RL2Def9
.= f.(<* v1,v2 *>/.2) * v2 by FINSEQ_4:17
.= f.v2 * v2 by FINSEQ_4:17;
1 in {1,2} by TARSKI:def 2;
then (f (#) <* v1,v2 *>).1 =
f.(<* v1,v2 *>/.1) * <* v1,v2 *>/.1 by A2,RL2Def9
.= f.(<* v1,v2 *>/.1) * v1 by FINSEQ_4:17
.= f.v1 * v1 by FINSEQ_4:17;
hence thesis by A1,A3,FINSEQ_1:44;
end;
theorem
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by RL2Def9
.= 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 = f.(<* v1,v2,v3 *>/.3) * <* v1,v2,v3 *>/.3
by A2,RL2Def9
.= f.(<* v1,v2,v3 *>/.3) * v3 by FINSEQ_4:18
.= f.v3 * v3 by FINSEQ_4:18;
2 in {1,2,3} by ENUMSET1:def 1; then
A4: (f (#) <* v1,v2,v3 *>).2 = f.(<* v1,v2,v3 *>/.2) * <* v1,v2,v3 *>/.2
by A2,RL2Def9
.= f.(<* v1,v2,v3 *>/.2) * v2 by FINSEQ_4:18
.= f.v2 * v2 by FINSEQ_4:18;
1 in {1,2,3} by ENUMSET1:def 1;
then
(f (#) <* v1,v2,v3 *>).1 = f.(<* v1,v2,v3 *>/.1) * <* v1,v2,v3 *>/.1
by A2,RL2Def9
.= f.(<* v1,v2,v3 *>/.1) * v1 by FINSEQ_4:18
.= f.v1 * v1 by FINSEQ_4:18;
hence thesis by A1,A4,A3,FINSEQ_1:45;
end;
definition
let V, L;
func Sum(L) -> Element of V means
:RL2Def10:
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 be Element of V;
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[set,set] means {$2} = F1 " {F2.$1};
A9: dom F2 = Seg(len F2) by FINSEQ_1:def 3;
A10: dom F1 = Seg(len F1) by FINSEQ_1:def 3;
A11: len F1 = len F2 by A3,A4,A6,A7,FINSEQ_1:48;
A12: for x st x in dom F1 ex y st y in dom F1 & P[x,y]
proof
let x;
assume x in dom F1;
then F2.x in rng F1 by A4,A7,A11,A10,A9,FUNCT_1:def 3;
then consider y 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 st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A15: f is one-to-one
proof
let y1, y2 be set;
assume that
A16: y1 in dom f and
A17: y2 in dom f and
A18: f.y1 = f.y2;
F2.y1 in rng F1 by A4,A7,A11,A10,A9,A16,FUNCT_1:def 3;
then
A19: {F2.y1} c= rng F1 by ZFMISC_1:31;
F2.y2 in rng F1 by A4,A7,A11,A10,A9,A17,FUNCT_1:def 3;
then
A20: {F2.y2} c= rng F1 by ZFMISC_1:31;
F1 " {F2.y1} = {f.y1} & F1 " {F2.y2} = {f.y2} by A14,A16,A17;
then {F2.y1} = {F2.y2} by A18,A19,A20,FUNCT_1:91;
then F2.y1 = F2.y2 by ZFMISC_1:3;
hence thesis by A6,A11,A10,A9,A16,A17,FUNCT_1:def 4;
end;
set G1 = L (#) F1;
A21: len G1 = len F1 by RL2Def9;
A22: rng f = dom F1
proof
now let y be set;
assume A23: y in dom F1;
then F1.y in rng F2 by A4,A7,FUNCT_1:def 3;
then consider x such that
A24: x in dom F2 and
A25: F2.x = F1.y by FUNCT_1:def 3;
F1 " {F2.x} = F1 " Im(F1,y) by A23,A25,FUNCT_1:59;
then F1 " {F2.x} c= {y} by A3,FUNCT_1:82;
then {f.x} c= {y} by A11,A10,A9,A14,A24;
then
A26: f.x = y by ZFMISC_1:18;
x in dom f by A11,A10,A9,A24,FUNCT_2:def 1;
hence y in rng f by A26,FUNCT_1:def 3;
end;
then dom F1 c= rng f by TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
then reconsider f as Permutation of dom F1 by A15,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 A21;
set G2 = L (#) F2;
A27: dom G2 = Seg(len G2) by FINSEQ_1:def 3;
A28: len G2 = len F2 by RL2Def9;
A29: dom(G1) = Seg(len G1) by FINSEQ_1:def 3;
now
let i;
assume
A30: i in dom G2;
then reconsider u = F2.i as VECTOR of V by A28,A9,A27,FUNCT_1:102;
A31: G2.i = L.(F2/.i) * F2/.i & F2.i = F2/.i
by A28,A9,A27,A30,RL2Def9,PARTFUN1:def 6;
i in dom f by A11,A21,A28,A29,A27,A30,FUNCT_2:def 1;
then
A32: f.i in dom F1 by A22,FUNCT_1:def 3;
then reconsider m = f.i as Element of NAT;
reconsider v = F1.m as VECTOR of V by A32,FUNCT_1:102;
{F1.(f.i)} = Im(F1,f.i) by A32,FUNCT_1:59
.= F1 .: (F1 " {F2.i}) by A11,A28,A10,A27,A14,A30;
then
A33: u = v by FUNCT_1:75,ZFMISC_1:18;
F1.m = F1/.m by A32,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A21,A10,A29,A32,A33,A31,RL2Def9;
end;
hence thesis by A3,A4,A5,A6,A7,A8,A21,A28,RLVECT_2:6,FINSEQ_1:48;
end;
end;
RL2Lm1: Sum(Z_ZeroLC(V)) = 0.V
proof
consider F such that
F is one-to-one and
A1: rng F = Carrier(Z_ZeroLC(V)) and
A2: Sum(Z_ZeroLC(V)) = Sum(Z_ZeroLC(V) (#) F) by RL2Def10;
Carrier(Z_ZeroLC(V)) = {} by RL2Def7;
then F = {} by A1,RELAT_1:41;
then len F = 0;
then len(Z_ZeroLC(V) (#) F) = 0 by RL2Def9;
hence thesis by A2,RLVECT_1:75;
end;
theorem
A <> {} & A is linearly-closed iff for l holds Sum(l) in A
proof
thus A <> {} & A is linearly-closed implies for l holds Sum(l) in A
proof
defpred P[Element of NAT] means for l st card(Carrier(l)) = $1 holds
Sum(l) in A;
assume that
A1: A <> {} and
A2: A is linearly-closed;
now
let l;
assume card(Carrier(l)) = 0;
then Carrier(l) = {};
then l = Z_ZeroLC(V) by RL2Def7;
then Sum(l) = 0.V by RL2Lm1;
hence Sum(l) in A by A1,A2,ZMODUL01:18;
end;
then
A3: P[0];
now
let k;
assume
A4: for l st card(Carrier(l)) = k holds Sum(l) in A;
let l;
deffunc F(Element of V)= l.$1;
consider F such that
A5: F is one-to-one and
A6: rng F = Carrier(l) and
A7: Sum(l) = Sum(l (#) F) by RL2Def10;
reconsider G = F | Seg k as FinSequence of V by FINSEQ_1:18;
assume
A8: card(Carrier(l)) = k + 1;
then
A9: len F = k + 1 by A5,A6,FINSEQ_4:62;
then
A10: len(l (#) F) = k + 1 by RL2Def9;
A11: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A12: k + 1 in dom F by A9,FINSEQ_1:def 3;
k+1 in dom F by A9,A11,FINSEQ_1:def 3;
then reconsider v = F.(k + 1) as VECTOR of V by FUNCT_1:102;
reconsider N0=0 as Element of INT by INT_1:def 2;
consider f being Function of the carrier of V, INT such that
A13: f.v = N0 and
A14: 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, INT) by FUNCT_2:8;
A15: v in Carrier(l) by A6,A12,FUNCT_1:def 3;
now
let u;
assume
A16: not u in Carrier(l);
hence f.u = l.u by A15,A14
.= 0 by A16;
end;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
A17: A \ {v} c= A by XBOOLE_1:36;
A18: Carrier(l) c= A by RL2Def8;
then
A19: l.v * v in A by A2,A15,ZMODUL01:def 8;
A20: Carrier(f) = Carrier(l) \ {v}
proof
thus Carrier(f) c= Carrier(l) \ {v}
proof
let x;
assume x in Carrier(f);
then consider u such that
A21: u = x and
A22: f.u <> 0;
f.u = l.u by A13,A14,A22;
then
A23: x in Carrier(l) by A21,A22;
not x in {v} by A13,A21,A22,TARSKI:def 1;
hence thesis by A23,XBOOLE_0:def 5;
end;
let x;
assume
A24: x in Carrier(l) \ {v};
then x in Carrier(l) by XBOOLE_0:def 5;
then consider u such that
A25: x = u and
A26: l.u <> 0;
not x in {v} by A24,XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then l.u = f.u by A14,A25;
hence thesis by A25,A26;
end;
then Carrier(f) c= A \ {v} by A18,XBOOLE_1:33;
then Carrier(f) c= A by A17,XBOOLE_1:1;
then reconsider f as Z_Linear_Combination of A by RL2Def8;
A27: len G = k by A9,FINSEQ_3:53;
then
A28: len (f (#) G) = k by RL2Def9;
A29: rng G = Carrier(f)
proof
thus rng G c= Carrier(f)
proof
let x;
assume x in rng G;
then consider y such that
A30: y in dom G and
A31: G.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A30;
A32: dom G c= dom F & G.y = F.y by A30,FUNCT_1:47,RELAT_1:60;
now
assume x = v;
then
A33: k + 1 = y by A5,A12,A30,A31,A32,FUNCT_1:def 4;
y <= k by A27,A30,FINSEQ_3:25;
hence contradiction by A33,XREAL_1:29;
end;
then
A34: not x in {v} by TARSKI:def 1;
x in rng F by A30,A31,A32,FUNCT_1:def 3;
hence thesis by A6,A20,A34,XBOOLE_0:def 5;
end;
let x;
assume
A35: x in Carrier(f);
then x in rng F by A6,A20,XBOOLE_0:def 5;
then consider y such that
A36: y in dom F and
A37: F.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A36;
now
assume not y in Seg k;
then y in dom F \ Seg k by A36,XBOOLE_0:def 5;
then y in Seg(k + 1) \ Seg k by A9,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 A20,A35,A37,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then y in dom F /\ Seg k by A36,XBOOLE_0:def 4;
then
A38: y in dom G by RELAT_1:61;
then G.y = F.y by FUNCT_1:47;
hence thesis by A37,A38,FUNCT_1:def 3;
end;
Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
.= dom(f (#) G) by A28,FINSEQ_1:def 3;
then
A39: dom(f (#) G) = dom(l (#) F) /\ Seg k by A10,FINSEQ_1:def 3;
now
let x;
assume
A40: x in dom(f (#) G);
then reconsider n = x as Element of NAT;
n in dom(l (#) F) by A39,A40,XBOOLE_0:def 4;
then
A41: n in dom F by A9,A10,FINSEQ_3:29;
then F.n in rng F by FUNCT_1:def 3;
then reconsider w = F.n as VECTOR of V;
A42: n in dom G by A27,A28,A40,FINSEQ_3:29;
then
A43: G.n in rng G by FUNCT_1:def 3;
then reconsider u = G.n as VECTOR of V;
not u in {v} by A20,A29,A43,XBOOLE_0:def 5;
then
A44: u <> v by TARSKI:def 1;
A45: (f (#) G).n = f.u * u by A42,RL2Th40
.= l.u * u by A14,A44;
w = u by A42,FUNCT_1:47;
hence (f (#) G).x = (l (#) F).x by A45,A41,RL2Th40;
end;
then
A46: f (#) G = (l (#) F) | Seg k by A39,FUNCT_1:46;
v in rng F by A12,FUNCT_1:def 3;
then {v} c= Carrier(l) by A6,ZFMISC_1:31;
then card(Carrier(f)) = k + 1 - card{v} by A8,A20,CARD_2:44
.= k + 1 - 1 by CARD_1:30
.= k;
then
A47: Sum(f) in A by A4;
G is one-to-one by A5,FUNCT_1:52;
then
A48: Sum(f (#) G) = Sum(f) by A29,RL2Def10;
dom(f (#) G) = Seg len (f (#) G) & (l (#) F).(len F) = l.v * v
by A9,A12,RL2Th40,FINSEQ_1:def 3;
then Sum(l (#) F) = Sum (f (#) G) + l.v * v
by A9,A10,A28,A46,RLVECT_1:38;
hence Sum(l) in A by A2,A7,A19,A48,A47,ZMODUL01:def 8;
end;
then
A49: for k st P[k] holds P[k+1];
let l;
A50: card(Carrier(l)) = card(Carrier(l));
for k holds P[k] from NAT_1:sch 1(A3,A49);
hence thesis by A50;
end;
assume
A51: for l holds Sum(l) in A;
hence A <> {};
Z_ZeroLC(V) is Z_Linear_Combination of A & Sum(Z_ZeroLC(V)) = 0.V
by RL2Lm1,RL2Th34;
then
A52: 0.V in A by A51;
A53: for a, v st v in A holds a * v in A
proof
let a, v;
assume
A54: v in A;
now
per cases;
suppose
a = 0;
hence thesis by A52,ZMODUL01:1;
end;
suppose
A55: a <> 0;
reconsider N0 = 0 as Element of INT by INT_1:def 2;
reconsider Na = a as Element of INT by INT_1:def 2;
deffunc F(Element of the carrier of V) = N0;
consider f such that
A56: f.v = Na and
A57: 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, INT)
by FUNCT_2:8;
now
let u;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0 by A57;
end;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
A58: Carrier(f) = {v}
proof
thus Carrier(f) c= {v}
proof
let x;
assume x in Carrier(f);
then consider u such that
A59: x = u and
A60: f.u <> 0;
u = v by A57,A60;
hence thesis by A59,TARSKI:def 1;
end;
let x;
assume x in {v};
then x = v by TARSKI:def 1;
hence thesis by A55,A56;
end;
{v} c= A by A54,ZFMISC_1:31;
then reconsider f as Z_Linear_Combination of A
by A58,RL2Def8;
consider F such that
A61: F is one-to-one & rng F = Carrier(f) and
A62: Sum(f (#) F) = Sum(f) by RL2Def10;
F = <* v *> by A58,A61,FINSEQ_3:97;
then f (#) F = <* f.v * v *> by RL2Th42;
then Sum(f) = a * v by A56,A62,RLVECT_1:44;
hence thesis by A51;
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
A63: v in A and
A64: u in A;
now
per cases;
suppose
u = v;
then v + u = 1 * v + v by ZMODUL01:def 5
.= 1 * v + 1 * v by ZMODUL01:def 5
.= (1 + 1) * v by ZMODUL01:def 3
.= 2 * v;
hence thesis by A53,A63;
end;
suppose
A65: v <> u;
reconsider N0=0 as Element of INT by INT_1:def 2;
reconsider N1=1 as Element of INT by INT_1:def 2;
deffunc F(Element of V)=N0;
consider f such that
A66: f.v = N1 & f.u = N1 and
A67: for w being Element of V st w <> v & w <> u holds f.w = F(w)
from FUNCT_2:sch 7(A65);
reconsider f as Element of Funcs(the carrier of V, INT)
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 by A67;
end;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
A68: Carrier(f) = {v,u}
proof
thus Carrier(f) c= {v,u}
proof
let x;
assume x in Carrier(f);
then ex w st x = w & f.w <> 0;
then x = v or x = u by A67;
hence thesis by TARSKI:def 2;
end;
let x;
assume x in {v,u};
then x = v or x = u by TARSKI:def 2;
hence thesis by A66;
end;
then
A69: Carrier(f) c= A by A63,A64,ZFMISC_1:32;
A70: 1 * u = u & 1 * v = v by ZMODUL01:def 5;
reconsider f as Z_Linear_Combination of A by A69,RL2Def8;
consider F such that
A71: F is one-to-one & rng F = Carrier(f) and
A72: Sum(f (#) F) = Sum(f) by RL2Def10;
F = <* v,u *> or F = <* u,v *> by A65,A68,A71,FINSEQ_3:99;
then f (#) F = <* 1 * v, 1 * u *> or f (#) F = <* 1 * u, 1* v *>
by A66,RL2Th43;
then Sum(f) = v + u by A72,A70,RLVECT_1:45;
hence thesis by A51;
end;
end;
hence thesis;
end;
thus thesis by A53;
end;
theorem
Sum(Z_ZeroLC(V)) = 0.V by RL2Lm1;
theorem RL2Th49:
for l being Z_Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V
proof
let l be Z_Linear_Combination of {}(the carrier of V);
l = Z_ZeroLC(V) by RL2Th35;
hence thesis by RL2Lm1;
end;
theorem RL2Th50:
for l being Z_Linear_Combination of {v} holds Sum(l) = l.v * v
proof
let l be Z_Linear_Combination of {v};
A1: Carrier(l) c= {v} by RL2Def8;
now
per cases by A1,ZFMISC_1:33;
suppose
Carrier(l) = {};
then
A2: l = Z_ZeroLC(V) by RL2Def7;
hence Sum(l) = 0.V by RL2Lm1
.= l.v * v by A2,RL2Th30,ZMODUL01:1;
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 RL2Def10;
F = <* v *> by A3,FINSEQ_3:97;
then l (#) F = <* l.v * v *> by RL2Th42;
hence thesis by A4,RLVECT_1:44;
end;
end;
hence thesis;
end;
theorem RL2Th51:
v1 <> v2 implies for l being Z_Linear_Combination of {v1,v2} holds
Sum(l) = l.v1 * v1 + l.v2 * v2
proof
assume
A1: v1 <> v2;
let l be Z_Linear_Combination of {v1,v2};
A2: Carrier(l) c= {v1,v2} by RL2Def8;
now
per cases by A2,ZFMISC_1:36;
suppose
Carrier(l) = {};
then
A3: l = Z_ZeroLC(V) by RL2Def7;
hence Sum(l) = 0.V by RL2Lm1
.= 0.V + 0.V by RLVECT_1:4
.= 0 * v1 + 0.V by ZMODUL01:1
.= 0 * v1 + 0 * v2 by ZMODUL01:1
.= l.v1 * v1 + 0 * v2 by A3,RL2Th30
.= l.v1 * v1 + l.v2 * v2 by A3,RL2Th30;
end;
suppose
A4: Carrier(l) = {v1};
then reconsider L = l as Z_Linear_Combination of {v1}
by RL2Def8;
A5: not v2 in Carrier(l) by A1,A4,TARSKI:def 1;
thus Sum(l) = Sum(L) .= l.v1 * v1 by RL2Th50
.= l.v1 * v1 + 0.V by RLVECT_1:4
.= l.v1 * v1 + 0 * v2 by ZMODUL01:1
.= l.v1 * v1 + l.v2 * v2 by A5;
end;
suppose
A6: Carrier(l) = {v2};
then reconsider L = l as Z_Linear_Combination of {v2}
by RL2Def8;
A7: not v1 in Carrier(l) by A1,A6,TARSKI:def 1;
thus Sum(l) = Sum(L) .= l.v2 * v2 by RL2Th50
.= 0.V + l.v2 * v2 by RLVECT_1:4
.= 0 * v1 + l.v2 * v2 by ZMODUL01:1
.= l.v1 * v1 + l.v2 * 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 RL2Def10;
F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A8,FINSEQ_3:99;
then l (#) F = <* l.v1 * v1, l.v2 * v2 *> or l (#) F =
<* l.v2 * v2, l.v1 * v1 *> by RL2Th43;
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 = Z_ZeroLC(V) by RL2Def7;
hence thesis by RL2Lm1;
end;
theorem RL2Th53:
Carrier(L) = {v} implies Sum(L) = L.v * v
proof
assume Carrier(L) = {v};
then L is Z_Linear_Combination of {v} by RL2Def8;
hence thesis by RL2Th50;
end;
theorem
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2
proof
assume that
A1: Carrier(L) = {v1,v2} and
A2: v1 <> v2;
L is Z_Linear_Combination of {v1,v2} by A1,RL2Def8;
hence thesis by A2,RL2Th51;
end;
definition
let V be non empty addLoopStr;
let L1, L2 be Z_Linear_Combination of V;
redefine pred L1 = L2 means
for v being Element of V holds L1.v = L2.v;
compatibility by FUNCT_2:63;
end;
definition
let V be non empty addLoopStr;
let L1, L2 be Z_Linear_Combination of V;
redefine func L1 + L2 -> Z_Linear_Combination of V means
:RL2Def12:
for v being Element of V holds it.v = L1.v + L2.v;
coherence
proof
reconsider f = L1+L2 as Element of Funcs(the carrier of V,INT)
by FUNCT_2:8;
now
let v be Element of V;
reconsider N0 = 0 as Element of INT by INT_1:def 2;
assume
A1: not v in Carrier(L1) \/ Carrier(L2);
then not v in Carrier(L2) by XBOOLE_0:def 3;
then
A2: L2.v = N0;
not v in Carrier(L1) by A1,XBOOLE_0:def 3;
then L1.v = N0;
hence f.v = N0 + N0 by A2,VALUED_1:1
.= 0;
end;
hence thesis by RL2Def5;
end;
compatibility
proof
let f be Z_Linear_Combination of V;
thus f=L1+L2 implies for v being Element of V holds f.v = L1.v + L2.v
by VALUED_1:1;
assume
A3: for v being Element of V holds f.v = L1.v + L2.v;
thus f = L1+L2
proof
let v be Element of the carrier of V;
thus f.v = L1.v+L2.v by A3
.= (L1+L2).v by VALUED_1:1;
end;
end;
commutativity;
end;
theorem RL2Th58:
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2)
proof
let x;
assume x in Carrier(L1 + L2);
then consider u such that
A1: x = u and
A2: (L1 + L2).u <> 0;
(L1 + L2).u = L1.u + L2.u by RL2Def12;
then L1.u <> 0 or L2.u <> 0 by A2;
then x in {v1 : L1.v1 <> 0} or x in {v2 : L2.v2 <> 0} by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem RL2Th59:
L1 is Z_Linear_Combination of A & L2 is Z_Linear_Combination of A
implies L1 + L2 is Z_Linear_Combination of A
proof
assume L1 is Z_Linear_Combination of A & L2 is Z_Linear_Combination of A;
then Carrier(L1) c= A & Carrier(L2) c= A by RL2Def8;
then
A1: Carrier(L1) \/ Carrier(L2) c= A by XBOOLE_1:8;
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by RL2Th58;
hence Carrier(L1 + L2) c= A by A1,XBOOLE_1:1;
end;
theorem RL2Th61:
L1 + (L2 + L3) = L1 + L2 + L3
proof
let v;
thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by RL2Def12
.= L1.v + (L2.v + L3.v) by RL2Def12
.= L1.v + L2.v + L3.v
.= (L1 + L2).v + L3.v by RL2Def12
.= (L1 + L2 + L3).v by RL2Def12;
end;
registration let V,L;
reduce L + Z_ZeroLC(V) to L;
reducibility
proof
let v;
reconsider N0 = 0 as Element of INT by INT_1:def 2;
thus (L + Z_ZeroLC(V)).v = L.v + (Z_ZeroLC(V)).v by RL2Def12
.= L.v + N0 by RL2Th30
.= L.v;
end;
end;
definition
let V, a, L;
func a * L -> Z_Linear_Combination of V means
:RL2Def13:
for v holds it.v = a * L.v;
existence
proof
deffunc F(Element of V)=a * L.$1;
consider f being Function of the carrier of V, INT 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,INT) by FUNCT_2:8;
now
let v;
reconsider N0 = 0 as Element of INT by INT_1:def 2;
assume not v in Carrier(L);
then L.v = N0;
hence f.v = a * N0 by A1
.= 0;
end;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
take f;
let v;
thus thesis by A1;
end;
uniqueness
proof
let L1, L2;
assume
A2: for v holds L1.v = a * L.v;
assume
A3: for v holds L2.v = a * L.v;
let v;
thus L1.v = a * L.v by A2
.= L2.v by A3;
end;
end;
theorem RL2Th65:
a <> 0 implies Carrier(a * L) = Carrier(L)
proof
set T = {u : (a * L).u <> 0};
set S = {v : L.v <> 0};
assume
A1: a <> 0;
T = S
proof
thus T c= S
proof
let x;
assume x in T;
then consider u such that
A2: x = u and
A3: (a * L).u <> 0;
(a * L).u = a * L.u by RL2Def13;
then L.u <> 0 by A3;
hence thesis by A2;
end;
let x;
assume x in S;
then consider v such that
A4: x = v and
A5: L.v <> 0;
(a * L).v = a * L.v by RL2Def13;
then (a * L).v <> 0 by A1,A5,XCMPLX_1:6;
hence thesis by A4;
end;
hence thesis;
end;
theorem RL2Th66:
0 * L = Z_ZeroLC(V)
proof
let v;
thus (0 * L).v = 0 * L.v by RL2Def13
.= (Z_ZeroLC(V)).v by RL2Th30;
end;
theorem RL2Th67:
L is Z_Linear_Combination of A implies a * L is Z_Linear_Combination of A
proof
assume
A1: L is Z_Linear_Combination of A;
now
per cases;
suppose
a = 0;
then a * L = Z_ZeroLC(V) by RL2Th66;
hence thesis by RL2Th34;
end;
suppose
a <> 0;
then Carrier(a * L) = Carrier(L) by RL2Th65;
hence thesis by A1,RL2Def8;
end;
end;
hence thesis;
end;
theorem RL2Th68:
(a + b) * L = a * L + b * L
proof
let v;
thus ((a + b) * L).v = (a + b) * L.v by RL2Def13
.= a * L.v + b * L.v
.= (a * L).v + b * L.v by RL2Def13
.= (a * L).v + (b * L). v by RL2Def13
.= ((a * L) + (b * L)).v by RL2Def12;
end;
theorem RL2Th69:
a * (L1 + L2) = a * L1 + a * L2
proof
let v;
thus (a * (L1 + L2)).v = a * (L1 + L2).v by RL2Def13
.= a * (L1.v + L2.v) by RL2Def12
.= a * L1.v + a * L2.v
.= (a * L1).v + a * L2.v by RL2Def13
.= (a * L1).v + (a * L2). v by RL2Def13
.= ((a * L1) + (a * L2)).v by RL2Def12;
end;
theorem RL2Th70:
a * (b * L) = (a * b) * L
proof
let v;
thus (a * (b * L)).v = a * (b * L).v by RL2Def13
.= a * (b * L.v) by RL2Def13
.= a * b * L.v
.= ((a * b) * L).v by RL2Def13;
end;
registration let V,L;
reduce 1*L to L;
reducibility
proof
let v;
thus (1 * L).v = 1 * L.v by RL2Def13
.= L.v;
end;
end;
definition
let V,L;
func - L -> Z_Linear_Combination of V equals
(- 1) * L;
coherence;
involutiveness
proof let L1,L be Z_Linear_Combination of V such that
Z: L1 = (-1)*L;
1*L = (-1)*(-1)*L .= (-1)*((-1)*L) by RL2Th70;
hence L = (-1)*L1 by Z;
end;
end;
theorem RL2Th73:
(- L).v = - L.v
proof
thus (- L).v = (- 1) * L.v by RL2Def13
.= - L.v;
end;
theorem
L1 + L2 = Z_ZeroLC(V) implies L2 = - L1
proof
assume
A1: L1 + L2 = Z_ZeroLC(V);
let v;
L1.v + L2.v = (Z_ZeroLC(V)).v by A1,RL2Def12
.= 0 by RL2Th30;
hence L2.v = - L1.v .= (- L1).v by RL2Th73;
end;
theorem
Carrier(- L) = Carrier(L) by RL2Th65;
theorem
L is Z_Linear_Combination of A
implies - L is Z_Linear_Combination of A by RL2Th67;
definition
let V,L1,L2;
func L1 - L2 -> Z_Linear_Combination of V equals
L1 + (- L2);
correctness;
end;
theorem RL2Th79:
(L1 - L2).v = L1.v - L2.v
proof
thus (L1 - L2).v = L1.v + (- L2).v by RL2Def12
.= L1.v + (- L2.v) by RL2Th73
.= L1.v - L2.v;
end;
theorem
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2)
proof
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(- L2) by RL2Th58;
hence thesis by RL2Th65;
end;
theorem
L1 is Z_Linear_Combination of A & L2 is Z_Linear_Combination of A implies
L1 - L2 is Z_Linear_Combination of A
proof
assume that
A1: L1 is Z_Linear_Combination of A and
A2: L2 is Z_Linear_Combination of A;
- L2 is Z_Linear_Combination of A by A2,RL2Th67;
hence thesis by A1,RL2Th59;
end;
theorem RL2Th82:
L - L = Z_ZeroLC(V)
proof
let v;
thus (L - L).v = L.v - L.v by RL2Th79
.= (Z_ZeroLC(V)).v by RL2Th30;
end;
definition
let V;
func LinComb(V) -> set means
:RL2Def16:
x in it iff x is Z_Linear_Combination of V;
existence
proof
defpred P[set] means $1 is Z_Linear_Combination of V;
consider A being set such that
A1: for x holds x in A iff x in Funcs(the carrier of V, INT) & P[x]
from XBOOLE_0:sch 1;
take A;
let x;
thus x in A implies x is Z_Linear_Combination of V by A1;
assume x is Z_Linear_Combination of V;
hence thesis by A1;
end;
uniqueness
proof
let D1, D2 be set;
assume
A2: for x holds x in D1 iff x is Z_Linear_Combination of V;
assume
A3: for x holds x in D2 iff x is Z_Linear_Combination of V;
thus D1 c= D2
proof
let x;
assume x in D1;
then x is Z_Linear_Combination of V by A2;
hence thesis by A3;
end;
let x;
assume x in D2;
then x is Z_Linear_Combination of V by A3;
hence thesis by A2;
end;
end;
registration
let V;
cluster LinComb(V) -> non empty;
coherence
proof
set x = the Z_Linear_Combination of V;
x in LinComb V by RL2Def16;
hence thesis;
end;
end;
reserve e, e1, e2 for Element of LinComb(V);
definition
let V, e;
func @e -> Z_Linear_Combination of V equals
e;
coherence by RL2Def16;
end;
definition
let V, L;
func @L -> Element of LinComb(V) equals
L;
coherence by RL2Def16;
end;
definition
let V;
func LCAdd(V) -> BinOp of LinComb(V) means
:RL2Def19:
for e1, e2 holds it.(e1,e2) = @e1 + @e2;
existence
proof
deffunc F(Element of LinComb(V),Element of LinComb(V))=@(@$1 + @$2);
consider o being BinOp of LinComb(V) such that
A1: for e1, e2 holds o.(e1,e2) = F(e1,e2) from BINOP_1:sch 4;
take o;
let e1, e2;
thus o.(e1,e2) = @(@e1 + @e2) by A1
.= @e1 + @e2;
end;
uniqueness
proof
let o1, o2 be BinOp of LinComb(V);
assume
A2: for e1, e2 holds o1.(e1,e2) = @e1 + @e2;
assume
A3: for e1, e2 holds o2.(e1,e2) = @e1 + @e2;
now
let e1, e2;
thus o1.(e1,e2) = @e1 + @e2 by A2
.= o2.(e1,e2) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let V;
func LCMult(V) -> Function of [:INT,LinComb(V):], LinComb(V) means
:RL2Def20:
for a, e holds it. [a,e] = a * @e;
existence
proof
defpred P[Element of INT,Element of LinComb(V),set] means ex a st a = $1
& $3 = a * @$2;
A1: for x being (Element of INT), e1 ex e2 st P[x,e1,e2]
proof
let x be (Element of INT), e1;
take @(x * @e1);
take x;
thus thesis;
end;
consider g being Function of [:INT,LinComb(V):], LinComb(V) such that
A2: for x being (Element of INT), e holds P[x,e,g.(x,e)] from BINOP_1
:sch 3 (A1);
take g;
let a, e;
reconsider a0=a as Element of INT by INT_1:def 2;
ex b st b = a0 & g.(a0,e) = b * @e by A2;
hence thesis;
end;
uniqueness
proof
let g1, g2 be Function of [:INT,LinComb(V):], LinComb(V);
assume
A3: for a, e holds g1. [a,e] = a * @e;
assume
A4: for a, e holds g2. [a,e] = a * @e;
now
let x be (Element of INT), e;
thus g1.(x,e) = x * @e by A3
.= g2.(x,e) by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let V;
func LC_Z_Module V -> Z_ModuleStruct equals
Z_ModuleStruct (# LinComb(V), @Z_ZeroLC(V), LCAdd(V), LCMult(V) #);
coherence;
end;
registration
let V;
cluster LC_Z_Module V -> strict non empty;
coherence;
end;
registration
let V;
cluster LC_Z_Module V -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
set S = LC_Z_Module V;
A1:
now
let v, u be (VECTOR of S), K,L;
A2: @@K = K & @@L = L;
assume v = K & u = L;
hence v + u = K + L by A2,RL2Def19;
end;
thus S is Abelian
proof
let u, v be Element of S;
reconsider K = u, L = v as Z_Linear_Combination of V by RL2Def16;
thus u + v = L + K by A1
.= v + u by A1;
end;
thus S is add-associative
proof
let u, v, w be Element of S;
reconsider L = u, K = v, M = w as Z_Linear_Combination of V by RL2Def16;
A3: v + w = K + M by A1;
u + v = L + K by A1;
hence (u + v) + w = L + K + M by A1
.= L + (K + M) by RL2Th61
.= u + (v + w) by A1,A3;
end;
thus S is right_zeroed
proof
let v be Element of S;
reconsider K = v as Z_Linear_Combination of V by RL2Def16;
thus v + 0.S = K + Z_ZeroLC V by A1
.= v;
end;
thus S is right_complementable
proof
let v be Element of S;
reconsider K = v as Z_Linear_Combination of V by RL2Def16;
- K in the carrier of S by RL2Def16;
then - K in S by STRUCT_0:def 5;
then - K = vector(S,- K) by RLVECT_2:def 1;
then v + vector(S,- K) = K - K by A1
.= 0.S by RL2Th82;
hence ex w being VECTOR of S st v + w = 0.S;
end;
A4:
now
let v be (VECTOR of S), L,a;
A5: @@L = L;
assume v = L;
hence a * v = a * L by A5,RL2Def20;
end;
thus S is vector-distributive
proof
let a be Integer;
let v, w be VECTOR of S;
reconsider K = v, M = w as Z_Linear_Combination of V by RL2Def16;
reconsider a as Integer;
A6: a * v = a * K & a * w = a * M by A4;
v + w = K + M by A1;
then a * (v + w) = a * (K + M) by A4
.= a * K + a * M by RL2Th69
.= a * v + a * w by A1,A6;
hence thesis;
end;
thus S is scalar-distributive
proof
let a, b be integer number;
let v be VECTOR of S;
reconsider K = v as Z_Linear_Combination of V by RL2Def16;
reconsider a, b as Integer;
A7: a * v = a * K & b * v = b * K by A4;
(a + b) * v = (a + b) * K by A4
.= a * K + b * K by RL2Th68
.= a * v + b * v by A1,A7;
hence thesis;
end;
thus S is scalar-associative
proof
let a, b be integer number;
let v be VECTOR of S;
reconsider K = v as Z_Linear_Combination of V by RL2Def16;
reconsider a,b as Integer;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by RL2Th70
.= a * (b * v) by A4,A8;
hence thesis;
end;
let v be VECTOR of S;
reconsider K = v as Z_Linear_Combination of V by RL2Def16;
thus 1 * v = 1 * K by A4 .= v;
end;
end;
theorem
the carrier of LC_Z_Module(V) = LinComb(V);
theorem
0.LC_Z_Module(V) = Z_ZeroLC(V);
theorem
the addF of LC_Z_Module(V) = LCAdd(V);
theorem
the Mult of LC_Z_Module(V) = LCMult(V);
theorem RL2Th96:
vector(LC_Z_Module(V),L1) + vector(LC_Z_Module(V),L2) = L1 + L2
proof
set v2 = vector(LC_Z_Module(V),L2);
A1: L1 = @@L1 & L2 = @@L2;
L2 in the carrier of LC_Z_Module(V) by RL2Def16;
then
A2: L2 in LC_Z_Module(V) by STRUCT_0:def 5;
L1 in the carrier of LC_Z_Module(V) by RL2Def16;
then L1 in LC_Z_Module(V) by STRUCT_0:def 5;
hence vector(LC_Z_Module(V),L1)
+ vector(LC_Z_Module(V),L2) = LCAdd(V). [L1,v2] by RLVECT_2:def 1
.= LCAdd(V).(@L1,@L2) by A2,RLVECT_2:def 1
.= L1 + L2 by A1,RL2Def19;
end;
theorem RL2Th97:
a * vector(LC_Z_Module(V),L) = a * L
proof
A1: @@L = L;
L in the carrier of LC_Z_Module(V) by RL2Def16;
then L in LC_Z_Module(V) by STRUCT_0:def 5;
hence a * vector(LC_Z_Module(V),L) = LCMult(V). [a,@L] by RLVECT_2:def 1
.= a * L by A1,RL2Def20;
end;
theorem RL2Th98:
- vector(LC_Z_Module(V),L) = - L
proof
thus - vector(LC_Z_Module(V),L) = (- 1) * (vector(LC_Z_Module(V),L)) by
ZMODUL01:2
.= - L by RL2Th97;
end;
theorem
vector(LC_Z_Module(V),L1) - vector(LC_Z_Module(V),L2) = L1 - L2
proof
- L2 in LinComb(V) by RL2Def16;
then
A1: - L2 in LC_Z_Module(V) by STRUCT_0:def 5;
- vector(LC_Z_Module(V),L2) = - L2 by RL2Th98
.= vector(LC_Z_Module(V),- L2) by A1,RLVECT_2:def 1;
hence thesis by RL2Th96;
end;
definition
let V,A;
func LC_Z_Module(A) -> strict Submodule of LC_Z_Module(V) means
the carrier of it = {l : not contradiction};
existence
proof
set X = {l : not contradiction};
X c= the carrier of LC_Z_Module(V)
proof
let x;
assume x in X;
then ex l st x = l;
hence thesis by RL2Def16;
end;
then reconsider X as Subset of LC_Z_Module(V);
A1: X is linearly-closed
proof
thus for v,u being VECTOR of LC_Z_Module(V) st v in X & u in X holds
v + u in X
proof
let v, u be VECTOR of LC_Z_Module(V);
assume that
A2: v in X and
A3: u in X;
consider l1 such that
A4: v = l1 by A2;
consider l2 such that
A5: u = l2 by A3;
A6: u = vector(LC_Z_Module(V),l2) by A5,RLVECT_2:def 1,RLVECT_1:1;
v = vector(LC_Z_Module(V),l1) by A4,RLVECT_2:def 1,RLVECT_1:1;
then v + u = l1 + l2 by A6,RL2Th96;
then v + u is Z_Linear_Combination of A by RL2Th59;
hence thesis;
end;
let a be integer number;
let v be VECTOR of LC_Z_Module(V);
assume v in X;
then consider l such that
A7: v = l;
a * v = a * vector(LC_Z_Module(V),l)
by A7,RLVECT_2:def 1,RLVECT_1:1
.= a * l by RL2Th97;
then a * v is Z_Linear_Combination of A by RL2Th67;
hence thesis;
end;
Z_ZeroLC(V) is Z_Linear_Combination of A by RL2Th34;
then Z_ZeroLC(V) in X;
hence thesis by A1,ZMODUL01:50;
end;
uniqueness by ZMODUL01:45;
end;
begin :: 3. Linearly independent subset of Z-module
reserve W, W1, W2, W3 for Submodule of V;
reserve v, v1, v2, u for VECTOR of V;
reserve A, B, C for Subset of V;
reserve T for finite Subset of V;
reserve L, L1, L2 for Z_Linear_Combination of V;
reserve l for Z_Linear_Combination of A;
reserve F, G, H for FinSequence of the carrier of V;
reserve f, g for Function of the carrier of V, INT;
RL3Lm1: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len H = len(f (#) F) + len(f (#) G) by FINSEQ_1:22
.= len F + len(f (#) G) by RL2Def9
.= len F + len G by RL2Def9
.= len I by FINSEQ_1:22;
A2: len F = len(f (#) F) by RL2Def9;
A3: len G = len(f (#) G) by RL2Def9;
now
let k;
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 A2,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
.= f.(I/.k) * I/.k by A5,A8,RL2Def9;
end;
suppose
A9: ex n be Nat st n in dom(f (#) G) & k = len(f (#) F) + n;
A10: k in dom I by A1,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 A2,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
.= f.(I/.k) * I/.k by A11,A14,RL2Def9;
end;
end;
hence H.k = f.(I/.k) * I/.k;
end;
hence thesis by A1,RL2Def9;
end;
theorem
f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by RL3Lm1;
theorem RL3Th1:
Sum(L1 + L2) = Sum(L1) + Sum(L2)
proof
consider F such that
A1: F is one-to-one and
A2: rng F = Carrier(L1 + L2) and
A3: Sum((L1 + L2) (#) F) = Sum(L1 + L2) by RL2Def10;
set A = Carrier(L1 + L2) \/ Carrier(L1) \/ Carrier(L2);
set C3 = A \ Carrier(L1 + L2);
consider r being FinSequence such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of the carrier of V by A4,FINSEQ_1:def 4;
set FF = F ^ r;
A6: A = Carrier(L1 + L2) \/ (Carrier(L1) \/ Carrier(L2)) by XBOOLE_1:4;
rng F misses rng r
proof
set x = the Element of rng F /\ rng r;
assume not thesis;
then rng F /\ rng r <> {} by XBOOLE_0:def 7;
then x in Carrier(L1 + L2) & x in C3 by A2,A4,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A7: FF is one-to-one by A1,A5,FINSEQ_3:91;
A8: len r = len((L1 + L2) (#) r) by RL2Def9;
now
let k;
assume
A9: k in dom r;
then r/.k = r.k by PARTFUN1:def 6;
then r/.k in C3 by A4,A9,FUNCT_1:def 3;
then
A10: not r/.k in Carrier((L1 + L2)) by XBOOLE_0:def 5;
k in dom((L1 + L2) (#) r) by A8,A9,FINSEQ_3:29;
then ((L1 + L2) (#) r).k = (L1 + L2).(r/.k) * r/.k by RL2Def9;
hence ((L1 + L2) (#) r).k = 0 * r/.k by A10;
end;
then
A11: Sum((L1 + L2) (#) r) = 0 * Sum(r) by A8,ZMODUL01:17
.= 0.V by ZMODUL01:1;
set f = (L1 + L2) (#) FF;
set C1 = A \ Carrier(L1);
consider G such that
A12: G is one-to-one and
A13: rng G = Carrier(L1) and
A14: Sum(L1 (#) G) = Sum(L1) by RL2Def10;
consider p being FinSequence such that
A15: rng p = C1 and
A16: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the carrier of V by A15,FINSEQ_1:def 4;
set GG = G ^ p;
A17: Sum(f) = Sum(((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by RL3Lm1
.= Sum((L1 + L2) (#) F) + 0.V by A11,RLVECT_1:41
.= Sum((L1 + L2) (#) F) by RLVECT_1:4;
set C2 = A \ Carrier(L2);
consider H such that
A18: H is one-to-one and
A19: rng H = Carrier(L2) and
A20: Sum(L2 (#) H) = Sum(L2) by RL2Def10;
consider q being FinSequence such that
A21: rng q = C2 and
A22: q is one-to-one by FINSEQ_4:58;
reconsider q as FinSequence of the carrier of V by A21,FINSEQ_1:def 4;
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 <> {} by XBOOLE_0:def 7;
then x in Carrier(L2) & x in C2 by A19,A21,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A23: HH is one-to-one by A18,A22,FINSEQ_3:91;
set h = L2 (#) HH;
A24: A = Carrier(L1) \/ (Carrier(L1 + L2) \/ Carrier(L2)) by XBOOLE_1:4;
rng GG = rng G \/ rng p by FINSEQ_1:31;
then rng GG = Carrier(L1) \/ A by A13,A15,XBOOLE_1:39;
then
A25: rng GG = A by A24,XBOOLE_1:7,12;
A26: len q = len(L2 (#) q) by RL2Def9;
now
let k;
assume
A27: k in dom q;
then q/.k = q.k by PARTFUN1:def 6;
then q/.k in C2 by A21,A27,FUNCT_1:def 3;
then
A28: not q/.k in Carrier(L2) by XBOOLE_0:def 5;
k in dom(L2 (#) q) by A26,A27,FINSEQ_3:29;
then (L2 (#) q).k = L2.(q/.k) * q/.k by RL2Def9;
hence (L2 (#) q).k = 0 * q/.k by A28;
end;
then
A29: Sum(L2 (#) q) = 0 * Sum(q) by A26,ZMODUL01:17
.= 0.V by ZMODUL01:1;
A30: Sum(h) = Sum((L2 (#) H) ^ (L2 (#) q)) by RL3Lm1
.= Sum(L2 (#) H) + 0.V by A29,RLVECT_1:41
.= Sum(L2 (#) H) by RLVECT_1:4;
deffunc Q(Nat)=FF <- (GG.$1);
set g = L1 (#) GG;
consider P being FinSequence such that
A31: len P = len FF and
A32: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A33: dom P = Seg(len FF) by A31,FINSEQ_1:def 3;
A34: len p = len(L1 (#) p) by RL2Def9;
now
let k;
assume
A35: k in dom p;
then p/.k = p.k by PARTFUN1:def 6;
then p/.k in C1 by A15,A35,FUNCT_1:def 3;
then
A36: not p/.k in Carrier(L1) by XBOOLE_0:def 5;
k in dom(L1 (#) p) by A34,A35,FINSEQ_3:29;
then (L1 (#) p).k = L1.(p/.k) * p/.k by RL2Def9;
hence (L1 (#) p).k = 0 * p/.k by A36;
end;
then
A37: Sum(L1 (#) p) = 0 * Sum(p) by A34,ZMODUL01:17
.= 0.V by ZMODUL01:1;
A38: Sum(g) = Sum((L1 (#) G) ^ (L1 (#) p)) by RL3Lm1
.= Sum(L1 (#) G) + 0.V by A37,RLVECT_1:41
.= Sum(L1 (#) G) by RLVECT_1:4;
rng FF = rng F \/ rng r by FINSEQ_1:31;
then rng FF = Carrier(L1 + L2) \/ A by A2,A4,XBOOLE_1:39;
then
A39: rng FF = A by A6,XBOOLE_1:7,12;
rng G misses rng p
proof
set x = the Element of rng G /\ rng p;
assume not thesis;
then rng G /\ rng p <> {} by XBOOLE_0:def 7;
then x in Carrier(L1) & x in C1 by A13,A15,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A40: GG is one-to-one by A12,A16,FINSEQ_3:91;
then
A41: len GG = len FF by A7,A25,A39,FINSEQ_1:48;
A42: dom P = Seg len FF by A31,FINSEQ_1:def 3;
A43:
now
let x;
assume
A44: x in dom GG;
then reconsider n = x as Element of NAT;
GG.n in rng FF by A25,A39,A44,FUNCT_1:def 3;
then
A45: FF just_once_values GG.n by A7,FINSEQ_4:8;
n in Seg(len FF) by A41,A44,FINSEQ_1:def 3;
then FF.(P.n) = FF.(FF <- (GG.n)) by A32,A42
.= GG.n by A45,FINSEQ_4:def 3;
hence GG.x = FF.(P.x);
end;
A46: rng P c= Seg(len FF)
proof
let x;
assume x in rng P;
then consider y such that
A47: y in dom P and
A48: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A47;
y in Seg(len FF) by A31,A47,FINSEQ_1:def 3;
then y in dom GG by A41,FINSEQ_1:def 3;
then GG.y in rng FF by A25,A39,FUNCT_1:def 3;
then
A49: FF just_once_values GG.y by A7,FINSEQ_4:8;
P.y = FF <- (GG.y) by A32,A47;
then P.y in dom FF by A49,FINSEQ_4:def 3;
hence thesis by A48,FINSEQ_1:def 3;
end;
now
let x;
thus x in dom GG implies x in dom P & P.x in dom FF
proof
assume x in dom GG;
then x in Seg(len P) by A41,A31,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;
then P.x in Seg(len FF) by A46;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A50: x in dom P and
P.x in dom FF;
x in Seg(len P) by A50,FINSEQ_1:def 3;
hence x in dom GG by A41,A31,FINSEQ_1:def 3;
end;
then
A51: GG = FF * P by A43,FUNCT_1:10;
Seg(len FF) c= rng P
proof
set f = FF" * GG;
now let x be set;
assume
A52: x in Seg(len FF);
dom(FF") = rng GG by A7,A25,A39,FUNCT_1:33;
then
A53: rng f = rng(FF") by RELAT_1:28
.= dom FF by A7,FUNCT_1:33;
A54: rng P c= dom FF by A46,FINSEQ_1:def 3;
f = FF " * FF * P by A51,RELAT_1:36
.= id(dom FF) * P by A7,FUNCT_1:39
.= P by A54,RELAT_1:53;
hence x in rng P by A52,A53,FINSEQ_1:def 3;
end;
hence thesis by TARSKI:def 3;
end;
then
A55: Seg(len FF) = rng P by A46,XBOOLE_0:def 10;
then
A56: P is one-to-one by A33,FINSEQ_4:60;
reconsider P as Function of Seg(len FF), Seg(len FF)
by FUNCT_2:1,A55,A42;
reconsider P as Permutation of Seg(len FF) by A55,A56,FUNCT_2:57;
A57: len f = len FF by RL2Def9;
then
A58: Seg len FF = dom f by FINSEQ_1:def 3;
then reconsider Fp = f * P as FinSequence of the carrier of V
by FINSEQ_2:47;
A59: len g = len GG by RL2Def9;
deffunc Q(Nat)=HH <- (GG.$1);
consider R being FinSequence such that
A60: len R = len HH and
A61: for k be Nat st k in dom R holds R.k =Q(k) from FINSEQ_1:sch 2;
A62: dom R = Seg(len HH) by A60,FINSEQ_1:def 3;
rng HH = rng H \/ rng q by FINSEQ_1:31;
then rng HH = Carrier(L2) \/ A by A19,A21,XBOOLE_1:39;
then
A63: rng HH = A by XBOOLE_1:7,12;
then
A64: len GG = len HH by A23,A40,A25,FINSEQ_1:48;
A65: dom R = Seg len HH by A60,FINSEQ_1:def 3;
A66:
now
let x;
assume
A67: x in dom GG;
then reconsider n = x as Element of NAT;
GG.n in rng HH by A25,A63,A67,FUNCT_1:def 3;
then
A68: HH just_once_values GG.n by A23,FINSEQ_4:8;
n in Seg(len HH) by A64,A67,FINSEQ_1:def 3;
then HH.(R.n) = HH.(HH <- (GG.n)) by A61,A65
.= GG.n by A68,FINSEQ_4:def 3;
hence GG.x = HH.(R.x);
end;
A69: rng R c= Seg(len HH)
proof
let x;
assume x in rng R;
then consider y such that
A70: y in dom R and
A71: R.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A70;
y in Seg(len HH) by A60,A70,FINSEQ_1:def 3;
then y in dom GG by A64,FINSEQ_1:def 3;
then GG.y in rng HH by A25,A63,FUNCT_1:def 3;
then
A72: HH just_once_values GG.y by A23,FINSEQ_4:8;
R.y = HH <- (GG.y) by A61,A70;
then R.y in dom HH by A72,FINSEQ_4:def 3;
hence thesis by A71,FINSEQ_1:def 3;
end;
now
let x;
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 A64,A60,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;
then R.x in Seg(len HH) by A69;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A73: x in dom R and
R.x in dom HH;
x in Seg(len R) by A73,FINSEQ_1:def 3;
hence x in dom GG by A64,A60,FINSEQ_1:def 3;
end;
then
A74: GG = HH * R by A66,FUNCT_1:10;
Seg(len HH) c= rng R
proof
set f = HH" * GG;
now let x;
assume
A75: x in Seg(len HH);
dom(HH") = rng GG by A23,A25,A63,FUNCT_1:33;
then
A76: rng f = rng(HH") by RELAT_1:28
.= dom HH by A23,FUNCT_1:33;
A77: rng R c= dom HH by A69,FINSEQ_1:def 3;
f = HH " * HH * R by A74,RELAT_1:36
.= id(dom HH) * R by A23,FUNCT_1:39
.= R by A77,RELAT_1:53;
hence x in rng R by A75,A76,FINSEQ_1:def 3;
end;
hence thesis by TARSKI:def 3;
end;
then
A78: Seg(len HH) = rng R by A69,XBOOLE_0:def 10;
then
A79: R is one-to-one by A62,FINSEQ_4:60;
reconsider R as Function of Seg(len HH), Seg(len HH) by
FUNCT_2:1,A78,A65;
reconsider R as Permutation of Seg(len HH) by A78,A79,FUNCT_2:57;
A80: len h = len HH by RL2Def9;
then
A81: Seg len HH = dom h by FINSEQ_1:def 3;
then reconsider Hp = h * R as FinSequence of the carrier of V
by FINSEQ_2:47;
A82: len Hp = len GG by A64,A80,A81,FINSEQ_2:44;
deffunc Q(Nat)=g/.$1 + Hp/.$1;
consider I being FinSequence such that
A83: len I = len GG and
A84: for k be Nat st k in dom I holds I.k = Q(k) from FINSEQ_1:sch 2;
dom I = Seg len GG by A83,FINSEQ_1:def 3;
then
A85: for k be Element of NAT st k in Seg(len GG) holds I.k = Q(k) by A84;
rng I c= the carrier of V
proof
let x;
assume x in rng I;
then consider y such that
A86: y in dom I and
A87: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A86;
I.y = g/.y + Hp/.y by A84,A86;
hence thesis by A87;
end;
then reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A88: len Fp = len I by A41,A57,A58,A83,FINSEQ_2:44;
A89:
now
let x;
assume
A90: x in dom I;
then reconsider k = x as Element of NAT;
A91: x in dom Hp by A83,A82,A90,FINSEQ_3:29;
k in dom R by A64,A62,A83,A90,FINSEQ_1:def 3;
then
A92: R.k in dom R by A78,A62,FUNCT_1:def 3;
then reconsider j = R.k as Element of NAT by FINSEQ_3:23;
set v = GG/.k;
A93: R.k in dom HH by A60,A92,FINSEQ_3:29;
A94: x in dom GG by A83,A90,FINSEQ_3:29;
then HH.j = GG.k by A66
.= GG/.k by A94,PARTFUN1:def 6;
then
A95: h.j = L2.v * v by A93,RL2Th40;
k in dom P by A41,A33,A83,A90,FINSEQ_1:def 3;
then
A96: P.k in dom P by A55,A33,FUNCT_1:def 3;
then reconsider l = P.k as Element of NAT by FINSEQ_3:23;
A97: P.k in dom FF by A31,A96,FINSEQ_3:29;
x in dom Fp by A88,A90,FINSEQ_3:29;
then
A98: Fp.k = f.(P.k) by FUNCT_1:12;
k in dom Hp by A83,A82,A90,FINSEQ_3:29;
then
A99: Hp/.k = (h * R).k by PARTFUN1:def 6
.= h.(R.k) by A91,FUNCT_1:12;
A100: x in dom g by A83,A59,A90,FINSEQ_3:29;
FF.l = GG.k by A43,A94
.= GG/.k by A94,PARTFUN1:def 6;
then
A101: f.l = (L1 + L2).v * v by A97, RL2Th40
.= (L1.v + L2.v) * v by RL2Def12
.= L1.v * v + L2.v * v by ZMODUL01:def 3;
k in dom g by A83,A59,A90,FINSEQ_3:29;
then g/.k = g.k by PARTFUN1:def 6
.= L1.v * v by A100,RL2Def9;
hence I.x = Fp.x by A84,A90,A99,A95,A98,A101;
end;
dom h = Seg(len h) by FINSEQ_1:def 3;
then
A102: Sum(Hp) = Sum(h) by A80,RLVECT_2:7;
dom f = Seg(len f) by FINSEQ_1:def 3;
then
A103: Sum(Fp) = Sum(f) by A57,RLVECT_2:7;
dom I = Seg(len I) & dom Fp = Seg(len I) by A88,FINSEQ_1:def 3;
then
A104: I = Fp by A89,FUNCT_1:2;
Seg len GG = dom g by A59,FINSEQ_1:def 3;
hence thesis
by A3,A14,A20,A38,A30,A17,A103,A102,A83,A85,A82,A59,A104,RLVECT_2:2;
end;
theorem RL3Th2:
Sum(a * L) = a * Sum(L)
proof
per cases;
suppose
A1: a <> 0;
set l = a * L;
consider F such that
A2: F is one-to-one and
A3: rng F = Carrier(a * L) and
A4: Sum(a * L) = Sum ((a * L) (#) F) by RL2Def10;
set f = (a * L) (#) F;
consider G such that
A5: G is one-to-one and
A6: rng G = Carrier(L) and
A7: Sum(L) = Sum(L (#) G) by RL2Def10;
A8: len G = len F by A1,A2,A3,A5,A6,FINSEQ_1:48,RL2Th65;
deffunc Q(Nat) = F <- (G.$1);
consider P being FinSequence such that
A9: len P = len F and
A10: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A11: Carrier(l) = Carrier(L) by A1,RL2Th65;
A12: rng P c= Seg(len F)
proof
let x;
assume x in rng P;
then consider y such that
A13: y in dom P and
A14: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A13;
y in Seg(len F) by A9,A13,FINSEQ_1:def 3;
then y in dom G by A8,FINSEQ_1:def 3;
then G.y in rng F by A3,A6,A11,FUNCT_1:def 3;
then
A15: F just_once_values G.y by A2,FINSEQ_4:8;
P.y = F <- (G.y) by A10,A13;
then P.y in dom F by A15,FINSEQ_4:def 3;
hence thesis by A14,FINSEQ_1:def 3;
end;
A16:
now
let x;
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 A9,A8,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;
then P.x in Seg(len F) by A12;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A17: x in dom P and
P.x in dom F;
x in Seg(len P) by A17,FINSEQ_1:def 3;
hence x in dom G by A9,A8,FINSEQ_1:def 3;
end;
A18: dom P = Seg len F by A9,FINSEQ_1:def 3;
now
let x;
assume
A19: x in dom G;
then reconsider n = x as Element of NAT;
G.n in rng F by A3,A6,A11,A19,FUNCT_1:def 3;
then
A20: F just_once_values G.n by A2,FINSEQ_4:8;
n in Seg(len F) by A8,A19,FINSEQ_1:def 3;
then F.(P.n) = F.(F <- (G.n)) by A10,A18
.= G.n by A20,FINSEQ_4:def 3;
hence G.x = F.(P.x);
end;
then
A21: G = F * P by A16,FUNCT_1:10;
Seg(len F) c= rng P
proof
set f = F" * G;
now let x be set;
assume
A22: x in Seg(len F);
dom(F") = rng G by A2,A3,A6,A11,FUNCT_1:33;
then
A23: rng f = rng(F") by RELAT_1:28
.= dom F by A2,FUNCT_1:33;
A24: rng P c= dom F by A12,FINSEQ_1:def 3;
f = F " * F * P by A21,RELAT_1:36
.= id(dom F) * P by A2,FUNCT_1:39
.= P by A24,RELAT_1:53;
hence x in rng P by A22,A23,FINSEQ_1:def 3;
end;
hence thesis by TARSKI:def 3;
end;
then
A25: Seg(len F) = rng P by A12,XBOOLE_0:def 10;
A26: dom P = Seg(len F) by A9,FINSEQ_1:def 3;
then
A27: P is one-to-one by A25,FINSEQ_4:60;
reconsider P as Function of Seg(len F), Seg(len F)
by FUNCT_2:1,A25,A26;
reconsider P as Permutation of Seg(len F) by A25,A27,FUNCT_2:57;
A28: len f = len F by RL2Def9;
then
A29: dom f = Seg(len F) by FINSEQ_1:def 3;
then reconsider Fp = f * P as FinSequence of the carrier of V
by FINSEQ_2:47;
set g = L (#) G;
dom f = Seg(len f) by FINSEQ_1:def 3;
then
A30: Sum(Fp) = Sum(f) by A28,RLVECT_2:7;
A31: len Fp = len f by A29,FINSEQ_2:44;
then
A32: len Fp = len g by A8,A28,RL2Def9;
A33:
now
let k, v;
assume that
A34: k in dom g and
A35: v = g.k;
A36: k in Seg len F by A28,A31,A32,A34,FINSEQ_1:def 3;
A37: k in dom G by A8,A28,A31,A32,A34,FINSEQ_3:29;
then G.k in rng G by FUNCT_1:def 3;
then F just_once_values G.k by A2,A3,A6,A11,FINSEQ_4:8;
then
A38: F <- (G.k) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G.k) as Element of NAT;
i in Seg(len f) by A28,A38,FINSEQ_1:def 3;
then
A39: i in dom f by FINSEQ_1:def 3;
A40: k in dom P by A9,A28,A31,A32,A34,FINSEQ_3:29;
A41: G/.k = G.k by A37,PARTFUN1:def 6
.= F.(P.k) by A21,A40,FUNCT_1:13
.= F.i by A10,A18,A36
.= F/.i by A38,PARTFUN1:def 6;
thus Fp.k = f.(P.k) by A40,FUNCT_1:13
.= f.(F <- (G.k)) by A10,A18,A36
.= l.(F/.i) * F/.i by A39,RL2Def9
.= a * L.(F/.i) * F/.i by RL2Def13
.= a * (L.(F/.i) * F/.i) by ZMODUL01:def 4
.= a * v by A34,A35,A41,RL2Def9;
end;
dom Fp = dom g by A32,FINSEQ_3:29;
hence thesis by A4,A7,A30,A32,A33,ZMODUL01:12;
end;
suppose
A42: a = 0;
hence Sum(a * L) = Sum(Z_ZeroLC(V)) by RL2Th66
.= 0.V by RL2Lm1
.= a * Sum(L) by A42,ZMODUL01:1;
end;
end;
theorem RL3Th3:
Sum(- L) = - Sum(L)
proof
thus Sum(- L) = (- 1) * Sum(L) by RL3Th2
.= - Sum(L) by ZMODUL01:2;
end;
theorem
Sum(L1 - L2) = Sum(L1) - Sum(L2)
proof
thus Sum(L1 - L2) = Sum(L1) + Sum(- L2) by RL3Th1
.= Sum(L1) - Sum(L2) by RL3Th3;
end;
definition
let V,A;
attr A is linearly-independent means
:RL3Def1:
for l st Sum(l) = 0.V holds Carrier(l) = {};
end;
notation
let V,A;
antonym A is linearly-dependent for A 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 Z_Linear_Combination of A;
reconsider L = l as Z_Linear_Combination of B by A1,RL2Th33;
assume Sum(l) = 0.V;
then Carrier(L) = {} by A2,RL3Def1;
hence thesis;
end;
theorem RL3Th7:
A is linearly-independent implies not 0.V in A
proof
assume that
A1: A is linearly-independent and
A2: 0.V in A;
reconsider N1=1,N0=0 as Element of INT by INT_1:def 2;
deffunc F(Element of V) = N0;
consider f such that
A3: f.(0.V) = N1 and
A4: 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, INT) by FUNCT_2:8;
ex T st for v st not v in T holds f.v = 0
proof
take T = {0.V};
let v;
assume not v in T;
then v <> 0.V by TARSKI:def 1;
hence thesis by A4;
end;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
A5: Carrier(f) = {0.V}
proof
thus Carrier(f) c= {0.V}
proof
let x;
assume x in Carrier(f);
then consider v such that
A6: v = x and
A7: f.v <> N0;
v = 0.V by A4,A7;
hence thesis by A6,TARSKI:def 1;
end;
let x;
assume x in {0.V};
then x = 0.V by TARSKI:def 1;
hence thesis by A3;
end;
then Carrier(f) c= A by A2,ZFMISC_1:31;
then reconsider f as Z_Linear_Combination of A by RL2Def8;
Sum(f) = f.(0.V) * 0.V by A5,RL2Th53
.= 0.V by ZMODUL01:1;
hence contradiction by A1,A5,RL3Def1;
end;
theorem RL3Th8:
{}(the carrier of V) is linearly-independent
proof
let l be Z_Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by RL2Def8;
hence thesis;
end;
registration
let V;
cluster linearly-independent for Subset of V;
existence
proof
take {}(the carrier of V);
thus thesis by RL3Th8;
end;
end;
theorem
V is Mult-cancelable implies
({v} is linearly-independent iff v <> 0.V)
proof
assume AS0: V is Mult-cancelable;
thus {v} is linearly-independent implies v <> 0.V
proof
assume {v} is linearly-independent;
then not 0.V in {v} by RL3Th7;
hence thesis by TARSKI:def 1;
end;
assume
A1: v <> 0.V;
let l be Z_Linear_Combination of {v};
A2: Carrier(l) c= {v} by RL2Def8;
assume
A3: Sum(l) = 0.V;
now
per cases by A2,ZFMISC_1:33;
suppose
Carrier(l) = {};
hence thesis;
end;
suppose
A4: Carrier(l) = {v};
then
A5: 0.V = l.v * v by A3,RL2Th53;
now
assume v in Carrier(l);
then ex u st v = u & l.u <> 0;
hence contradiction by A1,A5,AS0,ZMODUL01:def 7;
end;
hence thesis by A4,TARSKI:def 1;
end;
end;
hence thesis;
end;
registration let V;
cluster {0.V} -> linearly-dependent for Subset of V;
coherence
proof 0.V in {0.V} by TARSKI:def 1;
hence thesis by RL3Th7;
end;
end;
theorem RL3Th11:
{v1,v2} is linearly-independent implies v1 <> 0.V
proof
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
assume {v1,v2} is linearly-independent;
hence thesis by A1,RL3Th7;
end;
theorem
{v,0.V} is linearly-dependent by RL3Th11;
theorem RL3Th13:
V is Mult-cancelable implies
(v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V &
for a, b st b <> 0 holds b * v1 <> a * v2 )
proof
assume AS0: V is Mult-cancelable;
thus v1 <> v2 & {v1,v2} is linearly-independent implies v2 <> 0.V &
for a, b st b <> 0 holds b * v1 <> a * v2
proof
reconsider N0=0,N1=-1 as Element of INT by INT_1:def 2;
deffunc F(Element of V)=N0;
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent;
thus v2 <> 0.V by A2,RL3Th11;
let a, b;
assume AS1: b <> 0;
reconsider Na= a as Element of INT by INT_1:def 2;
reconsider Nb=-b as Element of INT;
consider f such that
A3: f.v1 = Nb & f.v2 = Na and
A4: for v being Element of V st v <> v1 & v <> v2 holds f.v = F(v)
from FUNCT_2:sch 7(A1);
reconsider f as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
now
let v;
assume not v in {v1,v2};
then v <> v1 & v <> v2 by TARSKI:def 2;
hence f.v = 0 by A4;
end;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
Carrier(f) c= {v1,v2}
proof
let x;
assume x in Carrier(f);
then
A5: ex u st x = u & f.u <> 0;
assume not x in {v1,v2};
then x <> v1 & x <> v2 by TARSKI:def 2;
hence thesis by A4,A5;
end;
then reconsider f as Z_Linear_Combination of {v1,v2} by RL2Def8;
f.v1 <> 0 by A3,AS1;
then
A6: v1 in Carrier(f);
set w = a * v2;
assume A61: b * v1 = a * v2;
Sum(f) = Nb*v1 + Na*v2 by A1,A3,RL2Th51
.= b*(-v1)+ Na*v2 by ZMODUL01:5
.= (- w) + w by A61,ZMODUL01:6
.= - (w - w) by RLVECT_1:33
.= - 0.V by RLVECT_1:15
.= 0.V by RLVECT_1:12;
hence thesis by A2,A6,RL3Def1;
end;
assume
A7: v2 <> 0.V;
assume
A8: for a, b st b <> 0 holds b * v1 <> a * v2;
A9: 1 * v2 = v2 & 1 * v1 = v1 by ZMODUL01:def 5;
hence v1 <> v2 by A8;
let l be Z_Linear_Combination of {v1,v2};
assume that
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
A12: 0.V = l.v1 * v1 + l.v2 * v2 by A8,A9,A10,RL2Th51;
set x = the Element of Carrier(l);
Carrier(l) c= {v1,v2} by RL2Def8;
then
A13: x in {v1,v2} by A11,TARSKI:def 3;
x in Carrier(l) by A11;
then
A14: ex u st x = u & l.u <> 0;
now
per cases by A14,A13,TARSKI:def 2;
suppose
A15: l.v1 <> 0;
l.v1 * v1 = - (l.v2 * v2) by A12,RLVECT_1:6
.= (- 1) * (l.v2 * v2) by ZMODUL01:2
.=(-1)*(l.v2)*v2 by ZMODUL01:def 4;
hence thesis by A8,A15;
end;
suppose
A16: l.v2 <> 0 & l.v1 = 0;
0.V = l.v1 * v1 + l.v2 * v2 by A8,A9,A10,RL2Th51
.= 0.V + l.v2 * v2 by A16,ZMODUL01:1
.= l.v2 * v2 by RLVECT_1:4;
hence thesis by AS0,A7,A16,ZMODUL01:def 7;
end;
end;
hence thesis;
end;
theorem
V is Mult-cancelable implies
(v1 <> v2 & {v1,v2} is linearly-independent iff
for a,b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0)
proof
assume AS0: V is Mult-cancelable;
thus v1 <> v2 & {v1,v2} is linearly-independent implies
for a,b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0
proof
assume
A1: v1 <> v2 & {v1,v2} is linearly-independent;
let a, b;
assume that
A2: a * v1 + b * v2 = 0.V and
A3: a <> 0 or b <> 0;
now
per cases by A3;
suppose
A4: a <> 0;
a * v1 = - (b * v2) by A2,RLVECT_1:6
.= (- 1) * (b * v2) by ZMODUL01:2
.=(-1)*b*v2 by ZMODUL01:def 4;
hence thesis by AS0,A1,A4,RL3Th13;
end;
suppose
A5: b <> 0;
b * v2 = - (a * v1) by A2,RLVECT_1:6
.= (- 1) * (a * v1) by ZMODUL01:2
.=(-1)*a*v1 by ZMODUL01:def 4;
hence thesis by AS0,A1,A5,RL3Th13;
end;
end;
hence thesis;
end;
assume
A6: for a, b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0;
A7:
now
let a, b;
assume X1: b <> 0;
assume b*v1 = a * v2;
then b*v1 = 0.V + a * v2 by RLVECT_1:4;
then 0.V = b*v1 - a * v2 by RLSUB_2:61
.= b*v1 + a * (- v2) by ZMODUL01:6
.= b*v1 + (- a) * v2 by ZMODUL01:5;
hence contradiction by X1,A6;
end;
now
assume
A8: v2 = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0 * v1 + 0.V by ZMODUL01:1
.= 0 * v1 + 1 * v2 by A8,ZMODUL01:1;
hence contradiction by A6;
end;
hence thesis by A7,AS0,RL3Th13;
end;
definition
let V,A;
func Lin(A) -> strict Submodule of V means
:RL3Def2:
the carrier of it = {Sum(l) : not contradiction};
existence
proof
set A1 = {Sum(l) : not contradiction};
A1 c= the carrier of V
proof
let x;
assume x in A1;
then ex l st x = Sum(l);
hence thesis;
end;
then reconsider A1 as Subset of V;
reconsider l = Z_ZeroLC(V) as Z_Linear_Combination of A by RL2Th34;
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 Z_Linear_Combination of A such that
A4: v = Sum(l1) by A2;
consider l2 being Z_Linear_Combination of A such that
A5: u = Sum(l2) by A3;
reconsider f = l1 + l2 as Z_Linear_Combination of A
by RL2Th59;
v + u = Sum(f) by A4,A5,RL3Th1;
hence thesis;
end;
let a, v;
assume v in A1;
then consider l such that
A6: v = Sum(l);
reconsider f = a * l as Z_Linear_Combination of A by RL2Th67;
a * v = Sum(f) by A6,RL3Th2;
hence thesis;
end;
Sum(l) = 0.V by RL2Lm1;
then 0.V in A1;
hence thesis by A1,ZMODUL01:50;
end;
uniqueness by ZMODUL01:45;
end;
theorem RL3Th17:
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 {Sum(l) : not contradiction} by RL3Def2;
hence thesis;
end;
given k being Z_Linear_Combination of A such that
A1: x = Sum(k);
x in {Sum(l): not contradiction} by A1;
then x in the carrier of Lin(A) by RL3Def2;
hence thesis by STRUCT_0:def 5;
end;
theorem RL3Th18:
x in A implies x in Lin(A)
proof
reconsider N1=1, N0=0 as Element of INT by INT_1:def 2;
deffunc F(Element of V)=N0;
assume
A1: x in A;
then reconsider v = x as VECTOR of V;
consider f being Function of the carrier of V, INT such that
A2: f.v = N1 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, INT) by FUNCT_2:8;
ex T st for u st not u in T holds f.u = 0
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 Z_Linear_Combination of V by RL2Def5;
A4: Carrier(f) c= {v}
proof
let x;
assume x in Carrier(f);
then consider u such that
A5: x = u and
A6: f.u <> N0;
u = v by A3,A6;
hence thesis by A5,TARSKI:def 1;
end;
then reconsider f as Z_Linear_Combination of {v} by RL2Def8;
A7: Sum(f) = N1 * v by A2,RL2Th50
.= v by ZMODUL01:def 5;
{v} c= A by A1,ZFMISC_1:31;
then Carrier(f) c= A by A4,XBOOLE_1:1;
then reconsider f as Z_Linear_Combination of A by RL2Def8;
Sum(f) = v by A7;
hence thesis by RL3Th17;
end;
theorem RL3Lm2:
x in (0).V iff x = 0.V
proof
thus x in (0).V implies x = 0.V
proof
assume x in (0).V;
then x in the carrier of (0).V by STRUCT_0:def 5;
then x in {0.V} by ZMODUL01:def 10;
hence thesis by TARSKI:def 1;
end;
thus thesis by ZMODUL01:33;
end;
reserve l0 for Z_Linear_Combination of {}(the carrier of V);
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 = {Sum (l0) : not contradiction} by RL3Def2;
then ex l0 st v = Sum(l0) by A1;
then v = 0.V by RL2Th49;
hence thesis by RL3Lm2;
end;
assume v in (0).V;
then v = 0.V by RL3Lm2;
hence v in A by ZMODUL01:33;
end;
hence thesis by ZMODUL01:46;
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;
assume x in A;
then x in Lin(A) by RL3Th18;
then x = 0.V by A1,RL3Lm2;
hence thesis by TARSKI:def 1;
end;
set y = the Element of A;
let x;
assume x in {0.V};
then
A3: x = 0.V by TARSKI:def 1;
y in A & y in Lin(A) by A2,RL3Th18;
hence thesis by A1,A3,RL3Lm2;
end;
theorem
for V being strict Z_Module,A being Subset of V holds
A = the carrier of V implies Lin(A) = V
proof
let V be strict Z_Module,A be Subset of V;
assume A = the carrier of V;
then for v being VECTOR of V holds
v in Lin(A) iff v in (Omega).V by STRUCT_0:def 5,RL3Th18;
hence thesis by ZMODUL01:46;
end;
RL3Lm4: W1 is Submodule of W2 & W1 is Submodule of W3
implies W1 is Submodule of W2 /\ W3
proof
assume
A1: W1 is Submodule of W2 & W1 is Submodule of W3;
now
let v;
assume v in W1;
then v in W2 & v in W3 by A1,ZMODUL01:23;
hence v in W2 /\ W3 by ZMODUL01:94;
end;
hence thesis by ZMODUL01:44;
end;
RL3Lm6: W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
Submodule of W3
proof
assume
A1: W1 is Submodule of W3 & W2 is Submodule of W3;
now
let v;
assume v in W1 + W2;
then consider v1,v2 such that
A2: v1 in W1 & v2 in W2 and
A3: v = v1 + v2 by ZMODUL01:92;
v1 in W3 & v2 in W3 by A1,A2,ZMODUL01:23;
hence v in W3 by A3,ZMODUL01:36;
end;
hence thesis by ZMODUL01:44;
end;
theorem RL3Th23:
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 RL3Th17;
reconsider l as Z_Linear_Combination of B by A1,RL2Th33;
Sum(l) = v by A2;
hence v in Lin(B) by RL3Th17;
end;
hence thesis by ZMODUL01:44;
end;
theorem
for V being strict Z_Module,A,B being Subset of V holds
Lin(A) = V & A c= B implies Lin(B) = V
proof
let V be strict Z_Module,A,B be Subset of V;
assume Lin(A) = V & A c= B;
then V is Submodule of Lin(B) by RL3Th23;
hence thesis by ZMODUL01:41;
end;
theorem
Lin(A \/ B) = Lin(A) + Lin(B)
proof
now
deffunc G(set)= 0;
let v;
assume v in Lin(A \/ B);
then consider l being Z_Linear_Combination of A \/ B such that
A1: v = Sum(l) by RL3Th17;
deffunc F(set)=l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred P[set] means $1 in C;
defpred D[set] means $1 in D;
A2: for x st x in the carrier of V holds (P[x] implies F(x) in INT) &
(not P[x] implies G(x) in INT) by INT_1:def 2;
consider f being Function of the carrier of V, INT such that
A3: for x 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, INT) by FUNCT_2:8;
for u holds not u in C implies f.u = 0 by A3;
then reconsider f as Z_Linear_Combination of V by RL2Def5;
A4: Carrier(f) c= C
proof
let x;
assume x in Carrier(f);
then
A5: ex u st x = u & f.u <> 0;
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,XBOOLE_1:1;
then reconsider f as Z_Linear_Combination of A by RL2Def8;
A6: for x st x in the carrier of V holds (D[x] implies F(x) in INT) &
(not D[x] implies G(x) in INT) by INT_1:def 2;
consider g being Function of the carrier of V, INT such that
A7: for x st x in the carrier of V holds (D[x] implies g.x = F(x)) &
(not D[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, INT) by FUNCT_2:8;
for u holds not u in D implies g.u = 0 by A7;
then reconsider g as Z_Linear_Combination of V by RL2Def5;
A8: D c= B
proof
let x;
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 RL2Def8;
hence thesis by A9,XBOOLE_0:def 3;
end;
Carrier(g) c= D
proof
let x;
assume x in Carrier(g);
then
A10: ex u st x = u & g.u <> 0;
assume not x in D;
hence thesis by A7,A10;
end;
then Carrier(g) c= B by A8,XBOOLE_1:1;
then reconsider g as Z_Linear_Combination of B by RL2Def8;
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;
B1: g.v = 0 by A7,A12;
thus (f + g).v = f.v + g.v by RL2Def12
.= l.v by A3,A11,B1;
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;
B2: f.v = 0 by A3,A13;
thus (f + g). v = f.v + g.v by RL2Def12
.= l.v by A7,A15,B2;
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;
B4: g.v = 0 by A7,A17;
thus (f + g).v = f.v + g.v by RL2Def12
.= 0 by A3,A18,B4
.= l.v by A16;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A19: v = Sum(f) + Sum(g) by A1,RL3Th1;
Sum(f) in Lin(A) & Sum(g) in Lin(B) by RL3Th17;
hence v in Lin(A) + Lin(B) by A19,ZMODUL01:92;
end;
then
A20: Lin(A \/ B) is Submodule of Lin(A) + Lin(B) by ZMODUL01:44;
Lin(A) is Submodule of Lin(A \/ B)
& Lin(B) is Submodule of Lin(A \/ B) by RL3Th23,XBOOLE_1:7;
then Lin(A) + Lin(B) is Submodule of Lin(A \/ B) by RL3Lm6;
hence thesis by A20,ZMODUL01:41;
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 RL3Th23,XBOOLE_1:17;
hence thesis by RL3Lm4;
end;
begin :: 4. Theorems related to submodule
theorem
W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3
proof
A1: W1 /\ W2 is Submodule of W1 by ZMODUL01:105;
assume W1 is Submodule of W3;
hence thesis by A1,ZMODUL01:42;
end;
theorem
W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of
W2 /\ W3 by RL3Lm4;
theorem
W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
Submodule of W3 by RL3Lm6;
theorem
W1 is Submodule of W2 implies W1 is Submodule of W2 + W3
proof
A1: W2 is Submodule of W2 + W3 by ZMODUL01:97;
assume W1 is Submodule of W2;
hence thesis by A1,ZMODUL01:42;
end;