:: Quotient Module of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 7, 2012
:: Copyright (c) 2012-2014 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, ARYTM_3, CARD_3, ORDINAL4, XXREAL_0, TARSKI,
CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1,
QC_LANG1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL02,
RLVECT_3, RMOD_2, INT_3, VECTSP_1, VECTSP_2, LOPBAN_1, MESFUNC1,
REALSET1, RSSPACE, MONOID_0, SETFAM_1, VECTSP10, EC_PF_1, INT_2,
ORDINAL1;
notations TARSKI, XBOOLE_0, ENUMSET1, 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, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2,
REALSET1, FINSEQ_1, VALUED_1, FINSEQ_4, STRUCT_0, ALGSTR_0,
RLVECT_1, VECTSP_1, RLVECT_2, INT_3, EC_PF_1, GROUP_1, VFUNCT_1,
VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, ZMODUL01;
constructors BINOP_2, FINSEQ_4, RELSET_1, RLVECT_2, ZMODUL01, VECTSP_4,
REALSET1, FUNCT_7, INT_3, NAT_D, GCD_1, VECTSP10, ALGSTR_1, VECTSP_6,
BINOP_1, VECTSP_7, VECTSP_5, PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0,
NAT_1, MEMBERED, VFUNCT_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, XCMPLX_0, ORDINAL1,
VECTSP_4, VECTSP_7, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, XBOOLE_0, RLVECT_1, FUNCT_2, ALGSTR_0, VECTSP_1,
ZMODUL01, BINOP_1, TARSKI, VECTSP_4, VECTSP_6, VECTSP_7;
equalities XBOOLE_0, RELAT_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, REALSET1,
ZMODUL01, BINOP_1, VECTSP_4, VECTSP_6;
expansions FUNCT_1, XBOOLE_0, RLVECT_1, FUNCT_2, STRUCT_0, ALGSTR_0, ZMODUL01,
BINOP_1, TARSKI, VECTSP_4, VECTSP_6;
theorems FUNCT_1, FUNCT_2, INT_1, RLSUB_2, RLVECT_1, TARSKI, ZMODUL01,
RLVECT_2, ZFMISC_1, RELAT_1, VECTSP_1, ALGSTR_0, EULER_1, EULER_2,
EC_PF_1, VECTSP_4, VECTSP_6, NUMBERS, INT_2, MOD_3, VECTSP_7;
schemes BINOP_1, FUNCT_2, 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 sequence of V;
definition
let V be Z_Module;
let a be Element of INT.Ring;
func a * V -> non empty Subset of V equals
the set of all a * v where v is Element of V;
correctness
proof
set S = the set of all a * v where v is Element of V;
A1: now let x be object;
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 A1,TARSKI:def 3;
end;
end;
definition
let V be Z_Module;
let a be Element of INT.Ring;
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 Element of INT.Ring;
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
A1: dom adds = [:a*V,a*V:] by RELAT_1:62;
for z be object st z in [:a*V,a*V:] holds adds.z in a*V
proof
let z be object such that
A2:z in [:a*V,a*V:];
consider x,y be object such that
A3:(x in a*V) & y in a*V & z = [x,y] by A2,ZFMISC_1:def 2;
consider v be Element of V such that
A4: x =a*v by A3;
consider w be Element of V such that
A5: y =a*w by A3;
adds.z = a*v+a*w by A2,A3,A4,A5,FUNCT_1:49
.= a*(v+w) by VECTSP_1:def 14;
hence adds.z in a*V;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let V be Z_Module;
let a be Element of INT.Ring;
func Mult_(a,V) -> Function of [:the carrier of INT.Ring,a*V :], a*V
equals
(the lmult of V) | [:INT,a*V:];
correctness
proof
set scmult = (the lmult 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 lmult of V) by FUNCT_2:def 1;
then
A1: dom scmult = [:INT,a*V:] by RELAT_1:62;
for z be object st z in [:INT,a*V:] holds scmult.z in a*V
proof
let z be object such that
A2:z in [:INT,a*V:];
consider x,y be object such that
A3:x in INT & y in a*V & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider i=x as Element of INT.Ring by A3;
consider v be Element of V such that
A4: y =a*v by A3;
scmult.z = i*(a*v) by A2,A3,A4,FUNCT_1:49
.= (i*a)*v by VECTSP_1:def 16
.= (a*i)*v
.= a*(i*v) by VECTSP_1:def 16;
hence scmult.z in a*V;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let V be Z_Module;
let a be Element of INT.Ring;
func a (*) V -> Submodule of V equals
ModuleStr (# a * V, Add_(a,V), Zero_(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);
Z0 = 0.V & AV1 = (the addF of V) ||V1
& MV1 = (the lmult of V) | [:the carrier of INT.Ring,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
the set of all A where A is Coset of W;
correctness
proof
set C = the set of all A where A is Coset of W;
A1: C c= bool the carrier of V
proof
let x be object;
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
:Def7:
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 VECTSP_4:def 6;
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 VECTSP_4:def 6;
reconsider z = (a+b) + W as Coset of W by VECTSP_4:def 6;
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 VECTSP_4:def 6;
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 VECTSP_4:def 6;
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;
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 VECTSP_4:def 6;
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 [:the carrier of INT.Ring,
CosetSet(V,W):], CosetSet(V,W) means
:Def9:
for z be Element of INT.Ring, 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.Ring, set, set] means for a be VECTOR of V
st $2 = a + W holds $3 = $1*a+W;
set cF = the carrier of INT.Ring;
set C = CosetSet(V,W);
A1:
now
let z be Element of INT.Ring;
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 VECTSP_4:def 6;
reconsider c = z*a + W as Coset of W by VECTSP_4:def 6;
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,VECTSP_1:def 14,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.Ring
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.Ring, A be Element of C, a be VECTOR of V;
assume
A7: A = a + W;
P[z,A, f.(z,A)] by A6;
hence thesis by A7;
end;
uniqueness
proof
set cF = the carrier of INT.Ring;
set C = CosetSet(V,W);
let f1,f2 be Function of [:cF, C:], C such that
A8: for z be Element of INT.Ring, 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
A9: for z be Element of INT.Ring, 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.Ring;
let A be Element of CosetSet(V,W);
A in C;
then consider A1 be Coset of W such that
A10: A1=A;
consider a be VECTOR of V such that
A11: A1 = a+W by VECTSP_4:def 6;
thus f1.(z,A) = z*a + W by A8,A10,A11
.= f2.(z,A) by A9,A10,A11;
end;
hence thesis;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func Z_ModuleQuot(V,W) -> strict Z_Module means
:Def10:
the carrier of it = CosetSet(V,W) &
the addF of it = addCoset(V,W) &
0.it = zeroCoset(V,W) &
the lmult 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 = ModuleStr (# C, aC, zC, 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 VECTSP_4:def 6;
0.A = 0.V + W by ZMODUL01:59;
hence A1 + 0.A = (a+0.V) +W by A2,A3,Def7
.= 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 VECTSP_4:def 6;
set A2 = -a+ W;
A2 is Coset of W by VECTSP_4:def 6;
then A2 in C;
then reconsider A2 as Element of A;
take A2;
thus A1 + A2 = (a+-a) +W by A6,A7,Def7
.= 0.A by A5,RLVECT_1:5;
end;
A8: now
let x,y be Element of INT.Ring;
let A1,A2 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A9: A1=aa;
A2 in C;
then consider bb be Coset of W such that
A10: A2=bb;
consider b be VECTOR of V such that
A11: bb = b+W by VECTSP_4:def 6;
A12: lC.(x,A2) = x*A2 & lC.(x,A2) =x*b+W by A10,A11,Def9;
consider a be VECTOR of V such that
A13: aa = a+W by VECTSP_4:def 6;
A14: aC.(A1,A2) =a+b+W by A9,A10,A13,A11,Def7;
A15: lC.(x,A1) =x*a+W by A9,A13,Def9;
thus x*(A1+A2) = x*(a+b) +W by A14,Def9
.= x*a+x*b +W by VECTSP_1:def 14
.= x*A1+x*A2 by A15,A12,Def7;
A16: lC.(y,A1) =y*a+W by A9,A13,Def9;
thus (x+y)*A1 = (x+y)*a +W by A9,A13,Def9
.= x*a + y*a + W by VECTSP_1:def 15
.= x*A1+y*A1 by A15,A16,Def7;
thus (x*y)*A1 = (x*y)*a +W by A9,A13,Def9
.= x*(y*a) +W by VECTSP_1:def 16
.=x*(y*A1) by A16,Def9;
thus (1.INT.Ring)*A1 = (1.INT.Ring)*a +W by A9,A13,Def9
.= A1 by A9,A13,VECTSP_1:def 17;
end;
A17: A is Abelian
proof
let A1,A2 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A18: A1=aa;
consider a be VECTOR of V such that
A19: aa = a+W by VECTSP_4:def 6;
A2 in C;
then consider bb be Coset of W such that
A20: A2=bb;
consider b be VECTOR of V such that
A21: bb = b+W by VECTSP_4:def 6;
thus A1+A2 = (a+b) +W by A18,A20,A19,A21,Def7
.= A2+A1 by A18,A20,A19,A21,Def7;
end;
Z1: 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
A22: A1=aa;
consider a be VECTOR of V such that
A23: aa = a+W by VECTSP_4:def 6;
A2 in C;
then consider bb be Coset of W such that
A24: A2=bb;
consider b be VECTOR of V such that
A25: bb = b+W by VECTSP_4:def 6;
A3 in C;
then consider cc be Coset of W such that
A26: A3=cc;
consider c be VECTOR of V such that
A27: cc = c+W by VECTSP_4:def 6;
A28: aC.(A2,A3) =b+c+W by A24,A26,A25,A27,Def7;
aC.(A1,A2) =a+b+W by A22,A24,A23,A25,Def7;
hence A1+A2 + A3 = a+b+c +W by A26,A27,Def7
.= a+(b+c) +W by RLVECT_1:def 3
.= A1+(A2+A3) by A22,A23,A28,Def7;
end;
reconsider A as strict Z_Module
by A17,A1,A4,A8,VECTSP_1:def 14,def 15,def 17,def 16,Z1;
take A;
thus thesis;
end;
uniqueness;
end;
theorem Th1:
for p be Element of INT.Ring, 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 Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of Z_ModuleQuot(V, W) such that
A1: W = p (*) V;
A2: x is Element of CosetSet(V,W) by Def10;
then x in the set of all A where A is Coset of W;
then consider xx be Coset of W such that
A3: xx = x;
consider v be VECTOR of V such that
A4: xx = v + W by VECTSP_4:def 6;
p * v in the carrier of W by A1;
then A5: p * v in W;
thus p * x = lmultCoset(V,W).(p, x) by Def10
.= (p * v) + W by A2,A3,A4,Def9
.= zeroCoset(V,W) by A5,ZMODUL01:63
.= 0.Z_ModuleQuot(V, W) by Def10;
end;
theorem Th2:
for p, i be Element of INT.Ring, 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 Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of Z_ModuleQuot(V, W) such that
A1: p <> 0 and
A2: W = p (*) V;
consider j be Element of INT.Ring such that
A3: j = i div p;
thus i * x = (j*p + (i mod p)) * x by A1,A3,INT_1:59
.= (j*p) * x + (i mod p) * x by VECTSP_1:def 15
.= j * (p*x) + (i mod p) * x by VECTSP_1:def 16
.= 0.Z_ModuleQuot(V, W) + (i mod p) * x by A2,Th1,ZMODUL01:1
.= (i mod p) * x by RLVECT_1:4;
end;
Lem1: for i being Integer holds
i in the carrier of INT.Ring
proof
let i be Integer;
i in INT by INT_1:def 2;
hence thesis;
end;
theorem
for p, q be Element of INT.Ring, 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_coprime
holds q * v = 0.V implies v + W = 0.Z_ModuleQuot(V, W)
proof
let p, q be Element of INT.Ring, V be Z_Module, W be Submodule of V,
v be VECTOR of V such that
A1: W = p (*) V and
A2: p > 1 & q > 1 & p,q are_coprime;
v + W is Coset of W by VECTSP_4:def 6;
then v + W in CosetSet(V,W);
then reconsider x = v + W as VECTOR of Z_ModuleQuot(V, W) by Def10;
p in NAT & q in NAT by A2,INT_1:3;
then reconsider pp=p, qq=q as Nat;
consider i, j be Integer such that
A3: i*pp + j*qq = 1 by A2,EULER_1:10;
a3: i*pp + j*qq = 1.INT.Ring by A3;
reconsider i, j as Element of INT.Ring by Lem1;
assume A4: q * v = 0.V;
A5: x is Element of CosetSet(V,W) by Def10;
A6: q * x = lmultCoset(V,W).(q,x) by Def10
.= 0.V + W by A4,A5,Def9
.= zeroCoset(V,W) by ZMODUL01:59
.= 0.Z_ModuleQuot(V, W) by Def10;
(i*p + j*q) * x = (i*p) * x + (j*q) * x by VECTSP_1:def 15
.= (i*p) * x + j * (q*x) by VECTSP_1:def 16
.= (i*p) * x + 0.Z_ModuleQuot(V, W) by A6,ZMODUL01:1
.= (i*p) * x by RLVECT_1:4
.= i * (p*x) by VECTSP_1:def 16
.= 0.Z_ModuleQuot(V, W) by A1,Th1,ZMODUL01:1;
hence 0.Z_ModuleQuot(V, W) = v + W by VECTSP_1:def 17,a3;
end;
registration
cluster -> integer for Element of INT.Ring;
coherence;
end;
registration
cluster prime for Element of INT.Ring;
existence
proof
2 in INT by NUMBERS:17; then
reconsider p = 2 as Element of INT.Ring;
take p;
p is prime by INT_2:28;
hence thesis;
end;
end;
registration
cluster prime -> natural for integer Number;
coherence
proof
let p be integer Number;
assume p is prime; then
p > 1 by INT_2:def 4; then
p >= 0; then
p in NAT by INT_1:3;
hence thesis;
end;
end;
definition
let p be prime Element of INT.Ring;
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
:Def11:
for a being Element of GF(p), i being Element of INT.Ring,
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 Element of INT.Ring st $1 = i mod p holds
$3 = (i mod p) * $2;
A1: 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
A2: a = i mod p by EC_PF_1:13;
i in INT by INT_1:def 2; then
reconsider i as Element of INT.Ring;
reconsider z = (i mod p) * x as Element of Z_ModuleQuot(V,p(*)V);
P[a,x,z] by A2;
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
A3: 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(A1);
take f;
thus thesis by A3;
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
A4: for a being Element of GF(p), i being Element of INT.Ring,
x being Element of Z_ModuleQuot(V,p(*)V) st a = i mod p
holds f1.(a,x) = (i mod p) * x;
assume
A5: for a being Element of GF(p), i being Element of INT.Ring,
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 A6: 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 A6;
consider i be Nat such that
A7: a0 = i mod p by EC_PF_1:13;
reconsider i as Element of INT.Ring by Lem1;
thus f1.(a,x) = (i mod p) * x0 by A4,A7
.= f2.(a,x) by A5,A7;
end;
end;
definition
let p be prime Element of INT.Ring, V be Z_Module;
func Z_MQ_VectSp(V,p) -> non empty strict ModuleStr over GF(p) equals
ModuleStr (# 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 Element of INT.Ring, 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 Element of INT.Ring by Lem1;
consider j be Nat such that
A2: y = j mod p by EC_PF_1:13;
reconsider j as Element of INT.Ring by Lem1;
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;
A4: x * v = (i mod p)*v1 by Def11,A1;
A5: y * v = (j mod p)*v1 by Def11,A2;
(((i mod p) + (j mod p)) mod p)*v1
= ((i mod p) + (j mod p))*v1 by Th2
.= (i mod p)*v1 + (j mod p)*v1 by VECTSP_1:def 15;
hence thesis by A3,A4,A5,Def11;
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
A6: x = i mod p by EC_PF_1:13;
reconsider i as Element of INT.Ring by Lem1;
reconsider v1=v,w1=w as Element of Z_ModuleQuot(V,p(*)V);
A7: x * w = (i mod p)*w1 by Def11,A6;
thus x * (v + w) =(i mod p)*(v1 + w1) by Def11,A6
.=(i mod p)*v1 + (i mod p)*w1 by VECTSP_1:def 14
.=(x * v) + (x * w) by A6,A7,Def11;
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
A8: x = i mod p by EC_PF_1:13;
reconsider i as Element of INT.Ring by Lem1;
consider j be Nat such that
A9: y = j mod p by EC_PF_1:13;
reconsider j as Element of INT.Ring by Lem1;
reconsider v1=v as Element of Z_ModuleQuot(V,p(*)V);
A10: x*y = (i * j) mod p by A8,A9,EC_PF_1:18;
A11: y * v = (j mod p)*v1 by Def11,A9;
A12: x * (y * v) = (i mod p)*((j mod p)*v1) by A8,A11,Def11;
((i * j) mod p)*v1 = (i*j)*v1 by Th2
.= i*(j*v1) by VECTSP_1:def 16
.= i*((j mod p)*v1) by Th2
.= (i mod p)*((j mod p)*v1) by Th2;
hence thesis by A10,A12,Def11;
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
A13: 1.F = i mod p by EC_PF_1:13;
reconsider i as Element of INT.Ring by Lem1;
thus (1.F)*v = (i mod p)*v1 by Def11,A13
.= 1.INT.Ring * v1 by A13,EC_PF_1:12
.= v by VECTSP_1:def 17;
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 Element of INT.Ring, 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 VECTSP_4:def 6;
then vq in the set of all A where A is Coset of p(*)V;
then vq is Element of CosetSet(V,p(*)V);
hence thesis by Def10;
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 lmult of X;
correctness;
end;
definition
let X be Z_Module;
func modetrans(X) -> non empty strict ModuleStr over INT.Ring equals
ModuleStr (#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 = ModuleStr (# X0, ADD,Z0,LMLT #);
A1: XP is vector-distributive
proof
let x be Scalar of INT.Ring;
let v,w be Element of XP;
set x1=x;
reconsider v1=v, w1=w as Element of X;
thus x*(v+w)=x1*(v1+w1)
.= x1*v1+x1*w1 by VECTSP_1:def 14
.= x*v+x*w;
end;
A2: XP is scalar-distributive
proof
let x,y be Scalar of INT.Ring;
let v be Element of XP;
set x1=x, y1=y;
reconsider v1=v as Element of X;
thus (x+y)*v=(x1+y1)*v1
.=x1*v1+y1*v1 by VECTSP_1:def 15
.= x*v+y*v;
end;
A3: XP is scalar-associative
proof
let x,y be Scalar of INT.Ring;
let v be Element of XP;
set x1=x, y1=y;
reconsider v1=v as Element of X;
thus (x*y)*v =(x1*y1)*v1
.= x1*(y1*v1) by VECTSP_1:def 16
.= x*(y*v);
end;
A4: XP is scalar-unital
proof
let v be Element of XP;
reconsider v1=v as Element of X;
thus (1.(INT.Ring))*v = (1.(INT.Ring))*v1 .= v1 by VECTSP_1:def 17
.= v;
end;
A5:
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;
A6:
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;
A7:
now let v be Element of XP;
reconsider v1=v as Element of X;
consider w1 be Element of X such that
A8: v1+w1= 0.X by ALGSTR_0:def 11;
reconsider w=w1 as Element of XP;
v + w = 0.XP by A8;
hence v is right_complementable;
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 A1,A2,A3,A4,A5,A6,A7;
end;
end;
definition
let X be LeftMod of INT.Ring;
func Mult_INT*(X) -> Function of
[:the carrier of INT.Ring,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 ModuleStr over INT.Ring equals
ModuleStr (#the carrier of X, the addF of X, the ZeroF 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 = ModuleStr (# X0, ADD, Z0, 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 Element of INT.Ring, v be Vector of XQ;
reconsider vd = v as Element of X;
reconsider ad=a,bd=b as Scalar of INT.Ring;
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 Element of INT.Ring, v,w be Vector of XQ;
reconsider ad=a as Element of INT.Ring;
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 Element of INT.Ring, v be Vector of XQ;
reconsider vd = v as Element of X;
reconsider ad=a,bd=b as Scalar of INT.Ring;
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.INT.Ring) * v = 1.(INT.Ring) *vd
.= v by VECTSP_1:def 17;
end;
hence thesis;
end;
end;
::$CT 4
begin :: 2. Linear combination of Z-module
definition
::$CD 6
end;
reserve K,L,L1,L2,L3 for Linear_Combination of V;
theorem
for V be Z_Module, L be Linear_Combination of V,
v be Element of V holds L.v = 0.INT.Ring iff not v in Carrier(L)
proof
let V be Z_Module,
L be Linear_Combination of V, v be Element of V;
thus L.v = 0.INT.Ring implies not v in Carrier(L)
proof
assume
A1: L.v = 0.INT.Ring;
assume not thesis;
then ex u be Element of V st u = v & L.u <> 0.INT.Ring;
hence thesis by A1;
end;
assume not v in Carrier(L);
hence thesis;
end;
theorem
for V be Z_Module, v be Element of V holds (ZeroLC(V)).v = 0.INT.Ring
proof
let V be Z_Module, v be Element of V;
Carrier (ZeroLC(V)) = {} & not v in {} by VECTSP_6:def 3;
hence thesis;
end;
reserve a, b for Element of INT.Ring;
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 V, INT.Ring,
i for Element of NAT;
reserve l, l1, l2 for Linear_Combination of A;
theorem
A c= B implies l is Linear_Combination of B by VECTSP_6:4;
theorem Th11:
ZeroLC(V) is Linear_Combination of A by VECTSP_6:5;
theorem
for l being Linear_Combination of {}the carrier of V holds l = ZeroLC(V)
by VECTSP_6:6;
theorem
i in dom F & v = F.i implies (f (#) F).i = f.v * v
by VECTSP_6:8;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V) by VECTSP_6:9;
theorem
f (#) <* v *> = <* f.v * v *> by VECTSP_6:10;
theorem
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *> by VECTSP_6:11;
theorem
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *> by VECTSP_6:12;
theorem
A <> {} & A is linearly-closed iff for l holds Sum(l) in A
proof
0.INT.Ring <> 1.INT.Ring; then
(A <> {} & A is linearly-closed iff for l holds Sum(l) in A)
by VECTSP_6:14;
hence thesis;
end;
theorem
Sum(ZeroLC(V)) = 0.V by VECTSP_6:15;
theorem
for l being Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V
by VECTSP_6:16;
theorem
for l being Linear_Combination of {v} holds Sum(l) = l.v * v
by VECTSP_6:17;
theorem Th22:
v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
Sum(l) = l.v1 * v1 + l.v2 * v2 by VECTSP_6:18;
theorem
Carrier(L) = {} implies Sum(L) = 0.V by VECTSP_6:19;
theorem Th24:
Carrier(L) = {v} implies Sum(L) = L.v * v by VECTSP_6:20;
theorem
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2
by VECTSP_6:21;
definition
::$CD 3
end;
theorem
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by VECTSP_6:23;
theorem Th27:
L1 is Linear_Combination of A & L2 is Linear_Combination of A
implies L1 + L2 is Linear_Combination of A by VECTSP_6:24;
theorem Th28:
L1 + (L2 + L3) = L1 + L2 + L3 by VECTSP_6:26;
registration let V,L;
reduce L + ZeroLC(V) to L;
reducibility by VECTSP_6:27;
end;
theorem
a <> 0.INT.Ring implies Carrier(a * L) = Carrier(L)
proof
set T = {u : (a * L).u <> 0.INT.Ring};
set S = {v : L.v <> 0.INT.Ring};
assume
A1: a <> 0.INT.Ring;
T = S
proof
thus T c= S
proof
let x be object;
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 VECTSP_6:def 9;
then L.u <> 0 by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v such that
A4: x = v and
A5: L.v <> 0.INT.Ring;
(a * L).v = a * L.v by VECTSP_6:def 9;
then (a * L).v <> 0.INT.Ring by A1,A5;
hence thesis by A4;
end;
hence thesis;
end;
theorem
0.INT.Ring * L = ZeroLC(V) by VECTSP_6:30;
theorem Th31:
L is Linear_Combination of A implies a * L is Linear_Combination of A
by VECTSP_6:31;
theorem Th32:
(a + b) * L = a * L + b * L by VECTSP_6:32;
theorem Th33:
a * (L1 + L2) = a * L1 + a * L2 by VECTSP_6:33;
theorem Th34:
a * (b * L) = (a * b) * L by VECTSP_6:34;
registration let V,L;
reduce (1.INT.Ring)*L to L;
reducibility by VECTSP_6:35;
end;
definition
::$CD 2
end;
theorem
(- L).v = - L.v by VECTSP_6:36;
theorem
L1 + L2 = ZeroLC(V) implies L2 = - L1 by VECTSP_6:37;
theorem
Carrier(- L) = Carrier(L) by VECTSP_6:38;
theorem
L is Linear_Combination of A
implies - L is Linear_Combination of A by VECTSP_6:39;
theorem
(L1 - L2).v = L1.v - L2.v by VECTSP_6:40;
theorem
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2) by VECTSP_6:41;
theorem
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A by VECTSP_6:42;
theorem Th42:
L - L = ZeroLC(V) by VECTSP_6:43;
definition
let V;
func LinComb(V) -> set means
:Def29:
x in it iff x is Linear_Combination of V;
existence
proof
defpred P[object] means $1 is Linear_Combination of V;
consider A being set such that
A1: for x being object
holds x in A iff x in Funcs(the carrier of V, the carrier of INT.Ring) & P[x]
from XBOOLE_0:sch 1;
take A;
let x;
thus x in A implies x is Linear_Combination of V by A1;
assume x is 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 Linear_Combination of V;
assume
A3: for x holds x in D2 iff x is Linear_Combination of V;
thus D1 c= D2
proof
let x be object;
assume x in D1;
then x is Linear_Combination of V by A2;
hence thesis by A3;
end;
let x be object;
assume x in D2;
then x is 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 Linear_Combination of V;
x in LinComb V by Def29;
hence thesis;
end;
end;
reserve e, e1, e2 for Element of LinComb(V);
definition
let V, e;
func @e -> Linear_Combination of V equals
e;
coherence by Def29;
end;
definition
let V, L;
func @L -> Element of LinComb(V) equals
L;
coherence by Def29;
end;
definition
let V;
func LCAdd(V) -> BinOp of LinComb(V) means
:Def32:
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;
end;
end;
definition
let V;
func LCMult(V) -> Function of [:the carrier of INT.Ring,LinComb(V):],
LinComb(V) means :Def33:
for a, e holds it. [a,e] = a * @e;
existence
proof
defpred P[Element of INT.Ring,Element of LinComb(V),set] means
ex a st a = $1 & $3 = a * @$2;
A1: for x being (Element of INT.Ring), e1 ex e2 st P[x,e1,e2]
proof
let x be (Element of INT.Ring), e1;
take @(x * @e1);
take x;
thus thesis;
end;
consider g being Function of [:the carrier of INT.Ring,
LinComb(V):], LinComb(V) such that
A2: for x being (Element of INT.Ring), 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;
ex b st b = a0 & g.(a0,e) = b * @e by A2;
hence thesis;
end;
uniqueness
proof
let g1, g2 be Function of [:the carrier of INT.Ring,
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.Ring), e;
thus g1.(x,e) = x * @e by A3
.= g2.(x,e) by A4;
end;
hence thesis;
end;
end;
definition let V;
func LC_Z_Module V -> ModuleStr over INT.Ring equals
ModuleStr (# LinComb(V), LCAdd(V), @ZeroLC(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,Def32;
end;
thus S is Abelian
proof
let u, v be Element of S;
reconsider K = u, L = v as Linear_Combination of V by Def29;
thus u + v = K + L by A1 .= L + K by VECTSP_6:25 .= 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 Linear_Combination of V by Def29;
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 Th28
.= u + (v + w) by A1,A3;
end;
thus S is right_zeroed
proof
let v be Element of S;
reconsider K = v as Linear_Combination of V by Def29;
thus v + 0.S = K + ZeroLC V by A1
.= v;
end;
thus S is right_complementable
proof
let v be Element of S;
reconsider K = v as Linear_Combination of V by Def29;
- K in the carrier of S by Def29;
then - K in S;
then - K = vector(S,- K) by RLVECT_2:def 1;
then v + vector(S,- K) = K - K by A1
.= 0.S by Th42;
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,Def33;
end;
thus S is vector-distributive
proof
let a be Element of INT.Ring;
let v, w be Vector of S;
reconsider K = v, M = w as Linear_Combination of V by Def29;
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 Th33
.= a * v + a * w by A1,A6;
hence thesis;
end;
thus S is scalar-distributive
proof
let a, b be Element of INT.Ring;
let v be Vector of S;
reconsider K = v as Linear_Combination of V by Def29;
A7: a * v = a * K & b * v = b * K by A4;
(a + b) * v = (a + b) * K by A4
.= a * K + b * K by Th32
.= a * v + b * v by A1,A7;
hence thesis;
end;
thus S is scalar-associative
proof
let a, b be Element of INT.Ring;
let v be Vector of S;
reconsider K = v as Linear_Combination of V by Def29;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th34
.= a * (b * v) by A4,A8;
hence thesis;
end;
let v be Vector of S;
reconsider K = v as Linear_Combination of V by Def29;
thus 1.INT.Ring * v = 1.INT.Ring * K by A4 .= v;
end;
end;
theorem
the carrier of LC_Z_Module(V) = LinComb(V);
theorem
0.LC_Z_Module(V) = ZeroLC(V);
theorem
the addF of LC_Z_Module(V) = LCAdd(V);
theorem
the lmult of LC_Z_Module(V) = LCMult(V);
theorem Th47:
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 Def29;
then
A2: L2 in LC_Z_Module(V);
L1 in the carrier of LC_Z_Module(V) by Def29;
then L1 in LC_Z_Module(V);
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,Def32;
end;
theorem Th48:
a * vector(LC_Z_Module(V),L) = a * L
proof
A1: @@L = L;
L in the carrier of LC_Z_Module(V) by Def29;
then L in LC_Z_Module(V);
hence a * vector(LC_Z_Module(V),L) = LCMult(V). [a,@L] by RLVECT_2:def 1
.= a * L by A1,Def33;
end;
theorem Th49:
- vector(LC_Z_Module(V),L) = - L
proof
thus - vector(LC_Z_Module(V),L) = (- 1.INT.Ring) *
(vector(LC_Z_Module(V),L)) by ZMODUL01:2
.= - L by Th48;
end;
theorem
vector(LC_Z_Module(V),L1) - vector(LC_Z_Module(V),L2) = L1 - L2
proof
- L2 in LinComb(V) by Def29; then
A1: - L2 in LC_Z_Module(V);
- vector(LC_Z_Module(V),L2) = - L2 by Th49
.= vector(LC_Z_Module(V),- L2) by A1,RLVECT_2:def 1;
hence thesis by Th47;
end;
definition
let V,A;
func LC_Z_Module(A) -> strict Submodule of LC_Z_Module(V) means
the carrier of it = the set of all l;
existence
proof
set X = the set of all l;
X c= the carrier of LC_Z_Module(V)
proof
let x be object;
assume x in X;
then ex l st x = l;
hence thesis by Def29;
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,Th47;
then v + u is Linear_Combination of A by Th27;
hence thesis;
end;
let a be Element of INT.Ring;
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 Th48;
then a * v is Linear_Combination of A by Th31;
hence thesis;
end;
ZeroLC(V) is Linear_Combination of A by Th11;
then 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 Linear_Combination of V;
reserve l for Linear_Combination of A;
reserve F, G, H for FinSequence of V;
reserve f, g for Function of V, INT.Ring;
theorem
f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by VECTSP_6:13;
theorem
Sum(L1 + L2) = Sum(L1) + Sum(L2) by VECTSP_6:44;
theorem
Sum(a * L) = a * Sum(L) by MOD_3:3;
theorem
Sum(- L) = - Sum(L) by VECTSP_6:46;
theorem
Sum(L1 - L2) = Sum(L1) - Sum(L2) by VECTSP_6:47;
theorem
A c= B & B is linearly-independent implies A is linearly-independent
by VECTSP_7:1;
theorem Th57:
A is linearly-independent implies not 0.V in A by VECTSP_7:2;
theorem
{}(the carrier of V) is linearly-independent;
registration
let V;
cluster linearly-independent for Subset of V;
existence
proof
take {}(the carrier of V);
thus thesis;
end;
end;
theorem
V is Mult-cancelable implies
({v} is linearly-independent iff v <> 0.V)
proof
assume A1: 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 Th57;
hence thesis by TARSKI:def 1;
end;
assume
A2: v <> 0.V;
let l be Linear_Combination of {v};
A3: Carrier(l) c= {v} by VECTSP_6:def 4;
assume
A4: Sum(l) = 0.V;
now
per cases by A3,ZFMISC_1:33;
suppose
Carrier(l) = {};
hence thesis;
end;
suppose
A5: Carrier(l) = {v};
then
A6: 0.V = l.v * v by A4,Th24;
now
assume v in Carrier(l);
then ex u st v = u & l.u <> 0;
hence contradiction by A2,A6,A1;
end;
hence thesis by A5,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 Th57;
end;
end;
theorem Th60:
{v1,v2} is linearly-independent implies v1 <> 0.V by VECTSP_7:4;
theorem
{v,0.V} is linearly-dependent by Th60;
theorem Th62:
V is Mult-cancelable implies
(v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V &
for a, b being Element of INT.Ring st b <> 0.INT.Ring holds
b * v1 <> a * v2)
proof
assume A1: V is Mult-cancelable;
thus v1 <> v2 & {v1,v2} is linearly-independent implies v2 <> 0.V &
for a, b being Element of INT.Ring st b <> 0.INT.Ring holds
b * v1 <> a * v2
proof
set N0=0.INT.Ring,N1=-1.INT.Ring;
deffunc F(Element of V)=0.INT.Ring;
assume that
A2: v1 <> v2 and
A3: {v1,v2} is linearly-independent;
thus v2 <> 0.V by A3,Th60;
let a, b be Element of INT.Ring;
assume A4: b <> 0.INT.Ring;
set Na= a;
set Nb=-b;
consider f such that
A5: f.v1 = Nb & f.v2 = Na and
A6: for v being Element of V st v <> v1 & v <> v2 holds f.v = F(v)
from FUNCT_2:sch 7(A2);
reconsider f as Element of Funcs(the carrier of V,
the carrier of INT.Ring) 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.INT.Ring by A6;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= {v1,v2}
proof
let x be object;
assume x in Carrier(f);
then
A7: ex u st x = u & f.u <> 0.INT.Ring;
assume not x in {v1,v2};
then x <> v1 & x <> v2 by TARSKI:def 2;
hence thesis by A6,A7;
end;
then reconsider f as Linear_Combination of {v1,v2} by VECTSP_6:def 4;
f.v1 <> 0.INT.Ring by A5,A4;
then
A8: v1 in Carrier(f);
set w = a * v2;
assume A9: b * v1 = a * v2;
Sum(f) = Nb*v1 + Na*v2 by A2,A5,Th22
.= b*(-v1)+ Na*v2 by ZMODUL01:5
.= (- w) + w by A9,ZMODUL01:6
.= - (w - w) by RLVECT_1:33
.= - 0.V by RLVECT_1:15
.= 0.V by RLVECT_1:12; then
Carrier f = {} by VECTSP_7:def 1,A3;
hence thesis by A8;
end;
assume
A10: v2 <> 0.V;
assume
A11: for a, b being Element of INT.Ring st b <> 0.INT.Ring holds
b * v1 <> a * v2;
A12: 1.INT.Ring * v2 = v2 & 1.INT.Ring * v1 = v1 by VECTSP_1:def 17;
hence v1 <> v2 by A11;
let l be Linear_Combination of {v1,v2};
assume that
A13: Sum(l) = 0.V and
A14: Carrier(l) <> {};
A15: 0.V = l.v1 * v1 + l.v2 * v2 by A11,A12,A13,Th22;
set x = the Element of Carrier(l);
Carrier(l) c= {v1,v2} by VECTSP_6:def 4;
then
A16: x in {v1,v2} by A14;
x in Carrier(l) by A14;
then
A17: ex u st x = u & l.u <> 0;
now
per cases by A17,A16,TARSKI:def 2;
suppose
A18: l.v1 <> 0;
l.v1 * v1 = - (l.v2 * v2) by A15,RLVECT_1:6
.= (- 1.INT.Ring) * (l.v2 * v2) by ZMODUL01:2
.=(-1.INT.Ring)*(l.v2)*v2 by VECTSP_1:def 16;
hence thesis by A11,A18;
end;
suppose
A19: l.v2 <> 0 & l.v1 = 0;
0.V = l.v1 * v1 + l.v2 * v2 by A11,A12,A13,Th22
.= 0.V + l.v2 * v2 by A19,ZMODUL01:1
.= l.v2 * v2 by RLVECT_1:4;
hence thesis by A1,A10,A19;
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 A1: 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
A2: v1 <> v2 & {v1,v2} is linearly-independent;
let a, b;
assume that
A3: a * v1 + b * v2 = 0.V and
A4: a <> 0 or b <> 0;
now
per cases by A4;
suppose
A5: a <> 0;
a * v1 = - (b * v2) by A3,RLVECT_1:6
.= (- 1.INT.Ring) * (b * v2) by ZMODUL01:2
.=(-1.INT.Ring)*b*v2 by VECTSP_1:def 16;
hence thesis by A1,A2,A5,Th62;
end;
suppose
A6: b <> 0;
b * v2 = - (a * v1) by A3,RLVECT_1:6
.= (- 1.INT.Ring) * (a * v1) by ZMODUL01:2
.=(-1.INT.Ring)*a*v1 by VECTSP_1:def 16;
hence thesis by A1,A2,A6,Th62;
end;
end;
hence thesis;
end;
assume
A7: for a, b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0;
A8:
now
let a, b;
assume A9: 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 A9,A7;
end;
now
assume
A10: v2 = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0.INT.Ring * v1 + 0.V by ZMODUL01:1
.= 0.INT.Ring * v1 + 1.INT.Ring * v2 by A10,ZMODUL01:1;
hence contradiction by A7;
end;
hence thesis by A8,A1,Th62;
end;
theorem
x in Lin(A) iff ex l st x = Sum(l) by MOD_3:4;
theorem Th65:
x in A implies x in Lin(A) by MOD_3:5;
theorem
for x being object holds x in (0).V iff x = 0.V
proof let x be object;
thus x in (0).V implies x = 0.V
proof
assume x in (0).V;
then x in the carrier of (0).V;
then x in {0.V} by VECTSP_4:def 3;
hence thesis by TARSKI:def 1;
end;
thus thesis by ZMODUL01:33;
end;
theorem
Lin({}(the carrier of V)) = (0).V by MOD_3:6;
theorem
Lin(A) = (0).V implies A = {} or A = {0.V} by MOD_3:7;
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 Th65;
hence thesis by ZMODUL01:46;
end;
Lm3: 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;
Lm4: 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
A c= B implies Lin(A) is Submodule of Lin(B) by MOD_3:10;
theorem
for V being strict Z_Module,A,B being Subset of V holds
Lin(A) = V & A c= B implies Lin(B) = V by MOD_3:11;
theorem
Lin(A \/ B) = Lin(A) + Lin(B) by MOD_3:12;
theorem
Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B) by MOD_3:13;
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 Lm3;
theorem
W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
Submodule of W3 by Lm4;
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;