:: Quotient Module of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 7, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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, FUNCSDOM, XCMPLX_0;
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, VECTSP10;
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 RELSET_1, FINSET_1, XREAL_0, STRUCT_0, INT_1, ZMODUL01,
XXREAL_0, ALGSTR_0, INT_3, VECTSP_1, XCMPLX_0, ORDINAL1, VECTSP_7,
MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET;
definitions XBOOLE_0, RLVECT_1, ALGSTR_0, VECTSP_1, BINOP_1, TARSKI, VECTSP_4,
VECTSP_7;
equalities XBOOLE_0, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, REALSET1, BINOP_1,
VECTSP_4, VECTSP_6, VECTSP10;
expansions RLVECT_1, STRUCT_0, ALGSTR_0, ZMODUL01, BINOP_1, TARSKI;
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, VECTSP10,
XCMPLX_1, NAT_D;
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 R for Ring;
reserve V for LeftMod of R;
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 R be Ring;
let V be LeftMod of R;
let a be Element of R;
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 R be Ring;
let V be LeftMod of R;
let a be Element of R;
func Zero_(a,V) -> Element of a*V equals
0.V;
correctness
proof
0.V = a*0.V by VECTSP_1:14;
then 0.V in a*V;
hence thesis;
end;
end;
definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
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 R be commutative Ring;
let V be VectSp of R;
let a be Element of R;
func Mult_(a,V) -> Function of [:the carrier of R,a*V :], a*V equals
(the lmult of V) | [:the carrier of R, a*V:];
correctness
proof
set I = the carrier of R;
set scmult = (the lmult of V)| [:the carrier of R, a*V:];
[:I,a*V:] c= [:I,the carrier of V:] by ZFMISC_1:96; then
[:I,a*V:] c= dom(the lmult of V) by FUNCT_2:def 1; then
A1: dom scmult = [:I, a*V:] by RELAT_1:62;
for z be object st z in [:I, a*V:] holds scmult.z in a*V
proof
let z be object such that
A2:z in [:I,a*V:];
consider x,y be object such that
A3:x in I & y in a*V & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider i=x as Element of R 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 R be commutative Ring;
let V be LeftMod of R;
let a be Element of R;
func a (*) V -> Subspace 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 R,V1:];
hence thesis by ZMODUL01:40;
end;
end;
definition
::$CD 5
end;
theorem Th1:
for p be Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of VectQuot(V, W) st W = p (*) V
holds p * x = 0.VectQuot(V, W)
proof
let p be Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of VectQuot(V, W) such that
A1: W = p (*) V;
A2: x is Element of CosetSet(V,W) by VECTSP10:def 6;
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 VECTSP10:def 6
.= (p * v) + W by A2,A3,A4,VECTSP10:def 5
.= zeroCoset(V,W) by A5,ZMODUL01:63
.= 0.VectQuot(V, W) by VECTSP10:def 6;
end;
theorem Th2:
for p, i be Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of VectQuot(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 VectQuot(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.VectQuot(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 by INT_1:def 2;
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.VectQuot(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 VectQuot(V, W) by VECTSP10:def 6;
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 VECTSP10:def 6;
A6: q * x = lmultCoset(V,W).(q,x) by VECTSP10:def 6
.= 0.V + W by A4,A5,VECTSP10:def 5
.= zeroCoset(V,W) by ZMODUL01:59
.= 0.VectQuot(V, W) by VECTSP10:def 6;
(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.VectQuot(V, W) by A6,ZMODUL01:1
.= (i*p) * x by RLVECT_1:4
.= i * (p*x) by VECTSP_1:def 16
.= 0.VectQuot(V, W) by A1,Th1,ZMODUL01:1;
hence 0.VectQuot(V, W) = v + W by a3;
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;
coherence
proof
let p be Integer;
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 VectQuot(V,p(*)V):],
the carrier of VectQuot(V,p(*)V) means
:Def11:
for a being Element of GF(p), i being Element of INT.Ring,
x being Element of VectQuot(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 VectQuot(V,p(*)V),
Element of VectQuot(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 VectQuot(V,p(*)V)
ex z being Element of VectQuot(V,p(*)V) st P[a,x,z]
proof
let a be Element of GF(p), x be Element of VectQuot(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 VectQuot(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 VectQuot(V,p(*)V):],
the carrier of VectQuot(V,p(*)V) such that
A3: for a being Element of GF(p)
for x being Element of VectQuot(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 VectQuot(V,p(*)V):],
the carrier of VectQuot(V,p(*)V);
assume
A4: for a being Element of GF(p), i being Element of INT.Ring,
x being Element of VectQuot(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 VectQuot(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 VectQuot(V,p(*)V);
then reconsider a0=a as Element of GF(p);
reconsider x0=x as Element of VectQuot(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 VectQuot(V,p(*)V),
the addF of VectQuot(V,p(*)V), the ZeroF of VectQuot(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 VectQuot(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 VectQuot(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 NAT_D:66;
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 VectQuot(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 VectQuot(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 VectQuot(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;
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 VectQuot(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 VectQuot(V,p(*)V);
thus u+(0.M) =u1+ 0.(VectQuot(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 VectQuot(V,p(*)V);
reconsider w =-v1 as Element of M;
take w;
thus v + w = v1+ -v1
.= 0.(VectQuot(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 VectQuot(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 VECTSP10:def 6;
end;
end;
definition
let R be Ring; let X be LeftMod of R;
func Mult_INT*(X) -> Function of
[:the carrier of R,the carrier of X:], the carrier of X equals
the lmult of X;
correctness;
end;
definition
let R be Ring;
let X be LeftMod of R;
func modetrans(X) -> non empty strict ModuleStr over R equals
ModuleStr (#the carrier of X, the addF of X, the ZeroF of X, Mult_INT*(X) #);
coherence;
end;
registration
let R be Ring; let X be LeftMod of R;
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 R;
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 R;
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 R;
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.R)*v = (1.R)*v1 .= v1
.= 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
::$CD 13
end;
::$CT 4
begin :: 2. Linear combination of Z-module
reserve K,L,L1,L2,L3 for Linear_Combination of V;
theorem
for R being Ring
for V be LeftMod of R, L be Linear_Combination of V,
v be Element of V holds L.v = 0.R iff not v in Carrier(L)
proof
let R be Ring;
let V be LeftMod of R,
L be Linear_Combination of V, v be Element of V;
thus L.v = 0.R implies not v in Carrier(L)
proof
assume
A1: L.v = 0.R;
assume not thesis;
then ex u be Element of V st u = v & L.u <> 0.R;
hence thesis by A1;
end;
assume not v in Carrier(L);
hence thesis;
end;
theorem
for R being Ring
for V be LeftMod of R, v be Element of V holds (ZeroLC(V)).v = 0.R
proof
let R be Ring;
let V be LeftMod of R, 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 R;
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, R,
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
R is non degenerated implies
(A <> {} & A is linearly-closed iff for l holds Sum(l) in A) by VECTSP_6:14;
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;
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 R,V,L;
reduce L + ZeroLC(V) to L;
reducibility by VECTSP_6:27;
end;
theorem
for V being Z_Module,
a being Element of INT.Ring,
L being Linear_Combination of V holds
a <> 0.INT.Ring implies Carrier(a * L) = Carrier(L)
proof
let V be Z_Module,
a be Element of INT.Ring,
L be Linear_Combination of V;
set R = INT.Ring;
set T = {u where u is Vector of V : (a * L).u <> 0.R};
set S = {v where v is Vector of V : L.v <> 0.R};
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 being Vector of V such that
A2: x = u and
A3: (a * L).u <> 0.R;
(a * L).u = a * L.u by VECTSP_6:def 9;
then L.u <> 0.R by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v being Vector of V such that
A4: x = v and
A5: L.v <> 0.R;
(a * L).v = a * L.v by VECTSP_6:def 9; then
(a * L).v <> 0.R by A1,A5;
hence thesis by A4;
end;
hence thesis;
end;
theorem
0.R * 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 R,V,L;
reduce (1.R)*L to L;
reducibility by VECTSP_6:35;
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 R,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 R) & 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 R,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 R,V, e;
func @e -> Linear_Combination of V equals
e;
coherence by Def29;
end;
definition
let R,V, L;
func @L -> Element of LinComb(V) equals
L;
coherence by Def29;
end;
definition
let R,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 R,V;
func LCMult(V) -> Function of [:the carrier of R, LinComb(V):],
LinComb(V) means :Def33:
for a, e holds it. [a,e] = a * @e;
existence
proof
defpred P[Element of R,Element of LinComb(V),set] means
ex a st a = $1 & $3 = a * @$2;
A1: for x being (Element of R), e1 ex e2 st P[x,e1,e2]
proof
let x be (Element of R), e1;
take @(x * @e1);
take x;
thus thesis;
end;
consider g being Function of [:the carrier of R,
LinComb(V):], LinComb(V) such that
A2: for x being (Element of R), 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 R;
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 R,
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 R), e;
thus g1.(x,e) = x * @e by A3
.= g2.(x,e) by A4;
end;
hence thesis;
end;
end;
definition let R,V;
func LC_Z_Module V -> ModuleStr over R equals
ModuleStr (# LinComb(V), LCAdd(V), @ZeroLC(V), LCMult(V) #);
coherence;
end;
registration let R,V;
cluster LC_Z_Module V -> strict non empty;
coherence;
end;
registration let R,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 .= 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 R;
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 R;
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 R;
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.R * v = 1.R * 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.R) *
(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 R,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 R;
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, R;
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
R is commutative &
A c= B & B is linearly-independent implies A is linearly-independent
by VECTSP_7:1;
theorem Th57:
R is non degenerated &
A is linearly-independent implies not 0.V in A by VECTSP_7:2;
theorem
{}(the carrier of V) is linearly-independent;
registration
let R be Ring;
let V be LeftMod of R;
cluster linearly-independent for Subset of V;
existence
proof
take {}(the carrier of V);
thus thesis;
end;
end;
theorem
R is non degenerated & V is Mult-cancelable implies
({v} is linearly-independent iff v <> 0.V)
proof
assume A1: R is non degenerated & 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,A1;
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.R;
hence contradiction by A2,A6,A1;
end;
hence thesis by A5,TARSKI:def 1;
end;
end;
hence thesis;
end;
registration let R be non degenerated Ring;
let V be LeftMod of R;
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:
R is commutative non degenerated &
{v1,v2} is linearly-independent implies v1 <> 0.V by VECTSP_7:4;
theorem
R is commutative non degenerated implies
{v,0.V} is linearly-dependent by Th60;
theorem Th62:
R = INT.Ring &
::: R is commutative non degenerated &
V is Mult-cancelable implies
(v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V &
for a, b being Element of R st b <> 0.R holds
b * v1 <> a * v2)
proof
assume A1: R = INT.Ring & V is Mult-cancelable;
thus v1 <> v2 & {v1,v2} is linearly-independent implies v2 <> 0.V &
for a, b being Element of R st b <> 0.R holds
b * v1 <> a * v2
proof
set N0=0.R,N1=-1.R;
deffunc F(Element of V)=0.R;
assume that
A2: v1 <> v2 and
A3: {v1,v2} is linearly-independent;
thus v2 <> 0.V by A3,Th60,A1;
let a, b be Element of R;
assume A4: b <> 0.R;
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 R) 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.R 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.R;
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;
Nb <> 0.R by A4,VECTSP_1:28; then
f.v1 <> 0.R by A5;
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,A1
.= (- w) + w by A9,ZMODUL01:6,A1
.= - (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 R st b <> 0.R holds
b * v1 <> a * v2;
A12: 1.R * v2 = v2 & 1.R * v1 = v1;
hence v1 <> v2 by A11,A1;
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,A1;
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.R;
now
per cases by A17,A16,TARSKI:def 2;
suppose
A18: l.v1 <> 0.R;
l.v1 * v1 = - (l.v2 * v2) by A15,RLVECT_1:6
.= (- 1.R) * (l.v2 * v2) by ZMODUL01:2
.=(-1.R)*(l.v2)*v2 by VECTSP_1:def 16;
hence thesis by A11,A18;
end;
suppose
A19: l.v2 <> 0.R & l.v1 = 0.R;
0.V = l.v1 * v1 + l.v2 * v2 by A11,A12,A13,Th22,A1
.= 0.V + l.v2 * v2 by A19,ZMODUL01:1,A1
.= l.v2 * v2 by RLVECT_1:4;
hence thesis by A1,A10,A19;
end;
end;
hence thesis;
end;
theorem
R = INT.Ring &
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.R & b = 0.R)
proof
assume A1: R = INT.Ring & 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.R & b = 0.R
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.R or b <> 0.R;
now
per cases by A4;
suppose
A5: a <> 0.R;
a * v1 = - (b * v2) by A3,RLVECT_1:6
.= (- 1.R) * (b * v2) by ZMODUL01:2
.=(-1.R)*b*v2 by VECTSP_1:def 16;
hence thesis by A1,A2,A5,Th62;
end;
suppose
A6: b <> 0.R;
b * v2 = - (a * v1) by A3,RLVECT_1:6
.= (- 1.R) * (a * v1) by ZMODUL01:2
.=(-1.R)*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.R & b = 0.R;
A8:
now
let a, b;
assume A9: b <> 0.R;
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 A1,ZMODUL01:6
.= b*v1 + (- a) * v2 by A1,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.R * v1 + 0.V by ZMODUL01:1,A1
.= 0.R * v1 + 1.R * v2 by A10;
hence contradiction by A7,A1;
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 LeftMod of R,A being Subset of V holds
A = the carrier of V implies Lin(A) = V
proof
let V be strict LeftMod of R, 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;