:: Free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 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, 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,
INT_2, MESFUNC1, MOD_3;
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, FINSEQ_1,
NAT_D,
FINSEQ_3, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1,
INT_1,
VECTSP_2, VECTSP_4, INT_2, VECTSP_6, VECTSP_9, MATRLIN, INT_3, BINOM,
EC_PF_1, VECTSP_7, VECTSP10, ZMODUL01, ZMODUL02;
constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, VECTSP_2,
RLVECT_2, REAL_1, CLASSES1, FUNCT_7, NAT_D, GR_CY_1, EUCLID, VECTSP_6,
VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL01, ZMODUL02, BINOP_1, VECTSP_7,
VECTSP_4, NEWTON, INT_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, ZMODUL02, ORDINAL1, VECTSP_7;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, VECTSP_6, VECTSP_7;
equalities STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, BINOM, ZMODUL02, VECTSP_4,
VECTSP_6, VECTSP10;
expansions TARSKI, STRUCT_0, VECTSP_6, VECTSP_7, ZMODUL01;
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, MOD_3, VECTSP10;
schemes FINSEQ_1, FUNCT_2, NAT_1, FUNCT_1, XFAMILY;
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 = ModuleStr(# the carrier of AG,
the addF of AG, the ZeroF of AG, Int-mult-left(AG) #);
A1: G is Z_Module by ZMODUL01:164;
G is non trivial;
hence thesis by A1;
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;
end;
end;
theorem Th1:
for u being Vector of V holds
ex l being 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
A3: for v being Element of V holds not v in {u} implies f.v = 0.INT.Ring
by A2;
reconsider f as Element of Funcs(the carrier of V,
the carrier of INT.Ring) by FUNCT_2:8;
reconsider f as Linear_Combination of V by A3,VECTSP_6:def 1;
take f;
thus thesis by A1,A2;
end;
Lm1:
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[Nat] means
for i be Integer st i = $1 holds i*r = $1*r;
reconsider rr = r as Integer;
A1: 0.(INT.Ring) = 0;
A2: P[ 0 ] by A1,BINOM:12;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A4: P[n];
now
let i be Integer;
assume A5: i = n+1;
reconsider Kn = n, K1 = 1 as Integer;
reconsider n1 = 1 as Element of NAT;
A6: K1 * r = n1*r by BINOM:13;
thus i*r = Kn*r + K1*r by A5
.= (n*r) + (n1*r) by A4,A6
.= (n+1) * r by BINOM:15;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th2:
for G be Z_Module, i being Element of INT.Ring,
w be Element of INT, v be Element of G
st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring,
the ZeroF 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.Ring,
w be Element of INT, v be Element of G;
assume A1: G = ModuleStr(# the carrier of INT.Ring,
the addF of INT.Ring, the ZeroF of INT.Ring,
Int-mult-left(INT.Ring) #) & v = w;
reconsider r = v as Element of INT.Ring by A1;
per cases;
suppose 0 <= i;
then reconsider n=i as Element of NAT by INT_1:3;
thus i*v = n*r by A1,ZMODUL01:def 20
.= i*w by A1,Lm1;
end;
suppose A2: not 0 <= i;
then reconsider n = -i as Element of NAT by INT_1:3;
thus i*v = n*(-r) by A1,A2,ZMODUL01:def 20
.= (-i)*(-r) by Lm1
.= i*w by A1;
end;
end;
definition
::$CD
:: let IT be Z_Module;
:: attr IT is free means :Def1:
:: ex A being Subset of IT
:: st A is linearly-independent & Lin(A) = the ModuleStr of IT;
end;
registration let V;
cluster (0).V -> free;
coherence by MOD_3:14;
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;
registration
let V be free Z_Module;
cluster base for Subset of V;
existence by VECTSP_7:def 4;
end;
definition
let V be free Z_Module;
mode Basis of V is base Subset of V;
::$CD
end;
registration
cluster -> Mult-cancelable for free Z_Module;
coherence
proof
let V be free Z_Module;
set I = the Basis of V;
assume A1: not V is Mult-cancelable;
consider a being Element of INT.Ring, v being Vector of V such that
A2: a * v = 0.V & a <> 0.INT.Ring & v <> 0.V by A1;
I is base; then
I is linearly-independent & Lin(I) = the ModuleStr of V;
then consider lv be Linear_Combination of I such that
A3: v = Sum(lv) by STRUCT_0:def 5,ZMODUL02:64;
Carrier(lv) <> {} by A2,A3,ZMODUL02:23;
then A4: Carrier(a*lv) <> {} by A2,ZMODUL02:29;
A5: a * lv is Linear_Combination of I by ZMODUL02:31;
Sum(a * lv) = 0.V by A2,A3,ZMODUL02:53;
hence contradiction by A4,A5,VECTSP_7:def 3,VECTSP_7:def 1;
end;
end;
registration
cluster free for non trivial Z_Module;
correctness
proof
set AG = INT.Ring;
set G = ModuleStr(# the carrier of AG, the addF of AG,
the ZeroF 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};
reconsider I as Subset of G;
for a be Element of INT.Ring for v being Vector of G st a * v = 0.G
holds a = 0.INT.Ring or v = 0.G
proof
let a be Element of INT.Ring, v be Vector of G;
assume A1: a * v = 0.G;
reconsider w = v as Element of INT;
a*w = 0 by A1,Th2;
hence a = 0.INT.Ring or v = 0.G by XCMPLX_1:6;
end;
then G is Mult-cancelable;
then A3: I is linearly-independent by ZMODUL02:59;
for x be object holds
x in the carrier of Lin(I) iff x in the carrier of G
proof
let x be object;
hereby assume A4: x in the carrier of Lin(I);
the carrier of Lin(I) c= the carrier of G by VECTSP_4:def 2;
hence x in the carrier of G by A4;
end;
assume x in the carrier of G;
then reconsider v0 = x as Vector of G;
reconsider w = v0 as Element of INT.Ring;
reconsider a = w as Integer;
reconsider i0 = 0 as Element of INT.Ring;
deffunc G(Vector of G) = 0.INT.Ring;
deffunc L0(Vector of G) = w;
consider g being Function of G, INT.Ring such that
A5: g.iv = w and
A6: 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, the carrier of
INT.Ring) 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.INT.Ring by A6;
end;
then reconsider g as Linear_Combination of G by VECTSP_6:def 1;
Carrier(g) c= {iv}
proof
let x be object;
assume x in Carrier(g);
then ex u being Vector of G st x = u & g.u <> 0;
then x = iv by A6;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {iv} by VECTSP_6:def 4;
Sum(g) = w * iv by A5,ZMODUL02:21
.= w*i1 by Th2
.= v0;
hence x in the carrier of (Lin(I)) by STRUCT_0:def 5,ZMODUL02:64;
end;
then Lin(I) = the ModuleStr of G by TARSKI:2,ZMODUL01:47; then
ex I being Subset of G st I is base by A3,VECTSP_7:def 3;
then G is free;
hence thesis;
end;
end;
reserve KL1, KL2 for Linear_Combination of V;
reserve X for Subset of V;
theorem Th3:
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 Linear_Combination of Carrier(KL1 - KL2) &
Sum(KL1 - KL2) = 0.V by ZMODUL02:55,VECTSP_6:def 4;
Carrier(KL1 - KL2) c= Carrier(KL1) \/ Carrier(KL2) by ZMODUL02:40; then
A5: Carrier(KL1 - KL2) is linearly-independent
by A1,A3,XBOOLE_1:1,ZMODUL02:56;
now
let v be Vector of V;
not v in Carrier(KL1 - KL2) by A5,A4;
then (KL1 - KL2).v = 0;
then KL1.v - KL2.v = 0 by ZMODUL02:39;
hence KL1.v = KL2.v;
end;
hence thesis;
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 Element of INT.Ring st
a * v in Lin(B))
proof
let V be free Z_Module, A be Subset of V such that
A1: 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
A2: for Z being set holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XFAMILY:sch 1;
A3: now
let Z be set;
assume that
A4: Z <> {} and
A5: Z c= Q and
A6: Z is c=-linear;
set W = union Z;
W c= the carrier of V
proof
let x be object;
assume x in W;
then consider X be set such that
A7: x in X and
A8: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A2,A5,A8;
hence thesis by A7;
end;
then reconsider W as Subset of V;
A9: W is linearly-independent
proof
deffunc Q(object)={C where C is Subset of V: $1 in C & C in Z};
let l be Linear_Combination of W;
assume that
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
consider f being Function such that
A12: dom f = Carrier(l) and
A13: for x being object st x in Carrier(l) holds f.x = Q(x)
from FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A11,A12,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A14:
now
assume {} in M;
then consider x being object such that
A15: x in dom f and
A16: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by VECTSP_6:def 4;
then consider X be set such that
A17: x in X and
A18: X in Z by A12,A15,TARSKI:def 4;
reconsider X as Subset of V by A2,A5,A18;
X in {C where C is Subset of V: x in C & C in Z} by A17,A18;
hence contradiction by A12,A13,A15,A16;
end;
then
A19: dom F = M by RLVECT_3:28;
then dom F is finite by A12,FINSET_1:8;
then
A20: S is finite by FINSET_1:8;
A21:
now
let X be set;
assume X in S;
then consider x being object such that
A22: x in dom F and
A23: F.x = X by FUNCT_1:def 3;
consider y being object such that
A24: y in dom f & f.y = x by A22,FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
A25: x = Q(y) by A12,A13,A24;
X in x by A14,A22,A23,ORDERS_1:89;
then ex C being Subset of V st C = X & y in C & C in Z by A25;
hence X in Z;
end;
A26:
now
let X,Y be set;
assume X in S & Y in S;
then X in Z & Y in Z by A21;
hence X c= Y or Y c= X by A6,ORDINAL1:def 8,XBOOLE_0:def 9;
end;
S <> {} by A19,RELAT_1:42;
then union S in Z by A20,A21,A26,CARD_2:62;
then consider B being Subset of V such that
A27: B = union S and
A c= B and
A28: B is linearly-independent by A2,A5;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume A29: x in Carrier(l);
then
A30: f.x = {C where C is Subset of V: x in C & C in Z} by A13;
A31: f.x in M by A12,A29,FUNCT_1:def 3;
then F.X in X by A14,ORDERS_1:89;
then
A32: ex C being Subset of V st F.X = C & x in C & C in Z by A30;
F.X in S by A19,A31,FUNCT_1:def 3;
hence thesis by A32,TARSKI:def 4;
end;
then l is Linear_Combination of B by A27,VECTSP_6:def 4;
hence thesis by A10,A11,A28;
end;
set x = the Element of Z;
x in Q by A4,A5; then
A33: ex B being Subset of V st B = x & A c= B & B is linearly-independent
by A2;
x c= W by A4,ZFMISC_1:74;
hence union Z in Q by A2,A9,A33,XBOOLE_1:1;
end;
Q <> {} by A1,A2;
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 A3,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 A2,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 Element of INT.Ring
st a * v in Lin(B);
then consider v being Vector of V such that
A39: for a being Element of INT.Ring holds not a * v in Lin(B);
A40: B \/ {v} is linearly-independent
proof
let l be 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.Ring;
deffunc G(Vector of V)=0.INT.Ring;
deffunc L(Vector of V)=l.$1;
consider f being Function of the carrier of V, the carrier of
INT.Ring such that
A42: f.v = i0 and
A43: 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,
the carrier of INT.Ring) 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 A42,A43;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= B
proof
let x be object;
A44: Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
assume x in Carrier(f);
then consider u being Vector of V such that
A45: u = x and
A46: f.u <> 0;
f.u = l.u by A42,A43,A46;
then u in Carrier(l) by A46;
then u in B or u in {v} by A44,XBOOLE_0:def 3;
hence thesis by A42,A45,A46,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of B by VECTSP_6:def 4;
reconsider lv = -l.v as Element of INT.Ring;
consider g being Function of the carrier of V,
the carrier of INT.Ring such that
A47: g.v = lv and
A48: 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, the carrier of INT.Ring) 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.INT.Ring by A48;
end;
then reconsider g as Linear_Combination of V by VECTSP_6:def 1;
Carrier(g) c= {v}
proof
let x be object;
assume x in Carrier(g);
then ex u being Vector of V st x = u & g.u <> 0;
then x = v by A48;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;
A49: Sum(g) = (- l.v) * v by A47,ZMODUL02:21;
f - g = l
proof
let u be Vector of V;
now
per cases;
suppose
A50: v = u;
thus (f - g).u = f.u - g.u by ZMODUL02:39
.= l.u by A42,A47,A50;
end;
suppose
A51: v <> u;
thus (f - g).u = f.u - g.u by ZMODUL02:39
.= l.u - g.u by A43,A51
.= l.u - 0.INT.Ring by A48,A51
.= 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 A49,RLVECT_1:4;
hence thesis by A39,ZMODUL02:64;
end;
suppose
A52: not v in Carrier(l);
Carrier(l) c= B
proof
let x be object;
assume
A53: x in Carrier(l);
Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
then x in B or x in {v} by A53,XBOOLE_0:def 3;
hence thesis by A52,A53,TARSKI:def 1;
end;
then l is Linear_Combination of B by VECTSP_6:def 4;
hence thesis by A38,A41;
end;
end;
hence thesis;
end;
v in {v} by TARSKI:def 1;
then
A54: v in B \/ {v} by XBOOLE_0:def 3;
not (1.(INT.Ring)) * v in Lin(B) by A39;
then not v in Lin(B) by VECTSP_1:def 17;
then A55: not v in B by ZMODUL02:65;
B c= B \/ {v} by XBOOLE_1:7;
then B \/ {v} in Q by A2,A37,A40,XBOOLE_1:1;
hence contradiction by A35,A36,A54,A55,XBOOLE_1:7;
end;
theorem Th5:
for L being 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 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 VECTSP_6:def 5;
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 VECTSP_6:def 5;
then
A6: dom F = dom p by FINSEQ_3:29;
len q = len G by VECTSP_6:def 5;
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
A9: k in dom q;
set l = P.k;
dom P = dom F & rng P = dom F by FUNCT_2:52,def 3;
then
A10: l in dom F by A7,A6,A9,FUNCT_1:def 3;
then reconsider l as Element of NAT;
G/.k = G.k by A7,A8,A6,A9,PARTFUN1:def 6
.= F.(P.k) by A1,A7,A8,A6,A9,FUNCT_1:12
.= F/.l by A10,PARTFUN1:def 6;
then q.k = L.(F/.l) * (F/.l) by A9,VECTSP_6:def 5
.= (L (#) F).(P.k) by A6,A10,VECTSP_6:def 5
.= r.k by A7,A4,A9,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 Th6:
for L being Linear_Combination of V for F being FinSequence of V st
Carrier(L) misses rng F holds Sum(L (#) F) = 0.V :::by VECTSP_9:2;
proof
let L be 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 being object st P[p] holds P[p^<*x*>]
proof
let p be FinSequence, x be object 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.INT.Ring * 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 Linear_Combination of V st Carrier(L) c= rng F holds
Sum(L (#) F) = Sum(L) :::by VECTSP_9:3;
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 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 VECTSP_6:def 6;
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,26;
reconsider F1, F2 = F - A as FinSequence of V by FINSEQ_3:86;
A8: 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 Th5
.= 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,A8,Th6,XBOOLE_0:def 7
.= Sum(L (#) G) + 0.V by A7,Th5
.= Sum(L) by A5,RLVECT_1:4;
hence thesis;
end;
theorem
for L being Linear_Combination of V for F being FinSequence of V holds
ex K being Linear_Combination of V st
Carrier(K) = rng F /\ Carrier(L) & L (#) F = K (#) F :::by VECTSP_9:4;
proof
let L be Linear_Combination of V, F be FinSequence of V;
defpred P[object, object] 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 being object st x in the carrier of V
ex y being object st y in INT & P[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x9 = x as Vector of V;
per cases;
suppose
A2: x in rng F;
L.x9 in INT;
hence thesis by A2;
end;
suppose
A3: not x in rng F;
thus thesis by A3;
end;
end;
ex K being Function of the carrier of V, INT st
for x being object 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
A4: for x being object st x in the carrier of V holds P[x, K.x];
A5:
now
let v be Vector of V;
assume
A6: not v in R /\ Carrier(L);
per cases by A6,XBOOLE_0:def 4;
suppose
not v in R;
hence K.v = 0 by A4;
end;
suppose
not v in Carrier(L);
then L.v = 0;
hence K.v = 0 by A4;
end;
end;
reconsider K as Element of Funcs(the carrier of V, INT) by FUNCT_2:8;
reconsider K as Linear_Combination of V by A5,VECTSP_6:def 1;
now
let v be object;
assume
A7: v in rng F /\ Carrier(L);
then reconsider v9= v as Vector of V;
v in Carrier(L) by A7,XBOOLE_0:def 4;
then
A8: L.v9 <> 0 by ZMODUL02:8;
v in R by A7,XBOOLE_0:def 4;
then K.v9 = L.v9 by A4;
hence v in Carrier(K) by A8;
end;
then
A9: rng F /\ Carrier(L) c= Carrier(K);
take K;
A10: L (#) F = K (#) F
proof
set p = L (#) F, q = K (#) F;
A11: len p = len F by VECTSP_6:def 5;
len q = len F by VECTSP_6:def 5;
then
A12: dom p = dom q by A11,FINSEQ_3:29;
A13: dom p = dom F by A11,FINSEQ_3:29;
now
let k be Nat;
set u = F/.k;
A14: P[u, K.u] by A4;
assume
A15: k in dom p;
then F/.k = F.k & p.k = L.u * u by A13,PARTFUN1:def 6,VECTSP_6:def 5;
hence p.k = q.k by A12,A13,A15,A14,FUNCT_1:def 3,VECTSP_6:def 5;
end;
hence thesis by A12,FINSEQ_1:13;
end;
now
let v be object;
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 A5;
end;
then Carrier(K) c= rng F /\ Carrier(L);
hence thesis by A9,A10,XBOOLE_0:def 10;
end;
theorem Th9:
for L being 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 Linear_Combination of A st Sum(L (#) F) = Sum(K)
proof
let L be Linear_Combination of V;
let A be Subset of V;
defpred P[Nat] means for F being FinSequence of V
st rng F c= the carrier of Lin(A) & len F = $1 holds ex K being
Linear_Combination of A st Sum(L (#) F) = Sum(K);
A1: for n being Nat st P[n] holds P[n + 1]
proof
let n be 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 object 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; then
A8: x in {x} implies x in the carrier of Lin(A);
then consider LA1 being 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;
len(G^<*x*>) = len G + len <*x*> by FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
then consider LA2 being 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 Linear_Combination of A by ZMODUL02:31; then
A11: LA2 + L.x * LA1 is 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(ZeroLC(V)) by ZMODUL02:19;
ZeroLC(V) is Linear_Combination of A by ZMODUL02:11;
hence thesis by A16;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A14, A1);
hence thesis by A12,A13;
end;
theorem Th10:
for L being Linear_Combination of V for A being Subset of V st
Carrier(L) c= the carrier of Lin(A) holds
ex K being Linear_Combination of A st Sum(L) = Sum(K)
proof
let L be 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 VECTSP_6:def 6;
assume Carrier(L) c= the carrier of Lin(A);
then consider K being Linear_Combination of A such that
A3: Sum(L (#) F) = Sum(K) by A1,Th9;
take K;
thus thesis by A2,A3;
end;
theorem Th11:
for L being Linear_Combination of V st Carrier(L) c= the carrier
of W for K being Linear_Combination of W st K = L|the carrier of W holds
Carrier(L) = Carrier(K) & Sum(L) = Sum(K)
proof
let L be Linear_Combination of V such that
A1: Carrier(L) c= the carrier of W;
let K be 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 object;
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);
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 VECTSP_6:def 6;
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 VECTSP_6:def 6;
now
let x be object;
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);
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 VECTSP_6:def 5;
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 VECTSP_6:def 5;
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 VECTSP_4:def 2;
rng q c= the carrier of V by A22;
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 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 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 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,VECTSP_6:def 5; then
A32: dom p = dom G by FINSEQ_3:29;
A33: dom q = dom(K (#) G) by A20,FINSEQ_3:29;
now
let i be Nat;
set v = F/.i;
set j = P.i;
assume
A34: i in dom p;
then
A35: F/.i = F.i by A30,A32,PARTFUN1:def 6;
then v in rng F by A30,A32,A34,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
A36: j in dom G by A32,A34,FUNCT_1:def 3;
then reconsider j as Element of NAT;
A37: G/.j = G.(P.i) by A36,PARTFUN1:def 6
.= v by A18,A30,A32,A34,A35,FUNCT_1:12;
q.i = (K (#) G).j by A21,A32,A34,FUNCT_1:12
.= K.w * w by A33,A21,A36,A37,VECTSP_6:def 5
.= L.v * w by A2,A3,FUNCT_1:47
.= L.v * v by ZMODUL01:29;
hence p.i = q.i by A34,VECTSP_6:def 5;
end;
then
A38: L (#) F = (K (#) G)*P by A21,A31,FINSEQ_1:13,FINSEQ_3:29;
len G = len (K (#) G) by VECTSP_6:def 5;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P as Permutation of dom (K (#) G);
q = (K (#) G)*P; then
A39: Sum(K (#) G) = Sum(q) by RLVECT_2:7;
A40: f9.len q9 is Element of V;
f9.0 = 0.V by A24,ZMODUL01:26;
hence thesis
by A7,A16,A12,A9,A38,A39,A23,A26,A40,RLVECT_1:def 12,XBOOLE_0:def 10;
end;
theorem Th12:
for K being Linear_Combination of W holds
ex L being Linear_Combination of V st
Carrier(K) = Carrier(L) & Sum(K) = Sum(L)
proof
let K be Linear_Combination of W;
defpred P[object, object] 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 VECTSP_4:def 2;
then reconsider C = Carrier(K) as finite Subset of V by XBOOLE_1:1;
A2: for x being object st x in the carrier of V
ex y being object st y in INT & P[x, y]
proof
let x be object;
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;
P[x, K.x] by A3;
hence thesis;
end;
suppose
A4: not x in W;
thus thesis by A4;
end;
end;
consider L being Function of the carrier of V, INT such that
A5: for x being object st x in the carrier of V holds P[x, L.x]
from FUNCT_2:sch 1(A2);
A6:
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 A5;
end;
L is Element of Funcs(the carrier of V, the carrier of INT.Ring)
by FUNCT_2:8;
then reconsider L as Linear_Combination of V by A6,VECTSP_6:def 1;
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 object;
assume that
A7: x in Carrier(L) and
A8: not x in the carrier of W;
consider v being Vector of V such that
A9: x = v and
A10: L.v <> 0 by A7;
P[v, 0] by A8,A9,STRUCT_0:def 5;
hence contradiction by A5,A10;
end;
then
A11: Carrier(L) c= the carrier of W;
now
let x be object;
assume
A12: x in the carrier of W;
then P[x, L.x] by A5,A1;
hence K9.x = L9.x by A12,FUNCT_1:49,STRUCT_0:def 5;
end;
then K9 = L9 by FUNCT_2:12;
hence thesis by A11,Th11;
end;
theorem Th13:
for L being Linear_Combination of V st
Carrier(L) c= the carrier of W
ex K being Linear_Combination of W
st Carrier(K) = Carrier(L) & Sum(K) = Sum (L)
proof
let L be 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 VECTSP_4:def 2;
then reconsider K = L|the carrier of W as
Function of the carrier of W, the carrier of INT.Ring by FUNCT_2:32;
A2: K is Element of Funcs(the carrier of W, the carrier of INT.Ring)
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 Linear_Combination of W by A2,VECTSP_6:def 1;
take K;
thus thesis by A1,Th11;
end;
theorem Th14:
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;
A1: v in the ModuleStr of V;
for I being Subset of V holds
I is base iff
I is linearly-independent & Lin(I) = the ModuleStr of V;
hence thesis by A1;
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 VECTSP_4:def 2;
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 Linear_Combination of A9 such that
A2: Sum(L) = 0.V and
A3: Carrier(L) <> {};
Carrier(L) c= A by VECTSP_6:def 4;
then consider LW being Linear_Combination of W such that
A4: Carrier(LW) = Carrier(L) and
A5: Sum(LW) = Sum(L) by Th13,XBOOLE_1:1;
reconsider LW as Linear_Combination of A by A4,VECTSP_6:def 4;
Sum(LW) = 0.W by A2,A5,ZMODUL01:26;
hence contradiction by A1,A3,A4;
end;
hence thesis;
end;
theorem Th16:
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 Linear_Combination of A9 such that
A3: Sum(K) = 0.W and
A4: Carrier(K) <> {};
consider L being Linear_Combination of V such that
A5: Carrier(L) = Carrier(K) and
A6: Sum(L) = Sum(K) by Th12;
reconsider L as Linear_Combination of A by A5,VECTSP_6:def 4;
Sum(L) = 0.V by A3,A6,ZMODUL01:26;
hence contradiction by A1,A4,A5;
end;
hence thesis;
end;
theorem Th17:
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 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 Linear_Combination of B such that
A6: v = Sum(L) by ZMODUL02:64;
A7: Carrier(L) c= B & Carrier(K) c= {v} by VECTSP_6:def 4;
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;
then
A8: L - K is Linear_Combination of A by XBOOLE_1:1,VECTSP_6:def 4;
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.INT.Ring 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 object 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;
end;
theorem Th18:
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 object 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 Th14;
hence contradiction by A7,A2,A4,A6,Th17,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 object;
assume w in the carrier of Lin(A);
then consider L being Linear_Combination of A such that
A2: w = Sum(L) by STRUCT_0:def 5,ZMODUL02:64;
Carrier(L) c= A by VECTSP_6:def 4;
then
ex K being Linear_Combination of W st Carrier(K) = Carrier (L) & Sum(L)
= Sum(K) by A1,Th13,XBOOLE_1:1;
hence w in the carrier of W by A2;
end;
hence thesis by TARSKI:def 3,ZMODUL01:43;
end;
theorem Th20:
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 object;
assume x in the carrier of Lin(A);
then consider L being Linear_Combination of A such that
A3: x = Sum(L) by STRUCT_0:def 5,ZMODUL02:64;
Carrier(L) c= A by VECTSP_6:def 4;
then consider K being Linear_Combination of W such that
A4: Carrier(K) = Carrier(L) and
A5: Sum(K) = Sum(L) by A2,Th13,XBOOLE_1:1;
reconsider K as Linear_Combination of B by A2,A4,VECTSP_6:def 4;
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);
now
let x be object;
assume x in the carrier of Lin(B);
then consider K being Linear_Combination of B such that
A7: x = Sum(K) by STRUCT_0:def 5,ZMODUL02:64;
consider L being Linear_Combination of V such that
A8: Carrier(L) = Carrier(K) and
A9: Sum(L) = Sum(K) by Th12;
reconsider L as Linear_Combination of A by A2,A8,VECTSP_6:def 4;
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);
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 base
proof
for x be object 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 Th16,TARSKI:def 3;
take B;
Lin(B) = the ModuleStr of Lin(A) by Th20;
hence thesis;
end;
hence thesis;
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 base by VECTSP_7:def 4;
A1: A is linearly-independent & Lin(A) = the ModuleStr of V
by a1;
ex AA being Subset of VV
st AA is linearly-independent & Lin(AA) = the ModuleStr of VV
proof
consider AA being Subset of VV such that
A2: AA = A;
take AA;
thus thesis by A1,A2,Th16,Th20;
end;
hence thesis;
end;
end;
begin :: Finite-rank free Z-module
definition
let IT be free Z_Module;
attr IT is finite-rank means :Def3:
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;
A1: Lin(WW) = (0).VV by ZMODUL02:67
.= VV by ZMODUL01:51;
reconsider WW as finite Subset of VV;
take WW;
thus thesis by A1,VECTSP_7:def 3;
end;
hence thesis;
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 object 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 Th16,TARSKI:def 3;
take AA;
Lin(A) = Lin(AA) by Th20;
hence thesis by VECTSP_7:def 3;
end;
hence thesis;
end;
end;
definition
let V be Z_Module;
attr V is finitely-generated means
ex A being finite Subset of V st Lin(A) = the ModuleStr 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;
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 Def3;
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 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 object;
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 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 VECTSP_6:def 4;
hence thesis by A4;
end;
then reconsider C as Subset of V by XBOOLE_1:1;
A6: 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,VECTSP_7:def 3;
then consider LA being Linear_Combination of A such that
A7: v = Sum(LA) by ZMODUL02:64;
Carrier(LA) c= the carrier of Lin(C)
proof
let w be object;
assume A8: w in Carrier(LA);
then reconsider w9= w as Vector of V;
w9 in Lin(B) by Th14;
then consider LB being Linear_Combination of B such that
A9: w = Sum(LB) by ZMODUL02:64;
Carrier(LA) c= A by VECTSP_6:def 4;
then ex i being object st i in dom p & w = p.i by A2,A8,FUNCT_1:def 3;
then
A10: Carrier(LB) in Car by A9;
Carrier(LB) c= C by A10,TARSKI:def 4;
then LB is Linear_Combination of C by VECTSP_6:def 4;
hence thesis by A9,STRUCT_0:def 5,ZMODUL02:64;
end;
then ex LC being Linear_Combination of C
st Sum(LA) = Sum(LC) by Th10;
hence v in Lin(C) by A7,ZMODUL02:64;
end;
assume v in Lin(C);
thus thesis;
end;
A11: B is linearly-independent by VECTSP_7:def 3;
C is linearly-independent by A3,VECTSP_7:def 3,ZMODUL02:56; then
A12: C is Basis of V by A6,VECTSP_7:def 3,ZMODUL01:46;
B c= C
proof
set D = B \ C;
assume not B c= C;
then ex v being object st v in B & not v in C;
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,Th18,XBOOLE_1:79;
end; then
A13: B = C by A3,XBOOLE_0:def 10;
defpred P[set, object] means ex L being 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 being object 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 Th14;
then consider L being 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 Linear_Combination of B such that
A22: y1 = Carrier(L1) & Sum(L1) = p.i by A20;
consider L2 being 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 VECTSP_6:def 4;
hence thesis by A22,A23,VECTSP_7:def 3,Th3;
end;
now
let x be object;
assume x in Car;
then consider L being 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;
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 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 Th21:
for p being prime Element of INT.Ring,
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 Element of INT.Ring, V be free Z_Module, I be Basis of V,
u1, u2 be Vector of V such that
A1: u1 <> u2 & u1 in I & u2 in I;
set uq1 = ZMtoMQV(V,p,u1), uq2 = ZMtoMQV(V,p,u2);
assume A2: uq1 = uq2;
consider u be Vector of V such that
A3: u in p(*)V & u1 + u = u2 by A2,ZMODUL01:75;
A4: I is linearly-independent & Lin(I) = the ModuleStr of V
by VECTSP_7:def 3;
B1: u in p * V by A3;
reconsider pp = p as Element of INT.Ring;
consider v be Vector of V such that
A5: u = pp * v by B1;
consider lv be Linear_Combination of I such that
A6: v = Sum(lv) by A4,STRUCT_0:def 5,ZMODUL02:64;
consider lu1 be Linear_Combination of V such that
A7: lu1.u1 = 1 & for v being Vector of V st v <> u1 holds lu1.v = 0
by Th1;
A8: Carrier(lu1) = {u1}
proof
for v being object holds v in Carrier(lu1) implies v in {u1}
proof
assume ex v being object st v in Carrier(lu1) & not v in {u1};
then consider v being Vector of V such that
A9: v in Carrier(lu1) & not v in {u1};
v <> u1 by A9,TARSKI:def 1;
then lu1.v = 0 by A7;
hence contradiction by A9,ZMODUL02:8;
end;
then A10: Carrier(lu1) c= {u1};
u1 in Carrier(lu1) by A7;
then {u1} c= Carrier(lu1) by ZFMISC_1:31;
hence thesis by A10,XBOOLE_0:def 10;
end;
then A11: Sum(lu1) = (1.(INT.Ring)) * u1 by A7,ZMODUL02:24
.= u1 by VECTSP_1:def 17;
reconsider lu1 as Linear_Combination of {u1} by A8,VECTSP_6:def 4;
reconsider lu1 as Linear_Combination of I by A1,ZFMISC_1:31,ZMODUL02:10;
consider lu2 be Linear_Combination of V such that
A12: lu2.u2 = 1 & for v being Vector of V st v <> u2 holds lu2.v = 0
by Th1;
A13: Carrier(lu2) = {u2}
proof
for v being object holds v in Carrier(lu2) implies v in {u2}
proof
assume ex v being object st v in Carrier(lu2) & not v in {u2};
then consider v being Vector of V such that
A14: v in Carrier(lu2) & not v in {u2};
v <> u2 by A14,TARSKI:def 1;
then lu2.v = 0 by A12;
hence contradiction by A14,ZMODUL02:8;
end;
then A15: Carrier(lu2) c= {u2};
u2 in Carrier(lu2) by A12;
then {u2} c= Carrier(lu2) by ZFMISC_1:31;
hence thesis by A15,XBOOLE_0:def 10;
end;
then A16: Sum(lu2) = 1.(INT.Ring) * u2 by A12,ZMODUL02:24
.= u2 by VECTSP_1:def 17;
reconsider lu2 as Linear_Combination of {u2} by A13,VECTSP_6:def 4;
reconsider lu2 as Linear_Combination of I by A1,ZFMISC_1:31,ZMODUL02:10;
A17: u = Sum(p * lv) by A5,A6,ZMODUL02:53;
A18: (p * lv).u1 <> -1
proof
assume A19: (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 A19;
then A20: (p * lv).u1 mod p <> 0 by INT_2:def 4;
reconsider pp = p as Element of INT.Ring;
A21: (pp * lv).u1 = pp * (lv.u1) by VECTSP_6:def 9;
pp divides (pp * lv).u1 - 0 by A21,INT_1:60,def 4;
hence contradiction by A20,INT_1:62;
end;
pp * lv is Linear_Combination of I by ZMODUL02:31;
then lu1 + pp * lv is Linear_Combination of I by ZMODUL02:27;
then reconsider lx = lu1 + pp * lv - lu2 as Linear_Combination of I
by ZMODUL02:41;
A22: 0.V = Sum(lu1 + pp * lv) - Sum(lu2)
by A3,A17,A11,A16,VECTSP_1:19,ZMODUL02:52
.= Sum(lx) by ZMODUL02:55;
A23: lx.u1 = (lu1 + pp * lv).u1 - lu2.u1 by ZMODUL02:39
.= lu1.u1 + (pp * lv).u1 - lu2.u1 by VECTSP_6:22
.= 1.INT.Ring + (pp * lv).u1 - 0.INT.Ring by A1,A7,A12
.= 1.INT.Ring + (pp * lv).u1;
lx.u1 <> 0 by A18,A23;
then u1 in Carrier(lx);
hence contradiction by A22,VECTSP_7:def 3,VECTSP_7:def 1;
end;
theorem Th22:
for p being prime Element of INT.Ring, 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 Element of INT.Ring, 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,VECTSP10:def 6;
then vq in the set of all A where A is Coset of p(*)V;
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,VECTSP_4:def 6;
take v;
thus thesis by A3;
end;
Lm2:
for p being prime Element of INT.Ring,
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 Element of INT.Ring, V be Z_Module,
v, w be Vector of V such that
A1: ZMtoMQV(V, p, w) /\ ZMtoMQV(V, p, v) <> {};
consider u being object 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 Th23:
for p being prime Element of INT.Ring, V being Z_Module,
I being Subset of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p)
holds ex l being 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 Element of INT.Ring, 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 A1: I is empty;
set l = the Linear_Combination of I;
take l;
thus thesis by A1;
end;
suppose A2: I is non empty;
set X = { ZMtoMQV(V,p,v) where v is Vector of V:v in I};
now let x be object;
assume x in X;
then consider v be Vector of V such that
A3: x = ZMtoMQV(V,p,v) & v in I;
thus x in the carrier of ZQ by A3;
end;
then
reconsider X as Subset of ZQ by TARSKI:def 3;
consider v0 be object such that A4: v0 in I by A2,XBOOLE_0:def 1;
reconsider v0 as Vector of V by A4;
ZMtoMQV(V,p,v0) in X by A4;
then reconsider X as non empty Subset of ZQ;
defpred F0[Element of X, Element of V] means
$2 in $1 & $2 in I;
A5: 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
A6: x = ZMtoMQV(V,p,v) & v in I;
thus ex v be Element of V st F0[x,v] by A6,ZMODUL01:58;
end;
consider F being Function of X, the carrier of V such that
A7: for x being Element of X holds F0[x,F.x] from FUNCT_2:sch 3(A5);
A8: now let y be object;
assume y in rng F;
then consider x be object such that
A9: x in X & F.x = y by FUNCT_2:11;
reconsider x as Element of X by A9;
thus y in I by A9,A7;
end;
then
A10: rng F c= I;
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);
A11: 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 A12: v in rng F;
reconsider y = lq.(ZMtoMQV(V,p,v)) as Element of GF(p);
take y;
thus thesis by A12;
end;
suppose A13: 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 A13;
end;
end;
A14: Segm(p) c= INT by NUMBERS:17;
consider f being Function of the carrier of V, GF(p) such that
A15: for v being Element of V holds P[v,f.v] from FUNCT_2:sch 3(A11);
A16: 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 be Vector of V;
assume v in I; then
A17: ZMtoMQV(V,p,v) in X; then
A18: F.(ZMtoMQV(V,p,v)) in rng F by FUNCT_2:4;
reconsider w = F.(ZMtoMQV(V,p,v)) as Element of V by A17,FUNCT_2:5;
take w;
A19: f.w = lq.(ZMtoMQV(V,p,w)) by A15,A17,FUNCT_2:4;
thus w in I by A18,A8;
thus w in ZMtoMQV(V,p,v) by A7,A17;
thus f.w = lq.(ZMtoMQV(V,p,v)) by A17,A19,A7,ZMODUL01:67;
end;
reconsider l = f as Function of the carrier of V, INT by A14,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};
A20:
now let v be object;
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;
A21:
now let x be object;
assume x in T;
then consider v be Element of V such that
A22: x = v & l.v <> 0;
thus x in rng F by A15,A22;
end;
then
A23: T c= rng F;
now let x be object;
assume A24: x in F"T;
then A25: x in X & F.x in T by FUNCT_2:38;
then consider v be Element of V such that
A26: F.x=v & l.v <> 0;
A27: P[v,f.v] by A15;
lq.(ZMtoMQV(V,p,v)) <> 0.GF(p) by A26,A27,EC_PF_1:11;
then
A28: ZMtoMQV(V,p,v) in Carrier(lq);
reconsider w=x as Element of X by A24;
A29: F.w in w & F.w in I by A7;
consider v1 be Vector of V such that
A30: w = ZMtoMQV(V,p,v1) & v1 in I by A25;
v in ZMtoMQV(V,p,v) by ZMODUL01:58;
then ZMtoMQV(V,p,v) /\ ZMtoMQV(V,p,v1) <> {}
by A26,A29,A30,XBOOLE_0:def 4;
hence x in Carrier(lq) by A28,A30,Lm2;
end;
then F"T c= Carrier(lq);
then reconsider T as finite Subset of V
by A20,A21,FINSET_1:9,TARSKI:def 3;
for v being Element of V st not v in T holds l.v = 0.INT.Ring;
then reconsider l as Linear_Combination of V by VECTSP_6:def 1;
T = Carrier(l);
then reconsider l as Linear_Combination of I
by A23,A10,XBOOLE_1:1,VECTSP_6:def 4;
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 A16;
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 Th24:
for p being prime Element of INT.Ring, V being free Z_Module,
I being Basis of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p)
holds ex l being 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 be prime Element of INT.Ring, V be free Z_Module, I be Basis of V,
lq be Linear_Combination of Z_MQ_VectSp(V,p);
consider l being Linear_Combination of I such that
A1: 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 Th23;
take l;
now let v be Vector of V;
assume A2:v in I;
then consider w be Vector of V such that
A3: w in I & w in ZMtoMQV(V,p,v)
& l.w = lq.(ZMtoMQV(V,p,v)) by A1;
ZMtoMQV(V,p,w) = ZMtoMQV(V,p,v) by A3,ZMODUL01:67;
hence l.v = lq.(ZMtoMQV(V,p,v)) by A2,A3,Th21;
end;
hence thesis;
end;
theorem Th25:
for p being prime Element of INT.Ring, 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 Element of INT.Ring, V be free Z_Module, I be Basis of V,
X be non empty Subset of Z_MQ_VectSp(V,p);
assume A1: 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;
A2: 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
A3: x = ZMtoMQV(V,p,v) & v in I by A1;
thus ex v be Element of V st F0[x,v] by A3,ZMODUL01:58;
end;
consider F being Function of X, the carrier of V such that
A4: for x being Element of X holds F0[x,F.x] from FUNCT_2:sch 3(A2);
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 A5: v in I;
then ZMtoMQV(V,p,v) in X by A1;
then reconsider w = ZMtoMQV(V,p,v) as Element of X;
A6: F.w in w & F.w in I by A4;
ZMtoMQV(V,p,F.w) = ZMtoMQV(V,p,v) by A4,ZMODUL01:67;
hence thesis by A5,A6,Th21;
end;
now let x1,x2 be object;
assume A7: 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
A8: x1 = ZMtoMQV(V,p,v1) & v1 in I by A7,A1;
consider v2 be Vector of V such that
A9: x2 = ZMtoMQV(V,p,v2) & v2 in I by A7,A1;
F.x10 in ZMtoMQV(V,p,v1) & F.x10 in ZMtoMQV(V,p,v2) by A7,A8,A9,A4;
then F.x10 in ZMtoMQV(V,p,v1) /\ ZMtoMQV(V,p,v2) by XBOOLE_0:def 4;
hence x1 = x2 by A8,A9,Lm2;
end;
hence F is one-to-one by FUNCT_2:19;
thus dom F = X by FUNCT_2:def 1;
now let y be object;
assume y in rng F;
then consider x be object such that
A10: x in X & F.x = y by FUNCT_2:11;
reconsider x as Element of X by A10;
thus y in I by A10,A4;
end;
then
A11: rng F c= I;
now let y be object;
assume A12:y in I;
then reconsider u=y as Vector of V;
ZMtoMQV(V,p,u) in X by A12,A1;
then reconsider z = ZMtoMQV(V,p,u) as Element of X;
A13: F.z in z & F.z in I by A4;
ZMtoMQV(V,p,F.z) = ZMtoMQV(V,p,u) by A4,ZMODUL01:67;
then F.z = u by Th21,A13,A12;
hence y in rng F by FUNCT_2:4;
end;
then I c= rng F;
hence I = rng F by A11,XBOOLE_0:def 10;
end;
theorem Th26:
for p being prime Element of INT.Ring, 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 Element of INT.Ring, 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 object such that
A2: v0 in X by XBOOLE_0:def 1;
consider u be Vector of V such that
A3: v0=ZMtoMQV(V,p,u) & u in I by A2;
thus contradiction by A3,A1;
end;
hence thesis by A1;
end;
suppose A4: I is non empty;
now let x be object;
assume x in X;
then consider v be Vector of V such that
A5: x = ZMtoMQV(V,p,v) & v in I;
thus x in the carrier of ZQ by A5;
end;
then reconsider X as Subset of ZQ by TARSKI:def 3;
consider v0 be object such that A6: v0 in I by A4,XBOOLE_0:def 1;
reconsider v0 as Vector of V by A6;
ZMtoMQV(V,p,v0) in X by A6;
then reconsider X as non empty Subset of ZQ;
consider F be Function of X, the carrier of V such that
A7: (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 Th25;
thus thesis by A7,CARD_1:5,WELLORD2:def 4;
end;
end;
theorem Th27:
for p being prime Element of INT.Ring, V being free Z_Module holds
ZMtoMQV(V,p,0. V) = 0.(Z_MQ_VectSp(V,p))
proof
let p be prime Element of INT.Ring, V be free Z_Module;
thus 0.(Z_MQ_VectSp(V,p)) = 0.(VectQuot(V,p(*)V))
.= zeroCoset(V,p(*)V) by VECTSP10:def 6
.= ZMtoMQV(V,p,0. V) by ZMODUL01:59;
end;
theorem Th28:
for p being prime Element of INT.Ring, 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 Element of INT.Ring, V be free Z_Module,
s, t be Element of V;
set s1 = ZMtoMQV(V,p,s), t1 = ZMtoMQV(V,p,t);
A1: ZMtoMQV(V,p,s) = s + p(*)V;
A2: ZMtoMQV(V,p,t) = t + p(*)V;
A3: s + p(*)V is Element of CosetSet(V,p(*)V) by A1,VECTSP10:def 6;
A4: t + p(*)V is Element of CosetSet(V,p(*)V) by A2,VECTSP10:def 6;
thus s1+t1 = addCoset(V,p(*)V).(s + p(*)V,t + p(*)V) by VECTSP10:def 6
.= ZMtoMQV(V,p,s+t) by A3,A4,VECTSP10:def 3;
end;
theorem Th29:
for p being prime Element of INT.Ring, 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 Element of INT.Ring, V be free Z_Module;
defpred P[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));
A1: P[ 0 ]
proof
let s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p);
assume that A2: 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 A2;
then Sum(s) = 0. V by RLVECT_1:43;
then
A3: ZMtoMQV(V,p,Sum(s)) = 0.(Z_MQ_VectSp(V,p)) by Th27;
t = <*>(the carrier of (Z_MQ_VectSp(V,p))) by A2;
hence thesis by A3,RLVECT_1:43;
end;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
now let s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p);
assume that
A6: len s = k+1 & len s = len t and
A7: 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;
A8: dom s = Seg (k+1) by A6,FINSEQ_1:def 3;
A9: dom t = Seg (k+1) by A6,FINSEQ_1:def 3;
A10: len s1 = k by A6,FINSEQ_1:59,NAT_1:11;
A11: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by A6,FINSEQ_1:59,NAT_1:11;
then
A12: s1 = s |dom s1 by FINSEQ_1:def 16;
reconsider t1 = t | k as FinSequence of Z_MQ_VectSp(V,p);
A13:dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg k by A6,FINSEQ_1:59,NAT_1:11;
then
A14: t1 = t |dom t1 by FINSEQ_1:def 16;
k in NAT by ORDINAL1:def 12;
then
A15: len t1 = k by A13,FINSEQ_1:def 3;
s.(len s) in rng s by A6,A8,FINSEQ_1:4,FUNCT_1:3;
then reconsider vs=s.(len s) as Element of V;
t.(len t) in rng t by A6,A9,FINSEQ_1:4,FUNCT_1:3;
then reconsider vt = t.(len t) as Element of Z_MQ_VectSp(V,p);
A16: len s1 = k & len s1 = len t1 by A10,A13,FINSEQ_1:def 3;
A17: 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 A18: 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
A19: si = s.i & t.i = ZMtoMQV(V,p,si) by A7,A11,A8,A18;
take si;
thus si = s1.i by A12,A18,A19,FUNCT_1:49;
thus t1.i = ZMtoMQV(V,p,si) by A14,A11,A13,A18,A19,FUNCT_1:49;
end;
A20: Sum(t1) = ZMtoMQV(V,p,Sum(s1)) by A5,A16,A17;
A21: len s = len s1 + 1 by A6,FINSEQ_1:59,NAT_1:11;
consider ssi be Vector of V such that
A22: ssi = s.(len s) & t.(len s) = ZMtoMQV(V,p,ssi)
by A6,A7,A8,FINSEQ_1:4;
thus Sum(t) = Sum(t1) + vt by A6,A14,A15,RLVECT_1:38
.= ZMtoMQV(V,p,Sum(s1)+vs) by A6,A20,A22,Th28
.= ZMtoMQV(V,p,Sum(s)) by A12,A21,RLVECT_1:38;
end;
hence P[k+1];
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
hence thesis;
end;
theorem Th30:
for p being prime Element of INT.Ring, V being free Z_Module,
s be Element of V,
a be Element of INT.Ring,
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 Element of INT.Ring, V be free Z_Module,
s be Element of V, a be Element of INT.Ring, b be Element of GF(p);
set t = ZMtoMQV(V,p,s);
assume A1: a=b;
A2: ZMtoMQV(V,p,s) = s + p(*)V;
reconsider t1 = t as Element of VectQuot(V,p(*)V);
A3: s + p(*)V is Element of CosetSet(V,p(*)V) by A2,VECTSP10:def 6;
reconsider i = b as Nat;
A4: b = i mod p by NAT_1:44,NAT_D:24;
i in INT by INT_1:def 2; then
reconsider i as Element of INT.Ring;
thus b*t = ((i mod p) qua Element of INT.Ring) * t1 by A4,ZMODUL02:def 11
.= lmultCoset(V,p(*)V).((i mod p),s + p(*)V) by VECTSP10:def 6
.= ZMtoMQV(V,p,a*s) by A1,A4,A3,VECTSP10:def 5;
end;
theorem Th31:
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
l being 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 Element of INT.Ring, V be free Z_Module, I be Basis of V,
l be 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
A2: for v being Vector of V st v in I holds
l.v = lq.(ZMtoMQV(V,p,v));
per cases;
suppose A3: I is empty;
IQ = {}
proof
assume IQ <> {};
then consider v0 be object such that
A4: v0 in IQ by XBOOLE_0:def 1;
consider u be Vector of V such that
A5: v0 = ZMtoMQV(V,p,u) & u in I by A4,A1;
thus contradiction by A5,A3;
end;
then IQ = {}(the carrier of Z_MQ_VectSp(V,p));
then lq = ZeroLC(Z_MQ_VectSp(V,p)) by VECTSP_6:6;
then
A6:Sum(lq) = 0.(Z_MQ_VectSp(V,p)) by VECTSP_6:15;
I = {}(the carrier of V) by A3;
then l = ZeroLC(V) by ZMODUL02:12;
then Sum(l) = 0. V by ZMODUL02:19;
hence Sum(lq) = ZMtoMQV(V,p,Sum(l)) by A6,Th27;
end;
suppose I is non empty; then
consider v0 be object such that
A7: v0 in I by XBOOLE_0:def 1;
reconsider v0 as Vector of V by A7;
ZMtoMQV(V,p,v0) in IQ by A7,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
A8: (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 Th25,A1;
consider Gq be FinSequence of Z_MQ_VectSp(V,p) such that
A9: Gq is one-to-one & rng Gq = Carrier(lq) & Sum(lq) = Sum(lq (#) Gq)
by VECTSP_6:def 6;
set n = len Gq;
A10: dom Gq = Seg n by FINSEQ_1:def 3;
A11: Carrier(lq) c= X by VECTSP_6:def 4;
A12: dom (F*Gq) = Seg n by A10,A9,A8,RELAT_1:27,VECTSP_6:def 4;
A13: rng (F*Gq) c= the carrier of V;
F*Gq is FinSequence by A8,A9,FINSEQ_1:16,VECTSP_6:def 4;
then reconsider FGq = F*Gq as FinSequence of V by A13,FINSEQ_1:def 4;
for x be object holds x in rng FGq iff x in Carrier(l)
proof
let x be object;
hereby assume x in rng FGq;
then consider z be object such that
A14: z in dom (FGq) & x = FGq.z by FUNCT_1:def 3;
A15: x = F.(Gq.z) by A14,FUNCT_1:12;
A16: z in dom Gq & Gq.z in dom F by A14,FUNCT_1:11;
then consider u be Vector of V such that
A17: Gq.z = ZMtoMQV(V,p,u) & u in I by A1,A8;
A18: F.(Gq.z) = u by A8,A17;
consider w be Element of Z_MQ_VectSp(V,p) such that
A19: Gq.z = w & lq.w <> 0.(GF(p)) by A9,A16,FUNCT_1:3,VECTSP_6:1;
l.u <> 0.(GF(p)) by A2,A17,A19;
then l.u <> 0 by EC_PF_1:11;
hence x in Carrier(l) by A15,A18;
end;
assume A20: x in Carrier(l);
then reconsider u=x as Vector of V;
A21: l.u <> 0 by A20,ZMODUL02:8;
A22: Carrier(l) c= I by VECTSP_6:def 4;
then lq.(ZMtoMQV(V,p,u)) <> 0 by A2,A21,A20;
then lq.(ZMtoMQV(V,p,u)) <> 0.(GF(p)) by EC_PF_1:11;
then
A23: ZMtoMQV(V,p,u) in rng Gq by A9;
then consider z be object such that
A24: z in dom Gq & ZMtoMQV(V,p,u) =Gq.z by FUNCT_1:def 3;
A25: F.(Gq.z) = u by A20,A22,A24,A8;
A26: z in dom (FGq) by A11,A9,A24,A8,A23,FUNCT_1:11;
then FGq.z = u by A25,FUNCT_1:12;
hence x in rng FGq by A26,FUNCT_1:def 3;
end;
then rng FGq = Carrier(l) by TARSKI:2;
then
A27: Sum(l) = Sum(l (#) FGq) by A9,A8,VECTSP_6:def 6;
A28: len (l (#) FGq) = len FGq by VECTSP_6:def 5;
then
A29: len (l (#) FGq) = n by A12,FINSEQ_1:def 3;
A30: len (lq (#) Gq) = n by VECTSP_6:def 5;
now let i be Element of NAT;
assume A31: i in dom (l (#) FGq);
then i in Seg (len (FGq)) by A28,FINSEQ_1:def 3;
then
A32: 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;
A33: (l (#) FGq ).i = (l.v)*v by A32,ZMODUL02:13;
i in Seg n by A29,A31,FINSEQ_1:def 3;
then
A34: i in dom Gq by FINSEQ_1:def 3;
then A35: Gq.i in rng Gq by FUNCT_1:3;
then
A36: Gq.i in X by A9,A11;
reconsider w = Gq.i as Element of Z_MQ_VectSp(V,p) by A35;
consider u be Vector of V such that
A37: Gq.i = ZMtoMQV(V,p,u) & u in I by A1,A36;
F.(Gq.i) = u by A8,A37;
then
A38: v = u by A32,FUNCT_1:12;
(lq (#) Gq).i = (lq.w)*w by A34,VECTSP_6:8
.= ZMtoMQV(V,p,(l.v)*v) by A2,A37,A38,Th30;
hence ex si be Vector of V st si=(l (#) FGq ).i &
(lq (#) Gq).i = ZMtoMQV(V,p,si) by A33;
end;
hence Sum(lq) = ZMtoMQV(V,p,Sum(l)) by A9,A27,A29,A30,Th29;
end;
end;
theorem Th32:
for p being prime Element of INT.Ring,
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 Element of INT.Ring, V be free Z_Module, I be Basis of V,
IQ be Subset of Z_MQ_VectSp(V,p) such that
A1: 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
A2: Sum(lq) = 0.Z_MQ_VectSp(V,p) and
A3: Carrier(lq) <> {};
consider Lq being Linear_Combination of Z_MQ_VectSp(V,p) such that
A4: Lq = lq;
consider l being Linear_Combination of I such that
A5: for v being Vector of V st v in I holds
l.v = Lq.(ZMtoMQV(V,p,v)) by Th24;
set vq0 = Sum(Lq);
set v0 = Sum(l);
A6: vq0 = ZMtoMQV(V,p,v0) by A1,A5,A4,Th31;
A7: vq0 = 0.(VectQuot(V,p(*)V)) by A2,A4
.= zeroCoset(V,p(*)V) by VECTSP10:def 6
.= 0.V + p(*)V by ZMODUL01:59;
consider vp being Vector of V such that
A8: vp in p(*)V & v0 + vp = 0.V by A6,A7,ZMODUL01:75;
reconsider pp = p as Element of INT.Ring;
vp in the set of all pp * v where v is Element of V by A8;
then consider vv being Element of V such that
A9: vp = pp * vv;
A10: I is linearly-independent & Lin(I) = the ModuleStr of V
by VECTSP_7:def 3;
consider lvv be Linear_Combination of I such that
A11: vv = Sum(lvv) by A10,STRUCT_0:def 5,ZMODUL02:64;
vp = Sum(p * lvv) by A9,A11,ZMODUL02:53; then
A12: 0.V = Sum(l + p * lvv) by A8,ZMODUL02:52;
reconsider pp = p as Element of INT.Ring;
p * lvv is Linear_Combination of I by ZMODUL02:31;
then l + pp * lvv is Linear_Combination of I by ZMODUL02:27;
then consider lpv being Linear_Combination of I such that
A13: lpv = l + pp * lvv;
ex vq being object st vq in Carrier(lq) by A3,XBOOLE_0:def 1;
then consider uq being Vector of Z_MQ_VectSp(V,p) such that
A14: uq in Carrier(lq);
uq in {v where v is Element of Z_MQ_VectSp(V,p) : lq.v <> 0.GF(p)}
by A14;
then consider uuq being Vector of Z_MQ_VectSp(V,p) such that
A15: uuq = uq & lq.uuq <> 0.GF(p);
A16: lq.uuq <> 0 by A15;
Carrier(lq) c= IQ by VECTSP_6:def 4;
then uq in IQ by A14;
then consider uu being Vector of V such that
A17: uq = ZMtoMQV(V, p, uu) & uu in I by A1;
A18: lq.uuq = l.uu by A4,A5,A15,A17;
lpv.uu <> 0.INT.Ring
proof
assume A19: lpv.uu = 0.INT.Ring;
(l+pp*lvv).uu = l.uu + (pp*lvv).uu by VECTSP_6:22
.= l.uu + pp * (lvv.uu) by VECTSP_6:def 9; then
0.INT.Ring = l.uu + pp * (lvv.uu) by A13,A19; then
l.uu = - (pp * (lvv.uu));
then l.uu = pp * (-lvv.uu);
then pp divides l.uu by INT_1:def 3;
then A20: l.uu mod p = 0 by INT_1:62;
thus contradiction by A16,A18,A20,NAT_1:44,NAT_D:63;
end;
then uu in Carrier(lpv);
hence contradiction by A12,A13,VECTSP_7:def 3,VECTSP_7:def 1;
end;
Lm3: for p being Prime, i be Element of INT
holds i mod p is Element of GF(p)
by INT_1:58,NAT_1:44;
Lm4: for p being prime Element of INT.Ring, V being free Z_Module,
i be Element of INT.Ring, v be Element of V
holds ZMtoMQV(V,p,((i mod p) qua Element of INT.Ring) * v) =
ZMtoMQV(V,p,i*v)
proof
let p be prime Element of INT.Ring, V be free Z_Module,
i be Element of INT.Ring, v be Element of V;
reconsider a = (i mod p) as Element of GF(p) by Lm3;
reconsider t1 = ZMtoMQV(V,p,v) as Element of VectQuot(V,p(*)V);
ZMtoMQV(V,p,v) = v + p(*)V; then
A1: v + p(*)V is Element of CosetSet(V,p(*)V) by VECTSP10:def 6;
thus ZMtoMQV(V,p,((i mod p) qua Element of INT.Ring) * v) =
a*ZMtoMQV(V,p,v) by Th30
.= ((i mod p) qua Element of INT.Ring) * t1 by ZMODUL02:def 11
.= i * t1 by ZMODUL02:2
.= lmultCoset(V,p(*)V).(i,v + p(*)V) by VECTSP10:def 6
.= ZMtoMQV(V,p,i*v) by A1,VECTSP10:def 5;
end;
theorem Th33:
for p being prime Element of INT.Ring, 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 Element of INT.Ring, 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[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);
A1: P[ 0 ]
proof
let s be FinSequence of V;
assume that A2: 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 A2;
then Sum(s) = 0. V by RLVECT_1:43;
then ZMtoMQV(V,p,Sum(s)) = 0.(Z_MQ_VectSp(V,p)) by Th27;
hence thesis by VECTSP_4:17;
end;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
now let s be FinSequence of V;
assume that
A5: len s = k+1 and
A6: 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;
A7: dom s = Seg (k+1) by A5,FINSEQ_1:def 3;
A8: len s1 = k by A5,FINSEQ_1:59,NAT_1:11;
A9: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by A5,FINSEQ_1:59,NAT_1:11; then
A10: s1 = s |dom s1 by FINSEQ_1:def 16;
s.(len s) in rng s by A5,A7,FINSEQ_1:4,FUNCT_1:3;
then reconsider vs = s.(len s) as Element of V;
A11: len s1 = k by A5,FINSEQ_1:59,NAT_1:11;
A12: 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 A13: 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
A14: si = s.i & ZMtoMQV(V,p,si) in Lin(IQ) by A6,A9,A7,A13;
take si;
thus si = s1.i by A10,A13,A14,FUNCT_1:49;
thus thesis by A14;
end;
A15: ZMtoMQV(V,p,Sum(s1)) in Lin(IQ) by A4,A11,A12;
consider ssi be Vector of V such that
A16: ssi = s.(len s) & ZMtoMQV(V,p,ssi) in Lin(IQ)
by A5,A6,A7,FINSEQ_1:4;
ZMtoMQV(V,p,Sum(s)) = ZMtoMQV(V,p,Sum(s1)+vs) by A5,A10,A8,RLVECT_1:38
.= ZMtoMQV(V,p,Sum(s1)) + ZMtoMQV(V,p,vs) by Th28;
hence ZMtoMQV(V,p,Sum(s)) in Lin(IQ) by A15,A16,VECTSP_4:20;
end;
hence P[k+1];
end;
A17: for k be Nat holds P[k] from NAT_1:sch 2(A1,A3);
now let s be FinSequence of V;
assume A18: 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 A17,A18;
end;
hence thesis;
end;
theorem Th34:
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p),
l be 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 be prime Element of INT.Ring,
V be free Z_Module, I be Basis of V,
IQ be Subset of Z_MQ_VectSp(V,p),
l be Linear_Combination of I;
assume A1: IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I};
consider G be FinSequence of V such that
A2: G is one-to-one & rng G = Carrier(l)
& Sum(l) = Sum(l (#) G) by VECTSP_6:def 6;
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 VECTSP_6:def 5;
then
A3: 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;
A4: (l (#) G ).i = (l.v)*v by A3,ZMODUL02:13;
reconsider b = ( (l.v) mod p ) as Element of GF(p) by Lm3;
reconsider a = ( (l.v) mod p ) as Element of INT.Ring;
reconsider k = l.v as Element of INT.Ring;
reconsider t = ZMtoMQV(V,p,v) as Element of Z_MQ_VectSp(V,p);
A5: b*t = ZMtoMQV(V,p,(a qua Element of INT.Ring) * v) by Th30
.= ZMtoMQV(V,p,(k qua Element of INT.Ring) * v) by Lm4;
A6: v in Carrier(l) by A3,A2,FUNCT_1:3;
Carrier(l) c= I by VECTSP_6:def 4;
then t in IQ by A1,A6;
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 A5,A4;
end;
hence ZMtoMQV(V,p,Sum(l)) in Lin(IQ) by A1,A2,Th33;
end;
theorem Th35:
for p being prime Element of INT.Ring,
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 Element of INT.Ring,
V be free Z_Module, I be Basis of V,
IQ be Subset of Z_MQ_VectSp(V,p);
assume A1: IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I};
A2: IQ is linearly-independent by Th32,A1;
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
A3: vq = ZMtoMQV(V,p,v) by Th22;
I is base; then
Lin (I) = the ModuleStr of V;
then consider l be Linear_Combination of I such that
A4: v = Sum(l) by STRUCT_0:def 5,ZMODUL02:64;
thus vq in Lin(IQ) by A1,A4,A3,Th34;
end; then
Lin IQ = the ModuleStr of Z_MQ_VectSp(V,p) by VECTSP_4:32; then
IQ is base by A2;
hence thesis;
end;
registration
let p be prime Element of INT.Ring, 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 object;
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 Th26;
then AQ is finite Subset of W;
hence thesis by Th35,MATRLIN:def 1;
end;
end;
theorem Th36:
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 Element of INT.Ring;
set AQ = {ZMtoMQV(V, p, u) where u is Vector of V : u in A};
now let x be object;
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 object;
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;
A1: card A = card AQ by Th26;
A2: card B = card BQ by Th26;
A3: AQ is Basis of Z_MQ_VectSp(V, p) by Th35;
BQ is Basis of Z_MQ_VectSp(V, p) by Th35;
hence card A = card B by A1,A2,A3,VECTSP_9:22;
end;
definition
let V be finite-rank free Z_Module;
func rank(V) -> Nat means :Def5:
for I being Basis of V holds it = card I;
existence
proof
consider A being finite Subset of V such that
A1: A is Basis of V by Def3;
consider n being Nat such that
A2: n = card A;
for I being Basis of V holds card I = n by A1,A2,Th36;
hence thesis;
end;
uniqueness
proof
let n, m be Nat;
assume that
A3: for I being Basis of V holds card I = n and
A4: for I being Basis of V holds card I = m;
consider A being finite Subset of V such that
A5: A is Basis of V by Def3;
card A = n by A3,A5;
hence thesis by A4,A5;
end;
end;
theorem
for p be prime Element of INT.Ring, V be finite-rank free Z_Module holds
rank V = dim Z_MQ_VectSp(V,p)
proof
let p be prime Element of INT.Ring, 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 object;
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;
A1: card A = card AQ by Th26;
AQ is Basis of W by Th35;
then dim W = card AQ by VECTSP_9:def 1;
hence thesis by A1,Def5;
end;