:: Submodule of free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-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 GAUSSINT, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0,
FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, RLSUB_2,
EQREL_1, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1,
FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, ORDINAL1,
RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2,
VECTSP_1, MESFUNC1, REALSET1, MONOID_0, VECTSP10, EC_PF_1, MOD_3,
ZMODUL02, RLVECT_5, ORDINAL2, ZMODUL04, INT_2, INT_3, FUNCSDOM, VECTSP_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, ORDINAL2, FINSET_1,
ORDERS_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2,
RAT_1, REALSET1, FINSEQ_1, EQREL_1, STRUCT_0, ALGSTR_0, GROUP_1,
RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
VECTSP_9, MATRLIN, INT_3, EC_PF_1, ZMODUL01, ZMODUL02, ZMODUL03,
GAUSSINT, VECTSP10;
constructors BINOP_2, RELSET_1, ORDERS_1, REALSET1, GR_CY_1, VECTSP_6,
GROUP_1, REAL_1, RLVECT_2, VECTSP_2, VECTSP_9, VECTSP10, ALGSTR_1,
ZMODUL02, ORDINAL3, ZMODUL03, GAUSSINT, VECTSP_4, VECTSP_7, ZMODUL01,
VECTSP_5, INT_3, VFUNCT_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0,
ORDINAL1, XXREAL_0, NAT_1, INT_3, RELAT_1, ZMODUL02, GAUSSINT, EQREL_1,
RAT_1, XCMPLX_0, ZMODUL03, ZMODUL01, VECTSP_7;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, ZMODUL03;
equalities STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, ZMODUL02, GAUSSINT, VECTSP_4,
VECTSP_6;
expansions STRUCT_0, XBOOLE_0;
theorems BINOP_1, CARD_1, CARD_2, SUBSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, INT_1,
NAT_1, RLVECT_1, TARSKI, ZMODUL01, BINOP_2, ZFMISC_1, RELAT_1, XTUPLE_0,
ZMODUL03, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDINAL1, STRUCT_0, VECTSP_1,
ALGSTR_0, EC_PF_1, INT_2, WELLORD2, ZMODUL02, VECTSP_6, VECTSP_7,
NUMBERS, VECTSP_4, VECTSP_9, EQREL_1, MATRLIN, RAT_1, GROUP_1, ORDINAL2,
VECTSP_5, VECTSP10;
schemes BINOP_1, FUNCT_2, NAT_1, EQREL_1, INT_1;
begin :: 1. Vector space of rational field generated by a free Z-module
reserve V for Z_Module;
reserve W, W1, W2 for Submodule of V;
Lem1:
for i being Integer holds i in the carrier of INT.Ring by INT_1:def 2;
theorem
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
WW1, WW2 being Subspace of W1 + W2
st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2
proof
let R be Ring;
let V be LeftMod of R, W1, W2 be Subspace of V,
WW1, WW2 be Subspace of W1 + W2 such that
A1: WW1 = W1 & WW2 = W2;
A2: WW1 + WW2 is Subspace of V by VECTSP_4:26;
for x being object holds x in W1 + W2 iff x in WW1 + WW2
proof
let x be object;
hereby
assume x in W1 + W2;
then consider v1, v2 being Vector of V such that
B2: v1 in W1 & v2 in W2 & x = v1 + v2 by VECTSP_5:1;
v1 in W1 + W2 & v2 in W1 + W2 by B2,VECTSP_5:2;
then reconsider vv1 = v1, vv2 = v2 as Vector of W1 + W2;
v1 in WW1 & v2 in WW2 & x = vv1 + vv2 by A1,B2,VECTSP_4:13;
hence x in WW1 + WW2 by VECTSP_5:1;
end;
assume x in WW1 + WW2;
then consider vv1, vv2 being Vector of W1 + W2 such that
B1: vv1 in WW1 & vv2 in WW2 & x = vv1 + vv2 by VECTSP_5:1;
thus x in W1 + W2 by B1;
end;
then for x being Vector of V holds x in W1 + W2 iff x in WW1 + WW2;
hence thesis by A2,VECTSP_4:30;
end;
theorem
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
WW1, WW2 being Subspace of W1 + W2
st WW1 = W1 & WW2 = W2 holds
W1 /\ W2 = WW1 /\ WW2
proof
let R be Ring;
let V be LeftMod of R, W1, W2 be Subspace of V,
WW1, WW2 be Subspace of W1 + W2 such that
A1: WW1 = W1 & WW2 = W2;
A2: WW1 /\ WW2 is Subspace of V by VECTSP_4:26;
for x being object holds x in W1 /\ W2 iff x in WW1 /\ WW2
proof
let x be object;
hereby
assume x in W1 /\ W2;
then x in WW1 & x in WW2 by A1,VECTSP_5:3;
hence x in WW1 /\ WW2 by VECTSP_5:3;
end;
assume x in WW1 /\ WW2;
then x in W1 & x in W2 by A1,VECTSP_5:3;
hence x in W1 /\ W2 by VECTSP_5:3;
end;
then for x being Vector of V holds x in W1 /\ W2 iff x in WW1/\ WW2;
hence thesis by A2,VECTSP_4:30;
end;
Lm19: for A, B being set st ( for z being object st z in A holds
ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds
ex x, y being object st z = [x,y] ) & ( for x, y being object holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
proof
let A, B be set;
assume that
A1: for z being object st z in A holds
ex x, y being object st z = [x,y] and
A2: for z being object st z in B holds
ex x, y being object st z = [x,y] and
A3: for x, y being object holds [x,y] in A iff [x,y] in B;
now
let z be object;
A4: z in B implies ex x, y being object st z = [x,y] by A2;
z in A implies ex x, y being object st z = [x,y] by A1;
hence z in A iff z in B by A3,A4;
end;
hence A = B by TARSKI:2;
end;
registration ::: generalize for arbitrary products
let V be Z_Module;
cluster [:the carrier of V,INT \ {0}:] -> non empty;
coherence
proof
X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then (INT \{0}) <> {} by X1,XBOOLE_0:def 5;
hence thesis;
end;
end;
definition
let V be Z_Module;
assume AS: V is Mult-cancelable;
func EQRZM(V) -> Equivalence_Relation of [:the carrier of V,INT \{0}:]
means :defEQRZM:
for S,T being object holds
[S,T] in it
iff ( S in [:the carrier of V,INT \{0}:]
& T in [:the carrier of V,INT \{0}:]
& ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st S=[z1,i1] & T=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2);
existence
proof
defpred P1[ object, object ] means
ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st $1=[z1,i1] & $2=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2;
A1: for x being object st x in [:the carrier of V,(INT \{0}):]
holds P1[x,x]
proof
let x be object;
assume x in [:the carrier of V,(INT \{0}):]; then
consider z1,i1 be object such that
A11: z1 in the carrier of V & i1 in INT \{0} & x = [z1,i1]
by ZFMISC_1:def 2;
reconsider z1 as Element of V by A11;
A12: i1 in INT & not i1 in {0} by XBOOLE_0:def 5,A11;
reconsider i1 as Integer by A11;
reconsider i1 as Element of INT.Ring by A11;
i1 <> 0 & i1 <> 0 & i1*z1 = i1*z1 by A12,TARSKI:def 1;
hence P1[x,x] by A11;
end;
A2: for x, y being object st P1[x,y] holds P1[y,x];
A3: for x, y, z being object st P1[x,y] & P1[y,z] holds P1[x,z]
proof
let x, y, z be object;
assume A31: P1[x,y] & P1[y,z]; then
consider z1, z2 be Element of V,i1,i2 be Element of INT.Ring such that
A32: x=[z1,i1] & y=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2;
consider z3, z4 be Element of V,i3,i4 be Element of INT.Ring such that
A33: y=[z3,i3] & z=[z4,i4] & i3 <> 0 & i4 <> 0 & i4*z3 = i3*z4 by A31;
A34: z2 = z3 & i2=i3 by A32,A33,XTUPLE_0:1;
i2*(i4*z1) = (i2*i4)*z1 by VECTSP_1:def 16
.= (i4*i2)*z1
.= i4*(i2*z1) by VECTSP_1:def 16
.= i4*(i1*z2) by A32
.= (i4*i1)*z2 by VECTSP_1:def 16
.= (i1*i4)*z2
.= i1*(i4*z2) by VECTSP_1:def 16
.= (i1*i2)*z4 by A33,A34,VECTSP_1:def 16
.= (i2*i1)*z4
.= i2*(i1*z4) by VECTSP_1:def 16;
hence P1[x,z] by AS,A32,A33,ZMODUL01:10;
end;
consider EqR being Equivalence_Relation
of [:the carrier of V,(INT \{0}):] such that
A4:for x, y being object holds
[x,y] in EqR iff ( x in [:the carrier of V,(INT \{0}):]
& y in [:the carrier of V,(INT \{0}):]
& P1[x,y] ) from EQREL_1:sch 1(A1,A2,A3);
take EqR;
thus thesis by A4;
end;
uniqueness
proof
let EqR1,EqR2 be Equivalence_Relation of [:the carrier of V,(INT \{0}):];
assume
A1: for S,T being object holds
( [S,T] in EqR1 iff ( S in [:the carrier of V,(INT \{0}):]
& T in [:the carrier of V,(INT \{0}):]
& ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st S=[z1,i1] & T=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2 ));
assume
A2: for S,T being object holds
[S,T] in EqR2
iff ( S in [:the carrier of V,(INT \{0}):]
& T in [:the carrier of V,(INT \{0}):]
& ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st S=[z1,i1] & T=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2 );
A3: for z being object st z in EqR1 holds
ex x, y being object st z = [x,y] by RELAT_1:def 1;
A4: for z being object st z in EqR2 holds
ex x, y being object st z = [x,y] by RELAT_1:def 1;
for x, y being object holds [x,y] in EqR1 iff [x,y] in EqR2
proof
let S, T be object;
[S,T] in EqR2 iff (S in [:the carrier of V,(INT \{0}):]
& T in [:the carrier of V,(INT \{0}):]
& ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st S=[z1,i1] & T=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2 ) by A2;
hence thesis by A1;
end;
hence EqR1 = EqR2 by Lm19,A3,A4;
end;
end;
theorem LMEQR001:
for V be Z_Module,
z1, z2 be Element of V, i1, i2 be Element of INT.Ring
st V is Mult-cancelable holds
[[z1,i1],[z2,i2]] in EQRZM(V) iff
i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2
proof
let V be Z_Module,
z1, z2 be Element of V,i1,i2 be Element of INT.Ring;
assume AS: V is Mult-cancelable;
hereby
assume [[z1,i1],[z2,i2]] in EQRZM(V);
then consider zz1, zz2 be Element of V,ii1,ii2 be Element of INT.Ring
such that
P2: [z1,i1] = [zz1,ii1] & [z2,i2] = [zz2,ii2]
& ii1 <> 0 & ii2 <> 0 & ii2*zz1 = ii1*zz2 by AS,defEQRZM;
z1 = zz1 & i1 = ii1 & z2 = zz2 & i2 = ii2 by P2,XTUPLE_0:1;
hence i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2 by P2;
end;
assume A2: i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2; then
A21: not i1 in {0} & not i2 in {0} by TARSKI:def 1;
i1 in INT \{0} & i2 in INT \{0} by XBOOLE_0:def 5,A21;
then [z1,i1] in [:the carrier of V,(INT \{0}):] &
[z2,i2] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
hence [[z1,i1],[z2,i2]] in EQRZM(V) by A2,AS,defEQRZM;
end;
definition
let V be Z_Module;
assume AS: V is Mult-cancelable;
func addCoset(V) -> BinOp of Class EQRZM(V) means :DefaddCoset:
for A, B be object st A in Class EQRZM(V) & B in Class EQRZM(V) holds
for z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st i1 <> 0.INT.Ring & i2 <> 0.INT.Ring
& A=Class(EQRZM(V),[z1,i1]) & B=Class(EQRZM(V),[z2,i2]) holds
it.(A,B) = Class(EQRZM(V),[i2*z1+i1*z2,i1*i2]);
existence
proof
defpred P[object,object,object] means
for z1, z2 be Element of V, i1, i2 be Element of INT.Ring
st i1 <>0 & i2 <> 0
& $1 = Class(EQRZM(V),[z1,i1]) & $2 = Class(EQRZM(V),[z2,i2])
holds $3 = Class(EQRZM(V),[i2*z1+i1*z2,i1*i2]);
set C = Class EQRZM(V);
A1:
now
let A, B be object;
assume A10: A in C & B in C;
then consider A1 be object such that
A2: A1 in [:the carrier of V,(INT \{0}):] & A = Class(EQRZM(V),A1)
by EQREL_1:def 3;
consider z1, i1 be object such that
A3: z1 in the carrier of V & i1 in INT \{0} & A1 = [z1,i1]
by A2,ZFMISC_1:def 2;
reconsider z1 as Element of V by A3;
i1 in INT & not i1 in {0} by XBOOLE_0:def 5,A3;
then A31: i1 in INT & i1 <> 0 by TARSKI:def 1;
reconsider i1 as Integer by A3;
reconsider i1 as Element of INT.Ring by A3;
consider B1 be object such that
A4: B1 in [:the carrier of V,(INT \{0}):] & B=Class(EQRZM(V),B1)
by A10,EQREL_1:def 3;
consider z2, i2 be object such that
A5: z2 in the carrier of V & i2 in INT \{0} & B1 = [z2,i2]
by A4,ZFMISC_1:def 2;
reconsider z2 as Element of V by A5;
i2 in INT & not i2 in {0} by XBOOLE_0:def 5,A5;
then A51: i2 in INT & i2 <> 0 by TARSKI:def 1;
reconsider i2 as Integer by A5;
reconsider i2 as Element of INT.Ring by A5;
A61: not i1*i2 in {0} by A31,A51,TARSKI:def 1;
i1*i2 in INT \ {0} by XBOOLE_0:def 5,A61;
then X1: [i2*z1+i1*z2,i1*i2] in [:the carrier of V,(INT \{0}):]
by ZFMISC_1:87;
set z = Class(EQRZM(V),[i2*z1+i1*z2,i1*i2]);
A7: z in C by X1,EQREL_1:def 3;
P[A,B,z]
proof
let zz1, zz2 be Element of V, ii1, ii2 be Element of INT.Ring;
assume A71: ii1 <>0 & ii2 <> 0
& A=Class(EQRZM(V),[zz1,ii1]) & B=Class(EQRZM(V),[zz2,ii2]);
then A72: not ii1 in {0} by TARSKI:def 1;
ii1 in INT \ {0} by XBOOLE_0:def 5,A72;
then X2: [zz1,ii1] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
X21: not ii2 in {0} by TARSKI:def 1,A71;
ii2 in INT \ {0} by XBOOLE_0:def 5,X21;
then X3: [zz2,ii2] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
X5: [[zz1,ii1],[z1,i1]] in EQRZM(V)
by X2,A2,A3,A71,EQREL_1:35;
then XX5: ii1 <> 0 & i1 <> 0 & i1*zz1 = ii1*z1 by LMEQR001,AS;
X7: [[zz2,ii2],[z2,i2]] in EQRZM(V)
by X3,A4,A5,A71,EQREL_1:35;
then XX7: ii2 <> 0 & i2 <> 0 & i2*zz2 = ii2*z2 by LMEQR001,AS;
(ii1*ii2)*(i2*z1+i1*z2)
= (ii1*ii2)*(i2*z1) + (ii1*ii2)*(i1*z2) by VECTSP_1:def 14
.= (ii1*ii2*i2)*z1 + (ii1*ii2)*(i1*z2) by VECTSP_1:def 16
.= (ii2*i2*ii1)*z1 + (ii1*ii2*i1)*z2 by VECTSP_1:def 16
.= (ii2*i2)*(ii1*z1) + (ii1*i1*ii2)*z2 by VECTSP_1:def 16
.= (ii2*i2)*(ii1*z1) + (ii1*i1)*(ii2*z2) by VECTSP_1:def 16
.= (ii2*i2)*(i1*zz1) + (ii1*i1)*(ii2*z2) by AS,X5,LMEQR001
.= (ii2*i2)*(i1*zz1) + (ii1*i1)*(i2*zz2) by AS,X7,LMEQR001
.= (ii2*i2*i1)*zz1 + (ii1*i1)*(i2*zz2) by VECTSP_1:def 16
.= (i2*i1*ii2)*zz1 + (ii1*i1*i2)*zz2 by VECTSP_1:def 16
.= (i1*i2)*(ii2*zz1) + (i1*i2*ii1)*zz2 by VECTSP_1:def 16
.= (i1*i2)*(ii2*zz1) + (i1*i2)*(ii1*zz2) by VECTSP_1:def 16
.= (i1*i2)*(ii2*zz1+ii1*zz2) by VECTSP_1:def 14;
then [[i2*z1+i1*z2,i1*i2], [ii2*zz1+ii1*zz2,ii1*ii2]] in EQRZM(V)
by XX5,XX7,LMEQR001,AS;
hence thesis by X1,EQREL_1:35;
end;
hence ex z be object st z in C & P[A,B,z] by A7;
end;
consider f be Function of [:C,C:],C such that
A14: for A,B be object st A in C & B in C holds P[A,B, f.(A,B)]
from BINOP_1:sch 1(A1);
reconsider f as BinOp of C;
take f;
thus thesis by A14;
end;
uniqueness
proof
defpred P[object,object,object] means
for z1, z2 be Element of V,i1,i2 be Element of INT.Ring
st i1 <> 0.INT.Ring & i2 <> 0.INT.Ring
& $1=Class(EQRZM(V),[z1,i1]) & $2=Class(EQRZM(V),[z2,i2])
holds $3= Class(EQRZM(V),[i2*z1+i1*z2,i1*i2]);
set C = Class EQRZM(V);
let f1, f2 be BinOp of C such that
A15: for A, B be object st A in C & B in C holds P[A,B,f1.(A,B)] and
A16: for A, B be object st A in C & B in C holds P[A,B,f2.(A,B)];
now
let A, B be set;
assume X0: A in C & B in C;
then consider A1 be object such that
A2: A1 in [:the carrier of V,(INT \{0}):]
& A = Class(EQRZM(V),A1) by EQREL_1:def 3;
consider z1, i1 be object such that
A3: z1 in the carrier of V & i1 in INT \{0}
& A1 = [z1,i1] by A2,ZFMISC_1:def 2;
reconsider z1 as Element of V by A3;
i1 in INT & not i1 in {0} by XBOOLE_0:def 5,A3;
then A31: i1 in INT & i1 <> 0 by TARSKI:def 1;
reconsider i1 as Integer by A3;
consider B1 be object such that
A4: B1 in [:the carrier of V,(INT \{0}):]
& B = Class(EQRZM(V),B1) by X0,EQREL_1:def 3;
consider z2, i2 be object such that
A5: z2 in the carrier of V & i2 in INT \{0}
& B1 = [z2,i2] by A4,ZFMISC_1:def 2;
reconsider z2 as Element of V by A5;
i2 in INT & not i2 in {0} by XBOOLE_0:def 5,A5;
then A51: i2 in INT & i2 <> 0 by TARSKI:def 1;
reconsider i2 as Integer by A5;
reconsider i1,i2 as Element of INT.Ring by Lem1;
thus f1.(A,B) = Class(EQRZM(V),[i2*z1+i1*z2,i1*i2])
by A2,A3,A4,A5,A15,A31,A51,X0
.=f2.(A,B) by A2,A3,A4,A5,A16,A31,A51,X0;
end;
hence thesis by BINOP_1:1;
end;
end;
definition
let V be Z_Module;
assume AS: V is Mult-cancelable;
func zeroCoset(V) -> Element of Class EQRZM(V) means :defZero:
for i be Integer st i <> 0 holds it = Class(EQRZM(V),[0.V,i]);
existence
proof
X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then 1 in (INT \{0}) by XBOOLE_0:def 5,X1;
then [0.V,1] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
then reconsider z = Class(EQRZM(V),[0.V,1]) as Element of Class EQRZM(V)
by EQREL_1:def 3;
take z;
for i be Integer st i <> 0 holds z = Class(EQRZM(V),[0.V,i])
proof
let i be Integer;
assume X2: i <> 0;
then X21: not i in {0} by TARSKI:def 1;
Z1: i in INT by INT_1:def 2;
then i in INT \{0} by XBOOLE_0:def 5,X21;
then X3: [0.V,i] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
reconsider i as Element of INT.Ring by Z1;
1.INT.Ring*0.V = 0.V by ZMODUL01:1
.= i*0.V by ZMODUL01:1;
then [[0.V,i],[0.V,1]] in EQRZM(V) by AS,X2,LMEQR001;
hence thesis by X3,EQREL_1:35;
end;
hence thesis;
end;
uniqueness
proof
let z1,z2 be Element of Class EQRZM(V);
assume
AS1: for i be Integer st i <> 0 holds z1 = Class(EQRZM(V),[0.V,i]);
assume
AS2: for i be Integer st i <> 0 holds z2 = Class(EQRZM(V),[0.V,i]);
thus z1 = Class(EQRZM(V),[0.V,1]) by AS1
.= z2 by AS2;
end;
end;
definition
let V be Z_Module;
assume AS: V is Mult-cancelable;
func lmultCoset(V) -> Function of
[:the carrier of F_Rat, Class EQRZM(V):], Class EQRZM(V) means
:DeflmultCoset:
for q be object, A be object st q in RAT & A in Class EQRZM(V) holds
for m,n,i be Integer, mm being Element of INT.Ring, z be Element of V
st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class(EQRZM(V),[z,i])
holds it.(q,A) = Class(EQRZM(V),[mm*z,n*i]);
existence
proof
defpred P[object, object, object] means
for m, n, i be Integer, mm being Element of INT.Ring, z be Element of V
st mm = m & n <> 0 & $1 = m/n &
i <> 0 & $2 = Class(EQRZM(V),[z,i])
holds $3 = Class(EQRZM(V),[mm*z,n*i]);
set cF = RAT;
set C = Class EQRZM(V);
A1:
now
let q, A be object;
assume AS0: q in RAT & A in C;
then consider A1 be object such that
A2: A1 in [:the carrier of V,(INT \{0}):]
& A = Class(EQRZM(V),A1) by EQREL_1:def 3;
consider z,i be object such that
A3: z in the carrier of V & i in INT \{0}
& A1 = [z,i] by A2,ZFMISC_1:def 2;
reconsider z as Element of V by A3;
i in INT & not i in {0} by XBOOLE_0:def 5,A3;
then A31: i in INT & i <> 0 by TARSKI:def 1;
reconsider i as Integer by A3;
consider m, n be Integer such that
A4: n > 0 & q = m/n by AS0,RAT_1:1;
reconsider I=i,mn = m,no=n as Element of INT.Ring by Lem1;
A61: not no*i in {0} by A31,A4,TARSKI:def 1;
no*i in INT by INT_1:def 2;
then no*i in INT \ {0} by XBOOLE_0:def 5,A61;
then X1: [mn*z,no*i] in [:the carrier of V,INT \ {0}:] by ZFMISC_1:87;
set w = Class(EQRZM(V),[mn*z,no*i]);
A7: w in C by X1,EQREL_1:def 3;
P[q,A,w]
proof
let mm, nn, ii be Integer, m1 be Element of INT.Ring,
zz be Element of V;
assume
A71: m1 = mm & nn <> 0 & q = mm/nn & ii <> 0 &
A = Class(EQRZM(V),[zz,ii]);
then A72: not ii in {0} by TARSKI:def 1;
ii in INT by INT_1:def 2;
then ii in INT \ {0} by XBOOLE_0:def 5,A72;
then X2: [zz,ii] in [:the carrier of V,INT \ {0}:] by ZFMISC_1:87;
reconsider i2 = ii, n1 = nn as Element of INT.Ring by
INT_1:def 2;
X51: [[zz,i2],[z,I]] in EQRZM(V) by X2,A2,A3,A71,EQREL_1:35;
(n1*i2)*(mn*z) = (n1*i2*mn)*z by VECTSP_1:def 16
.= (n1*mn*i2)*z
.= (n1*mn)*(i2*z) by VECTSP_1:def 16
.= (n1*mn)*(I*zz) by AS,X51,LMEQR001
.= (no*m1)*(I*zz) by A4,A71,XCMPLX_1:95
.= (no*m1*I)*zz by VECTSP_1:def 16
.= (no*I*m1)*zz
.= (no*I)*(m1*zz) by VECTSP_1:def 16;
then [[mn*z,no*I], [m1*zz,n1*i2]] in EQRZM(V)
by A31,A4,A71,LMEQR001,AS;
hence thesis by X1,EQREL_1:35;
end;
hence ex w be object st w in C & P[q,A,w] by A7;
end;
consider f be Function of [:RAT,C:],C such that
A14: for q,A be object st q in RAT & A in C
holds P[q,A, f.(q,A)] from BINOP_1:sch 1(A1);
reconsider f as Function of [:the carrier of F_Rat,C:],C;
take f;
thus thesis by A14;
end;
uniqueness
proof
set cF = the carrier of F_Rat;
set C = Class EQRZM(V);
let f1, f2 be Function of [:cF, C:], C;
assume
A7: for q, A be object st q in RAT & A in Class EQRZM(V)
holds for m, n, i be Integer, mm being Element of INT.Ring,
z be Element of V
st mm = m & n <> 0 & q = m/n & i <> 0 &
A = Class(EQRZM(V),[z,i])
holds f1.(q,A) = Class(EQRZM(V),[mm*z,n*i]);
assume
A8: for q be object, A be object st q in RAT & A in Class EQRZM(V)
holds for m,n,i be Integer, mm be Element of INT.Ring, z be Element of V
st mm = m & n <> 0 & q = m/n & i <> 0 &
A = Class(EQRZM(V),[z,i])
holds f2.(q,A) = Class(EQRZM(V),[mm*z,n*i]);
now
let q, A be object;
assume AS0: q in RAT & A in C;
then consider A1 be object such that
A2: A1 in [:the carrier of V,(INT \{0}):]
& A = Class(EQRZM(V),A1) by EQREL_1:def 3;
consider z, i be object such that
A3: z in the carrier of V & i in INT \{0}
& A1 = [z,i] by A2,ZFMISC_1:def 2;
reconsider z as Element of V by A3;
i in INT & not i in {0} by XBOOLE_0:def 5,A3;
then A31: i in INT & i <> 0 by TARSKI:def 1;
reconsider i as Integer by A3;
consider m, n be Integer such that
A4: n > 0 & q = m/n by AS0,RAT_1:1;
reconsider m, i, n as Element of INT.Ring by Lem1;
i <> 0.INT.Ring by A31;
hence f1.(q,A) = Class(EQRZM(V),[m*z,n*i]) by AS0,A2,A3,A4,A7
.= f2.(q,A) by AS0,A2,A3,A4,A8,A31;
end;
then
for q be Element of F_Rat, A be Element of C holds f1.(q,A) = f2.(q,A);
hence thesis by BINOP_1:2;
end;
end;
theorem LMEQR003:
for V be Z_Module,
z be Element of V,
i, n be Element of INT.Ring
st i <> 0.INT.Ring & n <> 0.INT.Ring & V is Mult-cancelable holds
Class(EQRZM(V),[z,i]) = Class(EQRZM(V),[n*z,n*i])
proof
let V be Z_Module, z be Element of V,
i, n be Element of INT.Ring;
assume AS: i <> 0.INT.Ring & n <> 0.INT.Ring & V is Mult-cancelable; then
B61: not i in {0} by TARSKI:def 1;
i in INT \ {0} by XBOOLE_0:def 5,B61; then
X1: [z,i] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
(n*i)*z = (i*n)*z .= i*(n*z) by VECTSP_1:def 16;
then [[z,i], [n*z,n*i]] in EQRZM(V) by AS,LMEQR001;
hence Class(EQRZM(V),[z,i])= Class(EQRZM(V),[n*z,n*i]) by X1,EQREL_1:35;
end;
theorem LMEQRZM1:
for V be Z_Module,
v be Element of
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #)
st V is Mult-cancelable holds
ex i be Element of INT.Ring, z be Element of V
st i <> 0.INT.Ring & v = Class(EQRZM(V),[z,i])
proof
let V be Z_Module, v be Element of
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #);
assume V is Mult-cancelable;
v in Class EQRZM(V);
then consider A1 be object such that
A1: A1 in [:the carrier of V,(INT \{0}):] & v=Class(EQRZM(V),A1)
by EQREL_1:def 3;
consider z, i be object such that
A2: z in the carrier of V & i in INT \{0} & A1 = [z,i]
by A1,ZFMISC_1:def 2;
reconsider z as Element of V by A2;
A31: i in INT & not i in {0} by XBOOLE_0:def 5,A2;
reconsider i as Integer by A2;
reconsider i as Element of INT.Ring by A2;
take i,z;
thus i <> 0.INT.Ring & v = Class(EQRZM(V),[z,i])
by A1,A2,A31,TARSKI:def 1;
end;
ThEQRZMV1:
for V be Z_Module st V is Mult-cancelable holds
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V),
lmultCoset(V) #) is VectSp of F_Rat
proof
let V be Z_Module;
assume AS: V is Mult-cancelable;
reconsider IT =
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #)
as non empty ModuleStr over F_Rat;
set F = F_Rat;
set AD = addCoset(V);
set ML = lmultCoset(V);
P1: for x being Element of F
for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w)
proof
let x be Element of F, v, w be Element of IT;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
consider j be Element of INT.Ring, y be Element of V such that
X2: j <> 0 & w = Class(EQRZM(V),[y,j]) by AS,LMEQRZM1;
consider m, n be Integer such that
X3: n > 0 & x = m/n by RAT_1:1;
reconsider m,n as Element of INT.Ring by Lem1;
X5: v + w = Class(EQRZM(V),[j*z+i*y,i*j]) by X1,X2,DefaddCoset,AS;
X7: x * v = Class(EQRZM(V),[m*z,n*i]) by DeflmultCoset,AS,X1,X3;
X8: x * w = Class(EQRZM(V),[m*y,n*j]) by DeflmultCoset,AS,X2,X3;
X11: (n*j)*(m*z) + (n*i)*(m*y) = (n*j*m)*z + (n*i)*(m*y)
by VECTSP_1:def 16
.= (n*m*j)*z + (n*i*m)*y by VECTSP_1:def 16
.= (n*m)*(j*z)+ (n*m*i)*y by VECTSP_1:def 16
.= (n*m)*(j*z)+ (n*m)*(i*y) by VECTSP_1:def 16
.= n*(m*(j*z))+ (n*m)*(i*y) by VECTSP_1:def 16
.= n*(m*(j*z))+ n*(m*(i*y)) by VECTSP_1:def 16
.= n*(m*(j*z)+ m*(i*y)) by VECTSP_1:def 14
.= n*(m*(j*z+ i*y)) by VECTSP_1:def 14;
(x * v) + (x * w)
= Class(EQRZM(V),[(n*j)*(m*z) + (n*i)*(m*y),(n*i)*(n*j)])
by X1,X2,X3,X7,X8,DefaddCoset,AS
.= Class(EQRZM(V),[n*(m*(j*z+ i*y)),n*(n*(i*j))]) by X11
.= Class(EQRZM(V),[m*(j*z+i*y),n*(i*j)]) by AS,X1,X2,X3,LMEQR003;
hence x * (v + w) = (x * v) + (x * w) by DeflmultCoset,AS,X1,X2,X3,X5;
end;
P2: for x, y being Element of F
for v being Element of IT holds (x + y) * v = (x * v) + (y * v)
proof
let x, y be Element of F, v be Element of IT;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
consider m, n be Integer such that
X3: n > 0 & x = m/n by RAT_1:1;
consider l, k be Integer such that
Y3: k > 0 & y = l/k by RAT_1:1;
Y4: x+y = (m/n) + (l/k) by X3,Y3
.= (k*m + n*l)/(n*k) by XCMPLX_1:116,X3,Y3;
reconsider l,k,m,n as Element of INT.Ring by Lem1;
X7: x * v = Class(EQRZM(V),[m*z,n*i]) by DeflmultCoset,AS,X1,X3;
X8: y * v = Class(EQRZM(V),[l*z,k*i]) by DeflmultCoset,AS,X1,Y3;
X11: (k*i)*(m*z) + (n*i)*(l*z)
= (k*i*m)*z + (n*i)*(l*z) by VECTSP_1:def 16
.= (i*(k*m))*z + (i*n*l)*z by VECTSP_1:def 16
.= i*((k*m)*z) + (i*(n*l))*z by VECTSP_1:def 16
.= i*((k*m)*z) + i*((n*l)*z) by VECTSP_1:def 16
.= i*((k*m)*z + (n*l)*z) by VECTSP_1:def 14
.= i*((k*m + n*l)*z ) by VECTSP_1:def 15;
(x * v) + (y * v)
= Class(EQRZM(V),[(k*i)*(m*z) + (n*i)*(l*z),(n*i)*(k*i)])
by X1,X3,X7,X8,Y3,DefaddCoset,AS
.= Class(EQRZM(V),[i*((k*m + n*l)*z ), i*((n*k)*i)]) by X11
.= Class(EQRZM(V),[(k*m + n*l)*z,(n*k)*i ]) by AS,X1,X3,Y3,LMEQR003;
hence (x + y) * v = (x * v) + (y * v) by DeflmultCoset,AS,X1,X3,Y3,Y4;
end;
P3: for x, y being Element of F
for v being Element of IT holds (x * y) * v = x * (y * v)
proof
let x, y be Element of F,v be Element of IT;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
consider m, n be Integer such that
X3: n > 0 & x = m/n by RAT_1:1;
consider l, k be Integer such that
Y3: k > 0 & y = l/k by RAT_1:1;
reconsider mm=m,nn=n,ll=l,kk=k as Element of INT.Ring by Lem1;
Y4: x*y = (m/n) * (l/k) by X3,Y3
.= (m*l)/(n*k) by XCMPLX_1:76;
X8: y * v = Class(EQRZM(V),[ll*z,kk*i]) by DeflmultCoset,AS,X1,Y3;
x * (y * v) = Class(EQRZM(V),[mm*(ll*z),nn*(kk*i)])
by DeflmultCoset,AS,X1,X3,X8,Y3
.= Class(EQRZM(V),[(mm*ll)*z, (nn*kk)*i]) by VECTSP_1:def 16;
hence (x * y) * v = x * (y * v) by DeflmultCoset,AS,X1,X3,Y3,Y4;
end;
P4: for v being Element of IT holds (1. F) * v = v
proof
let v be Element of IT;
set i1 = 1.INT.Ring;
reconsider ii1 = i1 as Integer;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
X2: 1.F = 1 .= ii1 / ii1;
thus (1.F) * v = Class(EQRZM(V),[i1*z,i1*i]) by DeflmultCoset,AS,X1,X2
.= v by X1,VECTSP_1:def 17;
end;
P5: for v being Element of IT holds v is right_complementable
proof
let v be Element of IT;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
X21: not -i in {0} by X1,TARSKI:def 1;
-i in INT \ {0} by XBOOLE_0:def 5,X21;
then [z,-i] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87;
then
reconsider w = Class(EQRZM(V),[z,-i]) as Element of IT by EQREL_1:def 3;
X3: (-i)*z+i*z = ((-i) + i)*z by VECTSP_1:def 15
.= 0.V by ZMODUL01:1;
v + w = Class(EQRZM(V),[(-i)*z+i*z,i*(-i)]) by X1,DefaddCoset,AS
.= 0.IT by AS,X1,X3,defZero;
hence v is right_complementable by ALGSTR_0:def 11;
end;
P6: for v, w being Element of IT holds v + w = w + v
proof
let v, w be Element of IT;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
consider j be Element of INT.Ring, y be Element of V such that
X2: j <> 0 & w = Class(EQRZM(V),[y,j]) by AS,LMEQRZM1;
v + w = Class(EQRZM(V),[j*z+i*y,i*j]) by X1,X2,DefaddCoset,AS;
hence v+w = w+v by AS,X1,X2,DefaddCoset;
end;
P7: for u, v, w being Element of IT holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of IT;
consider k be Element of INT.Ring, s be Element of V such that
X0: k <> 0 & u = Class(EQRZM(V),[s,k]) by AS,LMEQRZM1;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & v = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
consider j be Element of INT.Ring, y be Element of V such that
X2: j <> 0 & w = Class(EQRZM(V),[y,j]) by AS,LMEQRZM1;
X3: u + v = Class(EQRZM(V),[i*s+k*z,k*i]) by X0,X1,DefaddCoset,AS;
X4: u + v + w = Class(EQRZM(V),[j*(i*s+k*z)+(k*i)*y,(k*i)*j])
by X0,X1,X2,X3,DefaddCoset,AS;
X5: v + w = Class(EQRZM(V),[j*z+i*y,i*j]) by X1,X2,DefaddCoset,AS;
X6: u + (v + w) = Class(EQRZM(V),[(i*j)*s + k*(j*z+i*y),k*(i*j)])
by X0,X1,X2,X5,DefaddCoset,AS;
j*(i*s+k*z)+(k*i)*y = j*(i*s)+j*(k*z)+ (k*i)*y by VECTSP_1:def 14
.= (j*i)*s+j*(k*z)+ (k*i)*y by VECTSP_1:def 16
.= (i*j)*s +j*(k*z)+ (k*i)*y
.= (i*j)*s +j*(k*z)+ k*(i*y) by VECTSP_1:def 16
.= (i*j)*s +(j*k)*z+ k*(i*y) by VECTSP_1:def 16
.= (i*j)*s +(k*j)*z+ k*(i*y)
.= (i*j)*s +k*(j*z)+ k*(i*y) by VECTSP_1:def 16
.= (i*j)*s +(k*(j*z)+ k*(i*y)) by RLVECT_1:def 3
.= (i*j)*s + k*(j*z+i*y) by VECTSP_1:def 14;
hence (u+v)+w = u+(v+w) by X4,X6;
end;
for v being Element of IT holds v + (0. IT) = v
proof
let u be Element of IT;
consider i be Element of INT.Ring, z be Element of V such that
X1: i <> 0 & u = Class(EQRZM(V),[z,i]) by AS,LMEQRZM1;
reconsider i1 = 1.INT.Ring as Element of INT.Ring;
X3: 0.IT = Class(EQRZM(V),[0.V,i1]) by AS,defZero;
X5: u + (0. IT) = Class(EQRZM(V),[i1*z+i*0.V,i1*i])
by AS,X1,X3,DefaddCoset;
i1*z+i*0.V = z + i*0.V by VECTSP_1:def 17
.= z + 0.V by ZMODUL01:1
.= z;
hence u+(0. IT) = u by X5,X1;
end;
hence thesis
by P1,P2,P3,P4,P5,P6,P7,ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4,
VECTSP_1:def 14,def 15,def 16,def 17;
end;
definition
let V be Z_Module;
assume AS: V is Mult-cancelable;
func Z_MQ_VectSp(V) -> VectSp of F_Rat equals :defZMQVSp:
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #);
correctness by ThEQRZMV1,AS;
end;
ThEQRZMV2:
for V be Z_Module st V is Mult-cancelable holds
ex I be Function of V,Z_MQ_VectSp(V)
st I is one-to-one
& (for v be Element of V holds I.v = Class(EQRZM(V),[v,1]) )
& (for v,w be Element of V holds I.(v+w) = I.v + I.w )
& (for v be Element of V, i be Element of INT.Ring, q be Element of F_Rat
st i=q holds I.(i*v) = q*(I.v) )
& I.(0.V) = 0.(Z_MQ_VectSp(V))
proof
let V be Z_Module;
assume AS: V is Mult-cancelable; then
Z0: Z_MQ_VectSp(V) = ModuleStr (# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by defZMQVSp;
X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1; then
X2: 1 in (INT \{0}) by XBOOLE_0:def 5,X1;
set i1 = 1.INT.Ring;
defpred F0[Element of V, Element of Z_MQ_VectSp(V)] means
$2 = Class(EQRZM(V),[$1,1]);
A2: for x being Element of V holds
ex v being Element of Z_MQ_VectSp(V) st F0[x,v]
proof
let x be Element of V;
X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then 1 in (INT \{0}) by XBOOLE_0:def 5,X1; then
[x,1] in [:the carrier of V,(INT \{0}):] by ZFMISC_1:87; then
reconsider z = Class(EQRZM(V),[x,1])
as Element of Z_MQ_VectSp(V) by Z0,EQREL_1:def 3;
z = Class(EQRZM(V),[x,1]);
hence ex z be Element of Z_MQ_VectSp(V) st F0[x,z];
end;
consider F being Function of V, Z_MQ_VectSp(V) such that
X3: for x being Element of V holds F0[x,F.x] from FUNCT_2:sch 3(A2);
take F;
S2: now
let x1,x2 be object;
assume A1: x1 in the carrier of V & x2 in the carrier of V & F.x1 = F.x2;
then
reconsider x10=x1,x20=x2 as Element of V;
P1: F.x1 = Class(EQRZM(V),[x10,1]) by X3;
P2:[x10,1] in [:the carrier of V,(INT \{0}):] by X2,ZFMISC_1:87;
Class(EQRZM(V),[x10,i1]) = Class(EQRZM(V),[x20,i1]) by A1,P1,X3;
then P3: [[x10,i1],[x20,i1]] in EQRZM(V) by P2,EQREL_1:35;
thus x1 = i1*x10 by VECTSP_1:def 17
.= i1*x20 by AS,P3,LMEQR001
.= x2 by VECTSP_1:def 17;
end;
S3: for v,w be Element of V holds F.(v+w) = F.v + F.w
proof
let v, w be Element of V;
P1: F.v = Class(EQRZM(V),[v,1]) by X3;
P2: F.w = Class(EQRZM(V),[w,1]) by X3;
P8: i1*v+i1*w = i1*(v + w) by VECTSP_1:def 14
.= v+w by VECTSP_1:def 17;
F.v + F.w = Class(EQRZM(V),[i1*v+i1*w,i1*i1]) by AS,P1,P2,Z0,DefaddCoset
.= F.(v+w) by P8,X3;
hence thesis;
end;
S4: for v be Element of V, i be Element of INT.Ring,
q be Element of F_Rat
st i=q holds F.(i*v) = q*(F.v)
proof
let v be Element of V, i be Element of INT.Ring, x be Element of F_Rat;
assume AS0: i = x;
P1: F.v = Class(EQRZM(V),[v,i1]) by X3;
reconsider ii = i, ii1 = i1 as Integer;
i1 <> 0.INT.Ring & x = ii/ii1 by AS0; then
x*(F.v) = Class(EQRZM(V),[i*v,i1*i1]) by AS,P1,Z0,DeflmultCoset
.= F.(i*v) by X3;
hence thesis;
end;
F.(0.V) = Class(EQRZM(V),[0.V,1]) by X3
.= 0.(Z_MQ_VectSp(V)) by AS,Z0,defZero;
hence thesis by S2,S3,S4,X3,FUNCT_2:19;
end;
definition
let V be Z_Module;
assume AS: V is Mult-cancelable;
func MorphsZQ(V) -> Function of V, Z_MQ_VectSp(V) means
:defMorph:
it is one-to-one
& (for v be Element of V holds it.v = Class(EQRZM(V),[v,1]) )
& (for v,w be Element of V holds it.(v+w) = it.v + it.w)
& (for v be Element of V, i be Element of INT.Ring, q be Element of F_Rat
st i = q holds it.(i*v) = q*(it.v) )
& it.(0.V) = 0.(Z_MQ_VectSp(V));
existence by ThEQRZMV2,AS;
uniqueness
proof
let F1, F2 be Function of V, Z_MQ_VectSp(V);
assume
A1: F1 is one-to-one
& (for v be Element of V holds F1.v = Class(EQRZM(V),[v,1]) )
& (for v,w be Element of V holds F1.(v+w) = F1.v + F1.w )
& (for v be Element of V, i be Element of INT.Ring, q be Element of F_Rat
st i = q holds F1.(i*v) = q*(F1.v))
& F1.(0.V) = 0.(Z_MQ_VectSp(V));
assume
A2: F2 is one-to-one
& (for v be Element of V holds F2.v = Class(EQRZM(V),[v,1]) )
& (for v,w be Element of V holds F2.(v+w) = F2.v + F2.w )
& (for v be Element of V, i be Element of INT.Ring, q be Element of F_Rat
st i = q holds F2.(i*v) = q*(F2.v) )
& F2.(0.V) = 0.(Z_MQ_VectSp(V));
now
let v be Element of V;
thus F1.v = Class(EQRZM(V),[v,1]) by A1
.= F2.v by A2;
end;
hence F1 = F2 by FUNCT_2:def 8;
end;
end;
theorem XThSum:
for V be Z_Module st V is Mult-cancelable holds
for s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V)
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 = (MorphsZQ(V)).si holds
Sum(t) = (MorphsZQ(V)).Sum(s)
proof
let V be Z_Module;
assume AS: V is Mult-cancelable;
defpred P[Nat] means
for s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V)
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 = (MorphsZQ(V)).si holds Sum(t) = (MorphsZQ(V)).Sum(s);
A1: P[0]
proof
let s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V);
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 = (MorphsZQ(V)).si;
s = <*>(the carrier of V) by A2;
then Sum(s) = 0. V by RLVECT_1:43;
then
A3: (MorphsZQ(V)).Sum(s) = 0.(Z_MQ_VectSp(V)) by defMorph,AS;
t = <*>(the carrier of (Z_MQ_VectSp(V))) 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);
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 = (MorphsZQ(V)).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);
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);
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 = (MorphsZQ(V)).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 = (MorphsZQ(V)).si by A7,A11,A8,A18;
take si;
thus si = s1.i by A12,A18,A19,FUNCT_1:49;
thus t1.i = (MorphsZQ(V)).si by A14,A11,A13,A18,A19,FUNCT_1:49;
end;
A20: Sum(t1) = (MorphsZQ(V)).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) = (MorphsZQ(V)).ssi
by A6,A7,A8,FINSEQ_1:4;
thus Sum(t) = Sum(t1) + vt by A6,A14,A15,RLVECT_1:38
.= (MorphsZQ(V)).(Sum(s1)+vs) by AS,A6,A20,A22,defMorph
.= (MorphsZQ(V)).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 XThSum1:
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
l be Linear_Combination of I,
lq being Linear_Combination of IQ
st V is Mult-cancelable
& IQ =(MorphsZQ(V)).:I
& l = lq*MorphsZQ(V) holds
Sum(lq) = (MorphsZQ(V)).(Sum(l))
proof
let V be Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V),
l be Linear_Combination of I,
lq be Linear_Combination of IQ;
assume
AS0:V is Mult-cancelable & IQ =(MorphsZQ(V)).:I & l = lq*MorphsZQ(V);
per cases;
suppose A3: I is empty;
then IQ = {}(the carrier of Z_MQ_VectSp(V)) by AS0;
then lq = ZeroLC(Z_MQ_VectSp(V)) by VECTSP_6:6;
then
A6: Sum(lq) = 0.(Z_MQ_VectSp(V)) 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) = (MorphsZQ(V)).Sum(l) by A6,defMorph,AS0;
end;
suppose E1: I is non empty; then
consider v0 be object such that
A7: v0 in I;
reconsider v0 as Vector of V by A7;
(MorphsZQ(V)).v0 in IQ by A7,AS0,FUNCT_2:35;
then reconsider X = IQ as non empty Subset of Z_MQ_VectSp(V);
reconsider g = (MorphsZQ(V)) | I as Function of I,IQ
by FUNCT_2:101,AS0;
(MorphsZQ(V)) is one-to-one by defMorph,AS0; then
AX1: g is one-to-one by FUNCT_1:52;
AX2: rng g = IQ by RELAT_1:115,AS0; then
reconsider F= g" as Function of IQ,I by FUNCT_2:25,AX1;
reconsider F as Function of X, the carrier of V by E1,FUNCT_2:7;
X = IQ; then
AX2A: dom g = I by FUNCT_2:def 1; then
AX3: dom F = X & rng F = I by AX1,AX2,FUNCT_1:33;
A8: for u be Vector of V st u in I holds F.((MorphsZQ(V)).u) = u
proof
let u be Vector of V;
assume AS8: u in I;
hence F.((MorphsZQ(V)).u) = F.(g.u) by FUNCT_1:49
.= u by FUNCT_1:34,AS8,AX2A,AX1;
end;
consider Gq be FinSequence of Z_MQ_VectSp(V) 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,AX3,RELAT_1:27,VECTSP_6:def 4;
A13: rng (F*Gq) c= the carrier of V;
F*Gq is FinSequence by AX3,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: u in I & Gq.z = (MorphsZQ(V)).u by AS0,FUNCT_2:65;
A18: F.(Gq.z) = u by A8,A17;
consider w be Element of Z_MQ_VectSp(V) such that
A19: Gq.z = w & lq.w <> 0.F_Rat by A9,A16,FUNCT_1:3,VECTSP_6:1;
l.u <> 0.F_Rat by AS0,A17,A19,FUNCT_2:15;
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;
lq.((MorphsZQ(V)).u) <> 0 by AS0,A21,FUNCT_2:15; then
A23: (MorphsZQ(V)).u in rng Gq by A9;
then consider z be object such that
A24: z in dom Gq & (MorphsZQ(V)).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,AX3,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,AX1,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;
reconsider w = Gq.i as Element of Z_MQ_VectSp(V) by A35;
consider u be Vector of V such that
A37: u in I & Gq.i = (MorphsZQ(V)).u by AS0,A9,A11,A35,FUNCT_2:65;
A381: F.(Gq.i) = u by A8,A37; then
A38: v = u by A32,FUNCT_1:12;
A39: w = (MorphsZQ(V)).v by A32,A37,A381,FUNCT_1:12;
A40: lq.w = l.v by AS0,A37,A38,FUNCT_2:15;
T1: (lq.w)*w = (MorphsZQ(V)).((l.v)*v) by defMorph,A39,A40,AS0;
thus ex si be VECTOR of V st si=(l (#) FGq ).i &
(lq (#) Gq).i = (MorphsZQ(V)).si
proof
take si = (l (#) FGq).i;
thus thesis by A33,A34,VECTSP_6:8,T1;
end;
end;
hence Sum(lq) = (MorphsZQ(V)).Sum(l) by A9,A27,A29,A30,AS0,XThSum;
end;
end;
theorem ThEQRZMV3A:
for V be Z_Module, IQ being Subset of Z_MQ_VectSp(V) holds
for lq being Linear_Combination of IQ holds
ex m be Integer, a be Element of F_Rat
st m <> 0 & m = a & rng (a * lq) c= INT
proof
let V be Z_Module,
IQ be Subset of Z_MQ_VectSp(V);
defpred P[Nat] means
for lq being Linear_Combination of IQ st card(Carrier(lq)) = $1 holds
ex m be Integer, a be Element of F_Rat
st m <> 0 & m = a & rng (a * lq) c= INT;
P1: P[0]
proof
let lq be Linear_Combination of IQ such that
P2: card(Carrier(lq)) = 0;
P3: Carrier(lq) = {} by P2;
reconsider m = 1 as Integer;
reconsider a = m as Element of F_Rat;
Carrier(a * lq) c= Carrier(lq) by VECTSP_6:28;
then Carrier(a * lq) = {} by P3;
then
X1: a * lq = ZeroLC(Z_MQ_VectSp(V)) by VECTSP_6:def 3;
now
let y be object;
assume y in rng (a*lq); then
consider x being Element of Z_MQ_VectSp(V) such that
X2: y = (a*lq).x by FUNCT_2:113;
(a*lq).x = 0.(F_Rat) by X1,VECTSP_6:3
.= 0;
hence y in INT by X2;
end;
hence thesis by TARSKI:def 3;
end;
P2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P21: P[n];
now
let lq be Linear_Combination of IQ;
assume P22: card(Carrier(lq)) = n+1;
then Carrier(lq) <> {};
then consider x be object such that
P24: x in Carrier(lq) by XBOOLE_0:def 1;
reconsider x as Element of Z_MQ_VectSp(V) by P24;
P25: card(Carrier(lq) \ {x} ) = card(Carrier(lq)) - card({x})
by P24,CARD_2:44,ZFMISC_1:31
.= n+1 - 1 by P22,CARD_2:42
.= n;
defpred PN[Element of Z_MQ_VectSp(V), Element of F_Rat] means
($1 in {x} implies $2 = 0 ) &
(not $1 in {x} implies $2 = lq.$1);
A2: for v being Element of Z_MQ_VectSp(V) holds
ex y being Element of F_Rat st PN[v,y]
proof
let v be Element of Z_MQ_VectSp(V);
v in {x} or not v in {x};
hence thesis;
end;
consider lq0 being Function of the carrier of Z_MQ_VectSp(V),
the carrier of F_Rat such that
A4: for v being Element of
Z_MQ_VectSp(V) holds PN[v,lq0.v] from FUNCT_2:sch 3(A2);
reconsider lq0 as Element of
Funcs(the carrier of Z_MQ_VectSp(V), the carrier of F_Rat)
by FUNCT_2:8;
set T = {v where v is Element of Z_MQ_VectSp(V) : lq0.v <> 0.F_Rat};
A400: T c= Carrier(lq)\ {x}
proof
let v0 be object;
assume v0 in T; then
XX2: ex v1 being Element of Z_MQ_VectSp(V) st
v1 = v0 & lq0.v1 <> 0.F_Rat; then
reconsider v = v0 as Element of Z_MQ_VectSp(V);
XX4: not v in {x} by A4,XX2;
lq.v <> 0.F_Rat by A4,XX2;
then v0 in Carrier(lq);
hence v0 in Carrier(lq) \ {x} by XBOOLE_0:def 5,XX4;
end;
Carrier(lq)\ {x} c= Carrier(lq) by XBOOLE_1:36; then
A40: T c= Carrier(lq) by XBOOLE_1:1,A400;
reconsider T as finite Subset of Z_MQ_VectSp(V) by A400,XBOOLE_1:1;
for v being Element of Z_MQ_VectSp(V)
st not v in T holds lq0.v = 0.F_Rat;
then reconsider lq0 as Linear_Combination of Z_MQ_VectSp(V)
by VECTSP_6:def 1;
X5: T = Carrier(lq0);
Carrier(lq) c= IQ by VECTSP_6:def 4;
then reconsider lq0 as Linear_Combination of IQ
by A40,X5,VECTSP_6:def 4,XBOOLE_1:1;
Carrier(lq) \ {x} c= T
proof
let v0 be object;
assume YY11: v0 in Carrier(lq) \ {x}; then
YY1: v0 in Carrier(lq) & not v0 in {x} by XBOOLE_0:def 5;
reconsider v = v0 as Element of Z_MQ_VectSp(V) by YY11;
lq.v <> 0.F_Rat by YY1,VECTSP_6:2;
then lq0.v <> 0.F_Rat by A4,YY1;
hence v0 in T;
end;
then card(Carrier(lq0)) = n by A400,P25,XBOOLE_0:def 10;
then
consider m0 be Integer, a0 be Element of F_Rat such that
X8: m0 <> 0 & m0 = a0 & rng (a0 * lq0) c= INT by P21;
consider k0,n0 be Integer such that
X9: n0>0 & lq.x = k0/n0 by RAT_1:1;
reconsider m = n0*m0 as Integer;
reconsider a = m as Element of F_Rat by RAT_1:def 2;
reconsider b = n0 as Element of F_Rat by RAT_1:def 2;
for y be object st y in rng (a*lq) holds y in INT
proof let y be object;
assume y in rng (a*lq); then
consider z being Element of Z_MQ_VectSp(V) such that
X2: y = (a*lq).z by FUNCT_2:113;
per cases;
suppose B2: z in {x};
BB2: y = (a*lq).x by B2,X2,TARSKI:def 1
.= a*(lq.x) by VECTSP_6:def 9;
a*(lq.x) = m0*n0*(k0/n0) by X9
.= m0*(n0*(k0/n0))
.= m0*k0 by XCMPLX_1:87,X9;
hence y in INT by BB2,INT_1:def 2;
end;
suppose not z in {x}; then
B31: lq0.z = lq.z by A4;
BBB: a = b*a0 by X8;
B32: (a*lq).z = a*(lq.z) by VECTSP_6:def 9
.= b*(a0*(lq0.z)) by B31,BBB
.= b*((a0*lq0).z) by VECTSP_6:def 9;
(a0*lq0).z in rng (a0*lq0) by FUNCT_2:4;
then reconsider aqz= (a0*lq0).z as Integer by X8;
b*((a0*lq0).z) = n0*aqz;
hence y in INT by B32,X2,INT_1:def 2;
end;
end;
hence ex m be Integer, a be Element of F_Rat
st m <> 0 & m = a & rng (a * lq) c= INT by X8,X9,TARSKI:def 3;
end;
hence P[n+1];
end;
P3: for n be Nat holds P[n] from NAT_1:sch 2(P1,P2);
now
let lq be Linear_Combination of IQ;
card Carrier lq is Element of NAT;
hence ex m be Integer, a be Element of F_Rat
st m <> 0 & m = a & rng (a * lq) c= INT by P3;
end;
hence thesis;
end;
theorem ThEQRZMV3:
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
lq being Linear_Combination of IQ
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I) holds
ex m be Element of INT.Ring, a be Element of F_Rat,
l be Linear_Combination of I
st m <> 0.INT.Ring & m = a & l = (a * lq) * (MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq) = Carrier(l)
proof
let V be Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V),
lq be Linear_Combination of IQ;
assume AS: V is Mult-cancelable & IQ = (MorphsZQ(V)).:(I);
consider m be Integer, a be Element of F_Rat such that
X3: m <> 0 & m = a & rng (a * lq) c= INT by ThEQRZMV3A;
reconsider mm = m as Element of INT.Ring by INT_1:def 2;
P81: rng ((a*lq)*(MorphsZQ(V))) c= rng (a*lq) by RELAT_1:26;
dom ((a*lq)*(MorphsZQ(V))) = the carrier of V by FUNCT_2:def 1;
then (a*lq)*(MorphsZQ(V)) is Function of the carrier of V,INT
by P81,X3,FUNCT_2:2,XBOOLE_1:1;
then reconsider l = (a*lq)*(MorphsZQ(V))
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};
set F = MorphsZQ(V);
B2: 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;
R1: T c= F"(Carrier(lq))
proof
let x be object;
assume x in T;then
consider v be Element of V such that R11: x=v & l.v <> 0;
RRR: dom F = the carrier of V by FUNCT_2:def 1;
V1: l.v = (a*lq).(F.v) by FUNCT_1:13,RRR
.= a*(lq.(F.v)) by VECTSP_6:def 9;
lq.(F.v) <> 0.F_Rat by V1,R11;
then F.v in Carrier(lq);
hence x in F"(Carrier(lq)) by R11,FUNCT_2:38;
end;
F is one-to-one by AS,defMorph;
then F"(Carrier(lq)) = F".:(Carrier(lq)) by FUNCT_1:85;
then reconsider T as finite Subset of V by B2,R1,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;
F"(Carrier(lq)) c= T
proof
let x be object;
assume S21: x in F"(Carrier(lq));
then x in the carrier of V &
F.x in Carrier(lq) by FUNCT_2:38;
then consider w be Element of Z_MQ_VectSp(V) such that
R11: F.x=w & lq.w <> 0.(F_Rat);
reconsider v = x as Element of V by S21;
RRR: dom F = the carrier of V by FUNCT_2:def 1;
RR1: l.v = (a*lq).(F.v) by FUNCT_1:13,RRR
.= a*(lq.w) by R11,VECTSP_6:def 9;
reconsider a1 = a, d1 = (lq.w) as Rational;
l.v <> 0 by RR1,R11,X3;
hence x in T;
end; then
A9: F"(Carrier(lq)) = T by R1;
A7: T = Carrier(l);
AA1: F"(Carrier(lq)) c= F" (F.:(I)) by AS,RELAT_1:143,VECTSP_6:def 4;
dom F = the carrier of V by FUNCT_2:def 1;
then F is one-to-one & I c= dom F by AS,defMorph;
then T c= I by A9,AA1,FUNCT_1:94;
then
reconsider l1 = l as Linear_Combination of I by A7,VECTSP_6:def 4;
take mm;
take a;
take l1;
thus mm <> 0.INT.Ring & mm = a & l1 = (a * lq) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq) = Carrier(l1) by A9,X3;
end;
theorem ThEQRZMV3B:
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
lq being Linear_Combination of IQ,
m be Integer, a be Element of F_Rat,
l be Linear_Combination of I
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I)
& m <> 0 & m = a
& l = (a * lq) *(MorphsZQ(V))
holds a*(Sum(lq)) = (MorphsZQ(V)).(Sum(l))
proof
let V be Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V),
lq be Linear_Combination of IQ,
m be Integer, a be Element of F_Rat,
l be Linear_Combination of I;
assume AS: V is Mult-cancelable
& IQ =(MorphsZQ(V)).:(I)
& m <> 0 & m = a
& l = (a * lq) *(MorphsZQ(V));
reconsider lqa = a * lq as Linear_Combination of IQ by VECTSP_6:31;
thus a*(Sum(lq)) = Sum(lqa) by VECTSP_6:45
.= (MorphsZQ(V)).(Sum(l)) by AS,XThSum1;
end;
theorem ThEQRZMV3C:
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V)
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I)
& I is linearly-independent
holds IQ is linearly-independent
proof
let V be Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V);
assume
AS: V is Mult-cancelable & IQ = (MorphsZQ(V)).:I
& I is linearly-independent;
assume not IQ is linearly-independent;
then consider lq being Linear_Combination of IQ such that
P1: Sum(lq) = 0.(Z_MQ_VectSp(V)) & Carrier(lq) <> {} by VECTSP_7:def 1;
consider m be Element of INT.Ring, a be Element of F_Rat,
l be Linear_Combination of I such that
P2: m <> 0.INT.Ring & m = a & l = (a * lq) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq) = Carrier(l) by ThEQRZMV3,AS;
a*(Sum(lq)) = 0.(Z_MQ_VectSp(V)) by P1,VECTSP_1:15; then
X2: (MorphsZQ(V)).(Sum(l)) = 0.(Z_MQ_VectSp(V)) by AS,P2,ThEQRZMV3B;
X3:(MorphsZQ(V)).( 0.V ) = 0.(Z_MQ_VectSp(V)) by AS,defMorph;
(MorphsZQ(V)) is one-to-one by AS,defMorph; then
P3: Sum(l) = 0.V by X2,X3,FUNCT_2:19;
H6: Carrier(lq) c= IQ by VECTSP_6:def 4;
IQ c= rng (MorphsZQ(V)) by AS,RELAT_1:111; then
H2: Carrier(lq) = (MorphsZQ(V)).: Carrier(l)
by H6,P2,FUNCT_1:77,XBOOLE_1:1;
Carrier(l) <> {} by H2,P1;
hence contradiction by AS,P3,VECTSP_7:def 1;
end;
theorem ThEQRZMV4:
for V be Z_Module,
I being Subset of V,
l being Linear_Combination of I,
IQ being Subset of Z_MQ_VectSp(V)
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:I holds
ex lq be Linear_Combination of IQ
st l = lq*(MorphsZQ(V)) &
Carrier(lq) = (MorphsZQ(V)).:(Carrier(l))
proof
let V be Z_Module,
I be Subset of V,
l be Linear_Combination of I,
IQ be Subset of Z_MQ_VectSp(V);
assume
AS0: V is Mult-cancelable & IQ =(MorphsZQ(V)).:I;
reconsider I0 = Carrier(l) as finite Subset of V;
K2: (MorphsZQ(V)).:I0 c= IQ & (MorphsZQ(V)).:I0 is finite
by AS0,RELAT_1:123,VECTSP_6:def 4;
reconsider IQ0 = (MorphsZQ(V)).:I0 as finite Subset of Z_MQ_VectSp(V);
defpred P[object, object] means
($1 in IQ0 & ex v be Element of V
st v in I0 & $1=(MorphsZQ(V)).v & $2 = l.v)
or (not $1 in IQ0 & $2 = 0.F_Rat);
A2: for x being object st x in the carrier of Z_MQ_VectSp(V)
ex y being object st y in RAT & P[x, y]
proof
let x be object;
assume x in the carrier of Z_MQ_VectSp(V);
then reconsider x as Element of Z_MQ_VectSp(V);
per cases;
suppose
A3: x in IQ0;
then consider v be object such that
A4: v in the carrier of V & v in I0 & x=(MorphsZQ(V)).v
by FUNCT_2:64;
reconsider v as Element of V by A4;
l.v in RAT by NUMBERS:14,TARSKI:def 3;
hence thesis by A3,A4;
end;
suppose not x in IQ0;
hence thesis;
end;
end;
consider lq being Function of the carrier of Z_MQ_VectSp(V), RAT such that
A5: for x being object st x in the carrier of Z_MQ_VectSp(V)
holds P[x, lq.x] from FUNCT_2:sch 1(A2);
A6: for x being Element of Z_MQ_VectSp(V) st not x in IQ0
holds lq.x = 0.F_Rat by A5;
lq is Element of Funcs(the carrier of Z_MQ_VectSp(V), RAT) by FUNCT_2:8;
then reconsider lq as Linear_Combination of Z_MQ_VectSp(V)
by A6,VECTSP_6:def 1;
A11: Carrier(lq) c= IQ0
proof
let x be object;
assume that
A7: x in Carrier(lq) and
A8: not x in IQ0;
consider z being Element of Z_MQ_VectSp(V) such that
A9: x = z and
A10: lq.z <> 0.F_Rat by A7;
thus contradiction by A5,A8,A9,A10;
end;
then
reconsider lq as Linear_Combination of IQ by K2,VECTSP_6:def 4,XBOOLE_1:1;
A12: dom l = the carrier of V by FUNCT_2:def 1;
A13: dom (lq*(MorphsZQ(V))) = the carrier of V by FUNCT_2:def 1;
take lq;
F1: MorphsZQ(V) is one-to-one by defMorph,AS0;
for x be object st x in dom l holds l.x = (lq*(MorphsZQ(V))).x
proof
let x be object;
assume x in dom l;
then reconsider v=x as Element of V;
reconsider w = (MorphsZQ(V)).v as Element of Z_MQ_VectSp(V);
per cases;
suppose v in I0;
then w in IQ0 by FUNCT_2:35;
then consider v0 be Element of V such that
A16: v0 in I0 & w=(MorphsZQ(V)).v0 & lq.w = l.v0 by A5;
v0 = v by A16,FUNCT_2:19,F1;
hence l.x = (lq*(MorphsZQ(V))).x by A13,A16,FUNCT_1:12;
end;
suppose
A18: not v in I0;
then
A19: l.v = 0.F_Rat;
not w in IQ0
proof
assume w in IQ0;
then consider v0 be Element of V such that
A16: v0 in I0 & w=(MorphsZQ(V)).v0 & lq.w = l.v0 by A5;
thus contradiction by A16,A18,F1,FUNCT_2:19;
end; then
lq.w = 0.F_Rat by A5;
hence l.x = (lq*(MorphsZQ(V))).x by A13,A19,FUNCT_1:12;
end;
end;
hence U1: l = lq*(MorphsZQ(V)) by FUNCT_1:2,A12,A13;
IQ0 c= Carrier lq
proof
let x be object;
assume x in IQ0;
then consider v be object such that
A4: v in the carrier of V & v in I0 & x=(MorphsZQ(V)).v by FUNCT_2:64;
reconsider v as Element of V by A4;
x=(MorphsZQ(V)).v by A4;
then reconsider y = x as Element of Z_MQ_VectSp(V);
X1: lq.y = l.v by A4,A13,U1,FUNCT_1:12;
l.v <> 0 by ZMODUL02:8,A4;
hence x in Carrier(lq) by X1;
end;
hence Carrier(lq) = (MorphsZQ(V)).:(Carrier(l)) by A11;
end;
theorem ThQuotAX:
for V be free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
l be Linear_Combination of I,
i be Element of INT.Ring
st i <> 0.INT.Ring & IQ =(MorphsZQ(V)).:I
holds Class(EQRZM(V),[Sum(l),i]) in Lin(IQ)
proof
let V be free Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V),
l be Linear_Combination of I,
i be Element of INT.Ring;
assume AS: i <> 0.INT.Ring & IQ =(MorphsZQ(V)).:I;
Z0:Z_MQ_VectSp(V) = ModuleStr (# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by defZMQVSp;
consider lq be Linear_Combination of IQ such that
P1: l = lq * (MorphsZQ(V)) &
Carrier(lq) = (MorphsZQ(V)).:(Carrier(l)) by ThEQRZMV4,AS;
P2: (Sum(lq))= (MorphsZQ(V)).(Sum(l)) by AS,P1,XThSum1;
reconsider a = 1/i as Element of F_Rat by RAT_1:def 2;
P3: (MorphsZQ(V)).(Sum(l)) = Class(EQRZM(V),[Sum(l),1.INT.Ring])
by defMorph;
a*( (MorphsZQ(V)).(Sum(l))) = Class(EQRZM(V),[1.INT.Ring*Sum(l),
i*1.INT.Ring]) by AS,P3,Z0,DeflmultCoset
.= Class(EQRZM(V),[Sum(l),i]) by VECTSP_1:def 17;
hence thesis by P2,VECTSP_4:21,VECTSP_7:7;
end;
theorem ThEQRZMV3E:
for V be free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V)
st IQ =(MorphsZQ(V)).:I
holds card(I) = card(IQ)
proof
let V be free Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V);
assume AS1: IQ =(MorphsZQ(V)).:I;
P1: MorphsZQ(V) is one-to-one by defMorph;
the carrier of V = dom (MorphsZQ(V)) by FUNCT_2:def 1;
hence card(I) = card(IQ) by AS1,P1,CARD_1:5,CARD_1:33;
end;
theorem ThEQRZMV3D:
for V be free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V)
st IQ =(MorphsZQ(V)).:I & I is Basis of V
holds IQ is Basis of Z_MQ_VectSp(V)
proof
let V be free Z_Module,
I be Subset of V,
IQ be Subset of Z_MQ_VectSp(V);
assume
AS: IQ =(MorphsZQ(V)).:(I) & I is Basis of V; then
I is base; then
X0: I is linearly-independent & Lin (I) = the ModuleStr of V
by VECTSP_7:def 3;
X1: IQ is linearly-independent by AS,ThEQRZMV3C,VECTSP_7:def 3;
AS0: Z_MQ_VectSp(V) = ModuleStr (# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by defZMQVSp;
for vq being Element of Z_MQ_VectSp(V) holds vq in Lin (IQ)
proof
let vq be Element of Z_MQ_VectSp(V);
consider i be Element of INT.Ring, v be Element of V such that
P3: i <> 0 & vq=Class(EQRZM(V),[v,i]) by AS0,LMEQRZM1;
v in Lin (I) by X0; then
consider l be Linear_Combination of I such that
P4: v = Sum(l) by ZMODUL02:64;
thus vq in Lin(IQ) by AS,P4,P3,ThQuotAX;
end;
hence thesis by AS0,X1,VECTSP_4:32,VECTSP_7:def 3;
end;
registration
let V be finite-rank free Z_Module;
cluster Z_MQ_VectSp(V) -> finite-dimensional;
coherence
proof
consider I being finite Subset of V such that
P1: I is Basis of V by ZMODUL03:def 3;
reconsider IQ =(MorphsZQ(V)).:(I) as Subset of Z_MQ_VectSp(V);
IQ is Basis of Z_MQ_VectSp(V) by P1,ThEQRZMV3D;
hence thesis by MATRLIN:def 1;
end;
end;
theorem
for V be finite-rank free Z_Module holds
rank V = dim Z_MQ_VectSp(V)
proof
let V be finite-rank free Z_Module;
reconsider I = the Basis of V as Subset of V;
reconsider IQ = (MorphsZQ(V)).:(I) as Subset of Z_MQ_VectSp(V);
A1: IQ is Basis of Z_MQ_VectSp(V) by ThEQRZMV3D;
thus rank V = card I by ZMODUL03:def 5
.= card IQ by ThEQRZMV3E
.= dim Z_MQ_VectSp(V) by A1,VECTSP_9:def 1;
end;
theorem XXTh1:
for V be free Z_Module, I, A be finite Subset of V
st I is Basis of V & card (I) + 1 = card (A)
holds A is linearly-dependent
proof
let V be free Z_Module, I, A be finite Subset of V;
assume AS: I is Basis of V & card (I) + 1 = card (A);
reconsider IQ =(MorphsZQ(V)).:(I) as Subset of Z_MQ_VectSp(V);
reconsider IQ as finite Subset of Z_MQ_VectSp(V);
P2:IQ is Basis of Z_MQ_VectSp(V) by AS,ThEQRZMV3D;
assume P31: not A is linearly-dependent;
reconsider B = (MorphsZQ(V)).:(A) as Subset of Z_MQ_VectSp(V);
reconsider B as finite Subset of Z_MQ_VectSp(V);
PP: IQ is linearly-independent & Lin (IQ) = the ModuleStr of Z_MQ_VectSp(V)
by VECTSP_7:def 3,P2;
B is linearly-independent by P31,ThEQRZMV3C;
then P5: card(B) <= card(IQ) by VECTSP_9:19,PP;
card(IQ) = card(I) by ThEQRZMV3E;
then card(A) <= card(I) by P5,ThEQRZMV3E;
hence contradiction by AS,NAT_1:13;
end;
theorem XXTh2:
for V be free Z_Module, A, B be Subset of V
st A is linearly-dependent & A c= B
holds B is linearly-dependent by VECTSP_7:1;
theorem XXTh3:
for V be free Z_Module,D,A be Subset of V
st D is Basis of V & D is finite & card (D) c< card(A)
holds A is linearly-dependent
proof
let V be free Z_Module,D,A be Subset of V;
assume AS: D is Basis of V & D is finite & card (D) c< card(A);
reconsider D0 = D as finite Subset of V by AS;
A \ D0 <> {} by AS,CARD_1:68,ORDINAL1:11;
then consider x be object such that
P3: x in A \ D0 by XBOOLE_0:def 1;
x in A & not x in D0 by P3,XBOOLE_0:def 5;
then P5: card(D0 \/{x}) = card(D0) + 1 by CARD_2:41;
succ card(D0) = card(D0)+^1 by ORDINAL2:31
.= card(D0)+1 by CARD_2:36;
then P6: card(D0)+1 c= card(A) by AS,ORDINAL1:11,ORDINAL1:21;
consider f be Function such that
P7: f is one-to-one & dom f = (D0 \/{x} ) & rng f c= A by CARD_1:10,P5,P6;
set B = rng f;
P8: card (B) = card(D0)+1 by P5,P7,CARD_1:5,WELLORD2:def 4;
then reconsider B as finite set;
reconsider B as finite Subset of V by P7,XBOOLE_1:1;
B is linearly-dependent by XXTh1,P8,AS;
hence A is linearly-dependent by XXTh2,P7;
end;
theorem
for V be free Z_Module, I, A be Subset of V
st I is Basis of V & I is finite & A is linearly-independent
holds card (A) c= card (I) by XXTh3,XBOOLE_0:def 8;
begin :: 2. Subspace of free $\mathbb Z$-module
theorem
for V being Z_Module st (Omega).V is free holds V is free
proof
let V be Z_Module such that
A1: (Omega).V is free;
consider I be Subset of (Omega).V such that
a2: I is base by VECTSP_7:def 4,A1;
A2: I is linearly-independent & (Omega).V = Lin(I) by a2,VECTSP_7:def 3;
reconsider II = I as linearly-independent Subset of V by A2,ZMODUL03:15;
(Omega).V = Lin(II) by A2,ZMODUL03:20; then
II is base by VECTSP_7:def 3;
hence thesis by VECTSP_7:def 4;
end;
theorem
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
W1s, W2s being strict Subspace of V st W1s = (Omega).W1 & W2s = (Omega).W2
holds W1s + W2s = W1 + W2
proof
let R be Ring;
let V be LeftMod of R, W1, W2 be Subspace of V,
W1s, W2s be strict Subspace of V such that
A1: W1s = (Omega).W1 & W2s = (Omega).W2;
for x be Vector of V holds x in W1+W2 iff x in W1s + W2s
proof
let x be Vector of V;
hereby
assume x in W1+W2;
then consider x1, x2 be Vector of V such that
B1: x1 in W1 & x2 in W2 & x = x1 + x2 by VECTSP_5:1;
B2: x1 in W1s by A1,B1;
x2 in W2s by A1,B1;
hence x in W1s + W2s by B1,B2,VECTSP_5:1;
end;
assume x in W1s + W2s;
then consider x1, x2 be Vector of V such that
B1: x1 in W1s & x2 in W2s & x = x1 + x2 by VECTSP_5:1;
B2: x1 in W1 by A1,B1;
x2 in W2 by A1,B1;
hence x in W1 + W2 by B1,B2,VECTSP_5:1;
end;
hence W1 + W2 = W1s + W2s by VECTSP_4:30;
end;
theorem
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
W1s, W2s being strict Subspace of V st W1s = (Omega).W1 & W2s = (Omega).W2
holds W1s /\ W2s = W1 /\ W2
proof
let R be Ring;
let V be LeftMod of R, W1, W2 be Subspace of V,
W1s, W2s be strict Subspace of V such that
A1: W1s = (Omega).W1 & W2s = (Omega).W2;
for x be Vector of V holds x in W1 /\ W2 iff x in W1s /\ W2s
proof
let x be Vector of V;
hereby
assume x in W1 /\ W2; then
B1: x in W1 & x in W2 by VECTSP_5:3;
B2: x in W1s by A1,B1;
x in W2s by A1,B1;
hence x in W1s /\ W2s by B2,VECTSP_5:3;
end;
assume B1: x in W1s /\ W2s;
x in the ModuleStr of W1 by A1,B1,VECTSP_5:3;
then B2: x in W1;
x in the ModuleStr of W2 by A1,B1,VECTSP_5:3;
then x in W2;
hence x in W1 /\ W2 by B2,VECTSP_5:3;
end;
hence W1 /\ W2 = W1s /\ W2s by VECTSP_4:30;
end;
theorem Thn0V:
for R being Ring
for V be LeftMod of R, W be strict Subspace of V st W <> (0).V holds
ex v be Vector of V st v in W & v <> 0.V
proof
let R be Ring;
let V be LeftMod of R, W be strict Subspace of V such that
A1: W <> (0).V;
A2: 0.V in W by VECTSP_4:17;
the carrier of W <> {0.V} by A1,VECTSP_4:def 3;
then {0.V} c< the carrier of W by A2,ZFMISC_1:31;
then consider v be object such that
A3: v in the carrier of W and
A4: not v in {0.V} by XBOOLE_0:6;
reconsider v as Vector of V by A3,VECTSP_4:10;
take v;
thus thesis by A3,A4,TARSKI:def 1;
end;
theorem ThCarrier1:
for K being Ring
for V being VectSp of K
for A being Subset of V, l1, l2 being Linear_Combination of A
st Carrier(l1) /\ Carrier(l2) = {} holds
Carrier(l1 + l2) = Carrier(l1) \/ Carrier(l2)
proof
let K be Ring;
let V be VectSp of K;
let A be Subset of V,
l1, l2 be Linear_Combination of A such that
A0: Carrier(l1) /\ Carrier(l2) = {};
A1: Carrier(l1) misses Carrier(l2) by A0;
Carrier(l1) \/ Carrier(l2) c= Carrier(l1 + l2)
proof
let x be object;
assume B1: x in Carrier(l1) \/ Carrier(l2);
then reconsider x as Vector of V;
per cases by B1,XBOOLE_0:def 3;
suppose C1: x in Carrier(l1);
then not x in Carrier(l2) by A1,B1,XBOOLE_0:5;
then C2: l2.x = 0.K;
(l1 + l2).x = l1.x + l2.x by VECTSP_6:22
.= l1.x by C2;
then (l1 + l2).x <> 0.K by C1,VECTSP_6:2;
hence thesis;
end;
suppose C1: x in Carrier(l2);
then not x in Carrier(l1) by A1,B1,XBOOLE_0:5;
then C2: l1.x = 0.K;
(l1 + l2).x = l1.x + l2.x by VECTSP_6:22
.= l2.x by C2;
then (l1 + l2).x <> 0.K by C1,VECTSP_6:2;
hence thesis;
end;
end;
hence thesis by VECTSP_6:23;
end;
theorem ThCarrier2:
for R being Ring
for V being VectSp of R
for A1, A2 being Subset of V, l being Linear_Combination of A1 \/ A2
st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1, l2 being Linear_Combination of A2
st l = l1 + l2
proof
let K be Ring;
let V be VectSp of K;
let A1, A2 be Subset of V, l be Linear_Combination of A1 \/ A2 such that
A1: A1 /\ A2 = {};
A2: A1 misses A2 by A1;
defpred P[object, object] means
$1 is Vector of V implies
($1 in A1 & $2 = l.$1) or (not $1 in A1 & $2 = 0.K);
A3: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & 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 B1: x in A1;
l.x9 in the carrier of K;
hence thesis by B1;
end;
suppose not x in A1;
hence thesis;
end;
end;
ex l1 being Function of the carrier of V, the carrier of K st
for x being object st x in the carrier of V holds P[x, l1.x]
from FUNCT_2:sch 1(A3);
then consider l1 be Function of the carrier of V,
the carrier of K such that
A4: for x be object st x in the carrier of V holds P[x, l1.x];
A5:
now
let v be Vector of V;
assume
A6: not v in A1 /\ Carrier(l);
per cases by A6,XBOOLE_0:def 4;
suppose
not v in A1;
hence l1.v = 0.K by A4;
end;
suppose
not v in Carrier(l);
then l.v = 0.K;
hence l1.v = 0.K by A4;
end;
end;
reconsider l1 as Element of Funcs(the carrier of V, the carrier of K)
by FUNCT_2:8;
reconsider l1 as Linear_Combination of V by A5,VECTSP_6:def 1;
for x being object holds x in Carrier(l1) implies x in A1
proof
let x be object;
assume B1: x in Carrier(l1);
then reconsider x as Vector of V;
l1.x <> 0.K by B1,VECTSP_6:2;
hence thesis by A4;
end;
then AX1: l1 is Linear_Combination of A1 by TARSKI:def 3,VECTSP_6:def 4;
defpred Q[object, object] means
$1 is Vector of V implies
($1 in A2 & $2 = l.$1) or (not $1 in A2 & $2 = 0.K);
A7: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & Q[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 B1: x in A2;
l.x9 in the carrier of K;
hence thesis by B1;
end;
suppose not x in A2;
hence thesis;
end;
end;
ex l2 being Function of the carrier of V, the carrier of K st
for x being object st x in the carrier of V holds Q[x, l2.x]
from FUNCT_2:sch 1(A7);
then consider l2 be Function of the carrier of V, the carrier of K
such that
A8: for x being object st x in the carrier of V holds Q[x, l2.x];
A9:
now
let v be Vector of V;
assume
A10: not v in A2 /\ Carrier(l);
per cases by A10,XBOOLE_0:def 4;
suppose
not v in A2;
hence l2.v = 0.K by A8;
end;
suppose
not v in Carrier(l);
then l.v = 0.K;
hence l2.v = 0.K by A8;
end;
end;
reconsider l2 as Element of Funcs(the carrier of V, the carrier of K)
by FUNCT_2:8;
reconsider l2 as Linear_Combination of V by A9,VECTSP_6:def 1;
for x being object holds x in Carrier(l2) implies x in A2
proof
let x be object;
assume B1: x in Carrier(l2);
then reconsider x as Vector of V;
l2.x <> 0.K by B1,VECTSP_6:2;
hence thesis by A8;
end;
then AX2: l2 is Linear_Combination of A2 by TARSKI:def 3,VECTSP_6:def 4;
for v being Vector of V holds l.v = (l1+l2).v
proof
let v be Vector of V;
per cases;
suppose B1: v in A1;
then v in A1 \/ A2 by XBOOLE_0:def 3;
then B2: not v in A2 by A2,B1,XBOOLE_0:5;
thus l.v = l1.v + 0.K by A4,B1
.= l1.v + l2.v by A8,B2
.= (l1+l2).v by VECTSP_6:22;
end;
suppose B1: v in A2;
then v in A1 \/ A2 by XBOOLE_0:def 3;
then B2: not v in A1 by A2,B1,XBOOLE_0:5;
thus l.v = 0.K + l2.v by A8,B1
.= l1.v + l2.v by A4,B2
.= (l1+l2).v by VECTSP_6:22;
end;
suppose B1: not v in A1 & not v in A2;
then not v in A1 \/ A2 by XBOOLE_0:def 3;
then not v in Carrier(l) by TARSKI:def 3,VECTSP_6:def 4;
hence l.v = 0.K
.= l1.v + 0.K by A4,B1
.= l1.v + l2.v by A8,B1
.= (l1+l2).v by VECTSP_6:22;
end;
end;
hence thesis by AX1,AX2,VECTSP_6:def 7;
end;
theorem FRds1:
for V being Z_Module, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2 st V is_the_direct_sum_of W1,W2
holds I1 /\ I2 = {}
proof
let V be Z_Module, W1, W2 be free Subspace of V,
I1 be Basis of W1, I2 be Basis of W2 such that
A1: V is_the_direct_sum_of W1,W2;
assume I1 /\ I2 <> {};
then consider v be object such that
A2: v in I1 /\ I2 by XBOOLE_0:7;
A3: v in I1 by A2,XBOOLE_0:def 4;
not 0.W1 in I1 by ZMODUL02:57,VECTSP_7:def 3;
then A4: v <> 0.V by A3,ZMODUL01:26;
A5: v in W1 by A3;
v in W2 by A2; then
W1: v in W1 /\ W2 by A5,VECTSP_5:3;
W1 /\ W2 = (0).V by A1,VECTSP_5:def 4;
then v in (0).V by W1;
hence contradiction by A4,ZMODUL02:66;
end;
theorem FRds2:
for V being Z_Module, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds Lin(I) = the ModuleStr of V
proof
let V being Z_Module, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V such that
A1: V is_the_direct_sum_of W1,W2 and
A2: I = I1 \/ I2;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider II1 = I1 as Subset of V by XBOOLE_1:1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider II2 = I2 as Subset of V by XBOOLE_1:1;
A5: the ModuleStr of W1 = Lin(I1) by VECTSP_7:def 3
.= Lin(II1) by ZMODUL03:20;
A6: the ModuleStr of W2 = Lin(I2) by VECTSP_7:def 3
.= Lin(II2) by ZMODUL03:20;
for x be Vector of V holds x in W1+W2 iff x in Lin(II1) + Lin(II2)
proof
let x be Vector of V;
hereby
assume x in W1+W2;
then consider x1, x2 be Vector of V such that
B1: x1 in W1 & x2 in W2 & x = x1 + x2 by VECTSP_5:1;
B2: x1 in Lin(II1) by A5,B1;
x2 in Lin(II2) by A6,B1;
hence x in Lin(II1) + Lin(II2) by B1,B2,VECTSP_5:1;
end;
assume x in Lin(II1) + Lin(II2);
then consider x1, x2 be Vector of V such that
B1: x1 in Lin(II1) & x2 in Lin(II2) & x = x1 + x2 by VECTSP_5:1;
B2: x1 in W1 by A5,B1;
x2 in W2 by A6,B1;
hence x in W1 + W2 by B1,B2,VECTSP_5:1;
end; then
A7: W1 + W2 = Lin(II1) + Lin(II2) by VECTSP_4:30;
thus the ModuleStr of V = W1 + W2 by A1,VECTSP_5:def 4
.= Lin(I) by A2,A7,ZMODUL02:72;
end;
theorem FRds3:
for V being LeftMod of INT.Ring, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds I is linearly-independent
proof
let V being LeftMod of INT.Ring, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V such that
A1: V is_the_direct_sum_of W1,W2 and
A2: I = I1 \/ I2;
assume I is linearly-dependent;
then consider l be Linear_Combination of I such that
A3: Sum(l) = 0.V and
A4: Carrier(l) <> {} by VECTSP_7:def 1;
A5A: I1 /\ I2 = {} by A1,FRds1;
then A5B: I1 misses I2;
the carrier of W1 c= the carrier of V
& the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider II1 = I1, II2 = I2 as Subset of V by XBOOLE_1:1;
consider l1 be Linear_Combination of II1,
l2 be Linear_Combination of II2 such that
A6: l = l1 + l2 by A2,A5A,ThCarrier2;
reconsider ll1 = l1 as Linear_Combination of I
by A2,XBOOLE_1:7,ZMODUL02:10;
reconsider ll2 = l2 as Linear_Combination of I
by A2,XBOOLE_1:7,ZMODUL02:10;
A7: Sum(l) = Sum(ll1) + Sum(ll2) by A6,ZMODUL02:52;
set v1 = Sum(ll1);
set v2 = Sum(ll2);
Carrier(ll1) c= I1 & Carrier(ll2) c= I2 by VECTSP_6:def 4;
then A8: Carrier(ll1) /\ Carrier(ll2) = {}
by A5B,XBOOLE_0:def 7,XBOOLE_1:64;
A10: v1 <> 0.V
proof
assume B1: v1 = 0.V;
II1 is linearly-independent by VECTSP_7:def 3,ZMODUL03:15;
then B3: Carrier(l1) = {} by B1,VECTSP_7:def 1;
II2 is linearly-independent by VECTSP_7:def 3,ZMODUL03:15;
then Carrier(ll1) \/ Carrier(ll2) = {} by A3,A7,B1,B3,VECTSP_7:def 1;
hence contradiction by A4,A6,A8,ThCarrier1;
end;
A13: v1 = -v2 by A3,A7,RLVECT_1:6;
v1 in Lin(II1) by ZMODUL02:64;
then v1 in Lin(I1) by ZMODUL03:20;
then v1 in the ModuleStr of W1 by VECTSP_7:def 3;
then A14: v1 in W1;
v2 in Lin(II2) by ZMODUL02:64;
then v2 in Lin(I2) by ZMODUL03:20;
then v2 in the ModuleStr of W2 by VECTSP_7:def 3;
then v2 in W2;
then A15: v1 in W2 by A13,ZMODUL01:38;
W1 /\ W2 = (0).V by A1,VECTSP_5:def 4;
hence contradiction by A10,A14,A15,VECTSP_5:3,ZMODUL02:66;
end;
theorem FRdsX:
for V being Z_Module, W1, W2 being free Subspace of V
st V is_the_direct_sum_of W1,W2
holds V is free
proof
let V be Z_Module, W1, W2 be free Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
set I1 = the Basis of W1;
set I2 = the Basis of W2;
set I = I1 \/ I2;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then A3: I1 is Subset of V by XBOOLE_1:1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then I2 is Subset of V by XBOOLE_1:1;
then reconsider I as Subset of V by A3,XBOOLE_1:8;
the ModuleStr of V = Lin(I) by A1,FRds2; then
I is base by VECTSP_7:def 3,FRds3,A1;
hence thesis by VECTSP_7:def 4;
end;
theorem ThDirectSum:
for V being Z_Module, W1, W2 being free Subspace of V
st W1 /\ W2 = (0).V holds
W1 + W2 is free
proof
let V be Z_Module, W1, W2 be free Subspace of V such that
P1: W1 /\ W2 = (0).V;
reconsider W = W1 + W2 as strict Subspace of V;
reconsider WW1 = W1 as Subspace of W by ZMODUL01:97;
reconsider WW2 = W2 as Subspace of W by ZMODUL01:97;
A2: WW1 /\ WW2 is Subspace of V by ZMODUL01:42;
A3: WW1 + WW2 is Subspace of V by ZMODUL01:42;
for x being object holds x in WW1 /\ WW2 iff x in (0).V
proof
let x be object;
hereby
assume x in WW1 /\ WW2;
then x in WW1 & x in WW2 by VECTSP_5:3;
hence x in (0).V by P1,VECTSP_5:3;
end;
assume x in (0).V;
then x in W1 & x in W2 by P1,VECTSP_5:3;
hence x in WW1 /\ WW2 by VECTSP_5:3;
end;
then for x being Vector of V holds x in WW1 /\ WW2 iff x in (0).V;
then A4: WW1 /\ WW2 = (0).V by A2,VECTSP_4:30
.= (0).W by ZMODUL01:51;
for x being object holds x in W iff x in WW1 + WW2
proof
let x be object;
hereby
assume x in W;
then consider x1, x2 be Vector of V such that
B2: x1 in W1 & x2 in W2 & x = x1 + x2 by VECTSP_5:1;
x1 in W1 + W2 by B2,VECTSP_5:2;
then reconsider xx1 = x1 as Vector of W;
x2 in W1 + W2 by B2,VECTSP_5:2;
then reconsider xx2 = x2 as Vector of W;
x = xx1 + xx2 by B2,ZMODUL01:28;
hence x in WW1 + WW2 by B2,VECTSP_5:1;
end;
assume x in WW1 + WW2;
then consider x1, x2 be Vector of W such that
B2: x1 in WW1 & x2 in WW2 & x = x1 + x2 by VECTSP_5:1;
thus x in W by B2;
end;
then for x being Vector of V holds x in W iff x in WW1 + WW2;
then W = WW1 + WW2 by A3,VECTSP_4:30;
hence W1 + W2 is free by A4,FRdsX,VECTSP_5:def 4;
end;
theorem
for V being free Z_Module, I being Basis of V, v being Vector of V
st v in I holds
Lin(I \ {v}) is free & Lin{v} is free
proof
let V be free Z_Module, I be Basis of V,
v be Vector of V such that
A1: v in I;
A2: I is linearly-independent by VECTSP_7:def 3;
then I \ {v} is linearly-independent by XBOOLE_1:36,ZMODUL02:56;
hence Lin(I \ {v}) is free;
{v} is linearly-independent by A1,A2,ZFMISC_1:31,ZMODUL02:56;
hence Lin{v} is free;
end;
theorem FRdsY:
for V being free Z_Module, I being Basis of V, v being Vector of V
st v in I holds
V is_the_direct_sum_of Lin(I \ {v}),Lin{v}
proof
let V be free Z_Module, I be Basis of V,
v be Vector of V such that
A1: v in I;
I = (I \ {v}) \/ {v} by A1,XBOOLE_1:45,ZFMISC_1:31;
then Lin(I) = Lin(I \ {v}) + Lin{v} by ZMODUL02:72;
then A3: the ModuleStr of V = Lin(I \ {v}) + Lin{v} by VECTSP_7:def 3;
(the carrier of Lin(I \ {v})) /\ (the carrier of Lin{v}) = {0.V}
proof
assume B1: (the carrier of Lin(I \ {v})) /\
(the carrier of Lin{v}) <> {0.V};
0.V in Lin(I \ {v}) /\ Lin{v} by ZMODUL01:33;
then 0.V in (the carrier of Lin(I \ {v})) /\ (the carrier of Lin{v})
by VECTSP_5:def 2;
then {0.V} c< (the carrier of Lin(I \ {v})) /\
(the carrier of Lin{v}) by B1,ZFMISC_1:31;
then consider x be object such that
B2: x in (the carrier of Lin(I \ {v})) /\ (the carrier of Lin{v}) and
B3: not x in {0.V} by XBOOLE_0:6;
B4: x <> 0.V by B3,TARSKI:def 1;
B5: x in (Lin(I \ {v}) /\ Lin{v}) by B2,VECTSP_5:def 2;
then x in V by ZMODUL01:24;
then reconsider x as Vector of V;
x in Lin(I \ {v}) by B5,VECTSP_5:3;
then consider lx1 be Linear_Combination of I \ {v} such that
B6: x = Sum(lx1) by ZMODUL02:64;
B7: Carrier(lx1) <> {} by B4,B6,ZMODUL02:23;
B8: Carrier(lx1) c= I \ {v} by VECTSP_6:def 4;
x in Lin{v} by B5,VECTSP_5:3;
then consider lx2 be Linear_Combination of {v} such that
B9: -x = Sum(lx2) by ZMODUL01:38,ZMODUL02:64;
B11: Carrier(lx2) c= {v} by VECTSP_6:def 4;
reconsider llx1 = lx1 as Linear_Combination of I
by XBOOLE_1:36,ZMODUL02:10;
reconsider llx2 = lx2 as Linear_Combination of I
by A1,ZFMISC_1:31,ZMODUL02:10;
Carrier(lx1) misses Carrier(lx2) by B8,B11,XBOOLE_1:64,XBOOLE_1:79;
then Carrier(lx1) /\ Carrier(lx2) = {};
then B12: Carrier(llx1 + llx2) = Carrier(llx1) \/ Carrier(llx2)
by ThCarrier1;
B13: Sum(llx1) + Sum(llx2) = 0.V by B6,B9,RLVECT_1:5;
reconsider llx = llx1 + llx2 as Linear_Combination of I
by ZMODUL02:27;
Sum(llx) = 0.V by B13,ZMODUL02:52;
hence contradiction by B7,B12,VECTSP_7:def 1,VECTSP_7:def 3;
end;
then Lin(I \ {v}) /\ Lin{v} = (0).V by VECTSP_4:def 3,VECTSP_5:def 2;
hence thesis by A3,VECTSP_5:def 4;
end;
FRX:
for V being finite-rank free Z_Module, W being Subspace of V
holds W is free
proof
defpred P[Nat] means for V being finite-rank free Z_Module,
W being Subspace of V st rank(V) = $1 holds W is free;
A1: P[0]
proof
let V be finite-rank free Z_Module, W be Subspace of V such that
B1: rank(V) = 0;
set I = the Basis of V;
set sW = the ModuleStr of W;
B2: sW = (Omega).W;
B3: card I = 0 by B1,ZMODUL03:def 5;
then B31: I = {}(the carrier of V);
the ModuleStr of V = Lin(I) by VECTSP_7:def 3
.= (0).V by B31,ZMODUL02:67;
then the carrier of V = {0.V} by VECTSP_4:def 3;
then the carrier of W c= {0.V} by VECTSP_4:def 2;
then B5: the carrier of W c= {0.W} by ZMODUL01:26;
B6: I = {}(the carrier of W) by B3;
then reconsider II = I as Subset of W;
II = {}the carrier of W by B6; then
AA: II is linearly-independent;
sW = (0).W by B2,B5,XBOOLE_0:def 10,VECTSP_4:def 3
.= Lin(II) by B6,ZMODUL02:67; then
Lin II = the ModuleStr of W; then
II is base by VECTSP_7:def 3,AA; then
W is free by VECTSP_7:def 4;
hence thesis;
end;
A2: for m being Nat st P[m] holds P[m+1]
proof
let n be Nat such that
B1: P[n];
let V be finite-rank free Z_Module, W be Subspace of V
such that
B2: rank(V) = n+1;
set I = the Basis of V;
B3: card(I) = n+1 by B2,ZMODUL03:def 5;
card(I) > 0 by B2,ZMODUL03:def 5;
then I <> {};
then consider v be object such that
B4: v in I by XBOOLE_0:7;
reconsider v as Vector of V by B4;
set Iv = I \ {v};
B22: {v} is Subset of I by B4,SUBSET_1:41;
then B5: card(Iv) = n+1 - card({v}) by B3,CARD_2:44
.= n+1 - 1 by CARD_1:30
.= n;
I is linearly-independent by VECTSP_7:def 3;
then B6: Iv is linearly-independent by XBOOLE_1:36,ZMODUL02:56;
set Vv = Lin(Iv);
reconsider VVv = Vv as finite-rank free Z_Module by B6;
for x be object holds x in Iv implies x in the carrier of VVv
by STRUCT_0:def 5,ZMODUL02:65;
then reconsider IIv = Iv as linearly-independent Subset of VVv
by B6,TARSKI:def 3,ZMODUL03:16;
Lin(Iv) = Lin(IIv) by ZMODUL03:20;
then IIv is Basis of VVv by VECTSP_7:def 3;
then B8: rank(VVv) = n by B5,ZMODUL03:def 5;
set Wv = W /\ Vv;
reconsider WWv = W /\ Vv as Subspace of Vv by ZMODUL01:105;
reconsider WWv as free Subspace of Vv by B1,B8;
set IIwv = the Basis of WWv;
the carrier of WWv c= the carrier of V by VECTSP_4:def 2;
then reconsider Iwv = IIwv as Subset of V by XBOOLE_1:1;
B13: V is_the_direct_sum_of Vv,Lin{v} by B4,FRdsY;
set B = {l.v where l is Linear_Combination of I :
Sum(l) in W};
B15: B c= INT
proof
let b be object such that
CX1: b in B;
consider l be Linear_Combination of I such that
CX2: l.v = b & Sum(l) in W by CX1;
thus b in INT by CX2;
end;
B16: for b1, b2 be Element of INT st b1 in B & b2 in B holds
b1 + b2 in B
proof
let b1, b2 be Element of INT such that
C1: b1 in B & b2 in B;
set bb1 = b1, bb2 = b2;
consider l1 be Linear_Combination of I such that
C3: l1.v = bb1 & Sum(l1) in W by C1;
consider l2 be Linear_Combination of I such that
C4: l2.v = bb2 & Sum(l2) in W by C1;
Sum(l1) + Sum(l2) = Sum(l1 + l2) by ZMODUL02:52;
then C5: Sum(l1 + l2) in W by C3,C4,ZMODUL01:36;
l1 + l2 is Linear_Combination of I by ZMODUL02:27;
then (l1 + l2).v in B by C5; then
l1.v + l2.v in B by VECTSP_6:22; then
b1 + b2 in B by C3,C4;
hence thesis;
end;
B17: 0 in B
proof
set wv = the Element of Wv;
wv in WWv;
then consider lwv be Linear_Combination of Iv such that
C2: wv = Sum(lwv) by ZMODUL01:23,ZMODUL02:64;
Carrier(lwv) c= Iv by VECTSP_6:def 4;
then not v in Carrier(lwv) by ZFMISC_1:56;
then C4: lwv.v = 0;
wv in Vv /\ W;
then C5: wv in W by VECTSP_5:3;
lwv is Linear_Combination of I by XBOOLE_1:36,ZMODUL02:10;
hence 0 in B by C2,C4,C5;
end;
B18: for b be Element of INT st b in B holds -b in B
proof
let b be Element of INT such that
C1: b in B;
consider l be Linear_Combination of I such that
C2: l.v = b & Sum(l) in W by C1;
-Sum(l) in W by C2,ZMODUL01:38;
then C3: Sum(-l) in W by ZMODUL02:54;
consider bm be Element of INT.Ring such that
C4: bm = (-l).v;
reconsider bb = b as Element of INT.Ring;
bm = -bb by C2,C4,VECTSP_6:36; then
C5: bm = -b;
-l is Linear_Combination of I by ZMODUL02:38;
hence thesis by C3,C4,C5;
end;
B19: for b be Element of INT st b in B holds
for i be Element of INT holds i * b in B
proof
let b be Element of INT such that
C1: b in B;
defpred Q[Integer] means $1 * b in B;
C2: Q[0] by B17;
C3: for i be Integer st Q[i] holds Q[i-1] & Q[i+1]
proof
let i be Integer such that
D1: Q[i];
D3: -b in B by B18,C1;
i*b is Element of INT & -b is Element of INT by INT_1:def 2;
then (i*b) + (-b) in B by B16,D1,D3;
hence Q[i-1];
i * b is Element of INT by INT_1:def 2;
then (i*b) + b in B by B16,C1,D1;
hence Q[i+1];
end;
for i be Integer holds Q[i] from INT_1:sch 4(C2,C3);
hence thesis;
end;
set BP = B /\ NAT;
ex p be Element of INT st p in B &
for b be Element of INT st b in B holds p divides b
proof
C2: BP is non empty by B17,XBOOLE_0:def 4;
C5: BP c= NAT by XBOOLE_1:17;
set BPN = BP \ {0};
per cases;
suppose BPN = {};
then D1: BP = {0} by C2,ZFMISC_1:58;
D2: for b be object st b in B holds b = 0
proof
let b be object such that
E1: b in B;
reconsider bb = b as Element of INT by B15,E1;
assume E2: b <> 0;
then per cases;
suppose bb > 0;
then bb in NAT by INT_1:3;
then bb in BP by E1,XBOOLE_0:def 4;
hence contradiction by D1,E2,TARSKI:def 1;
end;
suppose bb < 0;
then F1: -bb in NAT by INT_1:3;
-bb in B by B18,E1;
then -bb in BP by F1,XBOOLE_0:def 4;
hence contradiction by D1,E2,TARSKI:def 1;
end;
end;
set p = 0;
reconsider p as Element of INT by INT_1:def 2;
take p;
thus thesis by B17,D2;
end;
suppose BPN <> {};
then reconsider BPN as non empty Subset of NAT by C5,XBOOLE_1:1;
set p = min* BPN;
D1: p in BPN by NAT_1:def 1;
then D2: p in B by XBOOLE_0:def 4;
D4: p <> 0 & p is Element of NAT by D1,ZFMISC_1:56;
D5: for b be Element of INT st b in BP holds p divides b
proof
let b be Element of INT such that
E1: b in BP;
assume E2: not p divides b;
set r = b mod p;
reconsider r as Element of NAT by INT_1:3;
E3: r <> 0 by D4,E2,INT_1:62;
E4: r in BPN
proof
set q = b div p;
reconsider q as Element of INT by INT_1:def 2;
F1: b = q * p + r by D4,INT_1:59;
F2: b in B by E1,XBOOLE_0:def 4;
F3: q * p is Element of INT by INT_1:def 2;
p is Element of INT by INT_1:def 2;
then F5: -(q * p) in B by B18,B19,D2,F3;
-q*p is Element of INT by INT_1:def 2;
then b + (- q*p) in B by B16,F2,F5;
then r in BP by F1,XBOOLE_0:def 4;
hence thesis by E3,ZFMISC_1:56;
end;
r < p by D4,INT_1:58;
hence contradiction by E4,NAT_1:def 1;
end;
D6: for b be Element of INT st b in B holds p divides b
proof
let b be Element of INT such that
E1: b in B;
assume E2: not p divides b;
per cases;
suppose b >= 0;
then b in NAT by INT_1:3;
then b in BP by E1,XBOOLE_0:def 4;
hence contradiction by D5,E2;
end;
suppose b < 0;
then F1: -b in NAT by INT_1:3;
-b in B by B18,E1;
then F2: -b in BP by F1,XBOOLE_0:def 4;
-b is Element of INT by INT_1:def 2;
hence contradiction by D5,E2,F2,INT_2:10;
end;
end;
reconsider p as Element of INT by INT_1:def 1;
take p;
thus thesis by D1,D6,XBOOLE_0:def 4;
end;
end;
then consider p be Element of INT such that
B20: p in B and
B21: for b be Element of INT st b in B holds p divides b;
reconsider pp = p as Element of INT.Ring;
set Ws = ModuleStr (# the carrier of W, the addF of W,
the ZeroF of W, the lmult of W #);
Ws is Subspace of V
proof
C2: the carrier of Ws c= the carrier of V by VECTSP_4:def 2;
C3: 0.Ws = 0.W
.= 0.V by ZMODUL01:26;
C4: the addF of Ws = (the addF of V) || the carrier of Ws
by VECTSP_4:def 2;
the lmult of Ws = (the lmult of V) | [:INT, the carrier of Ws:]
by VECTSP_4:def 2;
hence thesis by C2,C3,C4,ZMODUL01:40;
end;
then reconsider Ws as strict Subspace of V;
B24: for w be Vector of V holds w in Ws iff w in W;
per cases;
suppose p = 0.INT.Ring; then
C2: for b be Element of INT holds b in B implies b = 0 by B21,INT_2:3;
for w be Vector of V st w in W holds w in Vv
proof
let w be Vector of V such that
D1: w in W;
the ModuleStr of V = Lin(I) by VECTSP_7:def 3;
then w in Lin(I);
then consider lw be Linear_Combination of I such that
D2: w = Sum(lw) by ZMODUL02:64;
lw.v in B by D1,D2;
then not v in Carrier(lw) by C2,ZMODUL02:8;
then Carrier(lw) c= I \ {v} by ZFMISC_1:34,VECTSP_6:def 4;
then lw is Linear_Combination of Iv by VECTSP_6:def 4;
hence thesis by D2,ZMODUL02:64;
end;
then for w be Vector of V st w in Ws holds w in Vv by B24;
then C4: Ws is Subspace of Vv by ZMODUL01:44;
Ws is free by B1,B8,C4;
then consider Iws being Subset of Ws such that
c5: Iws is base by VECTSP_7:def 4;
C5: Iws is linearly-independent & Lin(Iws) = the ModuleStr of Ws
by c5,VECTSP_7:def 3;
reconsider IwsV = Iws as linearly-independent Subset of V
by C5,ZMODUL03:15;
reconsider IwsW = IwsV as linearly-independent Subset of W
by ZMODUL03:16;
Lin(IwsW) = Lin(IwsV) by ZMODUL03:20
.= the ModuleStr of W by C5,ZMODUL03:20; then
IwsW is base by VECTSP_7:def 3;
hence thesis by VECTSP_7:def 4;
end;
suppose C1: p <> 0.INT.Ring;
consider lwpv be Linear_Combination of I such that
C2: lwpv.v = p & Sum(lwpv) in W by B20;
set wpv = Sum(lwpv);
set vpv = wpv - pp*v;
consider lv be Linear_Combination of V such that
C3: lv.v = 1.INT.Ring &
for u being Vector of V st v <> u holds lv.u = 0.INT.Ring
by ZMODUL03:1;
C4: Carrier(lv) = {v}
proof
for u being object holds u in Carrier(lv) implies u in {v}
proof
assume ex u being object st u in Carrier(lv) & not u in {v};
then consider u being Vector of V such that
D1: u in Carrier(lv) & not u in {v};
u <> v by D1,TARSKI:def 1;
then lv.u = 0 by C3;
hence contradiction by D1,ZMODUL02:8;
end;
then D2: Carrier(lv) c= {v} by TARSKI:def 3;
v in Carrier(lv) by C3;
then {v} c= Carrier(lv) by ZFMISC_1:31;
hence thesis by D2;
end;
then C18: Sum(lv) = lv.v * v by ZMODUL02:24;
then C5: Sum(pp*lv) = pp*(lv.v*v) by ZMODUL02:53
.= pp*v by C3,VECTSP_1:def 17;
lv is Linear_Combination of {v} by C4,VECTSP_6:def 4;
then pp*lv is Linear_Combination of {v} by ZMODUL02:31;
then C6: pp*v in Lin{v} by C5,ZMODUL02:64;
C17: v <> 0.V by B22,ZMODUL02:56,VECTSP_7:def 3;
C8: not pp*v in Vv
proof
assume pp*v in Vv;
then pp*v in Vv /\ Lin{v} by C6,VECTSP_5:3;
then pp*v in (0).V by B13,VECTSP_5:def 4;
hence contradiction by C1,C17,ZMODUL01:def 7,ZMODUL02:66;
end;
C9: vpv in Vv
proof
the ModuleStr of V = Lin(I) by VECTSP_7:def 3;
then vpv in Lin(I);
then consider lvpv be Linear_Combination of I such that
D2: vpv = Sum(lvpv) by ZMODUL02:64;
Carrier(pp*lv) = {v} by C1,C4,ZMODUL02:29;
then reconsider lpv = pp*lv as Linear_Combination of I
by B4,ZFMISC_1:31,VECTSP_6:def 4;
D3: Sum(lvpv) = Sum(lwpv-lpv) by C5,D2,ZMODUL02:55;
lwpv - lpv is Linear_Combination of I by ZMODUL02:41;
then Carrier(lvpv) c= I & Carrier(lwpv-lpv) c= I
by VECTSP_6:def 4;
then lvpv = lwpv - lpv by D3,VECTSP_7:def 3,ZMODUL03:3;
then lvpv.v = lwpv.v-lpv.v by ZMODUL02:39
.= lwpv.v - pp*(lv.v) by VECTSP_6:def 9
.= 0 by C2,C3;
then not v in Carrier(lvpv) by ZMODUL02:8;
then Carrier(lvpv) c= Iv by ZFMISC_1:34,VECTSP_6:def 4;
then reconsider lvvpv = lvpv as Linear_Combination of Iv
by VECTSP_6:def 4;
vpv = Sum(lvvpv) by D2;
hence thesis by ZMODUL02:64;
end;
reconsider wpv as Vector of V;
set Iw = Iwv \/ {wpv};
C10: wpv <> 0.V
proof
assume wpv = 0.V;
then -(-pp*v) in Vv by C9,ZMODUL01:38;
hence contradiction by C8;
end;
set WX = Wv + Lin{wpv};
reconsider WXv = WWv as Subspace of WX by ZMODUL01:97;
reconsider Xwpv = Lin{wpv} as Subspace of WX by ZMODUL01:97;
C11: not wpv in Iwv
proof
assume wpv in Iwv;
then wpv in WWv;
then D2: wpv in Vv by ZMODUL01:23;
wpv - vpv = (wpv - wpv) + pp*v by RLVECT_1:29
.= 0.V + pp*v by RLVECT_1:15
.= pp*v;
hence contradiction by C8,C9,D2,ZMODUL01:39;
end;
C12: WX = WXv + Xwpv
proof
D1: Iwv /\ {wpv} = {} by C11,XBOOLE_0:def 7,ZFMISC_1:50;
for x being Vector of WX ex x1, x2 being Vector of WX
st x1 in WXv & x2 in Xwpv & x = x1 + x2
proof
let x being Vector of WX;
E1: Wv = Lin(IIwv) by VECTSP_7:def 3
.= Lin(Iwv) by ZMODUL03:20;
WX = Lin(Iwv \/ {wpv}) by E1,ZMODUL02:72;
then x in Lin(Iwv \/ {wpv});
then consider lx be Linear_Combination of Iwv \/ {wpv} such that
E3: x = Sum(lx) by ZMODUL02:64;
consider lx1 be Linear_Combination of Iwv,
lx2 be Linear_Combination of {wpv} such that
E4: lx = lx1 + lx2 by D1,ThCarrier2;
set x1 = Sum(lx1);
set x2 = Sum(lx2);
x1 in WXv by E1,ZMODUL02:64;
then x1 in WX by ZMODUL01:24;
then reconsider xx1 = x1 as Vector of WX;
x2 in Xwpv by ZMODUL02:64;
then x2 in WX by ZMODUL01:24;
then reconsider xx2 = x2 as Vector of WX;
E5: x1 + x2 = x by E3,E4,ZMODUL02:52;
take xx1,xx2;
thus thesis by E1,E5,ZMODUL01:28,ZMODUL02:64;
end;
hence thesis by ZMODUL01:133;
end;
C15: {wpv} is linearly-independent by C10,ZMODUL02:59;
WXv /\ Xwpv = (0).WX
proof
assume WXv /\ Xwpv <> (0).WX;
then consider x be Vector of WX such that
D2: x in WXv /\ Xwpv & x <> 0.WX by Thn0V;
D3: x in WXv by D2,VECTSP_5:3;
x in Lin{wpv} by D2,VECTSP_5:3;
then consider lx be Linear_Combination of {wpv} such that
D5: x = Sum(lx) by ZMODUL02:64;
x in V by D3,ZMODUL01:24;
then reconsider xx = x as Vector of V;
x in WWv by D2,VECTSP_5:3;
then D9: x in Vv by ZMODUL01:23;
D6: x = lx.wpv * wpv by D5,ZMODUL02:21;
D7: lx.wpv <> 0
proof
assume lx.wpv = 0;
then x = 0.V by D6,ZMODUL01:1
.= 0.WX by ZMODUL01:26;
hence contradiction by D2;
end;
vpv + pp*v = wpv - (pp*v - pp*v) by RLVECT_1:29
.= wpv - 0.V by RLVECT_1:15
.= wpv;
then x = lx.wpv * vpv + lx.wpv * (pp*v) by D6,VECTSP_1:def 14
.= lx.wpv * vpv + (lx.wpv*pp) * v by VECTSP_1:def 16;
then D8: xx - lx.wpv * vpv
= (lx.wpv*pp) * v + (lx.wpv * vpv - lx.wpv * vpv) by RLVECT_1:28
.= (lx.wpv*pp) * v + 0.V by RLVECT_1:15
.= (lx.wpv*pp) * v;
lx.wpv * vpv in Vv by C9,ZMODUL01:37;
then D10: (lx.wpv*pp) * v in Vv by D8,D9,ZMODUL01:39;
D11: Sum((lx.wpv*pp)*lv) = (lx.wpv*pp) * (lv.v*v) by C18,ZMODUL02:53
.= (lx.wpv*pp) * v by C3,VECTSP_1:def 17;
lv is Linear_Combination of {v} by C4,VECTSP_6:def 4;
then (lx.wpv*pp)*lv is Linear_Combination of {v} by ZMODUL02:31;
then (lx.wpv*pp)*v in Lin{v} by D11,ZMODUL02:64;
then (lx.wpv*pp)*v in Vv /\ Lin{v} by D10,VECTSP_5:3;
then (lx.wpv*pp)*v in (0).V by B13,VECTSP_5:def 4;
hence contradiction by C1,C17,D7,ZMODUL01:def 7,ZMODUL02:66;
end;
then C17: WX is free by C12,C15,FRdsX,VECTSP_5:def 4;
for x be Vector of V holds x in W iff x in WX
proof
let x be Vector of V;
hereby
assume D1: x in W;
the ModuleStr of V = Lin(I) by VECTSP_7:def 3;
then x in Lin(I);
then consider lx be Linear_Combination of I such that
D2: x = Sum(lx) by ZMODUL02:64;
lx.v in B by D1,D2;
then consider y be Integer such that
D4: lx.v = p * y by B21,INT_1:def 3;
reconsider y as Element of INT.Ring by Lem1;
y*wpv in W by C2,ZMODUL01:37;
then E3: x - y*wpv in W by D1,ZMODUL01:39;
x - y*wpv in Vv
proof
F2: y*wpv = Sum(y*lwpv) by ZMODUL02:53;
(lx - y*lwpv).v = lx.v - (y*lwpv).v by ZMODUL02:39
.= pp*y - y*(lwpv.v) by D4,VECTSP_6:def 9
.= 0 by C2;
then F3: not v in Carrier(lx - y*lwpv) by ZMODUL02:8;
y*lwpv is Linear_Combination of I by ZMODUL02:31;
then lx - y*lwpv is Linear_Combination of I by ZMODUL02:41;
then Carrier(lx - y*lwpv) c= Iv
by F3,ZFMISC_1:34,VECTSP_6:def 4;
then reconsider lxy = lx - y*lwpv as Linear_Combination of Iv
by VECTSP_6:def 4;
x - y*wpv = Sum(lxy) by D2,F2,ZMODUL02:55;
hence thesis by ZMODUL02:64;
end;
then E4: x - y*wpv in Wv by E3,VECTSP_5:3;
wpv in {wpv} by TARSKI:def 1;
then E5: y*wpv in Lin{wpv} by ZMODUL01:37,ZMODUL02:65;
(x - y*wpv) + y*wpv = x - (y*wpv-y*wpv) by RLVECT_1:29
.= x - 0.V by RLVECT_1:5
.= x;
hence x in WX by E4,E5,VECTSP_5:1;
end;
assume D1: x in WX;
D2: Wv is Subspace of W by ZMODUL01:105;
Lin{wpv} is Subspace of W by C2,ZFMISC_1:31,ZMODUL03:19;
then WX is Subspace of W by D2,ZMODUL02:76;
hence x in W by D1,ZMODUL01:23;
end;
then for x be Vector of V holds x in Ws iff x in WX by B24;
then Ws is free by C17,VECTSP_4:30;
then consider Iws being Subset of Ws such that
c18: Iws is base by VECTSP_7:def 4;
C18: Iws is linearly-independent & Lin(Iws) = the ModuleStr of Ws
by VECTSP_7:def 3,c18;
reconsider IwsV = Iws as linearly-independent Subset of V
by C18,ZMODUL03:15;
reconsider IwsW = IwsV as linearly-independent Subset of W
by ZMODUL03:16;
Lin(IwsW) = Lin(IwsV) by ZMODUL03:20
.= the ModuleStr of W by C18,ZMODUL03:20; then
IwsW is base by VECTSP_7:def 3;
hence thesis by VECTSP_7:def 4;
end;
end;
A3: for m being Nat holds P[m] from NAT_1:sch 2(A1,A2);
let V be finite-rank free Z_Module, W be Subspace of V;
set n = rank(V);
P[n] by A3;
hence thesis;
end;
registration
let V be finite-rank free Z_Module;
cluster -> free for Subspace of V;
correctness by FRX;
end;
theorem
for V being Z_Module, W being Subspace of V,
W1, W2 being free Subspace of V st
W1 /\ W2 = (0).V & the ModuleStr of W = W1 + W2
holds W is free
proof
let V be Z_Module, W be Subspace of V,
W1, W2 be free Subspace of V such that
A1: W1 /\ W2 = (0).V & the ModuleStr of W = W1 + W2;
reconsider Ws = W1 + W2 as free Subspace of V by A1,ThDirectSum;
consider I be Subset of Ws such that
a3: I is base by VECTSP_7:def 4;
A3: I is linearly-independent & Ws = Lin(I) by VECTSP_7:def 3,a3;
reconsider IV = I as linearly-independent Subset of V
by A3,ZMODUL03:15;
reconsider IW = IV as linearly-independent Subset of W by A1,ZMODUL03:16;
the ModuleStr of W = Lin(IV) by A1,A3,ZMODUL03:20
.= Lin(IW) by ZMODUL03:20; then
IW is base by VECTSP_7:def 3;
hence thesis by VECTSP_7:def 4;
end;
theorem
for p being prime Element of INT.Ring, V being free Z_Module
st Z_MQ_VectSp(V,p) is finite-dimensional
holds V is finite-rank
proof
let p be prime Element of INT.Ring, V be free Z_Module such that
A1: Z_MQ_VectSp(V,p) is finite-dimensional;
set I = the Basis of V;
set IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I};
now let x be object;
assume x in IQ;
then consider v be Vector of V such that
B1: x = ZMtoMQV(V,p,v) & v in I;
thus x in the carrier of Z_MQ_VectSp(V,p) by B1;
end;
then reconsider IQ as Subset of Z_MQ_VectSp(V,p) by TARSKI:def 3;
A3: IQ is Basis of Z_MQ_VectSp(V,p) by ZMODUL03:35;
A2: card IQ = card I by ZMODUL03:26;
IQ is finite by A1,A3,VECTSP_9:20;
then I is finite by A2;
hence thesis by ZMODUL03:def 3;
end;
theorem
for p being prime Element of INT.Ring, V being Z_Module,
s be Element of V, a be Element of INT.Ring, b be Element of GF(p)
st b = a mod p holds
b*ZMtoMQV(V,p,s) = ZMtoMQV(V,p,a*s)
proof
let p be prime Element of INT.Ring, V be Z_Module, s be Element of V,
a be Element of INT.Ring, b be Element of GF(p) such that
A1: b = a mod p;
A2: ZMtoMQV(V,p,s) = s + p(*)V;
set t = ZMtoMQV(V,p,s);
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;
thus b*t =(a mod p) * t1 by A1,ZMODUL02:def 11
.= a * t1 by ZMODUL02:2
.= lmultCoset(V,p(*)V).(a,s + p(*)V) by VECTSP10:def 6
.= ZMtoMQV(V,p,a*s) by A3,VECTSP10:def 5;
end;
LMX2: 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) *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 EC_PF_1:14;
reconsider t1 = ZMtoMQV(V,p,v) as Element of Z_MQ_VectSp(V,p);
reconsider t1 as Element of VectQuot(V,p(*)V);
ZMtoMQV(V,p,v) = v + p(*)V; then
Q1: v + p(*)V is Element of CosetSet(V,p(*)V) by VECTSP10:def 6;
thus ZMtoMQV(V,p,(i mod p) *v) = a*ZMtoMQV(V,p,v) by ZMODUL03:30
.= (i mod p) * t1 by ZMODUL02:def 11
.= i*t1 by ZMODUL02:2
.= lmultCoset(V,p(*)V).(i,t1) by VECTSP10:def 6
.= ZMtoMQV(V,p,i*v) by Q1,VECTSP10:def 5;
end;
theorem ThQuotBasis5A:
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),
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 Subset of V,
IQ be Subset of Z_MQ_VectSp(V,p),
l be 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 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
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 EC_PF_1:14;
reconsider a = (l.v) mod p as Element of INT.Ring;
reconsider k = l.v as Element of INT.Ring;
reconsider si = (l.v)*v as Element of V;
reconsider t = ZMtoMQV(V,p,v) as Element of Z_MQ_VectSp(V,p);
Y7: b*t = ZMtoMQV(V,p, a*v) by ZMODUL03:30
.= ZMtoMQV(V,p, k*v) by LMX2;
H1: v in Carrier(l) by Y3,P1,FUNCT_1:3;
Carrier(l) c= I by VECTSP_6:def 4;
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,ZMODUL03:33;
end;
theorem ThQuotBasis5:
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 Lin(I) = the ModuleStr of V &
IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
Lin(IQ) = the ModuleStr of Z_MQ_VectSp(V,p)
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) such that
P0: Lin(I) = the ModuleStr of V and
AS: IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I};
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 ZMODUL03:22;
consider l be Linear_Combination of I such that
P4: v = Sum(l) by P0,STRUCT_0:def 5,ZMODUL02:64;
thus vq in Lin(IQ) by AS,P4,P3,ThQuotBasis5A;
end;
hence thesis by VECTSP_4:32;
end;
theorem FG02:
for V being finitely-generated free Z_Module
holds ex A being finite Subset of V st A is Basis of V
proof
let V be finitely-generated free Z_Module;
set p = the prime Element of INT.Ring;
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 consider v be Vector of V such that
B1: x = ZMtoMQV(V,p,v) & v in A;
thus x in the carrier of Z_MQ_VectSp(V,p) by B1;
end;
then reconsider AQ as Subset of Z_MQ_VectSp(V,p) by TARSKI:def 3;
reconsider AQ as Basis of Z_MQ_VectSp(V,p) by ZMODUL03:35;
consider B being finite Subset of V such that
P1: Lin(B) = the ModuleStr of V by ZMODUL03:def 4;
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 consider v be Vector of V such that
B1: x = ZMtoMQV(V,p,v) & v in B;
thus x in the carrier of Z_MQ_VectSp(V,p) by B1;
end;
then reconsider BQ as Subset of Z_MQ_VectSp(V,p) by TARSKI:def 3;
deffunc F(Element of V) = ZMtoMQV(V,p,$1);
consider f be Function of the carrier of V, Z_MQ_VectSp(V,p) such that
P6: for x be Element of V holds f.x = F(x) from FUNCT_2:sch 4;
B c= the carrier of V;
then P8: B c= dom f by FUNCT_2:def 1;
for y be object st y in BQ ex x be object st x in dom (f|B) & y = (f|B).x
proof
let y be object such that
Q1: y in BQ;
consider x be Vector of V such that
Q2: y = ZMtoMQV(V,p,x) & x in B by Q1;
Q3: x in dom(f|B) by P8,Q2,RELAT_1:62;
Q4: y = f.x by P6,Q2
.= (f|B).x by Q3,FUNCT_1:47;
take x;
thus thesis by P8,Q2,Q4,RELAT_1:62;
end;
then P2: BQ c= rng (f | B) by FUNCT_1:9;
Lin(BQ) = the ModuleStr of Z_MQ_VectSp(V,p) by P1,ThQuotBasis5;
then consider IQ be Basis of Z_MQ_VectSp(V,p) such that
P4: IQ c= BQ by VECTSP_7:20;
P5: AQ is finite by P2,P4,MATRLIN:def 1,VECTSP_9:20;
card A = card AQ by ZMODUL03:26;
then A is finite by P5;
hence thesis;
end;
registration
cluster -> finite-rank for finitely-generated free Z_Module;
coherence
proof
let V be finitely-generated free Z_Module;
ex A being finite Subset of V st A is Basis of V by FG02;
hence thesis by ZMODUL03:def 3;
end;
end;
registration
cluster -> finitely-generated for finite-rank free Z_Module;
coherence
proof
let V be finite-rank free Z_Module;
consider A be finite Subset of V such that
A1: A is Basis of V by ZMODUL03:def 3;
take A;
thus thesis by A1,VECTSP_7:def 3;
end;
end;
theorem RL5Th25:
for V be finite-rank free Z_Module holds for A being Subset of V
st A is linearly-independent holds A is finite
proof
let V be finite-rank free Z_Module;
let A be Subset of V;
consider I be finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume A is linearly-independent;
then card A c= card I by A1,XXTh3,XBOOLE_0:def 8;
hence thesis;
end;
RL5Th28:
for V be finite-rank free Z_Module, W be Subspace of V holds
W is finite-rank
proof
let V be finite-rank free Z_Module, W be Subspace of V;
set A = the Basis of W;
reconsider A0 = A as linearly-independent Subset of V
by VECTSP_7:def 3,ZMODUL03:15;
A0 is finite by RL5Th25;
hence thesis by ZMODUL03:def 3;
end;
registration
let V be Z_Module, W1, W2 be finite-rank free Subspace of V;
cluster W1 /\ W2 -> free;
correctness
proof
W1 /\ W2 is Subspace of W1 by ZMODUL01:105;
hence thesis;
end;
end;
registration
let V be Z_Module, W1, W2 be finite-rank free Subspace of V;
cluster W1 /\ W2 -> finite-rank;
correctness
proof
W1 /\ W2 is Subspace of W1 by ZMODUL01:105;
hence thesis by RL5Th28;
end;
end;
registration
let V be finite-rank free Z_Module;
cluster -> finite-rank for Subspace of V;
correctness by RL5Th28;
end;