:: Free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 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,
PRELAMB, CLASSES1, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1,
FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, ZFMISC_1, INT_1, ORDINAL1,
RLVECT_2, ZMODUL01, ZMODUL03, ORDERS_1, RLVECT_3, RMOD_2, RANKNULL,
MSAFREE2, INT_3, VECTSP_1, NEWTON, MONOID_0, VECTSP10, EC_PF_1, ZMODUL02,
RLVECT_5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1, FINSET_1, ORDERS_1,
CARD_1, CLASSES1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, FINSEQ_1,
FINSEQ_3, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, VECTSP_6,
VECTSP_7, VECTSP_9, MATRLIN, INT_3, BINOM, EC_PF_1, ZMODUL01, ZMODUL02;
constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, CLASSES1,
FUNCT_7, NAT_D, GR_CY_1, EUCLID, VECTSP_6, VECTSP_9, VECTSP10, ALGSTR_1,
ZMODUL02, BINOP_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, XXREAL_0,
NAT_1, INT_3, RELAT_1, ALGSTR_1, VECTSP_1, ZMODUL02;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, BINOM, ZMODUL01,
ZMODUL02, CARD_1;
theorems CARD_1, CARD_2, SUBSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, 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, XREAL_1, ORDINAL1,
STRUCT_0, PARTFUN1, FINSET_1, ORDERS_1, RFINSEQ, VECTSP_1, EC_PF_1,
INT_2, WELLORD2, ZMODUL02, NAT_D, VECTSP_6, VECTSP_7, NUMBERS, VECTSP_4,
VECTSP_9, MATRLIN, BINOM, RLVECT_3;
schemes FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0, FUNCT_1;
begin :: 1. Free Z-module
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 W, W1, W2, W3 for Submodule of V;
registration
cluster non trivial for Z_Module;
correctness
proof
set AG = INT.Ring;
set G =
Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF of AG,
Int-mult-left(AG) #);
X1: G is Z_Module by ZMODUL01:164;
G is non trivial;
hence thesis by X1;
end;
end;
registration
let V be Z_Module;
cluster linearly-independent for finite Subset of V;
correctness
proof
reconsider W = {}(the carrier of V) as finite Subset of V;
take W;
thus W is linearly-independent by ZMODUL02:58;
end;
end;
definition
let K be Field;
let V be non empty VectSpStr over K;
let L be Linear_Combination of V;
let v be Vector of V;
redefine func L.v -> Element of K;
correctness
proof
L.v in K by STRUCT_0:def 5;
hence thesis;
end;
end;
theorem ThLC1:
for u being VECTOR of V holds
ex l being Z_Linear_Combination of V st l.u = 1 &
for v being VECTOR of V st v <> u holds l.v = 0
proof
let u be Element of V;
reconsider i0 = 0 as Element of INT by INT_1:def 2;
deffunc F(Element of V) = i0;
reconsider i1 = 1 as Element of INT by INT_1:def 2;
ex f being Function of the carrier of V, INT st
f.u = i1 & for v being Element of V st v <> u holds f.v = F(v)
from FUNCT_2:sch 6;
then consider f being Function of the carrier of V, INT such that
A1: f.u = 1 and
A2: for v being Element of V st v <> u holds f.v = 0;
for v being Element of V holds not v in {u} implies v <> u by TARSKI:def 1;
then
A4: for v being Element of V holds not v in {u} implies f.v = 0 by A2;
reconsider f as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
reconsider f as Z_Linear_Combination of V by A4,ZMODUL02:def 18;
take f;
thus thesis by A1,A2;
end;
LMTHX3:
for r be Element of INT.Ring,
n be Element of NAT, i be Integer st i = n
holds i*r = n*r
proof
let r be Element of INT.Ring;
defpred P[Element of NAT] means
for i be Integer st i = $1 holds i*r = $1*r;
reconsider rr = r as Integer;
Z1: 0.(INT.Ring) = 0;
P1: P[ 0 ] by Z1,BINOM:12;
P2: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT;
assume P20: P[n];
now
let i be Integer;
assume AS1: i = n+1;
reconsider Kn = n, K1 = 1 as Integer;
reconsider n1 = 1 as Element of NAT;
X2: K1 * r = n1*r by BINOM:13;
thus i*r = Kn*r + K1*r by AS1
.= (n*r) + (n1*r) by P20,X2
.= (n+1) * r by BINOM:15;
end;
hence P[n+1];
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(P1,P2);
hence thesis;
end;
theorem LMTHX4:
for G be Z_Module, i being Element of INT,
w be Element of INT, v be Element of G
st G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring,
the addF of INT.Ring, Int-mult-left(INT.Ring) #) & v = w
holds i*v = i*w
proof
let G be Z_Module, i be Element of INT,
w be Element of INT, v be Element of G;
assume AS: G = Z_ModuleStruct(# the carrier of INT.Ring,
the ZeroF of INT.Ring, the addF of INT.Ring,
Int-mult-left(INT.Ring) #) & v = w;
reconsider r = v as Element of INT.Ring by AS;
per cases;
suppose 0 <= i;
then reconsider n=i as Element of NAT by INT_1:3;
thus i*v = n*r by AS,ZMODUL01:def 23
.= i*w by AS,LMTHX3;
end;
suppose A2: not 0 <= i;
then reconsider n = -i as Element of NAT by INT_1:3;
thus i*v = n*(-r) by AS,A2,ZMODUL01:def 23
.= (-i)*(-r) by LMTHX3
.= i*w by AS;
end;
end;
definition
let IT be Z_Module;
attr IT is free means :DefFree:
ex A being Subset of IT
st A is linearly-independent & Lin(A) = the Z_ModuleStruct of IT;
end;
registration let V;
cluster (0).V -> free;
coherence
proof
set W = (0).V;
reconsider W as Z_Module;
set A = {}(the carrier of W);
reconsider A as Subset of W;
Lin(A) = (0).W by ZMODUL02:67
.= (0).V by ZMODUL01:51;
hence thesis by DefFree,ZMODUL02:58;
end;
end;
registration
cluster strict free for Z_Module;
existence
proof
take (0).the Z_Module;
thus thesis;
end;
end;
registration
let V be Z_Module;
cluster strict free for Submodule of V;
existence
proof
take (0).V;
thus thesis;
end;
end;
definition
let V be free Z_Module;
mode Basis of V -> Subset of V means :RL3Def3:
it is linearly-independent & Lin (it) = the Z_ModuleStruct of V;
existence by DefFree;
end;
registration
cluster -> Mult-cancelable for free Z_Module;
coherence
proof
let V be free Z_Module;
set I = the Basis of V;
assume AS: not V is Mult-cancelable;
consider a being Integer, v being VECTOR of V such that
A2: a * v = 0.V & a <> 0 & v <> 0.V by AS,ZMODUL01:def 7;
I is linearly-independent & Lin(I) = the Z_ModuleStruct of V
by RL3Def3;
then consider lv be Z_Linear_Combination of I such that
A4: v = Sum(lv) by STRUCT_0:def 5,ZMODUL02:64;
Carrier(lv) <> {} by A2,A4,ZMODUL02:23;
then A5: Carrier(a*lv) <> {} by A2,ZMODUL02:29;
A6: a * lv is Z_Linear_Combination of I by ZMODUL02:31;
Sum(a * lv) = 0.V by A2,A4,ZMODUL02:53;
hence contradiction by A5,A6,RL3Def3,ZMODUL02:def 36;
end;
end;
registration
cluster free for non trivial Z_Module;
correctness
proof
set AG = INT.Ring;
set G = Z_ModuleStruct(# the carrier of AG, the ZeroF of AG,
the addF of AG, Int-mult-left(AG) #);
reconsider G as non trivial Z_Module by ZMODUL01:164;
reconsider iv = 1 as VECTOR of G;
reconsider i1 = 1 as Element of INT by INT_1:def 2;
set I = {iv};
Z1: 0.G = 0;
reconsider I as Subset of G;
for a be Integer for v being VECTOR of G st a * v = 0.G
holds a = 0 or v = 0.G
proof
let a be Integer, v be VECTOR of G;
assume AS1: a * v = 0.G;
reconsider w= v as Element of INT;
X1: a is Element of INT by INT_1:def 2;
a*w = 0 by AS1,X1,LMTHX4;
hence a = 0 or v = 0.G by XCMPLX_1:6;
end;
then G is Mult-cancelable by ZMODUL01:def 7;
then X3: I is linearly-independent by Z1,ZMODUL02:59;
for x be element holds
x in the carrier of (Lin(I)) iff x in the carrier of G
proof
let x be element;
hereby assume AA: x in the carrier of (Lin(I));
the carrier of (Lin(I)) c= the carrier of G by ZMODUL01:def 9;
hence x in the carrier of G by AA;
end;
assume x in the carrier of G;
then reconsider v0 = x as VECTOR of G;
reconsider w = v0 as Element of INT;
reconsider a = w as Integer;
reconsider i0 = 0 as Element of INT by INT_1:def 2;
deffunc G(VECTOR of G) = i0;
deffunc L0(VECTOR of G) = w;
consider g being Function of the carrier of G, INT such that
A48: g.iv = w and
A49: for u being VECTOR of G st u <> iv holds g.u = G(u)
from FUNCT_2:sch 6;
reconsider g as Element of Funcs(the carrier of G, INT) by FUNCT_2:8;
now
let u be VECTOR of G;
assume not u in {iv};
then u <> iv by TARSKI:def 1;
hence g.u = 0 by A49;
end;
then reconsider g as Z_Linear_Combination of G by ZMODUL02:def 18;
Carrier(g) c= {iv}
proof
let x be element;
assume x in Carrier(g);
then ex u being VECTOR of G st x = u & g.u <> 0;
then x = iv by A49;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Z_Linear_Combination of {iv} by ZMODUL02:def 21;
Sum(g) = w * iv by A48,ZMODUL02:21
.= w*i1 by LMTHX4
.= v0;
hence x in the carrier of (Lin(I)) by STRUCT_0:def 5,ZMODUL02:64;
end;
then Lin(I) = the Z_ModuleStruct of G by TARSKI:2,ZMODUL01:47;
then G is free by X3,DefFree;
hence thesis;
end;
end;
reserve KL1, KL2 for Z_Linear_Combination of V;
reserve X for Subset of V;
theorem RL5Th1:
X is linearly-independent & Carrier(KL1) c= X & Carrier(KL2) c= X
& Sum(KL1) = Sum(KL2) implies KL1 = KL2
proof
assume A1: X is linearly-independent;
assume A2: Carrier(KL1) c= X;
assume Carrier(KL2) c= X;
then
A3: Carrier(KL1) \/ Carrier(KL2) c= X by A2,XBOOLE_1:8;
assume Sum(KL1) = Sum(KL2);
then Sum(KL1) - Sum(KL2) = 0.V by RLVECT_1:5;
then
A4: KL1 - KL2 is Z_Linear_Combination of Carrier(KL1 - KL2) &
Sum(KL1 - KL2) = 0.V by ZMODUL02:def 21,ZMODUL02:55;
Carrier(KL1 - KL2) c= Carrier(KL1) \/ Carrier(KL2) by ZMODUL02:40;
then
A5: Carrier(KL1 - KL2) is linearly-independent
by A1,A3,ZMODUL02:56,XBOOLE_1:1;
now
let v be VECTOR of V;
not v in Carrier(KL1 - KL2) by A5,A4,ZMODUL02:def 36;
then (KL1 - KL2).v = 0;
then KL1.v - KL2.v = 0 by ZMODUL02:39;
hence KL1.v = KL2.v;
end;
hence thesis by ZMODUL02:def 24;
end;
theorem
for V being free Z_Module, A being Subset of V st A is linearly-independent
ex B being Subset of V st A c= B & B is linearly-independent &
(for v being VECTOR of V holds ex a being Integer st a * v in Lin(B))
proof
let V be free Z_Module, A be Subset of V such that
P1: A is linearly-independent;
defpred P[set] means ex B being Subset of V st B = $1 & A c= B & B is
linearly-independent;
consider Q being set such that
A1: for Z being set holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XBOOLE_0:sch 1;
A2: now
let Z be set;
assume that
A3: Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear;
set W = union Z;
W c= the carrier of V
proof
let x be element;
assume x in W;
then consider X be set such that
A6: x in X and
A7: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A1,A4,A7;
hence thesis by A6;
end;
then reconsider W as Subset of V;
A8: W is linearly-independent
proof
deffunc Q(set)={C where C is Subset of V: $1 in C & C in Z};
let l be Z_Linear_Combination of W;
assume that
A9: Sum(l) = 0.V and
A10: Carrier(l) <> {};
consider f being Function such that
A11: dom f = Carrier(l) and
A12: for x st x in Carrier(l) holds f.x = Q(x) from FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A10,A11,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A13:
now
assume {} in M;
then consider x such that
A14: x in dom f and
A15: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by ZMODUL02:def 21;
then consider X be set such that
A16: x in X and
A17: X in Z by A11,A14,TARSKI:def 4;
reconsider X as Subset of V by A1,A4,A17;
X in {C where C is Subset of V: x in C & C in Z} by A16,A17;
hence contradiction by A11,A12,A14,A15;
end;
then
A18: dom F = M by RLVECT_3:28;
then dom F is finite by A11,FINSET_1:8;
then
A19: S is finite by FINSET_1:8;
A20:
now
let X be set;
assume X in S;
then consider x such that
A21: x in dom F and
A22: F.x = X by FUNCT_1:def 3;
consider y such that
A23: y in dom f & f.y = x by A21,FUNCT_1:def 3;
A24: x = Q(y) by A11,A12,A23;
X in x by A13,A21,A22,ORDERS_1:def 1;
then ex C being Subset of V st C = X & y in C & C in Z by A24;
hence X in Z;
end;
A25:
now
let X,Y be set;
assume X in S & Y in S;
then X in Z & Y in Z by A20;
hence X c= Y or Y c= X by A5,ORDINAL1:def 8,XBOOLE_0:def 9;
end;
S <> {} by A18,RELAT_1:42;
then union S in Z by A19,A20,A25,CARD_2:62;
then consider B being Subset of V such that
A26: B = union S and
A c= B and
A27: B is linearly-independent by A1,A4;
Carrier(l) c= union S
proof
let x be element;
set X = f.x;
assume A28: x in Carrier(l);
then
A29: f.x = {C where C is Subset of V: x in C & C in Z} by A12;
A30: f.x in M by A11,A28,FUNCT_1:def 3;
then F.X in X by A13,ORDERS_1:def 1;
then
A31: ex C being Subset of V st F.X = C & x in C & C in Z by A29;
F.X in S by A18,A30,FUNCT_1:def 3;
hence thesis by A31,TARSKI:def 4;
end;
then l is Z_Linear_Combination of B by A26,ZMODUL02:def 21;
hence thesis by A9,A10,A27,ZMODUL02:def 36;
end;
set x = the Element of Z;
x in Q by A3,A4,TARSKI:def 3; then
A32: ex B being Subset of V st B = x & A c= B & B is linearly-independent
by A1;
x c= W by A3,ZFMISC_1:74;
hence union Z in Q by A1,A8,A32,XBOOLE_1:1;
end;
Q <> {} by P1,A1;
then consider X be set such that
A34: X in Q and
A35: for Z be set st Z in Q & Z <> X holds not X c= Z by A2,ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: A c= B and
A38: B is linearly-independent by A1,A34;
take B;
thus A c= B & B is linearly-independent by A37,A38;
assume not for v being VECTOR of V holds ex a being Integer
st a * v in Lin(B);
then consider v being VECTOR of V such that
A39: for a being Integer holds not a * v in Lin(B);
A40: B \/ {v} is linearly-independent
proof
let l be Z_Linear_Combination of B \/ {v};
assume A41: Sum(l) = 0.V;
now
per cases;
suppose
v in Carrier(l);
reconsider i0 = 0 as Element of INT by INT_1:def 2;
deffunc G(VECTOR of V)=i0;
deffunc L(VECTOR of V)=l.$1;
consider f being Function of the carrier of V, INT such that
A43: f.v = i0 and
A44: for u being VECTOR of V st u <> v holds f.u = L(u)
from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in Carrier(l) \ {v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u = 0 & u <> v or u = v by TARSKI:def 1;
hence f.u = 0 by A43,A44;
end;
then reconsider f as Z_Linear_Combination of V by ZMODUL02:def 18;
Carrier(f) c= B
proof
let x be element;
A45: Carrier(l) c= B \/ {v} by ZMODUL02:def 21;
assume x in Carrier(f);
then consider u being VECTOR of V such that
A46: u = x and
A47: f.u <> 0;
f.u = l.u by A43,A44,A47;
then u in Carrier(l) by A47;
then u in B or u in {v} by A45,XBOOLE_0:def 3;
hence thesis by A43,A46,A47,TARSKI:def 1;
end;
then reconsider f as Z_Linear_Combination of B by ZMODUL02:def 21;
reconsider lv = -l.v as Element of INT by INT_1:def 2;
consider g being Function of the carrier of V, INT such that
A48: g.v = lv and
A49: for u being VECTOR of V st u <> v holds g.u = G(u)
from FUNCT_2:sch 6;
reconsider g as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence g.u = 0 by A49;
end;
then reconsider g as Z_Linear_Combination of V by ZMODUL02:def 18;
Carrier(g) c= {v}
proof
let x be element;
assume x in Carrier(g);
then ex u being VECTOR of V st x = u & g.u <> 0;
then x = v by A49;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Z_Linear_Combination of {v} by ZMODUL02:def 21;
A50: Sum(g) = (- l.v) * v by A48,ZMODUL02:21;
f - g = l
proof
let u be VECTOR of V;
now
per cases;
suppose
A51: v = u;
thus (f - g).u = f.u - g.u by ZMODUL02:39
.= l.u by A43,A48,A51;
end;
suppose
A52: v <> u;
thus (f - g).u = f.u - g.u by ZMODUL02:39
.= l.u - g.u by A44,A52
.= l.u - 0 by A49,A52
.= l.u;
end;
end;
hence thesis;
end;
then 0.V = Sum(f) - Sum(g) by A41,ZMODUL02:55;
then Sum(f) = 0.V + Sum(g) by RLSUB_2:61
.= (- l.v) * v by A50,RLVECT_1:4;
hence thesis by A39,ZMODUL02:64;
end;
suppose
A54: not v in Carrier(l);
Carrier(l) c= B
proof
let x be element;
assume
A55: x in Carrier(l);
Carrier(l) c= B \/ {v} by ZMODUL02:def 21;
then x in B or x in {v} by A55,XBOOLE_0:def 3;
hence thesis by A54,A55,TARSKI:def 1;
end;
then l is Z_Linear_Combination of B by ZMODUL02:def 21;
hence thesis by A38,A41,ZMODUL02:def 36;
end;
end;
hence thesis;
end;
v in {v} by TARSKI:def 1;
then
A56: v in B \/ {v} by XBOOLE_0:def 3;
not 1 * v in Lin(B) by A39;
then not v in Lin(B) by ZMODUL01:def 5;
then A57: not v in B by ZMODUL02:65;
B c= B \/ {v} by XBOOLE_1:7;
then B \/ {v} in Q by A1,A37,A40,XBOOLE_1:1;
hence contradiction by A35,A36,A56,A57,XBOOLE_1:7;
end;
theorem RL5Th5:
for L being Z_Linear_Combination of V for F, G being FinSequence of V
for P being Permutation of dom F st G = F*P holds
Sum(L (#) F) = Sum(L (#) G)
proof
let L be Z_Linear_Combination of V;
let F, G be FinSequence of V;
set p = L (#) F, q = L (#) G;
let P be Permutation of dom F such that
A1: G = F*P;
A2: len G = len F by A1,FINSEQ_2:44;
len F = len(L (#) F) by ZMODUL02:def 22;
then
A3: dom F = dom(L (#) F) by FINSEQ_3:29;
then reconsider r = (L (#) F)*P as FinSequence of V by FINSEQ_2:47;
len r = len(L (#) F) by A3,FINSEQ_2:44;
then
A4: dom r = dom(L (#) F) by FINSEQ_3:29;
A5: len p = len F by ZMODUL02:def 22;
then
A6: dom F = dom p by FINSEQ_3:29;
len q = len G by ZMODUL02:def 22;
then
A7: dom p = dom q by A1,A5,FINSEQ_2:44,FINSEQ_3:29;
A8: dom F = dom G by A2,FINSEQ_3:29;
now
let k be Nat;
assume
A10: k in dom q;
set l = P.k;
dom P = dom F & rng P = dom F by FUNCT_2:52,def 3;
then
A11: l in dom F by A7,A6,A10,FUNCT_1:def 3;
then reconsider l as Element of NAT;
G/.k = G.k by A7,A8,A6,A10,PARTFUN1:def 6
.= F.(P.k) by A1,A7,A8,A6,A10,FUNCT_1:12
.= F/.l by A11,PARTFUN1:def 6;
then q.k = L.(F/.l) * (F/.l) by A10,ZMODUL02:def 22
.= (L (#) F).(P.k) by A6,A11,ZMODUL02:def 22
.= r.k by A7,A4,A10,FUNCT_1:12;
hence q.k = r.k;
end;
hence Sum(p) = Sum(q) by A3,A4,A7,FINSEQ_1:13,RLVECT_2:7;
end;
theorem RL5Th6:
for L being Z_Linear_Combination of V for F being FinSequence of V st
Carrier(L) misses rng F holds Sum(L (#) F) = 0.V
proof
let L be Z_Linear_Combination of V;
defpred P[FinSequence] means for G being FinSequence of V st
G = $1 holds Carrier(L) misses rng G implies Sum(L (#) G) = 0.V;
A1: for p being FinSequence, x st P[p] holds P[p^<*x*>]
proof
let p be FinSequence, x such that
A2: P[p];
let G be FinSequence of V;
assume A3: G = p^<*x*>;
then reconsider p, x9= <*x*> as FinSequence of V by FINSEQ_1:36;
x in {x} by TARSKI:def 1;
then
A4: x in rng x9 by FINSEQ_1:38;
reconsider x as VECTOR of V by A4;
assume Carrier(L) misses rng G;
then
A5: {} = Carrier(L) /\ rng G by XBOOLE_0:def 7
.= Carrier(L) /\ (rng p \/ rng<*x*>) by A3,FINSEQ_1:31
.= Carrier(L) /\ (rng p \/ {x}) by FINSEQ_1:38
.= Carrier(L) /\ rng p \/ Carrier(L) /\ {x} by XBOOLE_1:23;
then Carrier(L) /\ rng p = {};
then
A6: Sum(L (#) p) = 0.V by A2,XBOOLE_0:def 7;
A7: Carrier(L) /\ {x} = {} by A5;
now
A8: x in {x} by TARSKI:def 1;
assume x in Carrier(L);
hence contradiction by A7,A8,XBOOLE_0:def 4;
end;
then
A9: L.x = 0;
Sum(L (#) G) = Sum((L (#) p) ^ (L (#) x9)) by A3,ZMODUL02:51
.= Sum(L (#) p) + Sum(L (#) x9) by RLVECT_1:41
.= 0.V + Sum(<* L.x * x *>) by A6,ZMODUL02:15
.= Sum(<* L.x * x *>) by RLVECT_1:4
.= 0 * x by A9,RLVECT_1:44
.= 0.V by ZMODUL01:1;
hence thesis;
end;
A10: P[{}]
proof
let G be FinSequence of V;
assume G = {};
then
A11: L (#) G = <*>(the carrier of V) by ZMODUL02:14;
assume Carrier(L) misses rng G;
thus thesis by A11,RLVECT_1:43;
end;
A12: for p being FinSequence holds P[p] from FINSEQ_1:sch 3(A10, A1);
let F be FinSequence of V;
assume Carrier(L) misses rng F;
hence thesis by A12;
end;
theorem
for F being FinSequence of V st F is one-to-one
for L being Z_Linear_Combination of V st Carrier(L) c= rng F holds
Sum(L (#) F) = Sum(L)
proof
let F be FinSequence of V such that
A1: F is one-to-one;
rng F c= rng F;
then reconsider X = rng F as Subset of rng F;
let L be Z_Linear_Combination of V such that
A2: Carrier(L) c= rng F;
consider G being FinSequence of V such that
A3: G is one-to-one and
A4: rng G = Carrier(L) and
A5: Sum(L) = Sum(L (#) G) by ZMODUL02:def 23;
reconsider A = rng G as Subset of rng F by A2,A4;
set F1 = F - A`;
X \ A` = X /\ A`` by SUBSET_1:13
.= A by XBOOLE_1:28; then
A6: rng F1 = rng G by FINSEQ_3:65;
F1 is one-to-one by A1,FINSEQ_3:87; then
A7: ex Q being Permutation of dom G st F1 = G*Q
by A3,A6,RFINSEQ:4,RFINSEQ:26;
reconsider F1, F2 = F - A as FinSequence of V by FINSEQ_3:86;
A9: rng F2 /\ rng G = (rng F \ rng G) /\ rng G by FINSEQ_3:65
.= {} by XBOOLE_0:def 7,XBOOLE_1:79;
ex P being Permutation of dom F st (F - A`) ^ (F - A) = F * P
by FINSEQ_3:115;
then Sum(L (#) F) = Sum(L (#) (F1^F2)) by RL5Th5
.= Sum((L (#) F1) ^ (L (#) F2)) by ZMODUL02:51
.= Sum(L (#) F1) + Sum(L (#) F2) by RLVECT_1:41
.= Sum(L (#) F1) + 0.V by A4,A9,RL5Th6,XBOOLE_0:def 7
.= Sum(L (#) G) + 0.V by A7,RL5Th5
.= Sum(L) by A5,RLVECT_1:4;
hence thesis;
end;
theorem
for L being Z_Linear_Combination of V for F being FinSequence of V holds
ex K being Z_Linear_Combination of V st
Carrier(K) = rng F /\ Carrier(L) & L (#) F = K (#) F
proof
let L be Z_Linear_Combination of V, F be FinSequence of V;
defpred P[set, set] means $1 is VECTOR of V implies
($1 in rng F & $2 = L.$1) or (not $1 in rng F & $2 = 0);
reconsider R = rng F as finite Subset of V;
A1: for x st x in the carrier of V ex y st y in INT & P[x, y]
proof
let x;
assume x in the carrier of V;
then reconsider x9 = x as VECTOR of V;
per cases;
suppose
B1: x in rng F;
L.x9 in INT;
hence thesis by B1;
end;
suppose
B1: not x in rng F;
0 in INT by INT_1:def 2;
hence thesis by B1;
end;
end;
ex K being Function of the carrier of V, INT st for x st x in the
carrier of V holds P[x, K.x] from FUNCT_2:sch 1(A1);
then consider K being Function of the carrier of V, INT such that
A2: for x st x in the carrier of V holds P[x, K.x];
A3:
now
let v be VECTOR of V;
assume
A4: not v in R /\ Carrier(L);
per cases by A4,XBOOLE_0:def 4;
suppose
not v in R;
hence K.v = 0 by A2;
end;
suppose
not v in Carrier(L);
then L.v = 0;
hence K.v = 0 by A2;
end;
end;
reconsider K as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
reconsider K as Z_Linear_Combination of V by A3,ZMODUL02:def 18;
now
let v be element;
assume
A5: v in rng F /\ Carrier(L);
then reconsider v9= v as VECTOR of V;
v in Carrier(L) by A5,XBOOLE_0:def 4;
then
A6: L.v9 <> 0 by ZMODUL02:8;
v in R by A5,XBOOLE_0:def 4;
then K.v9 = L.v9 by A2;
hence v in Carrier(K) by A6;
end;
then
A7: rng F /\ Carrier(L) c= Carrier(K) by TARSKI:def 3;
take K;
A8: L (#) F = K (#) F
proof
set p = L (#) F, q = K (#) F;
A9: len p = len F by ZMODUL02:def 22;
len q = len F by ZMODUL02:def 22;
then
A10: dom p = dom q by A9,FINSEQ_3:29;
A11: dom p = dom F by A9,FINSEQ_3:29;
now
let k be Nat;
set u = F/.k;
A12: P[u, K.u] by A2;
assume
A13: k in dom p;
then F/.k = F.k & p.k = L.u * u by A11,PARTFUN1:def 6,ZMODUL02:def 22;
hence p.k = q.k by A10,A11,A13,A12,FUNCT_1:def 3,ZMODUL02:def 22;
end;
hence thesis by A10,FINSEQ_1:13;
end;
now
let v be element;
assume v in Carrier(K);
then ex v9 being VECTOR of V st v9= v & K.v9 <> 0;
hence v in rng F /\ Carrier(L) by A3;
end;
then Carrier(K) c= rng F /\ Carrier(L) by TARSKI:def 3;
hence thesis by A7,A8,XBOOLE_0:def 10;
end;
theorem RL5Th9:
for L being Z_Linear_Combination of V for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of Lin(A) holds
ex K being Z_Linear_Combination of A st Sum(L (#) F) = Sum(K)
proof
let L be Z_Linear_Combination of V;
let A be Subset of V;
defpred P[Element of NAT] means for F being FinSequence of V
st rng F c= the carrier of Lin(A) & len F = $1 holds ex K being
Z_Linear_Combination of A st Sum(L (#) F) = Sum(K);
A1: for n being Element of NAT st P[n] holds P[n + 1]
proof
let n be Element of NAT;
assume
A2: P[n];
let F be FinSequence of V such that
A3: rng F c= the carrier of Lin(A) and
A4: len F = n + 1;
consider G being FinSequence, x being set such that
A5: F = G^<*x*> by A4,FINSEQ_2:18;
reconsider G, x9= <*x*> as FinSequence of V by A5,FINSEQ_1:36;
A6: rng(G^<*x*>) = rng G \/ rng <*x*> by FINSEQ_1:31
.= rng G \/ {x} by FINSEQ_1:38; then
A7: rng G c= rng F by A5,XBOOLE_1:7;
{x} c= rng F by A5,A6,XBOOLE_1:7;
then {x} c= the carrier of Lin(A) by A3,XBOOLE_1:1; then
A8: x in {x} implies x in the carrier of Lin(A);
then consider LA1 being Z_Linear_Combination of A such that
A9: x = Sum(LA1) by STRUCT_0:def 5,TARSKI:def 1,ZMODUL02:64;
x in V by A8,STRUCT_0:def 5,TARSKI:def 1,ZMODUL01:24;
then reconsider x as VECTOR of V by STRUCT_0:def 5;
len(G^<*x*>) = len G + len <*x*> by FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
then consider LA2 being Z_Linear_Combination of A such that
A10: Sum(L (#) G) = Sum(LA2) by A2,A3,A4,A5,A7,XBOOLE_1:1;
L.x * LA1 is Z_Linear_Combination of A by ZMODUL02:31; then
A11: LA2 + L.x * LA1 is Z_Linear_Combination of A by ZMODUL02:27;
Sum(L (#) F) = Sum((L (#) G) ^ (L (#) x9)) by A5,ZMODUL02:51
.= Sum(LA2) + Sum(L (#) x9) by A10,RLVECT_1:41
.= Sum(LA2) + Sum(<*L.x * x*>) by ZMODUL02:15
.= Sum(LA2) + L.x * Sum(LA1) by A9,RLVECT_1:44
.= Sum(LA2) + Sum(L.x * LA1) by ZMODUL02:53
.= Sum(LA2 + L.x * LA1) by ZMODUL02:52;
hence thesis by A11;
end;
let F be FinSequence of V;
assume
A12: rng F c= the carrier of Lin(A);
A13: len F is Element of NAT;
A14: P[0]
proof
let F be FinSequence of V;
assume that
rng F c= the carrier of Lin(A) and
A15: len F = 0;
F = <*>(the carrier of V) by A15;
then L (#) F = <*>(the carrier of V) by ZMODUL02:14;
then
A16: Sum(L (#) F) = 0.V by RLVECT_1:43
.= Sum(Z_ZeroLC(V)) by ZMODUL02:19;
Z_ZeroLC(V) is Z_Linear_Combination of A by ZMODUL02:11;
hence thesis by A16;
end;
for n being Element of NAT holds P[n] from NAT_1:sch 1(A14, A1);
hence thesis by A12,A13;
end;
theorem RL5Th10:
for L being Z_Linear_Combination of V for A being Subset of V st
Carrier(L) c= the carrier of Lin(A) holds
ex K being Z_Linear_Combination of A st Sum(L) = Sum(K)
proof
let L be Z_Linear_Combination of V, A be Subset of V;
consider F being FinSequence of V such that
F is one-to-one and
A1: rng F = Carrier(L) and
A2: Sum(L) = Sum(L (#) F) by ZMODUL02:def 23;
assume Carrier(L) c= the carrier of Lin(A);
then consider K being Z_Linear_Combination of A such that
A3: Sum(L (#) F) = Sum(K) by A1,RL5Th9;
take K;
thus thesis by A2,A3;
end;
theorem RL5Th11:
for L being Z_Linear_Combination of V st Carrier(L) c= the carrier
of W for K being Z_Linear_Combination of W st K = L|the carrier of W holds
Carrier(L) = Carrier(K) & Sum(L) = Sum(K)
proof
let L be Z_Linear_Combination of V such that
A1: Carrier(L) c= the carrier of W;
let K be Z_Linear_Combination of W such that
A2: K = L|the carrier of W;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now
let x be element;
assume x in Carrier(K);
then consider w being VECTOR of W such that
A4: x = w and
A5: K.w <> 0;
A6: w is VECTOR of V by ZMODUL01:25;
L.w <> 0 by A2,A3,A5,FUNCT_1:47;
hence x in Carrier(L) by A4,A6;
end;
then
A7: Carrier(K) c= Carrier(L) by TARSKI:def 3;
consider G being FinSequence of W such that
A8: G is one-to-one & rng G = Carrier(K) and
A9: Sum(K) = Sum(K (#) G) by ZMODUL02:def 23;
consider F being FinSequence of V such that
A10: F is one-to-one and
A11: rng F = Carrier(L) and
A12: Sum(L) = Sum(L (#) F) by ZMODUL02:def 23;
now
let x be element;
assume
A13: x in Carrier(L);
then consider v being VECTOR of V such that
A14: x = v and
A15: L.v <> 0;
K.v <> 0 by A1,A2,A3,A13,A14,A15,FUNCT_1:47;
hence x in Carrier(K) by A1,A13,A14;
end;
then
A16: Carrier(L) c= Carrier(K) by TARSKI:def 3;
then
A17: Carrier(K) = Carrier(L) by A7,XBOOLE_0:def 10;
F, G are_fiberwise_equipotent
by A7,A8,A10,A11,A16,RFINSEQ:26,XBOOLE_0:def 10;
then consider P being Permutation of dom G such that
A18: F = G*P by RFINSEQ:4;
len(K (#) G) = len G by ZMODUL02:def 22;
then
A19: dom(K (#) G) = dom G by FINSEQ_3:29;
then reconsider q = (K (#) G)*P as FinSequence of W by FINSEQ_2:47;
A20: len q = len (K (#) G) by A19,FINSEQ_2:44;
then len q = len G by ZMODUL02:def 22;
then
A21: dom q = dom G by FINSEQ_3:29;
set p = L (#) F;
A22: the carrier of W c= the carrier of V by ZMODUL01:def 9;
rng q c= the carrier of V by A22,XBOOLE_1:1;
then reconsider q9= q as FinSequence of V by FINSEQ_1:def 4;
consider f being Function of NAT, the carrier of W such that
A23: Sum(q) = f.(len q) and
A24: f.0 = 0.W and
A25: for i being Element of NAT, w being VECTOR of W st i < len q & w =
q.(i + 1) holds f.(i + 1) = f.i + w by RLVECT_1:def 12;
dom f = NAT & rng f c= the carrier of W by FUNCT_2:def 1;
then reconsider f9= f as Function of NAT, the carrier of V
by A22,FUNCT_2:2,XBOOLE_1:1;
A26: for i being Element of NAT, v being VECTOR of V st i < len q9 &
v = q9.(i + 1) holds f9.(i + 1) = f9.i + v
proof
let i be Element of NAT, v be VECTOR of V;
assume that
A27: i < len q9 and
A28: v = q9.(i + 1);
1 <= i + 1 & i + 1 <= len q by A27,NAT_1:11,13;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9= v as VECTOR of W by A28,FINSEQ_2:11;
f.(i + 1) = f.i + v9 by A25,A27,A28;
hence thesis by ZMODUL01:28;
end;
A29: len G = len F by A18,FINSEQ_2:44; then
A30: dom G = dom F by FINSEQ_3:29;
A31: len G = len (L (#) F) by A29,ZMODUL02:def 22; then
AA31: dom p = dom G by FINSEQ_3:29;
A32: dom q = dom(K (#) G) by A20,FINSEQ_3:29;
now
let i be Nat;
set v = F/.i;
set j = P.i;
assume
A33: i in dom p;
then
A34: F/.i = F.i by A30,AA31,PARTFUN1:def 6;
then v in rng F by A30,AA31,A33,FUNCT_1:def 3;
then reconsider w = v as VECTOR of W by A17,A11;
dom P = dom G & rng P = dom G by FUNCT_2:52,def 3;
then
A35: j in dom G by AA31,A33,FUNCT_1:def 3;
then reconsider j as Element of NAT;
A36: G/.j = G.(P.i) by A35,PARTFUN1:def 6
.= v by A18,A30,AA31,A33,A34,FUNCT_1:12;
q.i = (K (#) G).j by A21,AA31,A33,FUNCT_1:12
.= K.w * w by A32,A21,A35,A36,ZMODUL02:def 22
.= L.v * w by A2,A3,FUNCT_1:47
.= L.v * v by ZMODUL01:29;
hence p.i = q.i by A33,ZMODUL02:def 22;
end;
then
A37: L (#) F = (K (#) G)*P by A21,A31,FINSEQ_1:13,FINSEQ_3:29;
len G = len (K (#) G) by ZMODUL02:def 22;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P as Permutation of dom (K (#) G);
q = (K (#) G)*P; then
A38: Sum(K (#) G) = Sum(q) by RLVECT_2:7;
A39: f9.len q9 is Element of V;
f9.0 = 0.V by A24,ZMODUL01:26;
hence thesis
by A7,A16,A12,A9,A37,A38,A23,A26,A39,RLVECT_1:def 12,XBOOLE_0:def 10;
end;
theorem RL5Th12:
for K being Z_Linear_Combination of W holds
ex L being Z_Linear_Combination of V st
Carrier(K) = Carrier(L) & Sum(K) = Sum(L)
proof
let K be Z_Linear_Combination of W;
defpred P[set, set] means ($1 in W & $2 = K.$1) or (not $1 in W & $2 = 0);
reconsider K9= K as Function of the carrier of W, INT;
A1: the carrier of W c= the carrier of V by ZMODUL01:def 9;
then reconsider C = Carrier(K) as finite Subset of V by XBOOLE_1:1;
A2: for x st x in the carrier of V ex y st y in INT & P[x, y]
proof
let x;
assume x in the carrier of V;
then reconsider x as VECTOR of V;
per cases;
suppose
A3: x in W;
then reconsider x as VECTOR of W by STRUCT_0:def 5;
P[x, K.x] by A3;
hence thesis;
end;
suppose
B1: not x in W;
0 in INT by INT_1:def 2;
hence thesis by B1;
end;
end;
ex L being Function of the carrier of V, INT st for x st x in the
carrier of V holds P[x, L.x] from FUNCT_2:sch 1(A2);
then consider L being Function of the carrier of V, INT such that
A4: for x st x in the carrier of V holds P[x, L.x];
A5:
now
let v be VECTOR of V;
assume not v in C;
then P[v, K.v] & not v in C & v in the carrier of W or P[v, 0]
by STRUCT_0:def 5;
then P[v, K.v] & K.v = 0 or P[v, 0];
hence L.v = 0 by A4;
end;
L is Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
then reconsider L as Z_Linear_Combination of V by A5,ZMODUL02:def 18;
reconsider L9= L|the carrier of W as Function of the carrier of W, INT
by A1,FUNCT_2:32;
take L;
now
let x be element;
assume that
A6: x in Carrier(L) and
A7: not x in the carrier of W;
consider v being VECTOR of V such that
A8: x = v and
A9: L.v <> 0 by A6;
P[v, 0] by A7,A8,STRUCT_0:def 5;
hence contradiction by A4,A9;
end;
then
A10: Carrier(L) c= the carrier of W by TARSKI:def 3;
now
let x be set;
assume
A11: x in the carrier of W;
then P[x, L.x] by A4,A1;
hence K9.x = L9.x by A11,FUNCT_1:49,STRUCT_0:def 5;
end;
then K9 = L9 by FUNCT_2:12;
hence thesis by A10,RL5Th11;
end;
theorem RL5Th13:
for L being Z_Linear_Combination of V st
Carrier(L) c= the carrier of W
ex K being Z_Linear_Combination of W
st Carrier(K) = Carrier(L) & Sum(K) = Sum (L)
proof
let L be Z_Linear_Combination of V;
assume A1: Carrier(L) c= the carrier of W;
then reconsider C = Carrier(L) as finite Subset of W;
the carrier of W c= the carrier of V by ZMODUL01:def 9;
then reconsider K = L|the carrier of W as
Function of the carrier of W, INT by FUNCT_2:32;
A2: K is Element of Funcs(the carrier of W, INT) by FUNCT_2:8;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now
let w be VECTOR of W;
A4: w is VECTOR of V by ZMODUL01:25;
assume not w in C;
then L.w = 0 by A4;
hence K.w = 0 by A3,FUNCT_1:47;
end;
then reconsider K as Z_Linear_Combination of W by A2,ZMODUL02:def 18;
take K;
thus thesis by A1,RL5Th11;
end;
theorem RL5Th14:
for V being free Z_Module for I being Basis of V, v being VECTOR of V
holds v in Lin(I)
proof
let V be free Z_Module;
let I be Basis of V, v be VECTOR of V;
v in the Z_ModuleStruct of V by STRUCT_0:def 5;
hence thesis by RL3Def3;
end;
theorem
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
proof
let A be Subset of W;
the carrier of W c= the carrier of V by ZMODUL01:def 9;
then reconsider A9= A as Subset of V by XBOOLE_1:1;
assume A1: A is linearly-independent;
now
assume A9 is linearly-dependent;
then consider L being Z_Linear_Combination of A9 such that
A2: Sum(L) = 0.V and
A3: Carrier(L) <> {} by ZMODUL02:def 36;
Carrier(L) c= A by ZMODUL02:def 21;
then consider LW being Z_Linear_Combination of W such that
A4: Carrier(LW) = Carrier(L) and
A5: Sum(LW) = Sum(L) by RL5Th13,XBOOLE_1:1;
reconsider LW as Z_Linear_Combination of A by A4,ZMODUL02:def 21;
Sum(LW) = 0.W by A2,A5,ZMODUL01:26;
hence contradiction by A1,A3,A4,ZMODUL02:def 36;
end;
hence thesis;
end;
theorem RL5Th16:
for A being Subset of V st A is linearly-independent &
A c= the carrier of W holds A is linearly-independent Subset of W
proof
let A be Subset of V such that
A1: A is linearly-independent and
A2: A c= the carrier of W;
reconsider A9 = A as Subset of W by A2;
now
assume A9 is linearly-dependent;
then consider K being Z_Linear_Combination of A9 such that
A3: Sum(K) = 0.W and
A4: Carrier(K) <> {} by ZMODUL02:def 36;
consider L being Z_Linear_Combination of V such that
A5: Carrier(L) = Carrier(K) and
A6: Sum(L) = Sum(K) by RL5Th12;
reconsider L as Z_Linear_Combination of A by A5,ZMODUL02:def 21;
Sum(L) = 0.V by A3,A6,ZMODUL01:26;
hence contradiction by A1,A4,A5,ZMODUL02:def 36;
end;
hence thesis;
end;
theorem RL5Th18:
for V being Z_Module
for A being Subset of V st A is linearly-independent
for v being VECTOR of V st v in A for B being Subset of V st B = A \ {v}
holds not v in Lin(B)
proof
let V be Z_Module;
let A be Subset of V such that
A1: A is linearly-independent;
let v be VECTOR of V;
assume v in A; then
A2: {v} is Subset of A by SUBSET_1:41;
v in {v} by TARSKI:def 1;
then v in Lin({v}) by ZMODUL02:65;
then consider K being Z_Linear_Combination of {v} such that
A3: v = Sum(K) by ZMODUL02:64;
let B be Subset of V such that
A4: B = A \ {v};
B c= A by A4,XBOOLE_1:36;
then
A5: B \/ {v} c= A \/ A by A2,XBOOLE_1:13;
assume v in Lin(B);
then consider L being Z_Linear_Combination of B such that
A6: v = Sum(L) by ZMODUL02:64;
A7: Carrier(L) c= B & Carrier(K) c= {v} by ZMODUL02:def 21;
then Carrier(L) \/ Carrier(K) c= B \/ {v} by XBOOLE_1:13;
then Carrier(L - K) c= Carrier(L) \/ Carrier(K) & Carrier(L) \/ Carrier(K)
c= A by A5,ZMODUL02:40,XBOOLE_1:1;
then
A8: L - K is Z_Linear_Combination of A by XBOOLE_1:1,ZMODUL02:def 21;
A9: for x being VECTOR of V holds x in Carrier(L) implies K.x = 0
proof
let x be VECTOR of V;
assume x in Carrier(L);
then not x in Carrier(K) by A4,A7,XBOOLE_0:def 5;
hence thesis;
end;
A10:
now
let x be set such that
A11: x in Carrier(L) and
A12: not x in Carrier(L - K);
reconsider x as VECTOR of V by A11;
A13: L.x <> 0 by A11,ZMODUL02:8;
(L - K).x = L.x - K.x by ZMODUL02:39
.= L.x - 0 by A9,A11
.= L.x;
hence contradiction by A12,A13;
end;
v <> 0.V by A1,A2,ZMODUL02:56;
then Carrier(L) is non empty by A6,ZMODUL02:23;
then ex w being set st w in Carrier(L) by XBOOLE_0:def 1;
then
A14: Carrier(L - K) is non empty by A10;
0.V = Sum(L) + (- Sum(K)) by A6,A3,RLVECT_1:5
.= Sum(L) + Sum(-K) by ZMODUL02:54
.= Sum(L - K) by ZMODUL02:52;
hence contradiction by A1,A8,A14,ZMODUL02:def 36;
end;
theorem RL5Th19:
for V being free Z_Module for I being Basis of V
for A being non empty Subset of V st A misses I
for B being Subset of V st B = I \/ A holds B is linearly-dependent
proof
let V be free Z_Module;
let I be Basis of V;
let A be non empty Subset of V such that
A1: A misses I;
consider v being set such that
A2: v in A by XBOOLE_0:def 1;
let B be Subset of V such that
A3: B = I \/ A;
A4: A c= B by A3,XBOOLE_1:7;
reconsider v as VECTOR of V by A2;
reconsider Bv = B \ {v} as Subset of V;
A5: I \ {v} c= B \ {v} by A3,XBOOLE_1:7,33;
not v in I by A1,A2,XBOOLE_0:3;
then I c= Bv by A5,ZFMISC_1:57;
then
A6: Lin(I) is Submodule of Lin(Bv) by ZMODUL02:70;
assume A7: B is linearly-independent;
v in Lin(I) by RL5Th14;
hence contradiction by A7,A2,A4,A6,RL5Th18,ZMODUL01:23;
end;
theorem
for A being Subset of V st A c= the carrier of W holds
Lin(A) is Submodule of W
proof
let A be Subset of V;
assume A1: A c= the carrier of W;
now
let w be element;
assume w in the carrier of Lin(A);
then consider L being Z_Linear_Combination of A such that
A2: w = Sum(L) by STRUCT_0:def 5,ZMODUL02:64;
Carrier(L) c= A by ZMODUL02:def 21;
then
ex K being Z_Linear_Combination of W st Carrier(K) = Carrier (L) & Sum(L)
= Sum(K) by A1,RL5Th13,XBOOLE_1:1;
hence w in the carrier of W by A2;
end;
hence thesis by TARSKI:def 3,ZMODUL01:43;
end;
theorem RL5Th21:
for A being Subset of V, B being Subset of W st A = B holds Lin(A) = Lin(B)
proof
let A be Subset of V, B be Subset of W;
reconsider B9= Lin(B), V9= V as Z_Module;
A1: B9 is Submodule of V9 by ZMODUL01:42;
assume A2: A = B;
now
let x be element;
assume x in the carrier of Lin(A);
then consider L being Z_Linear_Combination of A such that
A3: x = Sum(L) by STRUCT_0:def 5,ZMODUL02:64;
Carrier(L) c= A by ZMODUL02:def 21;
then consider K being Z_Linear_Combination of W such that
A4: Carrier(K) = Carrier(L) and
A5: Sum(K) = Sum(L) by A2,RL5Th13,XBOOLE_1:1;
reconsider K as Z_Linear_Combination of B by A2,A4,ZMODUL02:def 21;
x = Sum(K) by A3,A5;
hence x in the carrier of Lin(B) by STRUCT_0:def 5,ZMODUL02:64;
end;
then
A6: the carrier of Lin(A) c= the carrier of Lin(B) by TARSKI:def 3;
now
let x be element;
assume x in the carrier of Lin(B);
then consider K being Z_Linear_Combination of B such that
A7: x = Sum(K) by STRUCT_0:def 5,ZMODUL02:64;
consider L being Z_Linear_Combination of V such that
A8: Carrier(L) = Carrier(K) and
A9: Sum(L) = Sum(K) by RL5Th12;
reconsider L as Z_Linear_Combination of A by A2,A8,ZMODUL02:def 21;
x = Sum(L) by A7,A9;
hence x in the carrier of Lin(A) by STRUCT_0:def 5,ZMODUL02:64;
end;
then the carrier of Lin(B) c= the carrier of Lin(A) by TARSKI:def 3;
hence thesis by A1,A6,XBOOLE_0:def 10,ZMODUL01:45;
end;
registration
let V be Z_Module, A be linearly-independent Subset of V;
cluster Lin(A) -> free;
correctness
proof
ex B being Subset of Lin(A)
st B is linearly-independent & Lin(B) = the Z_ModuleStruct of Lin(A)
proof
for x be element holds x in A implies x in the carrier of Lin(A)
by STRUCT_0:def 5,ZMODUL02:65;
then reconsider B = A as linearly-independent Subset of Lin(A)
by RL5Th16,TARSKI:def 3;
take B;
thus thesis by RL5Th21;
end;
hence thesis by DefFree;
end;
end;
registration
let V be free Z_Module;
cluster (Omega).V -> strict free;
coherence
proof
reconsider VV = (Omega).V as Z_Module;
consider A being Subset of V such that
A1: A is linearly-independent & Lin(A) = the Z_ModuleStruct of V
by DefFree;
ex AA being Subset of VV
st AA is linearly-independent & Lin(AA) = the Z_ModuleStruct of VV
proof
consider AA being Subset of VV such that
A5: AA = A;
take AA;
thus thesis by A1,A5,RL5Th16,RL5Th21;
end;
hence thesis;
end;
end;
begin :: Finite-rank free Z-module
definition
let IT be free Z_Module;
attr IT is finite-rank means :DefFR:
ex A being finite Subset of IT st A is Basis of IT;
end;
registration let V;
cluster (0).V -> finite-rank;
coherence
proof
reconsider VV = (0).V as free Z_Module;
ex A being finite Subset of VV st A is Basis of VV
proof
set WW = {}(the carrier of VV);
reconsider WW as Subset of VV;
B2: Lin(WW) = (0).VV by ZMODUL02:67
.= VV by ZMODUL01:51;
reconsider WW as finite Subset of VV;
take WW;
thus thesis by B2,RL3Def3,ZMODUL02:58;
end;
hence thesis by DefFR;
end;
end;
registration
cluster strict finite-rank for free Z_Module;
existence
proof
set V = the Z_Module;
take (0).V;
thus thesis;
end;
end;
registration
let V be Z_Module;
cluster strict finite-rank for free Submodule of V;
existence
proof
reconsider W = (0).V as strict free Submodule of V;
take W;
thus thesis;
end;
end;
registration
let V be Z_Module, A be finite linearly-independent Subset of V;
cluster Lin(A) -> finite-rank;
coherence
proof
ex AA being finite Subset of Lin(A) st AA is Basis of Lin(A)
proof
for x be element holds x in A implies x in the carrier of Lin(A)
by STRUCT_0:def 5,ZMODUL02:65;
then reconsider AA = A as finite linearly-independent Subset of Lin(A)
by RL5Th16,TARSKI:def 3;
take AA;
Lin(A) = Lin(AA) by RL5Th21;
hence thesis by RL3Def3;
end;
hence thesis by DefFR;
end;
end;
definition
let V be Z_Module;
attr V is finitely-generated means :DefFG:
ex A being finite Subset of V st Lin(A) = the Z_ModuleStruct of V;
end;
registration let V;
cluster (0).V -> finitely-generated;
coherence
proof
set W = (0).V;
reconsider W as Z_Module;
set A = {}(the carrier of W);
reconsider A as Subset of W;
Lin(A) = (0).W by ZMODUL02:67
.= (0).V by ZMODUL01:51;
hence thesis by DefFG;
end;
end;
registration
cluster strict finitely-generated free for Z_Module;
existence
proof
set V = the Z_Module;
take (0).V;
thus thesis;
end;
end;
registration let V be finite-rank free Z_Module;
cluster -> finite for Basis of V;
coherence
proof
consider A being finite Subset of V such that
A1: A is Basis of V by DefFR;
let B be Basis of V;
consider p being FinSequence such that
A2: rng p = A by FINSEQ_1:52;
reconsider p as FinSequence of V by A2,FINSEQ_1:def 4;
set Car = {Carrier(L) where L is Z_Linear_Combination of B:
ex i be Element of NAT st i in dom p & Sum(L) = p.i};
set C = union Car;
A3: C c= B
proof
let x be element;
assume x in C;
then consider R being set such that
A4: x in R and
A5: R in Car by TARSKI:def 4;
ex L being Z_Linear_Combination of B st R = Carrier(L) &
ex i be Element of NAT st i in dom p & Sum(L) = p.i by A5;
then R c= B by ZMODUL02:def 21;
hence thesis by A4;
end;
then reconsider C as Subset of V by XBOOLE_1:1;
AA10: for v being VECTOR of V holds v in (Omega).V iff v in Lin(C)
proof
let v be VECTOR of V;
hereby
assume v in (Omega).V;
then v in Lin(A) by A1,RL3Def3;
then consider LA being Z_Linear_Combination of A such that
A6: v = Sum(LA) by ZMODUL02:64;
Carrier(LA) c= the carrier of Lin(C)
proof
let w be element;
assume A7: w in Carrier(LA);
then reconsider w9= w as VECTOR of V;
w9 in Lin(B) by RL5Th14;
then consider LB being Z_Linear_Combination of B such that
A8: w = Sum(LB) by ZMODUL02:64;
Carrier(LA) c= A by ZMODUL02:def 21;
then ex i being set st i in dom p & w = p.i by A2,A7,FUNCT_1:def 3;
then
A9: Carrier(LB) in Car by A8;
Carrier(LB) c= C
proof
let x be element;
assume x in Carrier(LB);
hence thesis by A9,TARSKI:def 4;
end;
then LB is Z_Linear_Combination of C by ZMODUL02:def 21;
hence thesis by A8,STRUCT_0:def 5,ZMODUL02:64;
end;
then ex LC being Z_Linear_Combination of C
st Sum(LA) = Sum(LC) by RL5Th10;
hence v in Lin(C) by A6,ZMODUL02:64;
end;
assume v in Lin(C);
thus thesis by STRUCT_0:def 5;
end;
A11: B is linearly-independent by RL3Def3;
C is linearly-independent by A3,RL3Def3,ZMODUL02:56;
then
A12: C is Basis of V by AA10,RL3Def3,ZMODUL01:46;
B c= C
proof
set D = B \ C;
assume not B c= C;
then ex v being element st v in B & not v in C by TARSKI:def 3;
then reconsider D as non empty Subset of V by XBOOLE_0:def 5;
reconsider B as Subset of V;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3,XBOOLE_1:12;
then B = C \/ D;
hence contradiction by A11,A12,RL5Th19,XBOOLE_1:79;
end; then
A13: B = C by A3,XBOOLE_0:def 10;
defpred P[set, set] means ex L being Z_Linear_Combination of B st
$2 = Carrier(L) & Sum(L) = p.$1;
A14: for i be Nat st i in Seg len p ex x st P[i, x]
proof
let i be Nat;
assume i in Seg len p;
then i in dom p by FINSEQ_1:def 3;
then p.i in the carrier of V by FINSEQ_2:11;
then p.i in Lin(B) by RL5Th14;
then consider L being Z_Linear_Combination of B such that
A15: p.i = Sum(L) by ZMODUL02:64;
P[i, Carrier(L)] by A15;
hence thesis;
end;
ex q being FinSequence st dom q = Seg len p & for i be Nat st i in Seg
len p holds P[i, q.i] from FINSEQ_1:sch 1(A14);
then consider q being FinSequence such that
A16: dom q = Seg len p and
A17: for i be Nat st i in Seg len p holds P[i, q.i];
A18: dom p = dom q by A16,FINSEQ_1:def 3;
A19: for i be Nat, y1, y2 st i in Seg len p & P[i, y1] & P[i, y2]
holds y1 = y2
proof
let i be Nat, y1, y2;
assume that
i in Seg len p and
A20: P[i, y1] and
A21: P[i, y2];
consider L1 being Z_Linear_Combination of B such that
A22: y1 = Carrier(L1) & Sum(L1) = p.i by A20;
consider L2 being Z_Linear_Combination of B such that
A23: y2 = Carrier(L2) & Sum(L2) = p.i by A21;
Carrier(L1) c= B & Carrier(L2) c= B by ZMODUL02:def 21;
hence thesis by A22,A23,RL3Def3,RL5Th1;
end;
now
let x be element;
assume x in Car;
then consider L being Z_Linear_Combination of B such that
A24: x = Carrier(L) and
A25: ex i be Element of NAT st i in dom p & Sum(L) = p.i;
consider i be Element of NAT such that
A26: i in dom p and
A27: Sum(L) = p.i by A25;
P[i, q.i] by A16,A17,A18,A26;
then x = q.i by A19,A16,A18,A24,A26,A27;
hence x in rng q by A18,A26,FUNCT_1:def 3;
end;
then
A28: Car c= rng q by TARSKI:def 3;
for R being set st R in Car holds R is finite
proof
let R be set;
assume R in Car;
then ex L being Z_Linear_Combination of B st R = Carrier(L) &
ex i be Element of NAT st i in dom p & Sum(L) = p.i;
hence thesis;
end;
hence thesis by A13,A28,FINSET_1:7;
end;
end;
begin :: Rank of a finite-rank free Z-module
theorem ThQuotBasis1:
for p being Prime, V being free Z_Module, I being Basis of V,
u1, u2 being VECTOR of V
st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV(V,p,u1) <> ZMtoMQV(V,p,u2)
proof
let p be Prime, V be free Z_Module, I be Basis of V,
u1, u2 be VECTOR of V such that
A2: u1 <> u2 & u1 in I & u2 in I;
set uq1 = ZMtoMQV(V,p,u1), uq2 = ZMtoMQV(V,p,u2);
assume AS: uq1 = uq2;
consider u be VECTOR of V such that
A4: u in p(*)V & u1 + u = u2 by AS,ZMODUL01:75;
A5: I is linearly-independent & Lin(I) = the Z_ModuleStruct of V
by RL3Def3;
u in p * V by A4,STRUCT_0:def 5;
then consider v be VECTOR of V such that
A6: u = p * v;
consider lv be Z_Linear_Combination of I such that
A7: v = Sum(lv) by A5,STRUCT_0:def 5,ZMODUL02:64;
consider lu1 be Z_Linear_Combination of V such that
B1: lu1.u1 = 1 & for v being VECTOR of V st v <> u1 holds lu1.v = 0
by ThLC1;
B2: Carrier(lu1) = {u1}
proof
for v being element holds v in Carrier(lu1) implies v in {u1}
proof
assume ex v being element st v in Carrier(lu1) & not v in {u1};
then consider v being VECTOR of V such that
D1: v in Carrier(lu1) & not v in {u1};
v <> u1 by D1,TARSKI:def 1;
then lu1.v = 0 by B1;
hence contradiction by D1,ZMODUL02:8;
end;
then C1: Carrier(lu1) c= {u1} by TARSKI:def 3;
u1 in Carrier(lu1) by B1;
then {u1} c= Carrier(lu1) by ZFMISC_1:31;
hence thesis by C1,XBOOLE_0:def 10;
end;
then B3: Sum(lu1) = 1 * u1 by B1,ZMODUL02:24
.= u1 by ZMODUL01:def 5;
reconsider lu1 as Z_Linear_Combination of {u1} by B2,ZMODUL02:def 21;
reconsider lu1 as Z_Linear_Combination of I by A2,ZFMISC_1:31,ZMODUL02:10;
consider lu2 be Z_Linear_Combination of V such that
B4: lu2.u2 = 1 & for v being VECTOR of V st v <> u2 holds lu2.v = 0
by ThLC1;
B5: Carrier(lu2) = {u2}
proof
for v being element holds v in Carrier(lu2) implies v in {u2}
proof
assume ex v being element st v in Carrier(lu2) & not v in {u2};
then consider v being VECTOR of V such that
D1: v in Carrier(lu2) & not v in {u2};
v <> u2 by D1,TARSKI:def 1;
then lu2.v = 0 by B4;
hence contradiction by D1,ZMODUL02:8;
end;
then C1: Carrier(lu2) c= {u2} by TARSKI:def 3;
u2 in Carrier(lu2) by B4;
then {u2} c= Carrier(lu2) by ZFMISC_1:31;
hence thesis by C1,XBOOLE_0:def 10;
end;
then B6: Sum(lu2) = 1 * u2 by B4,ZMODUL02:24
.= u2 by ZMODUL01:def 5;
reconsider lu2 as Z_Linear_Combination of {u2} by B5,ZMODUL02:def 21;
reconsider lu2 as Z_Linear_Combination of I by A2,ZFMISC_1:31,ZMODUL02:10;
A11: u = Sum(p * lv) by A6,A7,ZMODUL02:53;
A12: (p * lv).u1 <> -1
proof
assume AS1: (p * lv).u1 = -1;
-p < -1 & 0 > -1 by INT_2:def 4,XREAL_1:24;
then (-1) mod p = p + (-1) by NAT_D:63;
then (p * lv).u1 mod p = p - 1 by AS1;
then C1: (p * lv).u1 mod p <> 0 by INT_2:def 4;
C2: (p * lv).u1 = p * (lv.u1) by ZMODUL02:def 26;
p divides (p * lv).u1 - 0 by C2,INT_1:def 4,INT_1:60;
hence contradiction by C1,INT_1:62;
end;
p * lv is Z_Linear_Combination of I by ZMODUL02:31;
then lu1 + p * lv is Z_Linear_Combination of I by ZMODUL02:27;
then reconsider lx = lu1 + p * lv - lu2 as Z_Linear_Combination of I
by ZMODUL02:41;
A14: 0.V = Sum(lu1 + p * lv) - Sum(lu2)
by A4,A11,B3,B6,VECTSP_1:19,ZMODUL02:52
.= Sum(lx) by ZMODUL02:55;
A15: lx.u1 = (lu1 + p * lv).u1 - lu2.u1 by ZMODUL02:39
.= lu1.u1 + (p * lv).u1 - lu2.u1 by ZMODUL02:def 25
.= 1 + (p * lv).u1 - 0 by A2,B1,B4
.= 1 + (p * lv).u1;
lx.u1 <> 0 by A12,A15;
then u1 in Carrier(lx);
hence contradiction by A14,RL3Def3,ZMODUL02:def 36;
end;
theorem ThZMtoMQV1:
for p being Prime, V being Z_Module,
ZQ being VectSp of GF(p), vq being Vector of ZQ
st ZQ = Z_MQ_VectSp(V,p)
holds ex v being VECTOR of V st vq = ZMtoMQV(V,p,v)
proof
let p be Prime, V be Z_Module,
ZQ be VectSp of GF(p), vq be Vector of ZQ such that
A1: ZQ = Z_MQ_VectSp(V,p);
vq is Element of CosetSet(V,p(*)V) by A1,ZMODUL02:def 10;
then vq in {A where A is Coset of p(*)V: not contradiction};
then consider vqq be Coset of p(*)V such that
A2: vqq = vq;
consider v be VECTOR of V such that
A3: vq = v + p(*)V by A2,ZMODUL01:def 13;
take v;
thus thesis by A3;
end;
LMThZMtoMQV21:
for p being Prime, V being Z_Module, v, w being VECTOR of V
st ZMtoMQV(V, p, w) /\ ZMtoMQV(V,p,v) <> {}
holds ZMtoMQV(V,p,w) = ZMtoMQV(V,p,v)
proof
let p be Prime, V be Z_Module, v, w be VECTOR of V such that
A1: ZMtoMQV(V, p, w) /\ ZMtoMQV(V, p, v) <> {};
consider u being set such that
A2: u in ZMtoMQV(V, p, w) /\ ZMtoMQV(V, p, v) by A1,XBOOLE_0:def 1;
A3: u in ZMtoMQV(V, p, w) & u in ZMtoMQV(V, p, v) by A2,XBOOLE_0:def 4;
then reconsider u as VECTOR of V;
w + p(*)V = u + p(*)V by A3,ZMODUL01:67
.= v + p(*)V by A3,ZMODUL01:67;
hence thesis;
end;
theorem ThZMtoMQV2:
for p being Prime, V being Z_Module, I being Subset of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p)
holds ex l being Z_Linear_Combination of I
st for v being VECTOR of V st v in I holds
ex w be VECTOR of V st w in I & w in ZMtoMQV(V,p,v)
& l.w = lq.(ZMtoMQV(V,p,v))
proof
let p be Prime, V be Z_Module, I be Subset of V,
lq be Linear_Combination of Z_MQ_VectSp(V,p);
set ZQ = Z_MQ_VectSp(V,p);
per cases;
suppose CS1: I is empty;
set l = the Z_Linear_Combination of I;
take l;
thus thesis by CS1;
end;
suppose CS2: I is non empty;
set X = { ZMtoMQV(V,p,v) where v is VECTOR of V:v in I};
now let x be element;
assume x in X;
then consider v be VECTOR of V such that
A11: x = ZMtoMQV(V,p,v) & v in I;
thus x in the carrier of ZQ by A11;
end;
then
reconsider X as Subset of ZQ by TARSKI:def 3;
consider v0 be set such that D1: v0 in I by CS2,XBOOLE_0:def 1;
reconsider v0 as VECTOR of V by D1;
ZMtoMQV(V,p,v0) in X by D1;
then reconsider X as non empty Subset of ZQ;
defpred F0[Element of X, Element of V] means
$2 in $1 & $2 in I;
X2: for x being Element of X holds
ex v being Element of V st F0[x,v]
proof
let x be Element of X;
x in X;
then consider v be VECTOR of V such that
A1: x = ZMtoMQV(V,p,v) & v in I;
thus ex v be Element of V st F0[x,v] by A1,ZMODUL01:58;
end;
consider F being Function of X, the carrier of V such that
X3: for x being Element of X holds F0[x,F.x]
from FUNCT_2:sch 3(X2);
X5:
now let y be element;
assume y in rng F;
then consider x be set such that
W1: x in X & F.x = y by FUNCT_2:11;
reconsider x as Element of X by W1;
thus y in I by W1,X3;
end;
then
XX5: rng F c= I by TARSKI:def 3;
defpred P[Element of V, Element of GF(p)] means
($1 in rng F implies $2 = lq.(ZMtoMQV(V,p,$1))) &
(not $1 in rng F implies $2 = 0);
A2: for v being Element of V holds
ex y being Element of GF(p) st P[v,y]
proof
let v be Element of V;
per cases;
suppose B2: v in rng F;
reconsider y = lq.(ZMtoMQV(V,p,v)) as Element of GF(p);
take y;
thus thesis by B2;
end;
suppose B2: not v in rng F;
0.GF(p) is Element of GF(p);
then reconsider F0 = 0 as Element of GF(p) by EC_PF_1:11;
take F0;
thus thesis by B2;
end;
end;
A3: Segm(p) c= INT by NUMBERS:17,XBOOLE_1:1;
consider f being Function of the carrier of V, GF(p) such that
A4: for v being Element of V holds P[v,f.v] from FUNCT_2:sch 3(A2);
A20: for v being VECTOR of V st v in I holds
ex w be VECTOR of V st w in I & w in ZMtoMQV(V,p,v) &
f.w = lq.(ZMtoMQV(V,p,v))
proof
let v being VECTOR of V;
assume v in I;
then
D0: ZMtoMQV(V,p,v) in X;
then
D1: F.(ZMtoMQV(V,p,v)) in rng F by FUNCT_2:4;
reconsider w = F.(ZMtoMQV(V,p,v)) as Element of V by D0,FUNCT_2:5;
take w;
D2: f.w = lq.(ZMtoMQV(V,p,w)) by A4,D0,FUNCT_2:4;
thus w in I by D1,X5;
thus w in ZMtoMQV(V,p,v) by X3,D0;
thus f.w = lq.(ZMtoMQV(V,p,v)) by D0,D2,X3,ZMODUL01:67;
end;
reconsider l = f as Function of the carrier of V, INT by A3,FUNCT_2:7;
reconsider l as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
set T = {v where v is Element of V : l.v <> 0};
BB2:
now let v be element;
assume v in T;
then ex v1 being Element of V st v1 = v & l.v1 <> 0;
hence v in the carrier of V;
end;
R1:
now let x be element;
assume x in T;
then consider v be Element of V such that
R11: x = v & l.v <> 0;
thus x in rng F by A4,R11;
end;
then
RR1: T c= rng F by TARSKI:def 3;
now let x be element;
assume SS2: x in F"T;
then S2: x in X & F.x in T by FUNCT_2:38;
then consider v be Element of V such that
R11: F.x=v & l.v <> 0;
R12: P[v,f.v] by A4;
lq.(ZMtoMQV(V,p,v)) <> 0.GF(p) by R11,R12,EC_PF_1:11;
then
R15: ZMtoMQV(V,p,v) in Carrier(lq) by VECTSP_6:2;
reconsider w=x as Element of X by SS2;
R18: F.w in w & F.w in I by X3;
consider v1 be VECTOR of V such that
R19: w = ZMtoMQV(V,p,v1) & v1 in I by S2;
v in ZMtoMQV(V,p,v) by ZMODUL01:58;
then ZMtoMQV(V,p,v) /\ ZMtoMQV(V,p,v1) <> {}
by R11,R18,R19,XBOOLE_0:def 4;
hence x in Carrier(lq) by R15,R19,LMThZMtoMQV21;
end;
then F"T c= Carrier(lq) by TARSKI:def 3;
then reconsider T as finite Subset of V
by BB2,R1,FINSET_1:9,TARSKI:def 3;
for v being Element of V st not v in T holds l.v = 0;
then reconsider l as Z_Linear_Combination of V by ZMODUL02:def 18;
T = Carrier(l);
then reconsider l as Z_Linear_Combination of I
by RR1,XX5,XBOOLE_1:1,ZMODUL02:def 21;
take l;
now let v be VECTOR of V;
assume v in I;
then ex w be VECTOR of V st w in I & w in ZMtoMQV(V,p,v) &
f.w = lq.(ZMtoMQV(V,p,v)) by A20;
hence ex w be VECTOR of V st w in I & w in ZMtoMQV(V,p,v) &
l.w = lq.(ZMtoMQV(V,p,v));
end;
hence thesis;
end;
end;
theorem ThZMtoMQV2A:
for p being Prime, V being free Z_Module, I being Basis of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p)
holds ex l being Z_Linear_Combination of I
st for v being VECTOR of V st v in I holds
l.v = lq.(ZMtoMQV(V,p,v))
proof
let p being Prime, V being free Z_Module, I being Basis of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p);
consider l being Z_Linear_Combination of I such that
P1: for v being VECTOR of V st v in I holds
ex w be VECTOR of V st w in I & w in ZMtoMQV(V,p,v)
& l.w = lq.(ZMtoMQV(V,p,v)) by ThZMtoMQV2;
take l;
now let v be VECTOR of V;
assume P2:v in I;
then consider w be VECTOR of V such that
P3: w in I & w in ZMtoMQV(V,p,v)
& l.w = lq.(ZMtoMQV(V,p,v)) by P1;
ZMtoMQV(V,p,w) = ZMtoMQV(V,p,v) by P3,ZMODUL01:67;
hence l.v = lq.(ZMtoMQV(V,p,v)) by P2,P3,ThQuotBasis1;
end;
hence thesis;
end;
theorem ThQuotBasis2A:
for p being Prime, V being free Z_Module, I being Basis of V,
X be non empty Subset of Z_MQ_VectSp(V,p)
st X = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I} holds
ex F be Function of X, the carrier of V
st (for u be VECTOR of V st u in I holds F.(ZMtoMQV(V,p,u)) = u)
& F is one-to-one & dom F = X & rng F = I
proof
let p be Prime, V be free Z_Module, I be Basis of V,
X be non empty Subset of Z_MQ_VectSp(V,p);
assume AS1: X = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
set ZQ = Z_MQ_VectSp(V,p);
defpred F0[Element of X, Element of V] means
$2 in $1 & $2 in I;
X2: for x being Element of X holds ex v being Element of V st F0[x,v]
proof
let x be Element of X;
x in X;
then consider v be VECTOR of V such that
A1: x = ZMtoMQV(V,p,v) & v in I by AS1;
thus ex v be Element of V st F0[x,v] by A1,ZMODUL01:58;
end;
consider F being Function of X, the carrier of V such that
X3: for x being Element of X holds F0[x,F.x] from FUNCT_2:sch 3(X2);
take F;
thus for v be VECTOR of V st v in I holds F.(ZMtoMQV(V,p,v)) = v
proof
let v be VECTOR of V;
assume P2: v in I;
then ZMtoMQV(V,p,v) in X by AS1;
then reconsider w = ZMtoMQV(V,p,v) as Element of X;
P3: F.w in w & F.w in I by X3;
ZMtoMQV(V,p,F.w) = ZMtoMQV(V,p,v) by X3,ZMODUL01:67;
hence thesis by P2,P3,ThQuotBasis1;
end;
now let x1,x2 be set;
assume A1: x1 in X & x2 in X & F.x1=F.x2;
then reconsider x10=x1,x20=x2 as Element of X;
consider v1 be VECTOR of V such that
A6: x1 = ZMtoMQV(V,p,v1) & v1 in I by A1,AS1;
consider v2 be VECTOR of V such that
A7: x2 = ZMtoMQV(V,p,v2) & v2 in I by A1,AS1;
F.x10 in ZMtoMQV(V,p,v1) & F.x10 in ZMtoMQV(V,p,v2) by A1,A6,A7,X3;
then F.x10 in ZMtoMQV(V,p,v1) /\ ZMtoMQV(V,p,v2) by XBOOLE_0:def 4;
hence x1 = x2 by A6,A7,LMThZMtoMQV21;
end;
hence F is one-to-one by FUNCT_2:19;
thus dom F = X by FUNCT_2:def 1;
now let y be element;
assume y in rng F;
then consider x be set such that
W1: x in X & F.x = y by FUNCT_2:11;
reconsider x as Element of X by W1;
thus y in I by W1,X3;
end;
then
X5: rng F c= I by TARSKI:def 3;
now let y be element;
assume X6:y in I;
then reconsider u=y as VECTOR of V;
ZMtoMQV(V,p,u) in X by X6,AS1;
then reconsider z = ZMtoMQV(V,p,u) as Element of X;
A3: F.z in z & F.z in I by X3;
ZMtoMQV(V,p,F.z) = ZMtoMQV(V,p,u) by X3,ZMODUL01:67;
then F.z = u by ThQuotBasis1,A3,X6;
hence y in rng F by FUNCT_2:4;
end;
then I c= rng F by TARSKI:def 3;
hence I = rng F by X5,XBOOLE_0:def 10;
end;
theorem ThQuotBasis2:
for p being Prime, V being free Z_Module, I being Basis of V holds
card ( {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I} )
= card(I)
proof
let p be Prime, V be free Z_Module, I be Basis of V;
set X = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
set ZQ = Z_MQ_VectSp(V,p);
per cases;
suppose A1: I is empty;
X = {}
proof
assume X <> {};
then consider v0 be set such that
D1: v0 in X by XBOOLE_0:def 1;
consider u be VECTOR of V such that
D2: v0=ZMtoMQV(V,p,u) & u in I by D1;
thus contradiction by D2,A1;
end;
hence thesis by A1;
end;
suppose A0: I is non empty;
now let x be element;
assume x in X;
then consider v be VECTOR of V such that
A11: x = ZMtoMQV(V,p,v) & v in I;
thus x in the carrier of ZQ by A11;
end;
then reconsider X as Subset of ZQ by TARSKI:def 3;
consider v0 be set such that D1: v0 in I by A0,XBOOLE_0:def 1;
reconsider v0 as VECTOR of V by D1;
ZMtoMQV(V,p,v0) in X by D1;
then reconsider X as non empty Subset of ZQ;
consider F be Function of X, the carrier of V such that
XX1: (for u be VECTOR of V st u in I holds F.(ZMtoMQV(V,p,u)) = u)
& F is one-to-one & dom F = X & rng F = I by ThQuotBasis2A;
thus thesis by XX1,CARD_1:5,WELLORD2:def 4;
end;
end;
theorem ThZMtoMQVC:
for p being Prime, V being free Z_Module holds
ZMtoMQV(V,p,0. V) = 0.(Z_MQ_VectSp(V,p))
proof
let p be Prime, V be free Z_Module;
thus 0.(Z_MQ_VectSp(V,p)) = 0.(Z_ModuleQuot(V,p(*)V))
.= zeroCoset(V,p(*)V) by ZMODUL02:def 10
.= ZMtoMQV(V,p,0. V) by ZMODUL01:59;
end;
theorem ThZMtoMQVD:
for p being Prime, V being free Z_Module,
s,t be Element of V holds
ZMtoMQV(V,p,s)+ZMtoMQV(V,p,t) = ZMtoMQV(V,p,s+t)
proof
let p be Prime, V be free Z_Module, s, t be Element of V;
set s1 = ZMtoMQV(V,p,s), t1 = ZMtoMQV(V,p,t);
P1: ZMtoMQV(V,p,s) = s + p(*)V;
P2: ZMtoMQV(V,p,t) = t + p(*)V;
Q1: s + p(*)V is Element of CosetSet(V,p(*)V) by P1,ZMODUL02:def 10;
Q2: t + p(*)V is Element of CosetSet(V,p(*)V) by P2,ZMODUL02:def 10;
thus s1+t1 = addCoset(V,p(*)V).(s + p(*)V,t + p(*)V) by ZMODUL02:def 10
.= ZMtoMQV(V,p,s+t) by Q1,Q2,ZMODUL02:def 7;
end;
theorem ThZMtoMQVA:
for p being Prime, V being free Z_Module,
s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p)
st len s = len t & for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & t.i = ZMtoMQV(V,p,si) holds
Sum(t) = ZMtoMQV(V,p,Sum(s))
proof
let p be Prime, V be free Z_Module;
defpred P[Element of NAT] means
for s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p)
st len s = $1 & len s = len t
& for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & t.i = ZMtoMQV(V,p,si) holds Sum(t) = ZMtoMQV(V,p,Sum(s));
P0: P[ 0 ]
proof
let s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p);
assume that AS1: len s = 0 & len s = len t and
for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & t.i = ZMtoMQV(V,p,si);
s = <*>(the carrier of V) by AS1;
then Sum(s) = 0. V by RLVECT_1:43;
then
P1: ZMtoMQV(V,p,Sum(s)) = 0.(Z_MQ_VectSp(V,p)) by ThZMtoMQVC;
t = <*>(the carrier of (Z_MQ_VectSp(V,p))) by AS1;
hence thesis by P1,RLVECT_1:43;
end;
P1: for k be Element of NAT st P[k] holds P[k+1]
proof
let k be Element of NAT;
assume P2: P[k];
now let s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p);
assume that
AS1: len s = k+1 & len s = len t and
AS2: for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & t.i = ZMtoMQV(V,p,si);
reconsider s1 = s | k as FinSequence of V;
M0: dom s = Seg (k+1) by AS1,FINSEQ_1:def 3;
M1: dom t = Seg (k+1) by AS1,FINSEQ_1:def 3;
D02: len s1 = k by AS1,FINSEQ_1:59,NAT_1:11;
D01: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by AS1,FINSEQ_1:59,NAT_1:11;
then
D0: s1 = s |dom s1 by FINSEQ_1:def 15;
reconsider t1 = t | k as FinSequence of Z_MQ_VectSp(V,p);
D11:dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg k by AS1,FINSEQ_1:59,NAT_1:11;
then
D1: t1 = t |dom t1 by FINSEQ_1:def 15;
D12: len t1 = k by D11,FINSEQ_1:def 3;
s.(len s) in rng s by AS1,M0,FINSEQ_1:4,FUNCT_1:3;
then reconsider vs=s.(len s) as Element of V;
t.(len t) in rng t by AS1,M1,FINSEQ_1:4,FUNCT_1:3;
then reconsider vt = t.(len t) as Element of Z_MQ_VectSp(V,p);
P3: len s1 = k & len s1 = len t1 by D02,D11,FINSEQ_1:def 3;
P4: for i be Element of NAT
st i in dom s1 holds ex si be VECTOR of V
st si = s1.i & t1.i = ZMtoMQV(V,p,si)
proof
let i be Element of NAT;
assume P4: i in dom s1;
Seg k c= Seg (k+1) by FINSEQ_1:5,NAT_1:11;
then consider si be VECTOR of V such that
P9: si = s.i & t.i = ZMtoMQV(V,p,si) by AS2,D01,M0,P4;
take si;
thus si = s1.i by D0,P4,P9,FUNCT_1:49;
thus t1.i = ZMtoMQV(V,p,si) by D1,D01,D11,P4,P9,FUNCT_1:49;
end;
P5: Sum(t1) = ZMtoMQV(V,p,Sum(s1)) by P2,P3,P4;
P6: len s = len s1 + 1 by AS1,FINSEQ_1:59,NAT_1:11;
consider ssi be VECTOR of V such that
P9: ssi = s.(len s) & t.(len s) = ZMtoMQV(V,p,ssi)
by AS1,AS2,M0,FINSEQ_1:4;
thus Sum(t) = Sum(t1) + vt by AS1,D1,D12,RLVECT_1:38
.= ZMtoMQV(V,p,Sum(s1)+vs) by AS1,P5,P9,ThZMtoMQVD
.= ZMtoMQV(V,p,Sum(s)) by D0,P6,RLVECT_1:38;
end;
hence P[k+1];
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(P0,P1);
hence thesis;
end;
theorem ThZMtoMQVB:
for p being Prime, V being free Z_Module,
s be Element of V,
a be Integer,
b be Element of GF(p) st a = b holds
b*ZMtoMQV(V,p,s) = ZMtoMQV(V,p,a*s)
proof
let p be Prime, V be free Z_Module,
s be Element of V, a be Integer, b be Element of GF(p);
set t = ZMtoMQV(V,p,s);
assume AS: a=b;
P1: ZMtoMQV(V,p,s) = s + p(*)V;
reconsider t1 = t as Element of Z_ModuleQuot(V,p(*)V);
Q1: s + p(*)V is Element of CosetSet(V,p(*)V) by P1,ZMODUL02:def 10;
reconsider i = b as Nat;
A1: b = i mod p by NAT_1:44,NAT_D:24;
reconsider i as Integer;
thus b*t =(i mod p) * t1 by ZMODUL02:def 11,A1
.= lmultCoset(V,p(*)V).((i mod p),s + p(*)V) by ZMODUL02:def 10
.= ZMtoMQV(V,p,a*s) by AS,A1,Q1,ZMODUL02:def 9;
end;
theorem ThZMtoMQV3:
for p being Prime, V being free Z_Module, I being Basis of V,
l being Z_Linear_Combination of I,
IQ being Subset of Z_MQ_VectSp(V,p),
lq being Linear_Combination of IQ
st IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I} &
(for v being VECTOR of V st v in I holds
l.v = lq.(ZMtoMQV(V,p,v)) ) holds
Sum(lq) = ZMtoMQV(V,p,Sum(l))
proof
let p be Prime, V be free Z_Module, I be Basis of V,
l be Z_Linear_Combination of I,
IQ be Subset of Z_MQ_VectSp(V,p),
lq be Linear_Combination of IQ such that
A1: IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
assume
AS: for v being VECTOR of V st v in I holds
l.v = lq.(ZMtoMQV(V,p,v));
per cases;
suppose CS1: I is empty;
IQ = {}
proof
assume IQ <> {};
then consider v0 be set such that
D1: v0 in IQ by XBOOLE_0:def 1;
consider u be VECTOR of V such that
D2: v0 = ZMtoMQV(V,p,u) & u in I by D1,A1;
thus contradiction by D2,CS1;
end;
then IQ = {}(the carrier of Z_MQ_VectSp(V,p));
then lq = ZeroLC(Z_MQ_VectSp(V,p)) by VECTSP_6:6;
then
X1:Sum(lq) = 0.(Z_MQ_VectSp(V,p)) by VECTSP_6:15;
I = {}(the carrier of V) by CS1;
then l = Z_ZeroLC(V) by ZMODUL02:12;
then Sum(l) = 0. V by ZMODUL02:19;
hence Sum(lq) = ZMtoMQV(V,p,Sum(l)) by X1,ThZMtoMQVC;
end;
suppose I is non empty; then
consider v0 be set such that
D1: v0 in I by XBOOLE_0:def 1;
reconsider v0 as VECTOR of V by D1;
ZMtoMQV(V,p,v0) in IQ by D1,A1;
then reconsider X = IQ as non empty Subset of Z_MQ_VectSp(V,p);
consider F be Function of X, the carrier of V such that
XX1: (for u be VECTOR of V st u in I holds F.(ZMtoMQV(V,p,u)) = u)
& F is one-to-one & dom F = X & rng F = I by ThQuotBasis2A,A1;
consider Gq be FinSequence of Z_MQ_VectSp(V,p) such that
P1: Gq is one-to-one & rng Gq = Carrier(lq) & Sum(lq) = Sum(lq (#) Gq)
by VECTSP_6:def 6;
set n = len Gq;
D1: dom Gq = Seg n by FINSEQ_1:def 3;
D2: Carrier(lq) c= X by VECTSP_6:def 4;
D4: dom (F*Gq) = Seg n by D1,P1,XX1,RELAT_1:27,VECTSP_6:def 4;
D6: rng (F*Gq) c= the carrier of V;
F*Gq is FinSequence by XX1,P1,FINSEQ_1:16,VECTSP_6:def 4;
then reconsider FGq = F*Gq as FinSequence of V by D6,FINSEQ_1:def 4;
for x be element holds x in rng FGq iff x in Carrier(l)
proof
let x be element;
hereby assume x in rng FGq;
then consider z be set such that
S1: z in dom (FGq) & x = FGq.z by FUNCT_1:def 3;
S2: x = F.(Gq.z) by S1,FUNCT_1:12;
S3: z in dom Gq & Gq.z in dom F by S1,FUNCT_1:11;
then consider u be VECTOR of V such that
S4: Gq.z = ZMtoMQV(V,p,u) & u in I by A1,XX1;
S5: F.(Gq.z) = u by XX1,S4;
consider w be Element of Z_MQ_VectSp(V,p) such that
S6: Gq.z = w & lq.w <> 0.(GF(p)) by P1,S3,FUNCT_1:3,VECTSP_6:1;
l.u <> 0.(GF(p)) by AS,S4,S6;
then l.u <> 0 by EC_PF_1:11;
hence x in Carrier(l) by S2,S5;
end;
assume T0: x in Carrier(l);
then reconsider u=x as VECTOR of V;
T1: l.u <> 0 by ZMODUL02:8,T0;
T2: Carrier(l) c= I by ZMODUL02:def 21;
then lq.(ZMtoMQV(V,p,u)) <> 0 by AS,T1,T0;
then lq.(ZMtoMQV(V,p,u)) <> 0.(GF(p)) by EC_PF_1:11;
then
X3: ZMtoMQV(V,p,u) in rng Gq by P1,VECTSP_6:2;
then consider z be set such that
T3: z in dom Gq & ZMtoMQV(V,p,u) =Gq.z by FUNCT_1:def 3;
T6: F.(Gq.z) = u by T0,T2,T3,XX1;
T7: z in dom (FGq) by D2,P1,T3,XX1,X3,FUNCT_1:11;
then FGq.z = u by FUNCT_1:12,T6;
hence x in rng FGq by T7,FUNCT_1:def 3;
end;
then rng FGq = Carrier(l) by TARSKI:2;
then
XX6: Sum(l) = Sum(l (#) FGq) by P1,XX1,ZMODUL02:def 23;
XX72A: len (l (#) FGq ) = len (FGq ) by ZMODUL02:def 22;
then
XX72B: len (l (#) FGq ) = n by D4,FINSEQ_1:def 3;
XX72D: len (lq (#) Gq) = n by VECTSP_6:def 5;
now let i be Element of NAT;
assume Y2: i in dom (l (#) FGq );
then i in Seg (len (FGq ) ) by XX72A,FINSEQ_1:def 3;
then
Y3: i in dom FGq by FINSEQ_1:def 3;
then FGq.i in rng FGq by FUNCT_1:3;
then reconsider v = FGq.i as Element of V;
Y4: (l (#) FGq ).i = (l.v)*v by Y3,ZMODUL02:13;
i in Seg n by XX72B,Y2,FINSEQ_1:def 3;
then
Y6: i in dom Gq by FINSEQ_1:def 3;
then YY7: Gq.i in rng Gq by FUNCT_1:3;
then
Y7: Gq.i in X by P1,D2;
reconsider w = Gq.i as Element of Z_MQ_VectSp(V,p) by YY7;
consider u be VECTOR of V such that
S4: Gq.i = ZMtoMQV(V,p,u) & u in I by A1,Y7;
F.(Gq.i) = u by XX1,S4;
then
SS9: v = u by Y3,FUNCT_1:12;
(lq (#) Gq).i = (lq.w)*w by Y6,VECTSP_6:8
.= ZMtoMQV(V,p,(l.v)*v) by AS,S4,SS9,ThZMtoMQVB;
hence ex si be VECTOR of V st si=(l (#) FGq ).i &
(lq (#) Gq).i = ZMtoMQV(V,p,si) by Y4;
end;
hence Sum(lq) = ZMtoMQV(V,p,Sum(l)) by P1,XX6,XX72B,XX72D,ThZMtoMQVA;
end;
end;
theorem ThQuotBasis3:
for p being Prime, V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p)
st IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I}
holds IQ is linearly-independent
proof
let p be Prime, V be free Z_Module, I be Basis of V,
IQ be Subset of Z_MQ_VectSp(V,p) such that
A2: IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
assume not IQ is linearly-independent;
then consider lq being Linear_Combination of IQ such that
A3: Sum(lq) = 0.Z_MQ_VectSp(V,p) and
A4: Carrier(lq) <> {} by VECTSP_7:def 1;
consider Lq being Linear_Combination of Z_MQ_VectSp(V,p) such that
A5: Lq = lq;
consider l being Z_Linear_Combination of I such that
A6: for v being VECTOR of V st v in I holds
l.v = Lq.(ZMtoMQV(V,p,v)) by ThZMtoMQV2A;
set vq0 = Sum(Lq);
set v0 = Sum(l);
A11: vq0 = ZMtoMQV(V,p,v0) by A2,A6,A5,ThZMtoMQV3;
A12: vq0 = 0.(Z_ModuleQuot(V,p(*)V)) by A3,A5
.= zeroCoset(V,p(*)V) by ZMODUL02:def 10
.= 0.V + p(*)V by ZMODUL01:59;
consider vp being VECTOR of V such that
A13: vp in p(*)V & v0 + vp = 0.V by A11,A12,ZMODUL01:75;
vp in {p * v where v is Element of V : not contradiction}
by A13,STRUCT_0:def 5;
then consider vv being Element of V such that
A14: vp = p * vv;
A15: I is linearly-independent & Lin(I) = the Z_ModuleStruct of V
by RL3Def3;
consider lvv be Z_Linear_Combination of I such that
A16: vv = Sum(lvv) by A15,ZMODUL02:64,STRUCT_0:def 5;
vp = Sum(p * lvv) by A14,A16,ZMODUL02:53; then
A17: 0.V = Sum(l + p * lvv) by A13,ZMODUL02:52;
p * lvv is Z_Linear_Combination of I by ZMODUL02:31;
then l + p * lvv is Z_Linear_Combination of I by ZMODUL02:27;
then consider lpv being Z_Linear_Combination of I such that
B1: lpv = l + p * lvv;
ex vq being set st vq in Carrier(lq) by A4,XBOOLE_0:def 1;
then consider uq being Vector of Z_MQ_VectSp(V,p) such that
B3: uq in Carrier(lq);
uq in {v where v is Element of Z_MQ_VectSp(V,p) : lq.v <> 0.GF(p)}
by B3,VECTSP_6:def 2;
then consider uuq being Vector of Z_MQ_VectSp(V,p) such that
A18: uuq = uq & lq.uuq <> 0.GF(p);
A19: lq.uuq <> 0 by A18,EC_PF_1:11;
Carrier(lq) c= IQ by VECTSP_6:def 4;
then uq in IQ by B3;
then consider uu being VECTOR of V such that
A20: uq = ZMtoMQV(V, p, uu) & uu in I by A2;
A22: lq.uuq = l.uu by A5,A6,A18,A20;
lpv.uu <> 0
proof
assume AS1: lpv.uu = 0;
(l+p * lvv).uu = l.uu + (p*lvv).uu by ZMODUL02:def 25
.= l.uu + p * (lvv.uu) by ZMODUL02:def 26;
then l.uu = p* (-lvv.uu ) by AS1,B1;
then p divides l.uu by INT_1:def 3;
then X1: l.uu mod p = 0 by INT_1:62;
thus contradiction by A19,A22,X1,NAT_1:44,NAT_D:63;
end;
then uu in Carrier(lpv);
hence contradiction by A17,B1,RL3Def3,ZMODUL02:def 36;
end;
LMX1: for p being Prime, i be Element of INT
holds i mod p is Element of GF(p)
proof
let p be Prime, i be Element of INT;
(i mod p) in NAT by INT_1:3,INT_1:57;
hence thesis by INT_1:58,NAT_1:44;
end;
LMX2: for p being Prime, V being free Z_Module,
i be Integer, v be Element of V
holds ZMtoMQV(V,p,(i mod p) *v) = ZMtoMQV(V,p,i*v)
proof
let p be Prime, V be free Z_Module,
i be Integer, v be Element of V;
i is Element of INT by INT_1:def 2;
then reconsider a = (i mod p) as Element of GF(p) by LMX1;
reconsider t1 = ZMtoMQV(V,p,v) as Element of Z_ModuleQuot(V,p(*)V);
ZMtoMQV(V,p,v) = v + p(*)V; then
Q1: v + p(*)V is Element of CosetSet(V,p(*)V) by ZMODUL02:def 10;
thus ZMtoMQV(V,p,(i mod p) *v) = a*ZMtoMQV(V,p,v) by ThZMtoMQVB
.= (i mod p) * t1 by ZMODUL02:def 11
.= i*t1 by ZMODUL02:2
.= lmultCoset(V,p(*)V).(i,v + p(*)V) by ZMODUL02:def 10
.= ZMtoMQV(V,p,i*v) by Q1,ZMODUL02:def 9;
end;
theorem ThZMtoMQVAD:
for p being Prime, V being free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V,p)
st IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I} holds
(for s be FinSequence of V
st (for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si=s.i & ZMtoMQV(V,p,si) in Lin(IQ))
holds ZMtoMQV(V,p,Sum(s)) in Lin(IQ))
proof
let p be Prime, V be free Z_Module, I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V,p);
assume IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
defpred P[Element of NAT] means
for s be FinSequence of V st len s = $1
& ( for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & ZMtoMQV(V,p,si) in Lin(IQ) ) holds
ZMtoMQV(V,p,Sum(s)) in Lin(IQ);
P0: P[ 0 ]
proof
let s be FinSequence of V;
assume that AS1: len s = 0 and
for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & ZMtoMQV(V,p,si) in Lin(IQ);
s = <*>(the carrier of V) by AS1;
then Sum(s) = 0. V by RLVECT_1:43;
then ZMtoMQV(V,p,Sum(s)) = 0.(Z_MQ_VectSp(V,p)) by ThZMtoMQVC;
hence thesis by VECTSP_4:17;
end;
P1: for k be Element of NAT st P[k] holds P[k+1]
proof
let k be Element of NAT;
assume P2: P[k];
now let s be FinSequence of V;
assume that
AS1: len s = k+1 and
AS2: for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & ZMtoMQV(V,p,si) in Lin(IQ);
reconsider s1 = s | k as FinSequence of V;
M0: dom s = Seg (k+1) by AS1,FINSEQ_1:def 3;
D02: len s1 = k by AS1,FINSEQ_1:59,NAT_1:11;
D01: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by AS1,FINSEQ_1:59,NAT_1:11;
then
D0: s1 = s |dom s1 by FINSEQ_1:def 15;
s.(len s) in rng s by AS1,M0,FINSEQ_1:4,FUNCT_1:3;
then reconsider vs = s.(len s) as Element of V;
P3: len s1 = k by AS1,FINSEQ_1:59,NAT_1:11;
P4: for i be Element of NAT
st i in dom s1 holds ex si be VECTOR of V
st si = s1.i & ZMtoMQV(V,p,si) in Lin(IQ)
proof
let i be Element of NAT;
assume P4: i in dom s1;
Seg k c= Seg (k+1) by FINSEQ_1:5,NAT_1:11;
then consider si be VECTOR of V such that
P9: si = s.i & ZMtoMQV(V,p,si) in Lin(IQ) by AS2,D01,M0,P4;
take si;
thus si = s1.i by D0,P4,P9,FUNCT_1:49;
thus thesis by P9;
end;
P5: ZMtoMQV(V,p,Sum(s1)) in Lin(IQ) by P2,P3,P4;
consider ssi be VECTOR of V such that
P9: ssi = s.(len s) & ZMtoMQV(V,p,ssi) in Lin(IQ)
by AS1,AS2,M0,FINSEQ_1:4;
ZMtoMQV(V,p,Sum(s)) = ZMtoMQV(V,p,Sum(s1)+vs) by AS1,D0,D02,RLVECT_1:38
.= ZMtoMQV(V,p,Sum(s1)) + ZMtoMQV(V,p,vs) by ThZMtoMQVD;
hence ZMtoMQV(V,p,Sum(s)) in Lin(IQ) by P5,P9,VECTSP_4:20;
end;
hence P[k+1];
end;
G1: for k be Element of NAT holds P[k] from NAT_1:sch 1(P0,P1);
now let s be FinSequence of V;
assume A1: for i be Element of NAT
st i in dom s holds ex si be VECTOR of V
st si = s.i & ZMtoMQV(V,p,si) in Lin(IQ);
len s = len s;
hence ZMtoMQV(V,p,Sum(s)) in Lin(IQ) by G1,A1;
end;
hence thesis;
end;
theorem ThQuotBasis4A:
for p being Prime, V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p),
l be Z_Linear_Combination of I
st IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I} holds
ZMtoMQV(V,p,Sum(l)) in Lin(IQ)
proof
let p being Prime, V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p),
l be Z_Linear_Combination of I;
assume AS: IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
consider G be FinSequence of V such that
P1: G is one-to-one & rng G = Carrier(l)
& Sum(l) = Sum(l (#) G) by ZMODUL02:def 23;
now let i be Element of NAT;
assume i in dom (l (#) G );
then i in Seg (len (l (#) G )) by FINSEQ_1:def 3;
then i in Seg (len (G ) ) by ZMODUL02:def 22;
then
Y3: i in dom G by FINSEQ_1:def 3;
then G.i in rng G by FUNCT_1:3;
then reconsider v = G.i as Element of V;
Y5: (l (#) G ).i = (l.v)*v by Y3,ZMODUL02:13;
reconsider b = ( (l.v) mod p ) as Element of GF(p) by LMX1;
reconsider a = ( (l.v) mod p ) as Integer;
reconsider k = l.v as Integer;
reconsider t = ZMtoMQV(V,p,v) as Element of Z_MQ_VectSp(V,p);
Y7: b*t = ZMtoMQV(V,p, a*v) by ThZMtoMQVB
.= ZMtoMQV(V,p, k*v) by LMX2;
H1: v in Carrier(l) by Y3,P1,FUNCT_1:3;
Carrier(l) c= I by ZMODUL02:def 21;
then t in IQ by AS,H1;
then b*t in Lin(IQ) by VECTSP_4:21,VECTSP_7:8;
hence ex si be VECTOR of V
st si = (l (#) G ).i & ZMtoMQV(V,p,si) in Lin(IQ) by Y7,Y5;
end;
hence ZMtoMQV(V,p,Sum(l)) in Lin(IQ) by AS,P1,ThZMtoMQVAD;
end;
theorem ThQuotBasis4:
for p being Prime, V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p)
st IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I} holds
IQ is Basis of Z_MQ_VectSp(V,p)
proof
let p be Prime, V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p);
assume AS: IQ = {ZMtoMQV(V,p,u) where u is VECTOR of V : u in I};
P1: IQ is linearly-independent by ThQuotBasis3,AS;
for vq being Element of Z_MQ_VectSp(V,p) holds vq in Lin (IQ)
proof
let vq be Element of Z_MQ_VectSp(V,p);
consider v being VECTOR of V such that
P3: vq = ZMtoMQV(V,p,v) by ThZMtoMQV1;
Lin (I) = the Z_ModuleStruct of V by RL3Def3;
then consider l be Z_Linear_Combination of I such that
P4: v = Sum(l) by STRUCT_0:def 5,ZMODUL02:64;
thus vq in Lin(IQ) by AS,P4,P3,ThQuotBasis4A;
end;
hence thesis by P1,VECTSP_4:32,VECTSP_7:def 3;
end;
registration
let p be Prime, V be finite-rank free Z_Module;
cluster Z_MQ_VectSp(V,p) -> finite-dimensional;
coherence
proof
set W = Z_MQ_VectSp(V,p);
set A = the Basis of V;
set AQ = {ZMtoMQV(V, p, u) where u is VECTOR of V : u in A};
now let x be element;
assume x in AQ;
then ex u be VECTOR of V st x = ZMtoMQV(V, p, u) & u in A;
hence x in the carrier of Z_MQ_VectSp(V, p);
end;
then reconsider AQ as Subset of W by TARSKI:def 3;
card A = card AQ by ThQuotBasis2;
then AQ is finite Subset of W;
hence thesis by MATRLIN:def 1,ThQuotBasis4;
end;
end;
theorem RL5Th26:
for V be finite-rank free Z_Module
holds for A, B being Basis of V holds
card A = card B
proof
let V be finite-rank free Z_Module;
let A, B be Basis of V;
set p = the Prime;
set AQ = {ZMtoMQV(V, p, u) where u is VECTOR of V : u in A};
now let x be element;
assume x in AQ; then
ex u be VECTOR of V st x = ZMtoMQV(V, p, u) & u in A;
hence x in the carrier of Z_MQ_VectSp(V, p);
end;
then reconsider AQ as Subset of Z_MQ_VectSp(V, p) by TARSKI:def 3;
set BQ = {ZMtoMQV(V, p, u) where u is VECTOR of V : u in B};
now let x be element;
assume x in BQ;
then ex u be VECTOR of V st x = ZMtoMQV(V, p, u) & u in B;
hence x in the carrier of Z_MQ_VectSp(V, p);
end;
then reconsider BQ as Subset of Z_MQ_VectSp(V, p) by TARSKI:def 3;
A2: card A = card AQ by ThQuotBasis2;
A5: card B = card BQ by ThQuotBasis2;
A6: AQ is Basis of Z_MQ_VectSp(V, p) by ThQuotBasis4;
BQ is Basis of Z_MQ_VectSp(V, p) by ThQuotBasis4;
hence card A = card B by A2,A5,A6,VECTSP_9:22;
end;
definition
let V be finite-rank free Z_Module;
func rank(V) -> Nat means :DefRank:
for I being Basis of V holds it = card I;
existence
proof
consider A being finite Subset of V such that
A2: A is Basis of V by DefFR;
consider n being Nat such that
A3: n = card A;
for I being Basis of V holds card I = n by A2,A3,RL5Th26;
hence thesis;
end;
uniqueness
proof
let n, m be Nat;
assume that
A4: for I being Basis of V holds card I = n and
A5: for I being Basis of V holds card I = m;
consider A being finite Subset of V such that
A6: A is Basis of V by DefFR;
card A = n by A4,A6;
hence thesis by A5,A6;
end;
end;
theorem
for p be Prime, V be finite-rank free Z_Module holds
rank V = dim Z_MQ_VectSp(V,p)
proof
let p be Prime, V be finite-rank free Z_Module;
set W = Z_MQ_VectSp(V,p);
set A = the Basis of V;
set AQ = {ZMtoMQV(V, p, u) where u is VECTOR of V : u in A};
now let x be element;
assume x in AQ;
then ex u be VECTOR of V st x = ZMtoMQV(V, p, u) & u in A;
hence x in the carrier of Z_MQ_VectSp(V, p);
end;
then reconsider AQ as Subset of W by TARSKI:def 3;
A2: card A = card AQ by ThQuotBasis2;
AQ is Basis of W by ThQuotBasis4;
then dim W = card AQ by VECTSP_9:def 1;
hence thesis by A2,DefRank;
end;