:: Torsion $\mathbb Z$-module and Torsion-free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received November 29, 2014
:: Copyright (c) 2014-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, SUBSET_1, RLVECT_1, STRUCT_0, PBOOLE, FUNCT_4,
FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOM,
RLSUB_2, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1,
NAT_1, FUNCT_2, FINSET_1, FUNCOP_1, RLSUB_1, ZFMISC_1, INT_1, RLVECT_2,
ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2, INT_3,
COMPLEX1, INT_2, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, MONOID_0,
ZMODUL02, RLVECT_5, ZMODUL04, ZMODUL05, ZMODUL06, MOD_3, FUNCSDOM,
VECTSP_2, BINOP_1, LATTICES, VECTSP10;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1,
ORDINAL1, PARTFUN1,
FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1, INT_2, REALSET1, FUNCT_4,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4,
VECTSP_5, VECTSP_6, INT_3, VECTSP_7, VECTSP_9, VECTSP10, MATRLIN, BINOM,
ZMODUL01, ZMODUL02, RANKNULL, ZMODUL03, GAUSSINT, MOD_2, ZMODUL04,
ZMODUL05;
constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, FUNCT_4,
VECTSP_6, VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL04, ZMODUL05, INT_2,
ZMODUL01, ZMODUL02, MATRLIN, MOD_2, INT_3, RANKNULL;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0,
STRUCT_0, RLVECT_1, CARD_1, INT_1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1,
INT_3, RELAT_1, ZMODUL02, GAUSSINT, FUNCT_4, RAT_1, XCMPLX_0, ZMODUL03,
ZMODUL04, ZMODUL05, VECTSP_4, VECTSP_7, VECTSP10, VECTSP_1, MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions VECTSP_1, VECTSP_7;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, INT_3, GAUSSINT, ZMODUL02, SUBSET_1,
VECTSP_4, VECTSP_6;
expansions TARSKI, STRUCT_0, ZMODUL03, VECTSP_5, ZMODUL01, VECTSP_7;
theorems CARD_1, CARD_2, SUBSET_1, FUNCT_1, FUNCT_2, INT_1, NAT_1, RLVECT_1,
TARSKI, ZMODUL01, BINOP_2, ZFMISC_1, RELAT_1, GAUSSINT, ZMODUL03,
XBOOLE_0, XBOOLE_1, XXREAL_0, STRUCT_0, XCMPLX_0, VECTSP_1, EULER_1,
INT_2, ZMODUL02, NAT_D, VECTSP_6, VECTSP_7, VECTSP_4, VECTSP_5, VECTSP_9,
BINOM, ABSVALUE, ZMODUL04, ZMODUL05, MOD_2, MOD_3, VECTSP_2;
schemes FUNCT_2, NAT_1;
begin :: 1. Torsion $\mathbb{Z}$-module and torsion-free $\mathbb{Z}$-module
theorem Th1V:
for R being commutative Ring
for V being LeftMod of R, W being Subspace of V
holds (1.R) (*) W = (Omega).W
proof
let R be commutative Ring;
let V be LeftMod of R, W be Subspace of V;
for v being Vector of V st v in (Omega).W holds v in (1.R) (*) W
proof
let v be Vector of V such that
B1: v in (Omega).W;
reconsider vv = v as Vector of W by B1;
(1.R) * vv in (1.R) (*) W;
hence thesis;
end; then
A2: for v being Vector of V holds v in (1.R) (*) W iff
v in (Omega).W;
A3: (Omega).W is Subspace of V by ZMODUL01:42;
(1.R) (*) W is Subspace of V by ZMODUL01:42;
hence thesis by A2,A3,ZMODUL01:46;
end;
theorem
for R being Ring
for V being LeftMod of R, W1, W2, W3 being Subspace of V holds
W1 /\ W2 is Subspace of (W1 + W3) /\ W2
proof
let R be Ring;
let V be LeftMod of R, W1, W2, W3 be Subspace of V;
for v being Vector of V st v in W1 /\ W2 holds v in (W1 + W3) /\ W2
proof
let v be Vector of V such that
A1: v in W1 /\ W2;
v in W1 by A1,VECTSP_5:3;
then A2: v in W1 + W3 by VECTSP_5:2;
v in W2 by A1,VECTSP_5:3;
hence thesis by A2,VECTSP_5:3;
end;
hence thesis by VECTSP_4:28;
end;
theorem ThIS1:
for R being Ring
for V being LeftMod of R, W1, W2, W3 being Subspace of V
st W1 /\ W2 <> (0).V holds (W1 + W3) /\ W2 <> (0).V
proof
let R be Ring;
let V be LeftMod of R, W1, W2, W3 be Subspace of V such that
A1: W1 /\ W2 <> (0).V;
consider v be Vector of V such that
A2: v in W1 /\ W2 & v <> 0.V by A1,ZMODUL04:24;
A3: v in W1 & v in W2 by A2,ZMODUL01:94;
then v in W1 + W3 by ZMODUL01:93;
hence thesis by A2,ZMODUL02:66,A3,ZMODUL01:94;
end;
theorem
for V being Z_Module, I, I1 being linearly-independent Subset of V
st I1 c= I holds
Lin(I \ I1) /\ Lin(I1) = (0).V
proof
let V be Z_Module, I, I1 be linearly-independent Subset of V such that
A1: I1 c= I;
assume Lin(I \ I1) /\ Lin(I1) <> (0).V;
then consider v be Vector of V such that
A2: v in Lin(I \ I1) /\ Lin(I1) & v <> 0.V by ZMODUL04:24;
v in Lin(I \ I1) by A2,ZMODUL01:94;
then consider l1 be Linear_Combination of I \ I1 such that
A3: v = Sum(l1) by ZMODUL02:64;
A4: Carrier(l1) c= I \ I1 by VECTSP_6:def 4;
v in Lin(I1) by A2,ZMODUL01:94;
then consider l2 be Linear_Combination of I1 such that
A5: v = Sum(l2) by ZMODUL02:64;
A6: Carrier(l2) c= I1 by VECTSP_6:def 4;
reconsider ll1 = l1 as Linear_Combination of I
by XBOOLE_1:36,ZMODUL02:10;
reconsider ll2 = l2 as Linear_Combination of I by A1,ZMODUL02:10;
Carrier(l1) misses Carrier(l2) by A4,A6,XBOOLE_1:64,79;
then Carrier(ll1) /\ Carrier(ll2) = {} by XBOOLE_0:def 7;
then A10: Carrier(ll1) /\ Carrier(-ll2) = {} by ZMODUL02:37;
reconsider ll2x = -ll2 as Linear_Combination of I by ZMODUL02:38;
A7: Carrier(ll1 - ll2) = Carrier(ll1) \/ Carrier(ll2x)
by A10,ZMODUL04:25;
A8: Sum(ll1) - Sum(ll2) = 0.V by A3,A5,RLVECT_1:5;
reconsider l = ll1 - ll2 as Linear_Combination of I by ZMODUL02:41;
A9: Sum(l) = 0.V by A8,ZMODUL02:55;
Carrier(ll1) <> {} by A2,A3,ZMODUL02:23;
hence contradiction by A9,A7,VECTSP_7:def 1;
end;
reserve V for Z_Module;
reserve W for Subspace of V;
reserve v, u for Vector of V;
reserve i for Element of INT.Ring;
definition
let R be Ring;
let V be LeftMod of R, v be Vector of V;
attr v is torsion means
ex i being Element of R st i <> 0.R & i*v = 0.V;
end;
ThTV1:
0.V is torsion
proof
(1.INT.Ring) * 0.V = 0.V;
hence thesis;
end;
registration let V be Z_Module;
cluster 0.V -> torsion;
coherence by ThTV1;
end;
theorem
v is torsion & u is torsion implies v + u is torsion
proof
assume v is torsion & u is torsion;
then consider i1, i2 be Element of INT.Ring such that
A1: i1 <> 0 & i1 * v = 0.V and
A2: i2 <> 0 & i2 * u = 0.V;
(i1*i2)*(v+u) = (i1*i2)*v + (i1*i2)*u by VECTSP_1:def 14
.= (i2*i1)*v + i1*(i2*u) by VECTSP_1:def 16
.= i2*(i1*v) + i1*(i2*u) by VECTSP_1:def 16
.= 0.V + i1*0.V by ZMODUL01:1,A1,A2
.= 0.V by ZMODUL01:1;
hence thesis by A1,A2;
end;
theorem
v is torsion implies -v is torsion
proof
assume v is torsion;
then consider i be Element of INT.Ring such that
A1: i <> 0 & i * v = 0.V;
i*(-v) = - (i*v) by ZMODUL01:6
.= 0.V by A1;
hence thesis by A1;
end;
theorem
v is torsion & u is torsion implies v - u is torsion
proof
assume v is torsion & u is torsion;
then consider i1, i2 be Element of INT.Ring such that
A1: i1 <> 0 & i1 * v = 0.V and
A2: i2 <> 0 & i2 * u = 0.V;
(i1*i2)*(v-u) = (i1*i2)*v - (i1*i2)*u by ZMODUL01:8
.= (i2*i1)*v - i1*(i2*u) by VECTSP_1:def 16
.= i2*(i1*v) - i1*(i2*u) by VECTSP_1:def 16
.= 0.V - i1*0.V by ZMODUL01:1,A1,A2
.= 0.V - 0.V by ZMODUL01:1
.= 0.V;
hence thesis by A1,A2;
end;
theorem
v is torsion implies i * v is torsion
proof
assume v is torsion;
then consider i1 be Element of INT.Ring such that
A1: i1 <> 0 & i1 * v = 0.V;
i1*(i*v) = (i1*i)*v by VECTSP_1:def 16
.= i*(i1*v) by VECTSP_1:def 16
.= 0.V by ZMODUL01:1,A1;
hence thesis by A1;
end;
theorem ThTV6:
for v being Vector of V, w being Vector of W st v = w holds
v is torsion iff w is torsion
proof
let v be Vector of V, w be Vector of W such that
A1: v = w;
hereby
assume v is torsion;
then consider i be Element of INT.Ring such that
B2: i <> 0 & i*v = 0.V;
i*w = i*v by A1,ZMODUL01:29
.= 0.W by ZMODUL01:26,B2;
hence w is torsion by B2;
end;
assume w is torsion;
then consider i be Element of INT.Ring such that
B2: i <> 0 & i*w = 0.W;
i*v = i*w by A1,ZMODUL01:29
.= 0.V by ZMODUL01:26,B2;
hence v is torsion by B2;
end;
registration
let V be Z_Module;
cluster torsion for Vector of V;
correctness
proof
take 0.V;
thus thesis;
end;
end;
theorem
v is non torsion implies -v is non torsion
proof
assume A1: not v is torsion;
assume -v is torsion;
then consider i be Element of INT.Ring such that
A3: i <> 0 & i*(-v) = 0.V;
(-i)*v = 0.V by A3,ZMODUL01:5;
hence contradiction by A1,A3;
end;
theorem
v is non torsion & i <> 0 implies i * v is non torsion
proof
assume A1: not v is torsion & i <> 0;
assume i * v is torsion;
then consider i1 be Element of INT.Ring such that
A3: i1 <> 0 & i1 * (i * v) = 0.V;
(i1 * i) * v = 0.V by A3,VECTSP_1:def 16;
hence contradiction by A1,A3;
end;
theorem ThnTV3:
v is non torsion iff {v} is linearly-independent
proof
A1: not v is torsion implies {v} is linearly-independent
proof
assume B1: not v is torsion;
let l be Linear_Combination of {v};
assume B4: Sum(l) = 0.V;
now
per cases by ZFMISC_1:33,VECTSP_6:def 4;
suppose
Carrier(l) = {};
hence thesis;
end;
suppose
B5: Carrier(l) = {v}; then
B6: 0.V = l.v * v by B4,ZMODUL02:24;
now
assume v in Carrier(l);
then ex u st v = u & l.u <> 0.INT.Ring;
hence contradiction by B1,B6;
end;
hence thesis by B5,TARSKI:def 1;
end;
end;
hence thesis;
end;
{v} is linearly-independent implies not v is torsion
proof
assume B1: {v} is linearly-independent;
assume v is torsion; then
consider i be Element of INT.Ring such that
C2: i <> 0 & i*v = 0.V;
consider l be Linear_Combination of V such that
C3: l.v = 1 & for u being Vector of V st v <> u holds l.u = 0.INT.Ring
by ZMODUL03:1;
for u being Vector of V st u <> v holds not u in Carrier(l)
proof
let u be Vector of V;
assume u <> v;
then l.u = 0 by C3;
hence not u in Carrier(l) by ZMODUL02:8;
end;
then for u being object holds u = v iff u in Carrier(l) by C3;
then C5: Carrier(l) = {v} by TARSKI:def 1;
then C6: Carrier(i*l) = {v} by C2,ZMODUL02:29;
C7: Carrier(i*l) <> {} by C2,C5,ZMODUL02:29;
reconsider li = i*l as Linear_Combination of {v}
by C6,VECTSP_6:def 4;
Sum(i*l) = i*Sum(l) by ZMODUL02:53
.= i*((1.INT.Ring)*v) by C3,C5,ZMODUL02:24
.= 0.V by C2;
then Sum(li) = 0.V;
hence contradiction by B1,C7;
end;
hence thesis by A1;
end;
definition
let V be Z_Module;
attr V is torsion means
:defTorsionModule:
for v being Vector of V holds v is torsion;
end;
ThTZM:
(0).V is torsion
proof
for x being Vector of (0).V holds x is torsion
proof
let x be Vector of (0).V;
x in (0).V;
then x = 0.V by ZMODUL02:66
.= 0.((0).V) by ZMODUL01:26;
hence thesis;
end;
hence thesis;
end;
registration let V be Z_Module;
cluster (0).V -> torsion;
coherence by ThTZM;
end;
registration
cluster torsion for Z_Module;
existence
proof
set V = the Z_Module;
take (0).V;
thus thesis;
end;
end;
theorem LMINTRNG1:
for v be Element of INT.Ring,v1 be Integer st v = v1 holds
for n be Nat holds (Nat-mult-left(INT.Ring)).(n,v) = n*v1
proof
let v be Element of INT.Ring,v1 be Integer;
assume A1: v = v1;
defpred P[Nat] means
(Nat-mult-left(INT.Ring)).($1,v) = $1*v1;
(Nat-mult-left(INT.Ring)).(0,v) = 0.(INT.Ring) by BINOM:def 3
.= (0.INT.Ring) * v1; then
X1: P[0];
X2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume X22: P[n];
(Nat-mult-left(INT.Ring)).(n+1,v) = v + (Nat-mult-left(INT.Ring)).(n,v)
by BINOM:def 3
.= (n+1)*v1 by A1,X22;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(X1,X2);
hence thesis;
end;
theorem LMINTRNG2:
for x be Element of INT.Ring, v be Element of INT.Ring,
v1 be Integer
st v = v1 holds (Int-mult-left INT.Ring).(x,v) = x*v1
proof
let x be Element of INT.Ring, v be Element of INT.Ring,
v1 be Integer;
assume A1: v = v1;
reconsider xx = x as Element of INT;
per cases;
suppose C1: x >= 0;
then reconsider x0 = x as Element of NAT by INT_1:3;
thus (Int-mult-left INT.Ring).(x,v) = (Nat-mult-left INT.Ring).(xx,v)
by C1,ZMODUL01:def 20
.= (Nat-mult-left INT.Ring).(x0,v)
.= x0*v1 by LMINTRNG1,A1
.= x*v1;
end;
suppose C2: x < 0;
then reconsider x0 = -x as Element of NAT by INT_1:3;
thus (Int-mult-left(INT.Ring)).(x,v)
= (Nat-mult-left INT.Ring) . (-x,-v) by C2,ZMODUL01:def 20
.= x0*(-v1) by LMINTRNG1,A1
.= x*v1;
end;
end;
registration
cluster non torsion for Z_Module;
existence
proof
set AG = INT.Ring;
set G =
ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,
Int-mult-left(AG) #);
reconsider G as Z_Module by ZMODUL01:164;
reconsider v = 1.INT.Ring as Vector of G;
set One = 1.INT.Ring;
for i being Element of INT.Ring st i <> 0 holds i*v <> 0.G
proof
assume ex i being Element of INT.Ring st i <> 0 & i*v = 0.G;
then consider i be Element of INT.Ring such that
B1: i <> 0 & i*v = 0.G;
i * v = (the lmult of G).(i,v) by VECTSP_1:def 12
.= (Int-mult-left(AG)).(i,v)
.= i * One by LMINTRNG2
.= i;
hence contradiction by B1;
end;
then v is non torsion;
hence thesis by defTorsionModule;
end;
end;
registration
let V be non torsion Z_Module;
cluster non torsion for Vector of V;
existence by defTorsionModule;
end;
definition
let V be Z_Module;
attr V is torsion-free means
:defTorsionFree:
for v being Vector of V st v <> 0.V holds v is non torsion;
end;
theorem ThMCTF:
V is Mult-cancelable iff V is torsion-free
proof
hereby
assume V is Mult-cancelable; then
for v being Vector of V st v <> 0.V holds v is non torsion;
hence V is torsion-free;
end;
assume AS: V is torsion-free;
for i being Element of INT.Ring, v being Vector of V holds
i <> 0.INT.Ring & v <> 0.V implies i * v <> 0.V
proof
let i be Element of INT.Ring, v be Vector of V;
assume A1: i <> 0.INT.Ring & v <> 0.V; then
v is non torsion by AS;
hence i * v <> 0.V by A1;
end;
hence V is Mult-cancelable;
end;
registration
cluster -> torsion-free for Mult-cancelable Z_Module;
coherence by ThMCTF;
end;
registration
cluster -> Mult-cancelable for torsion-free Z_Module;
coherence by ThMCTF;
end;
registration
cluster -> torsion-free for free Z_Module;
coherence;
end;
registration
cluster torsion-free free for Z_Module;
existence
proof
set V = the free Z_Module;
take V;
thus thesis;
end;
end;
theorem
for V being torsion-free Z_Module, v being Vector of V holds
v is torsion iff v = 0.V by defTorsionFree;
registration
let V be torsion-free Z_Module;
cluster -> torsion-free for Subspace of V;
coherence
proof
let W be Subspace of V;
for w being Vector of W st w <> 0.W holds w is non torsion
proof
let w be Vector of W such that
A1: w <> 0.W;
A2: w <> 0.V by A1,ZMODUL01:26;
reconsider v = w as Vector of V by ZMODUL01:25;
v is non torsion by A2,defTorsionFree;
hence thesis by ThTV6;
end;
hence thesis;
end;
end;
registration
let R be Ring;
let V be LeftMod of R;
cluster (0).V -> trivial;
coherence
proof
for x, y being Vector of (0).V holds x = y
proof
let x, y be Vector of (0).V;
x in (0).V & y in (0).V;
then x = 0.V & y = 0.V by VECTSP_4:35;
hence thesis;
end;
hence (0).V is trivial;
end;
end;
registration
cluster -> non torsion for non trivial torsion-free Z_Module;
coherence
proof
let V be non trivial torsion-free Z_Module;
(Omega).V <> (0).V;
then consider v be Vector of V such that
A2: v in (Omega).V & v <> 0.V by ZMODUL04:24;
thus thesis by A2,defTorsionFree;
end;
end;
registration
let R be Ring;
cluster trivial for LeftMod of R;
existence
proof
set V = the LeftMod of R;
take (0).V;
thus thesis;
end;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable
associative left_unital distributive non degenerated
non empty doubleLoopStr;
cluster Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
strict for non trivial ModuleStr over K;
existence
proof
take StructVectSp(K);
thus thesis;
end;
end;
registration
let R be non degenerated non empty Ring;
let V be non trivial LeftMod of R;
cluster non zero for Vector of V;
existence
proof
(Omega).V <> (0).V;
then consider v be Vector of V such that
A1: v in (Omega).V & v <> 0.V by ZMODUL04:24;
take v;
thus thesis by A1;
end;
end;
theorem ThnTV4:
v is non torsion iff Lin{v} is free & v <> 0.V
proof
hereby
assume v is non torsion;
then {v} is linearly-independent Subset of V by ThnTV3;
hence Lin{v} is free & v <> 0.V;
end;
assume A1: Lin{v} is free & v <> 0.V;
then A2: Lin{v} is torsion-free;
A3: v <> 0.Lin{v} by A1,ZMODUL01:26;
v in {v} by TARSKI:def 1;
then v in Lin{v} by ZMODUL02:65;
then reconsider vl = v as Vector of Lin{v};
vl is non torsion by A2,A3;
hence v is non torsion by ThTV6;
end;
registration
let V be non torsion Z_Module;
let v be non torsion Vector of V;
cluster Lin{v} -> free;
coherence by ThnTV4;
end;
theorem ThLIV1:
for V being Z_Module, A being Subset of V, v being Vector of V
st A is linearly-independent & v in A holds
v is non torsion
proof
let V be Z_Module, A be Subset of V, v be Vector of V such that
A1: A is linearly-independent & v in A;
{v} is linearly-independent by A1,ZMODUL02:56,ZFMISC_1:31;
hence v is non torsion by ThnTV3;
end;
theorem ThLin1:
for u being object holds u in Lin{v} implies
ex i being Element of INT.Ring st u = i*v
proof
let u be object;
assume u in Lin{v};
then consider l be Linear_Combination of {v} such that
A1: u = Sum(l) by ZMODUL02:64;
take l.v;
thus thesis by A1,ZMODUL02:21;
end;
theorem ThLin2:
v in Lin{v} by ZMODUL02:65,ZFMISC_1:31;
theorem
i*v in Lin{v} by ZMODUL01:37,ThLin2;
ThLin4:
for A being Subset of V holds A is Subset of Lin(A) by ZMODUL05:30;
theorem ThLin5:
for R being Ring
for V being LeftMod of R holds
Lin{0.V} = (0).V
proof
let R be Ring;
let V be LeftMod of R;
for x being object holds x in Lin{0.V} iff x in (0).V
proof
let x be object;
hereby
assume x in Lin{0.V};
then consider l be Linear_Combination of {0.V} such that
B2: x = Sum(l) by MOD_3:4;
Sum(l) = l.(0.V) * 0.V by VECTSP_6:17
.= 0.V by VECTSP_1:14;
hence x in (0).V by B2,VECTSP_4:17;
end;
assume x in (0).V;
then x = 0.V by VECTSP_4:35;
hence x in Lin{0.V} by VECTSP_4:17;
end;
then for x being Vector of V holds
x in Lin{0.V} iff x in (0).V;
hence thesis by VECTSP_4:30;
end;
registration
let V be torsion-free Z_Module;
let v be Vector of V;
cluster Lin{v} -> free;
coherence
proof
per cases;
suppose v = 0.V;
then Lin{v} = (0).V by ThLin5;
hence thesis;
end;
suppose v <> 0.V;
then v is non torsion by defTorsionFree;
hence thesis by ThnTV4;
end;
end;
end;
theorem
for A1, A2 being Subset of V
st A1 is linearly-independent & A2 is linearly-independent &
A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent holds
Lin(A1) /\ Lin(A2) <> (0).V
proof
let A1, A2 be Subset of V such that
A1: A1 is linearly-independent & A2 is linearly-independent and
A2: A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent;
consider l be Linear_Combination of A1 \/ A2 such that
A3: Sum(l) = 0.V & Carrier(l) <> {} by A2;
consider l1 be Linear_Combination of A1,
l2 be Linear_Combination of A2 such that
A4: l = l1 + l2 by A2,ZMODUL04:26;
A5: Sum(l) = Sum(l1) + Sum(l2) by ZMODUL02:52,A4;
A6: Carrier(l) c= Carrier(l1) \/ Carrier(l2) by A4,ZMODUL02:26;
per cases by A3,A6;
suppose Carrier(l1) <> {}; then
B2: Sum(l1) <> 0.V by A1;
B3: Sum(l1) = -Sum(l2) by A3,A5,RLVECT_1:6;
B4: -Sum(l2) in Lin(A2) by ZMODUL01:38,ZMODUL02:64;
B5: Sum(l1) in Lin(A1) by ZMODUL02:64;
assume Lin(A1) /\ Lin(A2) = (0).V;
hence contradiction by B2,B5,ZMODUL02:66,B3,B4,ZMODUL01:94;
end;
suppose Carrier(l2) <> {}; then
B2: Sum(l2) <> 0.V by A1;
B3: Sum(l2) = -Sum(l1) by A3,A5,RLVECT_1:6;
B4: -Sum(l1) in Lin(A1) by ZMODUL01:38,ZMODUL02:64;
B5: Sum(l2) in Lin(A2) by ZMODUL02:64;
assume Lin(A1) /\ Lin(A2) = (0).V;
hence contradiction by B2,B5,ZMODUL02:66,B3,B4,ZMODUL01:94;
end;
end;
ThLin7:
for V being Z_Module, A being linearly-independent Subset of V
holds A is Basis of Lin(A)
proof
let V be Z_Module, A be linearly-independent Subset of V;
reconsider AA = A as Subset of Lin(A) by ThLin4;
(Omega).Lin(A) = Lin(AA) by ZMODUL03:20;
hence thesis by VECTSP_7:def 3,ZMODUL03:16;
end;
theorem ThLin8:
for V being Z_Module, W being free Subspace of V,
I being Subset of V, v being Vector of V
st I is linearly-independent & Lin(I) = (Omega).W & v in I holds
(Omega).W = Lin(I \ {v}) + Lin{v} & Lin(I \ {v}) /\ Lin{v} = (0).V &
Lin(I \ {v}) is free & Lin{v} is free & v <> 0.V
proof
let V be Z_Module, W be free Subspace of V, I be Subset of V,
v be Vector of V such that
A1: I is linearly-independent & Lin(I) = (Omega).W & v in I;
A2: (I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A1,ZFMISC_1:40;
A3: I \ {v} is linearly-independent by A1,ZMODUL02:56,XBOOLE_1:36;
A4: v is non torsion by A1,ThLIV1;
Lin(I \ {v}) /\ Lin{v} = (0).V
proof
assume Lin(I \ {v}) /\ Lin{v} <> (0).V;
then consider x be Vector of V such that
B2: x in Lin(I \ {v}) /\ Lin{v} & x <> 0.V by ZMODUL04:24;
x in Lin(I \ {v}) by B2,ZMODUL01:94;
then consider lx1 be Linear_Combination of I \ {v} such that
B3: x = Sum(lx1) by ZMODUL02:64;
B4: Carrier(lx1) <> {} by B2,B3,ZMODUL02:23;
reconsider llx1 = lx1 as Linear_Combination of I
by XBOOLE_1:36,ZMODUL02:10;
x in Lin{v} by B2,ZMODUL01:94;
then consider lx2 be Linear_Combination of {v} such that
B5: -x = Sum(lx2) by ZMODUL01:38,ZMODUL02:64;
reconsider llx2 = lx2 as Linear_Combination of I
by A1,ZFMISC_1:31,ZMODUL02:10;
B6: Carrier(lx1) c= I \ {v} by VECTSP_6:def 4;
Carrier(lx2) c= {v} by VECTSP_6:def 4;
then Carrier(lx1) misses Carrier(lx2) by B6,XBOOLE_1:64,XBOOLE_1:79;
then Carrier(lx1) /\ Carrier(lx2) = {} by XBOOLE_0:def 7;
then B7: Carrier(llx1 + llx2) = Carrier(llx1) \/ Carrier(llx2)
by ZMODUL04:25;
B8: Sum(llx1) + Sum(llx2) = 0.V by B3,B5,RLVECT_1:5;
reconsider llx = llx1 + llx2 as Linear_Combination of I
by ZMODUL02:27;
Sum(llx) = 0.V by B8,ZMODUL02:52;
hence contradiction by A1,B4,B7;
end;
hence thesis by A2,A3,A4,A1,ZMODUL02:72,ThnTV4;
end;
LmGCD1:
for i1, i2 being Integer st i1,i2 are_coprime
holds ex j1, j2 being Element of INT.Ring st i1*j1 + i2*j2 = 1
proof
let i1, i2 be Integer such that
A1: i1,i2 are_coprime;
A2: |.i1.| gcd |.i2.| = i1 gcd i2 by INT_2:34
.= 1 by A1,INT_2:def 3;
reconsider n1 = |.i1.|, n2 = |.i2.| as Nat;
consider jj1, jj2 be Integer such that
A3: jj1*n1 + jj2*n2 = 1 by A2,EULER_1:10,INT_2:def 3;
reconsider jj1, jj2 as Element of INT.Ring by INT_1:def 2;
per cases;
suppose i1 >= 0 & i2 >= 0;
then B1: |.i1.| = i1 & |.i2.| = i2 by ABSVALUE:def 1;
take jj1,jj2;
thus thesis by B1,A3;
end;
suppose i1 >= 0 & i2 < 0;
then B1: |.i1.| = i1 & |.i2.| = -i2 by ABSVALUE:def 1;
take jj1,-jj2;
thus thesis by B1,A3;
end;
suppose i1 < 0 & i2 >= 0;
then B1: |.i1.| = -i1 & |.i2.| = i2 by ABSVALUE:def 1;
take -jj1,jj2;
thus thesis by B1,A3;
end;
suppose i1 < 0 & i2 < 0;
then B1: |.i1.| = -i1 & |.i2.| = -i2 by ABSVALUE:def 1;
take -jj1,-jj2;
thus thesis by B1,A3;
end;
end;
LmGCD:
for i1, i2 being Element of INT.Ring st i1,i2 are_coprime
holds ex j1, j2 being Element of INT.Ring st i1*j1 + i2*j2 = 1
proof
let i1, i2 be Element of INT.Ring;
assume
A1: i1,i2 are_coprime;
reconsider ii1 = i1, ii2 = i2 as Integer;
consider j1, j2 being Element of INT.Ring such that
T1: ii1*j1 + ii2*j2 = 1 by LmGCD1,A1;
i1*j1 + i2*j2 = 1 by T1;
hence thesis;
end;
theorem
for V being Z_Module, W being free Subspace of V holds
ex A being Subset of V st A is Subset of W &
A is linearly-independent & Lin(A) = (Omega).W
proof
let V be Z_Module, W be free Subspace of V;
consider AW be Subset of W such that
a1: AW is base by VECTSP_7:def 4;
AW c= the carrier of W & the carrier of W c= the carrier of V
by VECTSP_4:def 2;
then AW c= the carrier of V;
then reconsider A = AW as Subset of V;
Lin(A) = (Omega).W by a1,ZMODUL03:20;
hence thesis by a1,ZMODUL03:15;
end;
theorem LmFree2:
for V being Z_Module, W being finite-rank free Subspace of V holds
ex A being finite Subset of V st A is finite Subset of W &
A is linearly-independent & Lin(A) = (Omega).W & card(A) = rank(W)
proof
let V be Z_Module, W be finite-rank free Subspace of V;
consider AW be finite Subset of W such that
A1: AW is Basis of W by ZMODUL03:def 3;
A2: AW is linearly-independent & Lin(AW) = (Omega).W by A1,VECTSP_7:def 3;
AW c= the carrier of W & the carrier of W c= the carrier of V
by VECTSP_4:def 2;
then AW c= the carrier of V;
then reconsider A = AW as finite Subset of V;
A3: A is linearly-independent by ZMODUL03:15,A1,VECTSP_7:def 3;
A4: rank(W) = card(A) by A1,ZMODUL03:def 5;
Lin(A) = (Omega).W by A2,ZMODUL03:20;
hence thesis by A3,A4;
end;
theorem LmSumMod1:
for V being torsion-free Z_Module, v1, v2 being Vector of V
st v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V
ex u being Vector of V st u <> 0.V & Lin{v1} /\ Lin{v2} = Lin{u}
proof
let V be torsion-free Z_Module, v1, v2 be Vector of V such that
A1: v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V;
consider x be Vector of V such that
A2: x in Lin{v1} /\ Lin{v2} & x <> 0.V by A1,ZMODUL04:24;
x in Lin{v1} by A2,ZMODUL01:94;
then consider ii1 be Element of INT.Ring such that
A4: x = ii1*v1 by ThLin1;
x in Lin{v2} by A2,ZMODUL01:94;
then consider ii2 be Element of INT.Ring such that
A6: x = ii2*v2 by ThLin1;
A8: ii1 <> 0 by A2,A4,ZMODUL01:1;
consider i1, i2 be Integer such that
A10: ii1 = (ii1 gcd ii2)*i1 & ii2 = (ii1 gcd ii2)*i2 &
i1,i2 are_coprime by A8,INT_2:23;
reconsider I1 = i1, I2 = i2 as Element of INT.Ring by INT_1:def 2;
AX1:ii1 gcd ii2 <> 0 by A8,INT_2:5;
reconsider igi = ii1 gcd ii2 as Element of INT.Ring by INT_1:def 2;
a10:ii1 = igi*I1 & ii2 = igi*I2 by A10; then
A11: x = igi*(I1*v1) by VECTSP_1:def 16,A4;
x = igi * (I2*v2) by VECTSP_1:def 16,A6,a10;
then A12: I1*v1 = I2*v2 by A11,AX1,ZMODUL01:10;
I1*v1 in Lin{v1} & I2*v2 in Lin{v2} by ZMODUL01:37,ThLin2;
then A13: I1*v1 in Lin{v1} /\ Lin{v2} by A12,ZMODUL01:94;
A14: for y being Vector of V st y in Lin{I1*v1} holds
y in Lin{v1} /\ Lin{v2}
proof
let y be Vector of V such that
B1: y in Lin{I1*v1};
consider iy be Element of INT.Ring such that
B2: y = iy*(I1*v1) by B1,ThLin1;
thus y in Lin{v1} /\ Lin{v2} by A13,B2,ZMODUL01:37;
end;
A16: Lin{I1*v1} = Lin{v1} /\ Lin{v2}
proof
assume Lin{I1*v1} <> Lin{v1} /\ Lin{v2};
then consider y be Vector of V such that
B2: y in Lin{v1} /\ Lin{v2}
& not y in Lin{I1*v1} by A14,ZMODUL01:46;
y in Lin{v1} by B2,ZMODUL01:94;
then consider iy1 be Element of INT.Ring such that
B4: y = iy1*v1 by ThLin1;
consider J1, Jy1 be Integer such that
B5: i1 gcd iy1 = J1*i1 + Jy1*iy1 by NAT_D:68;
reconsider j1 = J1, jy1 = Jy1 as Element of INT.Ring by INT_1:def 2;
reconsider iyi = i1 gcd iy1 as Element of INT.Ring by INT_1:def 2;
iyi = j1*I1 + jy1*iy1 by B5; then
B6: iyi*v1 = (j1*I1)*v1 + (jy1*iy1)*v1 by VECTSP_1:def 15
.= j1*(I1*v1) + (jy1*iy1)*v1 by VECTSP_1:def 16
.= j1*(I1*v1) + jy1*y by B4,VECTSP_1:def 16;
B7: j1*(I1*v1) in Lin{v1} /\ Lin{v2} by A13,ZMODUL01:37;
jy1*y in Lin{v1} /\ Lin{v2} by B2,ZMODUL01:37;
then B8: iyi*v1 in Lin{v1} /\ Lin{v2} by B6,B7,ZMODUL01:36;
iyi*v1 in Lin{v2} by B8,ZMODUL01:94;
then consider iiy2 be Element of INT.Ring such that
B10: iyi*v1 = iiy2*v2 by ThLin1;
(i1 gcd iy1) divides i1 by INT_2:def 2;
then consider I3 be Integer such that
B11: i1 = (i1 gcd iy1)*I3 by INT_1:def 3;
reconsider i3 = I3 as Element of INT.Ring by INT_1:def 2;
i1 = iyi*i3 by B11; then
B12: I1*v1 = i3*(iyi*v1) by VECTSP_1:def 16
.= (i3*iiy2)*v2 by VECTSP_1:def 16,B10;
per cases;
suppose i3*iiy2 = i2; then
C3: i3 divides i2 by INT_1:def 3;
C2: i3 divides i1 by B11,INT_1:def 3;
per cases;
suppose i1 gcd i2 = 1;
then i3 = 1 or i3 = -1 by INT_2:13,C3,C2,INT_2:22;
then i1 divides iy1 or -i1 divides iy1 by INT_2:def 2,B11;
then consider iy3 be Integer such that
D2: iy1 = i1 * iy3 by INT_1:def 3,INT_2:10;
reconsider Iy3 = iy3 as Element of INT.Ring by INT_1:def 2;
iy1 = I1 * Iy3 by D2; then
y = Iy3 * (I1*v1) by VECTSP_1:def 16,B4;
hence contradiction by B2,ZMODUL01:37,ThLin2;
end;
suppose i1 gcd i2 <> 1;
hence contradiction by A10,INT_2:def 3;
end;
end;
suppose i3*iiy2 <> i2;
then C2: i2 - i3*iiy2 <> 0;
0.V = I2*v2 - (i3*iiy2)*v2 by RLVECT_1:15,A12,B12
.= (I2-i3*iiy2)*v2 by ZMODUL01:9;
then v2 is torsion by C2;
hence contradiction by A1,defTorsionFree;
end;
end;
i1 <> 0.INT.Ring by A10,A2,A4,ZMODUL01:1;
hence thesis by A16,A1,ZMODUL01:def 7;
end;
theorem LmSumMod2:
for V being torsion-free Z_Module, v1, v2 being Vector of V
st v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V
ex u being Vector of V st u <> 0.V & Lin{v1} + Lin{v2} = Lin{u}
proof
let V be torsion-free Z_Module, v1, v2 be Vector of V such that
A1: v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V;
consider x be Vector of V such that
A2: x <> 0.V & Lin{v1} /\ Lin{v2} = Lin{x} by A1,LmSumMod1;
A3: x in Lin{x} by ZMODUL02:65,ZFMISC_1:31;
then x in Lin{v1} by A2,ZMODUL01:94;
then consider i1 be Element of INT.Ring such that
A4: x = i1*v1 by ThLin1;
x in Lin{v2} by A2,A3,ZMODUL01:94;
then consider i2 be Element of INT.Ring such that
A5: x = i2*v2 by ThLin1;
|.i1.| gcd |.i2.| = 1
proof
set n1 = |.i1.|;
set n2 = |.i2.|;
assume ASB: n1 gcd n2 <> 1;
per cases;
suppose n1 gcd n2 = 0;
then n1 = 0 & n2 = 0 by INT_2:5;
hence contradiction by ABSVALUE:2,A2,A4,ZMODUL01:1;
end;
suppose n1 gcd n2 <> 0;
then n1 gcd n2 > 1 by ASB,NAT_1:25;
then C1: i1 gcd i2 > 1 by INT_2:34;
(i1 gcd i2) divides i1 by INT_2:def 2;
then consider k1 be Integer such that
C2: i1 = (i1 gcd i2)*k1 by INT_1:def 3;
(i1 gcd i2) divides i2 by INT_2:def 2;
then consider k2 be Integer such that
C3: i2 = (i1 gcd i2)*k2 by INT_1:def 3;
reconsider K1 = k1, K2 = k2 as Element of INT.Ring by INT_1:def 2;
reconsider igi = i1 gcd i2 as Element of INT.Ring by INT_1:def 2;
c2: i1 = igi*K1 & i2 = igi*K2 by C2,C3; then
C4: igi*(K1*v1) = (igi*K2)*v2 by VECTSP_1:def 16,A4,A5
.= igi*(K2*v2) by VECTSP_1:def 16;
C5: K1*v1 = K2*v2 by ZMODUL01:10,C1,C4;
C6: K1*v1 in Lin{v1} by ZMODUL01:37,ThLin2;
K2*v2 in Lin{v2} by ZMODUL01:37,ThLin2;
then consider ikv be Element of INT.Ring such that
C8: K1*v1 = ikv*x by ThLin1,A2,C5,C6,ZMODUL01:94;
x = igi*(K1*v1) by VECTSP_1:def 16,A4,c2
.= (igi*ikv)*x by VECTSP_1:def 16,C8;
then C9: 0.V = (igi*ikv)*x - x by RLVECT_1:15
.= (igi*ikv)*x - 1.INT.Ring*x
.= (igi*ikv - 1.INT.Ring)*x by ZMODUL01:9;
igi*ikv - 1.INT.Ring <> 0.INT.Ring by C1,INT_1:9;
hence contradiction by A2,C9,ZMODUL01:def 7;
end;
end;
then i1 gcd i2 = 1 by INT_2:34;
then consider j1, j2 be Element of INT.Ring such that
A7: i1*j1 + i2*j2 = 1 by LmGCD,INT_2:def 3;
reconsider J1 = j1, J2 = j2 as Element of INT.Ring;
a7: i1*J1 + i2*J2 = 1.INT.Ring by A7;
reconsider u = J1*v2 + J2*v1 as Vector of V;
A8: u in Lin{u} by ZMODUL02:65,ZFMISC_1:31;
B1: i1*u = i1*(J1*v2) + i1*(J2*v1) by VECTSP_1:def 14
.= i1*(J1*v2) + (i1*J2)*v1 by VECTSP_1:def 16
.= i1*(J1*v2) + J2*(i1*v1) by VECTSP_1:def 16
.= (i1*J1)*v2 + J2*(i2*v2) by VECTSP_1:def 16,A4,A5
.= (i1*J1)*v2 + (i2*J2)*v2 by VECTSP_1:def 16
.= (i1*J1 + i2*J2)*v2 by VECTSP_1:def 15
.= v2 by a7;
B3: i2*u = i2*(J1*v2) + i2*(J2*v1) by VECTSP_1:def 14
.= (i2*J1)*v2 + i2*(J2*v1) by VECTSP_1:def 16
.= J1*(i2*v2) + i2*(J2*v1) by VECTSP_1:def 16
.= J1*(i2*v2) + (i2*J2)*v1 by VECTSP_1:def 16
.= (i1*J1)*v1 + (i2*J2)*v1 by VECTSP_1:def 16,A4,A5
.= (i1*J1 + i2*J2)*v1 by VECTSP_1:def 15
.= v1 by a7;
Lin{v1} + Lin{v2} = Lin{u}
proof
B5: for vx being Vector of V st vx in Lin{v1} holds vx in Lin{u}
proof
let vx be Vector of V such that
C1: vx in Lin{v1};
consider ivx1 be Element of INT.Ring such that
C2: vx = ivx1*v1 by C1,ThLin1;
vx = (ivx1*i2)*u by VECTSP_1:def 16,B3,C2;
hence thesis by A8,ZMODUL01:37;
end;
B6: for vx being Vector of V st vx in Lin{v2} holds vx in Lin{u}
proof
let vx be Vector of V such that
C1: vx in Lin{v2};
consider ivx2 be Element of INT.Ring such that
C2: vx = ivx2*v2 by C1,ThLin1;
vx = (ivx2*i1)*u by VECTSP_1:def 16,B1,C2;
hence thesis by A8,ZMODUL01:37;
end;
for vx being Vector of V holds vx in Lin{v1}+Lin{v2} iff vx in Lin{u}
proof
let vx be Vector of V;
hereby
assume vx in Lin{v1}+Lin{v2};
then consider vx1, vx2 be Vector of V such that
C2: vx1 in Lin{v1} & vx2 in Lin{v2} & vx = vx1 + vx2 by ZMODUL01:92;
C3: vx1 in Lin{u} by B5,C2;
vx2 in Lin{u} by B6,C2;
hence vx in Lin{u} by C2,C3,ZMODUL01:36;
end;
assume vx in Lin{u};
then consider ivx be Element of INT.Ring such that
C2: vx = ivx*u by ThLin1;
C3: vx = ivx*(J1*v2) + ivx*(J2*v1) by VECTSP_1:def 14,C2
.= (ivx*J1)*v2 + ivx*(J2*v1) by VECTSP_1:def 16
.= (ivx*J1)*v2 + (ivx*J2)*v1 by VECTSP_1:def 16;
v1 in Lin{v1} by ZMODUL02:65,ZFMISC_1:31;
then C4: (ivx*J2)*v1 in Lin{v1} by ZMODUL01:37;
v2 in Lin{v2} by ZMODUL02:65,ZFMISC_1:31;
then (ivx*J1)*v2 in Lin{v2} by ZMODUL01:37;
hence vx in Lin{v1}+Lin{v2} by C3,C4,ZMODUL01:92;
end;
hence thesis by ZMODUL01:46;
end;
hence thesis by A1,B3,ZMODUL01:1;
end;
theorem LmSumMod3:
for V being torsion-free Z_Module, W being finite-rank free Subspace of V,
v, u being Vector of V
st v <> 0.V & u <> 0.V &
W /\ Lin{v} = (0).V & (W + Lin{u}) /\ Lin{v} <> (0).V &
Lin{u} /\ Lin{v} = (0).V
holds ex w1, w2 being Vector of V
st w1 <> 0.V & w2 <> 0.V &
(W + Lin{u}) + Lin{v} = (W + Lin{w1}) + Lin{w2} &
W /\ Lin{w1} <> (0).V & (W + Lin{w1}) /\ Lin{w2} = (0).V &
u in Lin{w1} + Lin{w2} & v in Lin{w1} + Lin{w2} &
w1 in Lin{u} + Lin{v} & w2 in Lin{u} + Lin{v}
proof
let V be torsion-free Z_Module, W be finite-rank free Subspace of V,
v, u be Vector of V such that
A1: v <> 0.V & u <> 0.V and
A2: W /\ Lin{v} = (0).V and
A3: (W + Lin{u}) /\ Lin{v} <> (0).V & Lin{u} /\ Lin{v} = (0).V;
consider x be Vector of V such that
A4: x in (W + Lin{u}) /\ Lin{v} & x <> 0.V by A3,ZMODUL04:24;
x in W + Lin{u} by A4,ZMODUL01:94;
then consider x1, x2 be Vector of V such that
A6: x1 in W & x2 in Lin{u} & x = x1 + x2 by ZMODUL01:92;
A7: x in Lin{v} by A4,ZMODUL01:94;
consider iv be Element of INT.Ring such that
A9: x = iv * v by A7,ThLin1;
A10: iv <> 0 by A4,A9,ZMODUL01:1;
consider iu2 be Element of INT.Ring such that
A11: x2 = iu2 * u by A6,ThLin1;
consider iiv, iiu2 be Integer such that
A13: iv = (iv gcd iu2)*iiv & iu2 = (iv gcd iu2)*iiu2 &
iiv,iiu2 are_coprime by A10,INT_2:23;
reconsider iiv, iiu2 as Element of INT.Ring by INT_1:def 2;
consider Jv, Ju2 being Element of INT.Ring such that
A14: iiv*Jv + iiu2*Ju2 = 1 by A13,LmGCD;
reconsider jv = Jv, ju2 = Ju2 as Element of INT.Ring;
a14: iiv*jv + iiu2*ju2 = 1.INT.Ring by A14;
A15: x - x2 = x1 + (x2 - x2) by RLVECT_1:def 3,A6
.= x1 + 0.V by RLVECT_1:15
.= x1;
set w1 = iiv*v - iiu2*u;
set w2 = jv*u + ju2*v;
A16: w1 <> 0.V
proof
assume w1 = 0.V;
then B1: iiv*v = iiu2*u by RLVECT_1:21;
B2: iiv*v in Lin{v} by ZMODUL01:37,ThLin2;
iiv*v in Lin{u} by B1,ZMODUL01:37,ThLin2;
then B3: iiv*v in Lin{u} /\ Lin{v} by B2,ZMODUL01:94;
iiv <> 0.INT.Ring by A13,A4,A9,ZMODUL01:1;
hence contradiction by A3,B3,ZMODUL02:66,A1,ZMODUL01:def 7;
end;
reconsider igu = iv gcd iu2 as Element of INT.Ring by INT_1:def 2;
a13: iv = igu*iiv & iu2 = igu*iiu2 by A13;
AX1: igu*w1 in W
proof
igu*w1 = igu*(iiv*v) - igu*(iiu2*u) by ZMODUL01:8
.= (igu*iiv)*v - igu*(iiu2*u) by VECTSP_1:def 16
.= iv*v - iu2*u by a13,VECTSP_1:def 16;
hence igu*w1 in W by A15,A6,A9,A11;
end;
AX2: (iv gcd iu2) <> 0.INT.Ring by A10,INT_2:5;
A17: W /\ Lin{w1} <> (0).V
proof
igu*w1 in Lin{w1} by ZMODUL01:37,ThLin2;
then igu*w1 in W /\ Lin{w1} by AX1,ZMODUL01:94;
hence thesis by ZMODUL02:66,A16,AX2,ZMODUL01:def 7;
end;
A18: u = iiv*w2 - ju2*w1
proof
thus iiv*w2 - ju2*w1 = iiv*(jv*u) + iiv*(ju2*v) - ju2*(iiv*v - iiu2*u)
by VECTSP_1:def 14
.= (iiv*jv)*u + iiv*(ju2*v) - ju2*(iiv*v - iiu2*u) by VECTSP_1:def 16
.= (iiv*jv)*u + (iiv*ju2)*v - ju2*(iiv*v - iiu2*u) by VECTSP_1:def 16
.= (iiv*ju2)*v + (iiv*jv)*u - (ju2*(iiv*v) - ju2*(iiu2*u))
by ZMODUL01:8
.= ((iiv*ju2)*v + (iiv*jv)*u - ju2*(iiv*v)) + ju2*(iiu2*u)
by RLVECT_1:29
.= ((iiv*jv)*u + (iiv*ju2)*v - ju2*(iiv*v)) + (ju2*iiu2)*u
by VECTSP_1:def 16
.= ((iiv*jv)*u + ((iiv*ju2)*v - ju2*(iiv*v))) + (ju2*iiu2)*u
by RLVECT_1:28
.= ((iiv*jv)*u + ((iiv*ju2)*v - (ju2*iiv)*v)) + (ju2*iiu2)*u
by VECTSP_1:def 16
.= ((iiv*jv)*u + 0.V) + (ju2*iiu2)*u by RLVECT_1:15
.= (iiv*jv + iiu2*ju2)*u by VECTSP_1:def 15
.= u by a14;
end;
A19: v = jv*w1 + iiu2*w2
proof
thus jv*w1 + iiu2*w2 = jv*(iiv*v) - jv*(iiu2*u) + iiu2*(jv*u + ju2*v)
by ZMODUL01:8
.= (jv*iiv)*v - jv*(iiu2*u) + iiu2*(jv*u + ju2*v) by VECTSP_1:def 16
.= (jv*iiv)*v + iiu2*(jv*u + ju2*v) - jv*(iiu2*u)
by RLVECT_1:def 3
.= (jv*iiv)*v + (iiu2*(jv*u + ju2*v) - jv*(iiu2*u)) by RLVECT_1:def 3
.= (jv*iiv)*v + (iiu2*(ju2*v + jv*u) - (jv*iiu2)*u) by VECTSP_1:def 16
.= (jv*iiv)*v + (iiu2*(ju2*v) + iiu2*(jv*u) - (jv*iiu2)*u)
by VECTSP_1:def 14
.= (iiv*jv)*v + (iiu2*(ju2*v) + (iiu2*(jv*u) - (jv*iiu2)*u))
by RLVECT_1:28
.= (iiv*jv)*v + (iiu2*(ju2*v) + ((iiu2*jv)*u - (iiu2*jv)*u))
by VECTSP_1:def 16
.= (iiv*jv)*v + (iiu2*(ju2*v) + 0.V) by RLVECT_1:15
.= (iiv*jv)*v + (iiu2*ju2)*v by VECTSP_1:def 16
.= (iiv*jv + iiu2*ju2)*v by VECTSP_1:def 15
.= v by a14;
end;
A20: u in Lin{w1} + Lin{w2}
proof
ju2*w1 in Lin{w1} by ZMODUL01:37,ThLin2;
then B1: -ju2*w1 in Lin{w1} by ZMODUL01:38;
iiv*w2 in Lin{w2} by ZMODUL01:37,ThLin2;
hence thesis by A18,B1,ZMODUL01:92;
end;
A21: v in Lin{w1} + Lin{w2}
proof
B1: jv*w1 in Lin{w1} by ZMODUL01:37,ThLin2;
iiu2*w2 in Lin{w2} by ZMODUL01:37,ThLin2;
hence thesis by A19,B1,ZMODUL01:92;
end;
A22: w1 in Lin{u} + Lin{v}
proof
iiu2*u in Lin{u} by ZMODUL01:37,ThLin2;
then B1: -iiu2*u in Lin{u} by ZMODUL01:38;
iiv*v in Lin{v} by ZMODUL01:37,ThLin2;
hence thesis by B1,ZMODUL01:92;
end;
A23: w2 in Lin{u} + Lin{v}
proof
B1: jv*u in Lin{u} by ZMODUL01:37,ThLin2;
ju2*v in Lin{v} by ZMODUL01:37,ThLin2;
hence thesis by B1,ZMODUL01:92;
end;
A24: for x being object holds
x in (W + Lin{u}) + Lin{v} implies x in (W + Lin{w1}) + Lin{w2}
proof
let x be object;
assume x in (W + Lin{u}) + Lin{v};
then consider xx, x3 be Vector of V such that
B1: xx in W + Lin{u} & x3 in Lin{v} & x = xx + x3 by ZMODUL01:92;
consider x1, x2 be Vector of V such that
B2: x1 in W & x2 in Lin{u} & xx = x1 + x2 by B1,ZMODUL01:92;
consider ix2 be Element of INT.Ring such that
B3: x2 = ix2*u by B2,ThLin1;
consider ix3 be Element of INT.Ring such that
B4: x3 = ix3*v by B1,ThLin1;
B5: x2 in Lin{w1} + Lin{w2} by A20,B3,ZMODUL01:37;
x3 in Lin{w1} + Lin{w2} by A21,B4,ZMODUL01:37;
then x2 + x3 in Lin{w1} + Lin{w2} by B5,ZMODUL01:36;
then x1 + (x2 + x3) in W + (Lin{w1} + Lin{w2}) by B2,ZMODUL01:92;
then xx + x3 in W + (Lin{w1} + Lin{w2}) by B2,RLVECT_1:def 3;
hence x in (W + Lin{w1}) + Lin{w2} by B1,ZMODUL01:96;
end;
for x being object holds
x in (W + Lin{w1}) + Lin{w2} implies x in (W + Lin{u}) + Lin{v}
proof
let x be object;
assume x in (W + Lin{w1}) + Lin{w2};
then consider xx, x3 be Vector of V such that
B1: xx in (W + Lin{w1}) & x3 in Lin{w2} & x = xx + x3 by ZMODUL01:92;
consider x1, x2 be Vector of V such that
B2: x1 in W & x2 in Lin{w1} & xx = x1 + x2 by B1,ZMODUL01:92;
consider ix2 be Element of INT.Ring such that
B3: x2 = ix2*w1 by B2,ThLin1;
consider ix3 be Element of INT.Ring such that
B4: x3 = ix3*w2 by B1,ThLin1;
B5: x2 in Lin{u} + Lin{v} by A22,B3,ZMODUL01:37;
x3 in Lin{u} + Lin{v} by A23,B4,ZMODUL01:37;
then x2 + x3 in Lin{u} + Lin{v} by B5,ZMODUL01:36;
then x1 + (x2 + x3) in W + (Lin{u} + Lin{v}) by B2,ZMODUL01:92;
then xx + x3 in W + (Lin{u} + Lin{v}) by B2,RLVECT_1:def 3;
hence x in (W + Lin{u}) + Lin{v} by B1,ZMODUL01:96;
end;
then for x being Vector of V holds
x in (W + Lin{u}) + Lin{v} iff x in (W + Lin{w1}) + Lin{w2} by A24;
then A25: (W + Lin{u}) + Lin{v} = (W + Lin{w1}) + Lin{w2} by ZMODUL01:46;
A26: w2 <> 0.V
proof
assume B0: w2 = 0.V;
then B1: ju2*v = -jv*u by RLVECT_1:6;
B2: ju2*v in Lin{v} by ZMODUL01:37,ThLin2;
jv*u in Lin{u} by ZMODUL01:37,ThLin2;
then ju2*v in Lin{u} by B1,ZMODUL01:38;
then B3: ju2*v in Lin{u} /\ Lin{v} by B2,ZMODUL01:94;
ju2 <> 0.INT.Ring
proof
assume C1: ju2 = 0.INT.Ring;
then jv*u + 0.V = 0.V by B0,ZMODUL01:1;
then jv = 0.INT.Ring by A1,ZMODUL01:def 7;
hence contradiction by A14,C1;
end;
hence contradiction by A3,B3,ZMODUL02:66,A1,ZMODUL01:def 7;
end;
(W + Lin{w1}) /\ Lin{w2} = (0).V
proof
assume (W + Lin{w1}) /\ Lin{w2} <> (0).V;
then consider wx be Vector of V such that
B2: wx in (W + Lin{w1}) /\ Lin{w2} & wx <> 0.V by ZMODUL04:24;
wx in W + Lin{w1} by B2,ZMODUL01:94;
then consider wx1, wx2 be Vector of V such that
B3: wx1 in W & wx2 in Lin{w1} & wx = wx1 + wx2 by ZMODUL01:92;
consider iwx1 be Element of INT.Ring such that
B4: wx2 = iwx1 * w1 by B3,ThLin1;
reconsider igu = iv gcd iu2 as Element of INT.Ring by INT_1:def 2;
B5: igu*wx in W
proof
C1: igu*wx = igu*wx1 + igu*wx2 by VECTSP_1:def 14,B3
.= igu*wx1 + (igu*iwx1)*w1 by VECTSP_1:def 16,B4
.= igu*wx1 + iwx1 * (igu*w1) by VECTSP_1:def 16;
C2: igu*wx1 in W by B3,ZMODUL01:37;
iwx1 * (igu*w1) in W by AX1,ZMODUL01:37;
hence thesis by C1,C2,ZMODUL01:36;
end;
wx in Lin{w2} by B2,ZMODUL01:94;
then consider iwx2 be Element of INT.Ring such that
B6: wx = iwx2*w2 by ThLin1;
B7: iwx2 <> 0 by B2,B6,ZMODUL01:1;
ex wiu1, wiu2 being Vector of V
st iu2*w2 = wiu1 + wiu2 & wiu1 in W & wiu2 = igu*v
proof
C1: iu2*w2 = iu2*(jv*u) + iu2*(ju2*v) by VECTSP_1:def 14
.= (iu2*jv)*u + iu2*(ju2*v) by VECTSP_1:def 16
.= (jv*iu2)*u + (iu2*ju2)*v by VECTSP_1:def 16
.= jv*(iu2*u) + (iu2*ju2)*v by VECTSP_1:def 16;
reconsider wiviu = iv*v - iu2*u as Vector of W by A15,A6,A9,A11;
C2: wiviu in W;
reconsider wiviu as Vector of V;
iv*v - wiviu = (iv*v - iv*v) + iu2*u by RLVECT_1:29
.= 0.V + iu2*u by RLVECT_1:15
.= iu2*u;
then C3: iu2*w2 = jv*(iv*v) - jv*wiviu + (iu2*ju2)*v by ZMODUL01:8,C1
.= jv*(iv*v) + (iu2*ju2)*v - jv*wiviu by RLVECT_1:def 3
.= (jv*iv)*v + (iu2*ju2)*v - jv*wiviu by VECTSP_1:def 16
.= (jv*iv + iu2*ju2)*v - jv*wiviu by VECTSP_1:def 15
.= (igu*(iiv*jv + iiu2*ju2))*v - jv*wiviu by A13
.= (-jv*wiviu) + igu*v by A14;
C4: jv*wiviu in W by C2,ZMODUL01:37;
take -jv*wiviu, igu*v;
thus thesis by C3,C4,ZMODUL01:38;
end;
then consider wiu1, wiu2 be Vector of V such that
B8: iu2*w2 = wiu1 + wiu2 & wiu1 in W & wiu2 = igu*v;
B9: iu2*wx = (iu2*iwx2)*w2 by VECTSP_1:def 16,B6
.= iwx2*(iu2*w2) by VECTSP_1:def 16
.= iwx2*wiu1 + iwx2*(igu*v) by VECTSP_1:def 14,B8
.= iwx2*wiu1 + (iwx2*igu)*v by VECTSP_1:def 16;
iu2*wx = iiu2*(igu*wx) by VECTSP_1:def 16,a13;
then B10: iu2*wx in W by B5,ZMODUL01:37;
iwx2*wiu1 in W by B8,ZMODUL01:37;
then B11: iu2*wx - iwx2*wiu1 in W by B10,ZMODUL01:39;
B12: iu2*wx - iwx2*wiu1 = iwx2*wiu1 - iwx2*wiu1 + (iwx2*igu)*v
by RLVECT_1:def 3,B9
.= 0.V + (iwx2*igu)*v by RLVECT_1:15
.= (iwx2*igu)*v;
(iwx2*igu)*v in Lin{v} by ZMODUL01:37,ThLin2;
then (iwx2*igu)*v in W /\ Lin{v} by B12,ZMODUL01:94,B11;
hence contradiction by A2,ZMODUL02:66,A1,ZMODUL01:def 7,AX2,B7;
end;
hence thesis by A16,A17,A20,A21,A22,A23,A25,A26;
end;
theorem LmSumModX:
for V being torsion-free Z_Module, W being finite-rank free Subspace of V,
v being Vector of V
st v <> 0.V & W /\ Lin{v} <> (0).V holds
W + Lin{v} is free
proof
let V be torsion-free Z_Module;
defpred P[Nat] means for W being finite-rank free Subspace of V,
v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V
& rank(W) = $1 + 1 holds W + Lin{v} is free;
A1: P[0]
proof
let W be finite-rank free Subspace of V, v be Vector of V such that
B1: v <> 0.V & W /\ Lin{v} <> (0).V and
B2: rank(W) = 0 + 1;
ex x being Vector of V st x <> 0.V & W + Lin{v} = Lin{x}
proof
consider w be Vector of W such that
C1: w <> 0.W & (Omega).W = Lin{w} by ZMODUL05:5,B2;
reconsider wv = w as Vector of V by ZMODUL01:25;
C2: (Omega).W = Lin{wv} by C1,ZMODUL03:20;
C3: (Omega).Lin{v} = Lin{v};
then C4: W + Lin{v} = Lin{wv} + Lin{v} by C2,ZMODUL04:22;
C5: Lin{wv} /\ Lin{v} <> (0).V by B1,C2,C3,ZMODUL04:23;
wv <> 0.V by C1,ZMODUL01:26;
hence thesis by B1,C4,C5,LmSumMod2;
end;
then consider x being Vector of V such that
B3: x <> 0.V & W + Lin{v} = Lin{x};
thus thesis by B3;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let W be finite-rank free Subspace of V, v be Vector of V such that
B2: v <> 0.V & W /\ Lin{v} <> (0).V & rank(W) = (n+1) + 1;
set I = the Basis of W;
B3: card(I) = n+2 by B2,ZMODUL03:def 5;
then I <> {}(the carrier of W);
then consider w be object such that
B4: w in I by XBOOLE_0:7;
reconsider w as Vector of W by B4;
B5: W is_the_direct_sum_of Lin(I \ {w}),Lin{w} by B4,ZMODUL04:33;
I c= the carrier of W & the carrier of W c= the carrier of V
by VECTSP_4:def 2;
then I c= the carrier of V;
then reconsider IV = I as finite Subset of V;
reconsider wv = w as Vector of V by ZMODUL01:25;
B6: Lin(I \ {w}) = Lin(IV \ {wv}) by ZMODUL03:20;
B7: Lin{w} = Lin{wv} by ZMODUL03:20;
then reconsider WLinIw = Lin(I \ {w}), WLinw = Lin{w}
as Subspace of Lin(IV \ {wv}) + Lin{wv} by B6,ZMODUL01:97;
B8: Lin(IV \ {wv}) /\ Lin{wv} = (0).V
proof
C1: for x being object holds
x in Lin(IV \ {wv}) /\ Lin{wv} implies x in (0).V
proof
let x be object;
assume D1: x in Lin(IV \ {wv}) /\ Lin{wv};
D2: Lin(I \ {w}) /\ Lin{w} = (0).V by ZMODUL01:51,B5;
x in Lin(I \ {w}) & x in Lin{w} by B6,B7,D1,ZMODUL01:94;
hence thesis by D2,ZMODUL01:94;
end;
for x being object holds
x in (0).V implies x in Lin(IV \ {wv}) /\ Lin{wv}
proof
let x be object;
assume x in (0).V;
then x = 0.V by ZMODUL02:66;
hence thesis by ZMODUL01:33;
end;
then for x being Vector of V holds
x in Lin(IV \ {wv}) /\ Lin{wv} iff x in (0).V by C1;
hence thesis by ZMODUL01:46;
end;
I is linearly-independent by VECTSP_7:def 3;
then I \ {w} is linearly-independent by XBOOLE_1:36,ZMODUL02:56;
then B9: IV \ {wv} is linearly-independent by ZMODUL03:15;
reconsider LinIw = Lin(IV \ {wv}) as finite-rank free Subspace of V
by B9;
reconsider IVwv = IV \ {wv} as Subset of Lin(IV \ {wv}) by ThLin4;
(Omega).Lin(IV \ {wv}) = Lin(IVwv) by ZMODUL03:20;
then B11: IVwv is Basis of LinIw by VECTSP_7:def 3,B9,ZMODUL03:16;
B12: card(I \ {w}) = card(I) - card{w} by B4,ZFMISC_1:31,CARD_2:44
.= (n+2) - 1 by B3,CARD_1:30
.= n+1;
B13: rank(LinIw) = n+1 by B12,B11,ZMODUL03:def 5;
B15: Lin(IV \ {wv}) + Lin{v} is free
proof
per cases;
suppose Lin(IV \ {wv}) /\ Lin{v} = (0).V;
hence thesis by B9,ZMODUL04:31;
end;
suppose Lin(IV \ {wv}) /\ Lin{v} <> (0).V;
hence thesis by B1,B2,B13;
end;
end;
B16: (Lin(IV \ {wv}) + Lin{v}) + Lin{wv} is free
proof
per cases;
suppose (Lin(IV \ {wv}) + Lin{v}) /\ Lin{wv} = (0).V;
hence thesis by B15,ZMODUL04:31;
end;
suppose C1: (Lin(IV \ {wv}) + Lin{v}) /\ Lin{wv} <> (0).V;
I is linearly-independent by VECTSP_7:def 3;
then {w} is linearly-independent by B4,ZFMISC_1:31,ZMODUL02:56;
then {wv} is linearly-independent by ZMODUL03:15;
then C3: wv <> 0.V;
per cases;
suppose Lin{v} /\ Lin{wv} <> (0).V;
then consider wx be Vector of V such that
D1: wx <> 0.V & Lin{v} + Lin{wv} = Lin{wx} by B2,C3,LmSumMod2;
Lin(IV \ {wv}) + Lin{wx} is free
proof
per cases;
suppose Lin(IV \ {wv}) /\ Lin{wx} = (0).V;
hence thesis by B9,ZMODUL04:31;
end;
suppose Lin(IV \ {wv}) /\ Lin{wx} <> (0).V;
hence thesis by B1,B13,D1;
end;
end;
hence thesis by D1,ZMODUL01:96;
end;
suppose Lin{v} /\ Lin{wv} = (0).V;
then consider w1, w2 be Vector of V such that
D2: w1 <> 0.V & w2 <> 0.V &
(LinIw + Lin{v}) + Lin{wv} = (LinIw + Lin{w1}) + Lin{w2} &
LinIw /\ Lin{w1} <> (0).V &
(LinIw + Lin{w1}) /\ Lin{w2} = (0).V &
v in Lin{w1} + Lin{w2} & wv in Lin{w1} + Lin{w2} &
w1 in Lin{v} + Lin{wv} & w2 in Lin{v} + Lin{wv}
by B2,B8,C1,C3,LmSumMod3;
Lin(IV \ {wv}) + Lin{w1} is free by B1,B13,D2;
hence thesis by D2,ZMODUL04:31;
end;
end;
end;
B17: (Omega).W = Lin(IV \ {wv}) + Lin{wv}
proof
for x being object holds
x in (Omega).W iff x in Lin(IV \ {wv}) + Lin{wv}
proof
let x be object;
hereby
assume x in (Omega).W;
then consider xx1, xx2 be Vector of W such that
C2: xx1 in Lin(I \ {w}) & xx2 in Lin{w} & x = xx1 + xx2
by ZMODUL01:92,B5;
reconsider x1 = xx1, x2 = xx2 as Vector of V by ZMODUL01:25;
C3: x1 in Lin(IV \ {wv}) & x2 in Lin{wv} by C2,ZMODUL03:20;
x = x1 + x2 by C2,ZMODUL01:28;
hence x in Lin(IV \ {wv}) + Lin{wv} by C3,ZMODUL01:92;
end;
assume x in Lin(IV \ {wv}) + Lin{wv};
then consider x1, x2 be Vector of V such that
C2: x1 in Lin(IV \ {wv}) & x2 in Lin{wv} & x = x1 + x2
by ZMODUL01:92;
C3: x1 in Lin(I \ {w}) & x2 in Lin{w} by C2,ZMODUL03:20;
Lin(I \ {w}) is Subspace of Lin(I \ {w}) + Lin{w} by ZMODUL01:97;
then C4: x1 in Lin(I \ {w}) + Lin{w} by C3,ZMODUL01:24;
Lin{w} is Subspace of Lin(I \ {w}) + Lin{w} by ZMODUL01:97;
then x2 in Lin(I \ {w}) + Lin{w} by C3,ZMODUL01:24;
then reconsider xx1 = x1, xx2 = x2 as Vector of W by B5,C4;
x = xx1 + xx2 by C2,ZMODUL01:28;
hence x in (Omega).W;
end;
then CX1: for x being Vector of V holds
x in (Omega).W iff x in Lin(IV \ {wv}) + Lin{wv};
reconsider Wo = (Omega).W as Subspace of V by ZMODUL01:42;
Wo = Lin(IV \ {wv}) + Lin{wv} by CX1,ZMODUL01:46;
hence thesis;
end;
reconsider Ws = (Omega).W as strict Subspace of V by ZMODUL01:42;
reconsider Linvs = (Omega).Lin{v} as strict Subspace of V;
(Lin(IV \ {wv}) + Lin{v}) + Lin{wv} = Ws + Linvs by B17,ZMODUL01:96
.= W + Lin{v} by ZMODUL04:22;
hence thesis by B16;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let W be finite-rank free Subspace of V, v be Vector of V such that
A4: v <> 0.V & W /\ Lin{v} <> (0).V;
set rk = rank(W);
rk-1 is Nat
proof
assume not rk - 1 is Nat;
then rk = 0;
then B1: (Omega).W = (0).W by ZMODUL05:1
.= (0).V by ZMODUL01:51;
(Omega).Lin{v} = Lin{v};
then W /\ Lin{v} = (0).V /\ Lin{v} by B1,ZMODUL04:23
.= (0).V by ZMODUL01:107;
hence contradiction by A4;
end;
then reconsider rk1 = rk-1 as Nat;
P[rk1] by A3;
hence thesis by A4;
end;
registration
let V be torsion-free Z_Module;
let v be Vector of V;
let W be finite-rank free Subspace of V;
cluster W + Lin{v} -> free;
coherence
proof
per cases;
suppose B1: v = 0.V;
reconsider Ws = (Omega).W as strict Subspace of V by ZMODUL01:42;
reconsider Lw = (Omega).Lin{v} as strict Subspace of V;
W + Lin{v} = Ws + Lw by ZMODUL04:22
.= Ws + (0).V by B1,ThLin5
.= Ws by ZMODUL01:99;
hence thesis;
end;
suppose A1: v <> 0.V;
per cases;
suppose W /\ Lin{v} = (0).V;
hence thesis by ZMODUL04:31;
end;
suppose W /\ Lin{v} <> (0).V;
hence thesis by A1,LmSumModX;
end;
end;
end;
end;
registration
let V be Z_Module;
let v be Vector of V;
let W be finitely-generated Subspace of V;
cluster W + Lin{v} -> finitely-generated;
coherence
proof
consider A be finite Subset of W such that
A1: (Omega).W = Lin(A) by ZMODUL03:def 4;
A c= the carrier of W & the carrier of W c= the carrier of V
by VECTSP_4:def 2;
then reconsider A as finite Subset of V by XBOOLE_1:1;
reconsider Ws = (Omega).W as strict Subspace of V by ZMODUL01:42;
reconsider Lv = (Omega).Lin{v} as strict Subspace of V;
Ws + Lv = Lin(A) + Lin{v} by A1,ZMODUL03:20
.= Lin(A \/ {v}) by ZMODUL02:72;
hence thesis by ZMODUL04:22;
end;
end;
registration
let V be Z_Module;
let W1, W2 be finitely-generated Subspace of V;
cluster W1 + W2 -> finitely-generated;
coherence
proof
consider A1 be finite Subset of W1 such that
A1: (Omega).W1 = Lin(A1) by ZMODUL03:def 4;
A1 c= the carrier of W1 & the carrier of W1 c= the carrier of V
by VECTSP_4:def 2;
then reconsider A1 as finite Subset of V by XBOOLE_1:1;
consider A2 be finite Subset of W2 such that
A2: (Omega).W2 = Lin(A2) by ZMODUL03:def 4;
A2 c= the carrier of W2 & the carrier of W2 c= the carrier of V
by VECTSP_4:def 2;
then reconsider A2 as finite Subset of V by XBOOLE_1:1;
reconsider W1s = (Omega).W1, W2s = (Omega).W2
as strict Subspace of V by ZMODUL01:42;
A3: W1s = Lin(A1) by A1,ZMODUL03:20;
W1 + W2 = W1s + W2s by ZMODUL04:22
.= Lin(A1) + Lin(A2) by A2,ZMODUL03:20,A3
.= Lin(A1 \/ A2) by ZMODUL02:72;
hence thesis;
end;
end;
theorem LMThSumMod2:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
W1s, W2s being Subspace of W,
W1, W2 being Subspace of V
st W1s = W1 & W2s = W2
holds W1s + W2s = W1 + W2
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V,
W1s, W2s be Subspace of W,
W1, W2 be Subspace of V;
assume AS: W1s = W1 & W2s = W2;
reconsider SWs12 = W1s + W2s as strict Subspace of V by VECTSP_4:26;
for v be Vector of V holds v in SWs12 iff v in W1 + W2
proof
let v be Vector of V;
hereby assume v in SWs12;
then consider x1, x2 be Vector of W such that
B1: x1 in W1s & x2 in W2s & v = x1 + x2 by VECTSP_5:1;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider xx1 = x1 as Vector of V by AS,B1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider xx2 = x2 as Vector of V by AS,B1;
v = xx1 + xx2 by VECTSP_4:13,B1;
hence v in W1 + W2 by VECTSP_5:1,AS,B1;
end;
assume v in W1 + W2;
then consider x1, x2 be Vector of V such that
B1: x1 in W1 & x2 in W2 & v = x1 + x2 by VECTSP_5:1;
the carrier of W1s c= the carrier of W by VECTSP_4:def 2;
then reconsider xx1 = x1 as Vector of W by AS,B1;
the carrier of W2s c= the carrier of W by VECTSP_4:def 2;
then reconsider xx2 = x2 as Vector of W by AS,B1;
v = xx1 + xx2 by VECTSP_4:13,B1;
hence v in SWs12 by AS,B1,VECTSP_5:1;
end;
hence thesis by VECTSP_4:30;
end;
registration
let V be torsion-free Z_Module;
let U1, U2 be finite-rank free Subspace of V;
cluster U1 + U2 -> free;
correctness
proof
defpred P[Nat] means for W1, W2 being finite-rank free Subspace of V
st rank(W1) = $1 holds W1 + W2 is finite-rank free Subspace of V;
A1: P[0]
proof
let W1, W2 be finite-rank free Subspace of V such that
C2: rank(W1) = 0;
reconsider W2s = (Omega).W2 as strict Subspace of V by ZMODUL01:42;
(Omega).W1 = (0).W1 by C2,ZMODUL05:1
.= (0).V by ZMODUL01:51;
then W1 + W2 = (0).V + W2s by ZMODUL04:22
.= (Omega).W2 by ZMODUL01:99;
hence thesis;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A21: P[n];
let W1, W2 be finite-rank free Subspace of V;
assume A22:rank(W1) = n+1;
reconsider W1s = (Omega).W1 as strict Subspace of V by ZMODUL01:42;
reconsider W2s = (Omega).W2 as strict Subspace of V by ZMODUL01:42;
consider I being finite Subset of W1 such that
C30: I is Basis of W1 by ZMODUL03:def 3;
reconsider I as Basis of W1 by C30;
C31: card I <> 0 & card I = n+1 by A22,ZMODUL03:def 5;
then I <> {};
then consider u be object such that
C32: u in I by XBOOLE_0:7;
reconsider u0 = u as Vector of W1 by C32;
I c= the carrier of W1
& the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider u as Vector of V by C32;
D33: I \ {u} c= I & I c= the carrier of W1 by XBOOLE_1:36;
reconsider J = I \ {u} as finite Subset of W1;
card(I) - card{u} = n+1 -1 by C31,CARD_1:30;
then
C34: card(J) = n by C32,ZFMISC_1:31,CARD_2:44;
D34: J is linearly-independent by D33,VECTSP_7:def 3,ZMODUL02:56;
reconsider W10 = Lin(J) as finite-rank free Subspace of V
by ZMODUL01:42;
reconsider W10s = (Omega).W10 as strict Subspace of V;
for x being object st x in J holds x in the carrier of W10
proof
let x be object;
assume x in J;
then x in Lin(J) by ZMODUL02:65;
hence x in the carrier of W10;
end;
then J c= the carrier of W10;
then reconsider J0 = J as linearly-independent Subset of W10
by D34,ZMODUL03:16;
W10s = Lin(J0) & Lin(J0)=Lin(J) by ZMODUL03:20;
then J0 is Basis of W10 by VECTSP_7:def 3;
then rank W10 = n by C34,ZMODUL03:def 5;
then reconsider W3 = W10 + W2 as finite-rank free Subspace of V by A21;
R2: Lin({u0})=Lin({u}) by ZMODUL03:20;
W1 is_the_direct_sum_of Lin(J),Lin{u0} by C32,ZMODUL04:33;
then
Q2: W1s = W10s + Lin{u} by LMThSumMod2,R2;
W1 + W2 = W1s + W2s by ZMODUL04:22
.= Lin{u} + (W10s +W2s) by ZMODUL01:96,Q2
.= Lin{u} + W3 by ZMODUL04:22;
hence thesis;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
set rk = rank(U1);
P[rk] by A3;
hence thesis;
end;
end;
registration
cluster -> free for finitely-generated torsion-free Z_Module;
correctness
proof
let V be finitely-generated torsion-free Z_Module;
consider A be finite Subset of V such that
A2: Lin(A) = (Omega).V by ZMODUL03:def 4;
A3: Lin(A \ {0.V}) is free
proof
defpred P[Nat] means
for B being finite Subset of V st card(B \ {0.V}) = $1 holds
Lin(B \ {0.V}) is free;
B2: P[0]
proof
let B be finite Subset of V such that
C1: card(B \ {0.V}) = 0;
B \ {0.V} = {}(the carrier of V) by C1;
hence thesis;
end;
B3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
C1: P[n];
let B be finite Subset of V such that
C2: card(B \ {0.V}) = n+1;
B \ {0.V} <> {} by C2;
then consider u be object such that
C3: u in B \ {0.V} by XBOOLE_0:7;
reconsider u as Vector of V by C3;
C4: card((B \ {0.V}) \ {u}) = card(B \ {0.V}) - card{u}
by C3,ZFMISC_1:31,CARD_2:44
.= n+1 - 1 by C2,CARD_1:30
.= n;
(B \ {0.V}) \ {u} = B \ ({0.V} \/ {u}) by XBOOLE_1:41
.= (B \ {u}) \ {0.V} by XBOOLE_1:41;
then C5: Lin((B \ {0.V}) \ {u}) is free by C1,C4;
Lin((B \ {0.V}) \ {u}) + Lin{u} = Lin(((B \ {0.V}) \ {u}) \/ {u})
by ZMODUL02:72
.= Lin((B \ {0.V}) \/ {u}) by XBOOLE_1:39
.= Lin(B \ {0.V}) by C3,ZFMISC_1:40;
hence thesis by C5;
end;
B4: for n being Nat holds P[n] from NAT_1:sch 2(B2,B3);
set n = card(A \ {0.V});
P[n] by B4;
hence thesis;
end;
per cases;
suppose B1: 0.V in A;
B2: Lin{0.V} = (0).V by ThLin5;
V is_the_direct_sum_of Lin(A \ {0.V}),Lin{0.V}
proof
Lin(A \ {0.V}) + Lin{0.V} = Lin((A \ {0.V}) \/ {0.V}) by ZMODUL02:72
.= Lin(A \/ {0.V}) by XBOOLE_1:39
.= Lin(A) by B1,ZFMISC_1:40;
hence thesis by A2,B2,ZMODUL01:107;
end;
hence thesis by A3,ZMODUL04:30;
end;
suppose not 0.V in A;
then Lin(A) is free by A3,ZFMISC_1:57;
hence thesis by A2,ZMODUL04:21;
end;
end;
end;
begin :: 2. Rank of finite-rank free $\mathbb{Z}$-module
theorem ThRankDirectSum:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V
st W1 /\ W2 = (0).V holds rank(W1 + W2) = rank W1 + rank W2
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V such that
A1: W1 /\ W2 = (0).V;
set W = W1 + W2;
reconsider WW1 = W1, WW2 = W2 as Subspace of W by ZMODUL01:97;
WW1 /\ WW2 = (0).V by A1,ZMODUL04:2
.= (0).W by ZMODUL01:51;
then A3: W is_the_direct_sum_of WW1,WW2 by ZMODUL04:1;
reconsider WW1, WW2 as finite-rank free Subspace of W;
set I1 = the Basis of WW1;
set I2 = the Basis of WW2;
A4: card(I1) = rank(WW1) by ZMODUL03:def 5;
I1 /\ I2 = {} by A3,ZMODUL04:27;
then A7: card(I1 \/ I2) = card(I1) + card(I2) by CARD_2:40,XBOOLE_0:def 7
.= rank(WW1) + rank(WW2) by ZMODUL03:def 5,A4;
set I = I1 \/ I2;
the carrier of WW1 c= the carrier of W by VECTSP_4:def 2;
then A11: I1 is Subset of W by XBOOLE_1:1;
the carrier of WW2 c= the carrier of W by VECTSP_4:def 2;
then I2 is Subset of W by XBOOLE_1:1;
then reconsider I as Subset of W by A11,XBOOLE_1:8;
Lin(I) = (Omega).W by A3,ZMODUL04:28;
then I1 \/ I2 is Basis of W by VECTSP_7:def 3,A3,ZMODUL04:29;
hence thesis by A7,ZMODUL03:def 5;
end;
theorem
for V being finite-rank free Z_Module,
W1, W2 being finite-rank free Subspace of V
st V is_the_direct_sum_of W1,W2 holds rank V = rank W1 + rank W2
proof
let V be finite-rank free Z_Module,
W1, W2 be finite-rank free Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
rank((Omega).V) = rank(W1) + rank(W2) by ThRankDirectSum,A1;
hence thesis by ZMODUL05:4;
end;
theorem ThISRank1:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V holds
rank(W1 /\ W2) <= rank(W1)
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V;
W1 /\ W2 is Subspace of W1 by ZMODUL01:105;
hence thesis by ZMODUL05:2;
end;
theorem LmRank0a:
for V being torsion-free Z_Module, v being Vector of V st v <> 0.V
holds rank(Lin{v}) = 1
proof
let V be torsion-free Z_Module, v be Vector of V such that
A1: v <> 0.V;
v in Lin{v} by ZMODUL02:65,ZFMISC_1:31;
then reconsider vv = v as Vector of Lin{v};
A2: vv <> 0.Lin{v} by A1,ZMODUL01:26;
(Omega).Lin{v} = Lin{vv} by ZMODUL03:20;
hence thesis by A2,ZMODUL05:5;
end;
theorem
for V being Z_Module holds rank((0).V) = 0
proof
let V be Z_Module;
reconsider 0Vs = (Omega).((0).V) as strict finite-rank free Z_Module;
(Omega).0Vs = (0).((0).V) by ZMODUL01:51;
hence thesis by ZMODUL05:1;
end;
theorem LmRank1:
for V being torsion-free Z_Module,
v, u being Vector of V st v <> 0.V & u <> 0.V & Lin{v} /\ Lin{u} <> (0).V
holds rank(Lin{v} + Lin{u}) = 1
proof
let V be torsion-free Z_Module,
v, u be Vector of V such that
A1: v <> 0.V & u <> 0.V & Lin{v} /\ Lin{u} <> (0).V;
consider w be Vector of V such that
A2: w <> 0.V & Lin{v} + Lin{u} = Lin{w} by A1,LmSumMod2;
w in Lin{w} by ZMODUL02:65,ZFMISC_1:31;
then reconsider ww = w as Vector of Lin{w};
A3: ww <> 0.Lin{w} by A2,ZMODUL01:26;
(Omega).Lin{w} = Lin{ww} by ZMODUL03:20;
hence thesis by A2,A3,ZMODUL05:5;
end;
theorem LmRank2:
for V being torsion-free Z_Module,
W being finite-rank free Subspace of V,
v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V holds
rank(W + Lin{v}) = rank(W)
proof
let V be torsion-free Z_Module;
defpred P[Nat] means for W being finite-rank free Subspace of V,
v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V
& rank(W) = $1 + 1 holds
rank(W + Lin{v}) = rank(W);
A1: P[0]
proof
let W be finite-rank free Subspace of V,
v be Vector of V such that
B1: v <> 0.V & W /\ Lin{v} <> (0).V & rank(W) = 0 + 1;
consider uu be Vector of W such that
B3: uu <> 0.W & (Omega).W = Lin{uu} by B1,ZMODUL05:5;
reconsider u = uu as Vector of V by ZMODUL01:25;
B4: u <> 0.V by ZMODUL01:26,B3;
reconsider Ws = (Omega).W as strict Subspace of V by ZMODUL01:42;
reconsider Lv = (Omega).Lin{v} as strict Subspace of V;
B6: Lin{u} + Lin{v} = Ws + Lv by B3,ZMODUL03:20
.= W + Lin{v} by ZMODUL04:22;
Lin{u} /\ Lin{v} = Ws /\ Lv by B3,ZMODUL03:20
.= W /\ Lin{v} by ZMODUL04:23;
hence rank(W + Lin{v}) = rank(W) by B6,B1,B4,LmRank1;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let W be finite-rank free Subspace of V, v be Vector of V such that
B2: v <> 0.V & W /\ Lin{v} <> (0).V & rank(W) = (n+1) + 1;
consider I be finite Subset of V such that
B3: I is finite Subset of W &
I is linearly-independent & Lin(I) = (Omega).W & card(I) = rank(W)
by LmFree2;
I <> {}(the carrier of W) by B2,B3;
then consider w be object such that
B5: w in I by XBOOLE_0:7;
reconsider w as Vector of V by B5;
B6: (Omega).W = Lin(I \ {w}) + Lin{w} & Lin(I \ {w}) /\ Lin{w} = (0).V &
Lin(I \ {w}) is free & Lin{w} is free & w <> 0.V by B3,B5,ThLin8;
reconsider LIw = Lin(I \ {w}), Lw = Lin{w}
as finite-rank free Subspace of V;
B7: card(I \ {w}) = card(I) - card{w} by B5,ZFMISC_1:31,CARD_2:44
.= (n+2) - 1 by CARD_1:30,B2,B3
.= n+1;
reconsider Lv = Lin{v} as finite-rank free Subspace of V;
I \ {w} is linearly-independent by B3,ZMODUL02:56,XBOOLE_1:36;
then reconsider Iw = I \ {w} as Basis of Lin(I \ {w}) by ThLin7;
B10: rank(Lin(I \ {w})) = card(Iw) by ZMODUL03:def 5
.= n+1 by B7;
per cases;
suppose C1: (Lin(I \ {w}) + Lin{v}) /\ Lin{w} = (0).V;
then C2: rank((Lin(I \ {w}) + Lin{v}) + Lin{w})
= rank(Lin(I \ {w}) + Lin{v}) + rank(Lin{w}) by ThRankDirectSum;
C3: Lin(I \ {w}) /\ Lin{v} <> (0).V
proof
assume D1: Lin(I \ {w}) /\ Lin{v} = (0).V;
consider x be Vector of V such that
D2: x in W /\ Lin{v} & x <> 0.V by B2,ZMODUL04:24;
x in W by D2,ZMODUL01:94;
then x in (Omega).W;
then consider x1, x2 be Vector of V such that
D3: x1 in Lin(I \ {w}) & x2 in Lin{w} & x = x1 + x2
by B6,ZMODUL01:92;
D4: x in Lin{v} by D2,ZMODUL01:94;
D5: x - x1 = x2 + (x1 - x1) by RLVECT_1:28,D3
.= x2 + 0.V by RLVECT_1:15
.= x2;
-x1 in Lin(I \ {w}) by D3,ZMODUL01:38;
then D6: x2 in Lin(I \ {w}) + Lin{v} by D4,D5,ZMODUL01:92;
x2 <> 0.V by D1,D2,ZMODUL02:66,D4,ZMODUL01:94,D3;
hence contradiction by C1,D6,ZMODUL02:66,D3,ZMODUL01:94;
end;
C4: rank(LIw + Lin{v}) = n+1 by B10,B1,B2,C3;
C5: rank((LIw + Lin{v}) + Lin{w}) = n+1 + 1 by C2,C4,B6,LmRank0a
.= n+2;
(Omega).Lin{v} = Lin{v};
then W + Lin{v} = (Lin(I \ {w}) + Lin{w}) + Lin{v}
by B6,ZMODUL04:22
.= (Lin(I \ {w}) + Lin{v}) + Lin{w} by ZMODUL01:96;
hence thesis by B2,C5;
end;
suppose C1: (Lin(I \ {w}) + Lin{v}) /\ Lin{w} <> (0).V;
per cases;
suppose Lin{v} /\ Lin{w} = (0).V;
then consider w1, w2 be Vector of V such that
D2: w1 <> 0.V & w2 <> 0.V &
(LIw + Lin{v}) + Lin{w} = (LIw + Lin{w1}) + Lin{w2} &
LIw /\ Lin{w1} <> (0).V & (LIw + Lin{w1}) /\ Lin{w2} = (0).V &
v in Lin{w1} + Lin{w2} & w in Lin{w1} + Lin{w2} &
w1 in Lin{v} + Lin{w} & w2 in Lin{v} + Lin{w}
by B2,B6,LmSumMod3,C1;
(Omega).Lin{v} = Lin{v};
then D3: W + Lin{v} = (Lin(I \ {w}) + Lin{w}) + Lin{v}
by B6,ZMODUL04:22
.= (Lin(I \ {w}) + Lin{w1}) + Lin{w2} by D2,ZMODUL01:96;
D4: rank(LIw + Lin{w1}) = n+1 by B10,B1,D2;
rank(W + Lin{v}) = rank(Lin(I \ {w}) + Lin{w1}) + rank(Lin{w2})
by D3,D2,ThRankDirectSum
.= n+1 + 1 by D4,D2,LmRank0a
.= n+2;
hence thesis by B2;
end;
suppose D1: Lin{v} /\ Lin{w} <> (0).V;
consider u be Vector of V such that
D2: u <> 0.V & Lin{v} + Lin{w} = Lin{u} by B2,B6,D1,LmSumMod2;
(Omega).Lin{v} = Lin{v};
then D3: W + Lin{v} = (Lin(I \ {w}) + Lin{w}) + Lin{v}
by B6,ZMODUL04:22
.= Lin(I \ {w}) + Lin{u} by D2,ZMODUL01:96;
Lin(I \ {w}) /\ Lin{u} = (0).V
proof
assume Lin(I \ {w}) /\ Lin{u} <> (0).V;
then consider x be Vector of V such that
E2: x in Lin(I \ {w}) /\ Lin{u} & x <> 0.V by ZMODUL04:24;
x in Lin{u} by E2,ZMODUL01:94;
then consider iux be Element of INT.Ring such that
E3: x = iux * u by ThLin1;
w in Lin{w} by ZMODUL02:65,ZFMISC_1:31;
then w in Lin{u} by D2,ZMODUL01:93;
then consider iuw be Element of INT.Ring such that
E4: w = iuw * u by ThLin1;
E5: iux * w in Lin{w} by ZMODUL01:37,ThLin2;
iux * w = (iux * iuw) * u by VECTSP_1:def 16,E4
.= iuw * x by E3,VECTSP_1:def 16;
then iux * w in Lin(I \ {w}) /\ Lin{u} by E2,ZMODUL01:37;
then iux * w in Lin(I \ {w}) by ZMODUL01:94;
then E6: iux * w in Lin(I \ {w}) /\ Lin{w} by E5,ZMODUL01:94;
iux <> 0.INT.Ring by E2,E3,ZMODUL01:1;
hence contradiction by E6,ZMODUL02:66,B6,ZMODUL01:def 7;
end;
then rank(LIw + Lin{u}) = rank(LIw) + rank(Lin{u}) by ThRankDirectSum
.= n+1 + 1 by B10,D2,LmRank0a
.= n+2;
hence thesis by B2,D3;
end;
end;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let W be finite-rank free Subspace of V,
v be Vector of V such that
A4: v <> 0.V & W /\ Lin{v} <> (0).V;
set rk = rank(W);
rk-1 is Nat
proof
assume not rk - 1 is Nat;
then rk = 0;
then B1: (Omega).W = (0).W by ZMODUL05:1
.= (0).V by ZMODUL01:51;
(Omega).Lin{v} = Lin{v};
then W /\ Lin{v} = (0).V /\ Lin{v} by B1,ZMODUL04:23
.= (0).V by ZMODUL01:107;
hence contradiction by A4;
end;
then reconsider rk1 = rk-1 as Nat;
P[rk1] by A3;
hence thesis by A4;
end;
theorem LmISRank21:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V,
v being Vector of V
st W1 /\ Lin{v} <> (0).V & W2 /\ Lin{v} <> (0).V
holds (W1 /\ W2) /\ Lin{v} <> (0).V
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V, v be Vector of V such that
A1: W1 /\ Lin{v} <> (0).V & W2 /\ Lin{v} <> (0).V;
consider u1 be Vector of V such that
A2: u1 in W1 /\ Lin{v} & u1 <> 0.V by A1,ZMODUL04:24;
consider u2 be Vector of V such that
A3: u2 in W2 /\ Lin{v} & u2 <> 0.V by A1,ZMODUL04:24;
A6: u1 in Lin{v} by A2,ZMODUL01:94;
then consider iu1 be Element of INT.Ring such that
A4: u1 = iu1*v by ThLin1;
u2 in Lin{v} by A3,ZMODUL01:94;
then consider iu2 be Element of INT.Ring such that
A5: u2 = iu2*v by ThLin1;
A7: iu2 <> 0.INT.Ring by A3,A5,ZMODUL01:1;
A8: iu2 * u1 = (iu2*iu1) * v by VECTSP_1:def 16,A4
.= iu1 * u2 by A5,VECTSP_1:def 16;
u1 in W1 by A2,ZMODUL01:94;
then A9: iu2 * u1 in W1 by ZMODUL01:37;
u2 in W2 by A3,ZMODUL01:94;
then iu2 * u1 in W2 by A8,ZMODUL01:37;
then A10: iu2 * u1 in W1 /\ W2 by A9,ZMODUL01:94;
iu2 * u1 in Lin{v} by A6,ZMODUL01:37;
then iu2 * u1 in (W1 /\ W2) /\ Lin{v} by A10,ZMODUL01:94;
hence thesis by ZMODUL02:66,A2,A7,ZMODUL01:def 7;
end;
theorem ThTF3C:
for R being Ring
for V, W being LeftMod of R,
T be linear-transformation of V,W,
A being Subset of V
holds T.:(the carrier of Lin(A)) c= the carrier of Lin(T.: A)
proof
let R be Ring;
let V, W be LeftMod of R,
T be linear-transformation of V,W,
A be Subset of V;
for y be object st y in T.:(the carrier of Lin(A)) holds
y in the carrier of Lin(T.:A)
proof
let y be object;
assume y in T.:(the carrier of Lin(A));
then consider x be Element of V such that
A2: x in the carrier of Lin(A) & y = T.x by FUNCT_2:65;
x in Lin(A) by A2;
then consider l be Linear_Combination of A such that
A3: x = Sum(l) by MOD_3:4;
reconsider l as Linear_Combination of V;
reconsider Tl = T @* l as
Linear_Combination of T.:(Carrier l) by ZMODUL05:44;
Sum(Tl) = T.(Sum l) by ZMODUL05:46; then
A5: y in Lin(T.:Carrier l) by A2,A3,MOD_3:4;
T .: (Carrier l) c= T.: A by RELAT_1:123,VECTSP_6:def 4;
then Lin(T.:Carrier l) is Subspace of Lin(T.:A) by MOD_3:10;
then the carrier of Lin(T.:Carrier l)
c= the carrier of Lin(T.:A) by VECTSP_4:def 2;
hence y in the carrier of Lin(T.:A) by A5;
end;
hence thesis;
end;
theorem HM0:
for R being Ring
for X, Y be LeftMod of R, L be linear-transformation of X, Y
holds L.(0.X) = 0.Y
proof
let R be Ring;
let X,Y be LeftMod of R,
L be linear-transformation of X, Y;
thus L.(0.X) = L.(0.R * 0.X) by VECTSP_1:14
.= 0.R * L.(0.X) by MOD_2:def 2
.= 0.Y by VECTSP_1:14;
end;
theorem HM1:
for R being Ring
for X, Y be LeftMod of R, L be linear-transformation of X, Y
st L is bijective holds
ex K be linear-transformation of Y, X
st K = L" & K is bijective
proof
let R be Ring;
let X, Y be LeftMod of R,
L be linear-transformation of X, Y;
assume
A1: L is bijective; then
P2: rng L = the carrier of Y by FUNCT_2:def 3;
then reconsider K = L" as Function of Y,X by A1,FUNCT_2:25;
D0: dom L = the carrier of X by FUNCT_2:def 1;
B0: K is additive
proof
let x, y be Element of Y;
consider a be Element of X such that
B01: x = L.a by P2,FUNCT_2:113;
consider b be Element of X such that
B02: y = L.b by P2,FUNCT_2:113;
B03: K.x = a by A1,FUNCT_1:34,D0,B01;
B04: K.y = b by A1,FUNCT_1:34,D0,B02;
x+y =L.(a+b) by VECTSP_1:def 20,B01,B02;
hence K.(x+y) = K.x + K.y by B03,B04,A1,FUNCT_1:34,D0;
end;
for r be Element of R,x be Element of Y holds K.(r*x) = r*K.x
proof
let r be Element of R, x be Element of Y;
consider a be Element of X such that
B01: x = L.a by P2,FUNCT_2:113;
B03: K.x = a by A1,FUNCT_1:34,D0,B01;
r*x = L.(r*a) by MOD_2:def 2,B01;
hence K.(r*x) = r*K.x by B03,A1,FUNCT_1:34,D0;
end;
then reconsider K as linear-transformation of Y, X by B0,MOD_2:def 2;
take K;
rng K = the carrier of X by D0,FUNCT_1:33,A1; then
K is onto by FUNCT_2:def 3;
hence thesis by A1;
end;
theorem
for R being Ring
for X, Y be LeftMod of R, l be Linear_Combination of X,
L be linear-transformation of X, Y st L is bijective
holds L@*l = l*L"
proof
let R be Ring;
let X, Y be LeftMod of R,
l be Linear_Combination of X,
L be linear-transformation of X, Y;
assume
A1: L is bijective; then
Q4: rng L = the carrier of Y by FUNCT_2:def 3;
then reconsider K = L" as Function of Y, X by A1,FUNCT_2:25;
P3: dom (l*K) = the carrier of Y by FUNCT_2:def 1;
X1: L|(Carrier l) is one-to-one by A1,FUNCT_1:52;
then P4: L .: (Carrier l) = Carrier ( L@*l) by ZMODUL05:56;
for a being Element of Y holds (L@*l).a = (l*K).a
proof
let a be Element of Y;
per cases;
suppose X0: not a in Carrier (L@*l);
reconsider v = K.a as Element of X;
X4: L.v = a by Q4,A1,FUNCT_1:35;
Y2: not v in Carrier l by X0,X4,FUNCT_2:35,P4;
(l*K).a = l.v by P3,FUNCT_1:12
.= 0.R by Y2;
hence thesis by X0;
end;
suppose a in Carrier (L@*l);
then consider v being object such that
X5: v in dom L & v in (Carrier l) & a = L.v by FUNCT_1:def 6,P4;
reconsider v as Element of X by X5;
X6: K.a = v by A1,FUNCT_1:34,X5;
thus (L@*l).a = l.v by ZMODUL05:54,X1,X5
.= (l*K).a by P3,FUNCT_1:12,X6;
end;
end;
hence thesis by FUNCT_2:def 8;
end;
theorem
for R being Ring
for X, Y be LeftMod of R, X0 be Subset of X,
L be linear-transformation of X, Y,
l be Linear_Combination of L.:X0
st X0 = the carrier of X & L is one-to-one
holds L#l = l*L
proof
let R be Ring;
let X, Y be LeftMod of R,
X0 be Subset of X,
L be linear-transformation of X, Y,
l be Linear_Combination of L.:X0;
assume that
A0: X0 = the carrier of X and
A1: L is one-to-one;
X1: L|X0 is one-to-one by A1,FUNCT_1:52;
X3: X0` = {} by XBOOLE_1:37,A0;
L#l = (l*L) +* ({} --> 0.R) by X3,X1,ZMODUL05:def 9
.= l*L;
hence thesis;
end;
HM4:
for R being Ring
for X, Y be LeftMod of R, A be Subset of X,
L be linear-transformation of X, Y
st L is bijective & A is linearly-independent
holds L.:A is linearly-independent
proof
let R be Ring;
let X, Y be LeftMod of R,
A be Subset of X,
L be linear-transformation of X, Y;
assume that AS1: L is bijective and
AS2: A is linearly-independent;
consider K be linear-transformation of Y, X such that
AS3: K= L" & K is bijective by HM1,AS1;
D1: dom L = the carrier of X by FUNCT_2:def 1;
R1: rng L = the carrier of Y by FUNCT_2:def 3,AS1;
for l be Linear_Combination of L.:A st Sum(l) = 0.Y holds Carrier(l) = {}
proof
let l be Linear_Combination of L.:A;
assume P0: Sum(l) = 0.Y;
reconsider m = K@*l as Linear_Combination of K.:(Carrier l)
by ZMODUL05:44;
P2: Sum m = K.(0.Y) by P0,ZMODUL05:46
.= 0.X by HM0;
K.:(Carrier l) c= K.:(L.:A) by RELAT_1:123,VECTSP_6:def 4; then
P4: K.:(Carrier l) c= A by D1,AS1,AS3,FUNCT_1:107;
K|(Carrier l) is one-to-one by AS3,FUNCT_1:52; then
P5: K .: (Carrier l) = Carrier ( K@*l) by ZMODUL05:56;
then m is Linear_Combination of A by VECTSP_6:def 4,P4; then
P6: L.: (K.: Carrier(l)) = L.:{} by P5,AS2,P2
.= {};
L.:(K.: Carrier(l)) = L.:(L"Carrier(l)) by FUNCT_1:85,AS1,AS3
.=Carrier(l) by R1,FUNCT_1:77;
hence Carrier(l) = {} by P6;
end;
hence thesis;
end;
theorem HM6:
for R being Ring
for X, Y be LeftMod of R, A be Subset of X,
L be linear-transformation of X, Y
st L is bijective
holds A is linearly-independent
iff L.:A is linearly-independent
proof
let R be Ring;
let X, Y be LeftMod of R, A be Subset of X,
L be linear-transformation of X, Y;
assume AS1: L is bijective;
D1: dom L = the carrier of X by FUNCT_2:def 1;
consider K be linear-transformation of Y, X such that
AS3: K= L" & K is bijective by HM1,AS1;
thus A is linearly-independent implies L.:A is linearly-independent
by AS1,HM4;
assume L.:A is linearly-independent;
then K.: (L.:A) is linearly-independent by AS3,HM4;
hence thesis by D1,AS1,AS3,FUNCT_1:107;
end;
theorem HM7:
for R being Ring
for X, Y be LeftMod of R, A be Subset of X,
T be linear-transformation of X, Y
st T is bijective holds
T.:(the carrier of Lin(A)) = the carrier of Lin(T.: A)
proof
let R be Ring;
let X, Y be LeftMod of R,
A be Subset of X,
T be linear-transformation of X, Y;
assume AS1: T is bijective;
X1: T.:(the carrier of Lin(A)) c= the carrier of Lin(T.: A) by ThTF3C;
reconsider B = T.: A as Subset of Y;
D1: dom T = the carrier of X by FUNCT_2:def 1;
R1: rng T = the carrier of Y by FUNCT_2:def 3,AS1;
consider K be linear-transformation of Y, X such that
AS3: K= T" & K is bijective by HM1,AS1;
K.: B = A by D1,AS1,AS3,FUNCT_1:107; then
X3: T.: (K.:(the carrier of Lin(B))) c= T.: the carrier of Lin(A)
by RELAT_1:123,ThTF3C;
X4: the carrier of Lin(B) c= rng T by R1,VECTSP_4:def 2;
T.:(K.: the carrier of Lin(B)) = T.:(T" the carrier of Lin(B))
by FUNCT_1:85,AS1,AS3
.= the carrier of Lin(B) by X4,FUNCT_1:77;
hence thesis by X1,XBOOLE_0:def 10,X3;
end;
theorem HM8:
for R being Ring
for Y be LeftMod of R, A be Subset of Y
holds Lin(A) is strict Subspace of (Omega).Y
proof
let R be Ring;
let Y be LeftMod of R, A be Subset of Y;
U1: the carrier of Lin(A) c= the carrier of Y
& 0.Lin(A) = 0.Y
& the addF of Lin(A) = (the addF of Y) ||the carrier of Lin(A)
& the lmult of Lin(A) = (the lmult of Y) |
[:the carrier of R, the carrier of Lin(A):]
by VECTSP_4:def 2;
the carrier of Y = the carrier of ((Omega).Y )
& 0.Y = 0.((Omega).Y)
& the addF of Y = the addF of ((Omega).Y)
& the lmult of Y = the lmult of ((Omega).Y);
hence Lin(A) is strict Subspace of (Omega).Y by U1,VECTSP_4:def 2;
end;
HM9:
for R being Ring
for X, Y be LeftMod of R, T be linear-transformation of X, Y
st T is bijective holds
X is free implies Y is free
proof
let R be Ring;
let X, Y be LeftMod of R, T be linear-transformation of X, Y;
assume AS1: T is bijective;
D1: dom T = the carrier of X by FUNCT_2:def 1;
R1: rng T = the carrier of Y by FUNCT_2:def 3,AS1;
assume X is free;
then consider A being Subset of X such that
p1: A is base;
P2: T.:A is linearly-independent by HM6,AS1,p1;
the carrier of Lin(T.: A) = T.: (the carrier of the ModuleStr of X)
by p1,AS1,HM7
.= the carrier of (Omega).Y by D1,R1,RELAT_1:113; then
Lin (T.:A) = (Omega).Y by VECTSP_4:29
.= the ModuleStr of Y; then
T.:A is base by P2;
hence Y is free;
end;
theorem
for R being Ring
for X, Y be LeftMod of R, T be linear-transformation of X, Y
st T is bijective holds
X is free iff Y is free
proof
let R be Ring;
let X, Y be LeftMod of R, T be linear-transformation of X, Y;
assume AS1: T is bijective;
consider K be linear-transformation of Y, X such that
AS3: K= T" & K is bijective by HM1,AS1;
thus thesis by HM9,AS1,AS3;
end;
HM11:
for X, Y be free Z_Module, T be linear-transformation of X, Y,
A be Subset of X st T is bijective holds
A is Basis of X implies T.: A is Basis of Y
proof
let X, Y be free Z_Module,
T be linear-transformation of X, Y,
A be Subset of X;
assume AS1: T is bijective;
assume A is Basis of X; then
P1: A is linearly-independent &
Lin (A) = the ModuleStr of X by VECTSP_7:def 3;
D1: dom T = the carrier of X by FUNCT_2:def 1;
R1: rng T = the carrier of Y by FUNCT_2:def 3,AS1;
P2: T.:A is linearly-independent by HM6,AS1,P1;
P6: Lin(T.: A) is strict Subspace of (Omega).Y by HM8;
the carrier of Lin(T.: A) = T.: (the carrier of (the ModuleStr of X) )
by P1,AS1,HM7
.= the carrier of (Omega).Y by D1,R1,RELAT_1:113;
hence thesis by P2,VECTSP_7:def 3,P6,ZMODUL01:47;
end;
theorem HM12:
for X, Y be free Z_Module, T be linear-transformation of X, Y,
A be Subset of X st T is bijective holds
A is Basis of X iff T.: A is Basis of Y
proof
let X, Y be free Z_Module,
L be linear-transformation of X, Y,
A be Subset of X;
assume AS1: L is bijective;
D1: dom L = the carrier of X by FUNCT_2:def 1;
consider K be linear-transformation of Y, X such that
AS3: K= L" & K is bijective by HM1,AS1;
thus A is Basis of X implies L.:A is Basis of Y by AS1,HM11;
assume L.:A is Basis of Y;
then K.: (L.:A) is Basis of X by AS3,HM11;
hence thesis by D1,AS1,AS3,FUNCT_1:107;
end;
HM13:
for X, Y be free Z_Module, T be linear-transformation of X, Y
st T is bijective holds
X is finite-rank implies Y is finite-rank
proof
let X, Y be free Z_Module,
L be linear-transformation of X, Y;
assume AS1: L is bijective;
assume X is finite-rank;
then consider A being finite Subset of X such that
P1: A is Basis of X;
L.: A is Basis of Y by P1,HM12,AS1;
hence thesis;
end;
theorem
for X, Y be free Z_Module, T be linear-transformation of X, Y
st T is bijective holds
X is finite-rank iff Y is finite-rank
proof
let X, Y be free Z_Module,
T be linear-transformation of X, Y;
assume AS1: T is bijective;
consider K be linear-transformation of Y, X such that
AS3: K= T" & K is bijective by HM1,AS1;
thus thesis by HM13,AS1,AS3;
end;
theorem HM15:
for X, Y be finite-rank free Z_Module, T be linear-transformation of X, Y
st T is bijective holds
rank(X) = rank(Y)
proof
let X, Y be finite-rank free Z_Module,
T be linear-transformation of X, Y;
assume AS1: T is bijective;
for I being Basis of X holds rank(Y) = card I
proof
let I be Basis of X;
dom T = the carrier of X by FUNCT_2:def 1; then
X12: card I = card (T.:I) by CARD_1:5,AS1,CARD_1:33;
T.: I is Basis of Y by AS1,HM12;
hence rank(Y) = card I by X12,ZMODUL03:def 5;
end;
hence thesis by ZMODUL03:def 5;
end;
theorem ThRankS1:
for V being Z_Module, W being finite-rank free Subspace of V,
a being Element of INT.Ring st a <> 0.INT.Ring holds
rank(a (*) W) = rank(W)
proof
let V be Z_Module, W be finite-rank free Subspace of V,
a be Element of INT.Ring such that
A1: a <> 0.INT.Ring;
defpred P[Element of W,object] means $2 = a * $1;
P0: for x being Element of W ex y being Element of a (*) W st P[x,y]
proof
let x be Element of W;
a * x in the carrier of (a (*) W);
hence thesis;
end;
consider F be Function of W,a (*) W such that
A2: for x be Element of W holds P[x,F.x] from FUNCT_2:sch 3(P0);
X1X: for x1, x2 being object st x1 in the carrier of W
& x2 in the carrier of W & F.x1 = F.x2
holds x1 = x2
proof
let x1, x2 be object such that
D1: x1 in the carrier of W & x2 in the carrier of W & F.x1 = F.x2;
reconsider xx1 = x1, xx2 = x2 as Element of W by D1;
F.x1 = a*xx1 & F.x2= a*xx2 by A2;
hence thesis by A1,ZMODUL01:10,D1;
end;
for y being object st y in the carrier of a (*) W holds y in rng F
proof
let y be object such that
D1: y in the carrier of a (*) W;
consider v be Element of W such that
D2: y=a*v by D1;
F.v = a*v by A2;
hence y in rng F by D2,FUNCT_2:4;
end;
then X2X: the carrier of a (*) W c= rng F;
B0: F is additive
proof
let x, y be Element of W;
B03: F.x = a*x by A2;
B04: F.y = a*y by A2;
thus F.(x+y) = a*(x+y) by A2
.= a*x + a*y by VECTSP_1:def 14
.= F.x + F.y by ZMODUL01:28,B03,B04;
end;
for r be Element of INT.Ring, x be Element of W holds F.(r*x) = r*F.x
proof
let r be Element of INT.Ring, x be Element of W;
thus F.(r*x) = a*(r*x) by A2
.= (a*r)*x by VECTSP_1:def 16
.= r*(a*x) by VECTSP_1:def 16
.= r*F.x by ZMODUL01:29,A2;
end;
then reconsider F as linear-transformation of W, a (*) W
by B0,MOD_2:def 2;
reconsider aW = a (*) W as finite-rank free Z_Module;
reconsider W0 = W as finite-rank free Z_Module;
reconsider F as linear-transformation of W0, aW;
F is one-to-one onto by X1X,FUNCT_2:19,X2X,FUNCT_2:def 3,XBOOLE_0:def 10;
hence thesis by HM15;
end;
theorem
for V being Z_Module, W1, W2, W3 being finite-rank free Subspace of V,
a being Element of INT.Ring st a <> 0.INT.Ring & W3 = a (*) W1 holds
rank(W3 /\ W2) = rank(W1 /\ W2)
proof
let V be Z_Module, W1, W2, W3 be finite-rank free Subspace of V,
a be Element of INT.Ring such that
A1: a <> 0.INT.Ring & W3 = a (*) W1;
W3 /\ W2 is Subspace of W1 /\ W2
proof
W3 /\ W2 is Subspace of W3 by ZMODUL01:105;
then B2: W3 /\ W2 is Subspace of W1 by A1,ZMODUL01:42;
W3 /\ W2 is Subspace of W2 by ZMODUL01:105;
hence thesis by B2,ZMODUL02:75;
end;
then A2: rank(W3 /\ W2) <= rank(W1 /\ W2) by ZMODUL05:2;
a (*) (W1 /\ W2) is Subspace of W3 /\ W2
proof
reconsider WX = a (*) (W1 /\ W2) as Subspace of V by ZMODUL01:42;
for v being Vector of V st v in WX holds
v in W3 /\ W2
proof
let v be Vector of V such that
C1: v in WX;
consider vx be Vector of (W1 /\ W2) such that
C2: v = a * vx by C1;
reconsider vvx = vx as Vector of V by ZMODUL01:25;
CX: vvx in W1 /\ W2;
then vvx in W1 by ZMODUL01:94;
then reconsider vvvx = vvx as Vector of W1;
a * vvvx in a * W1;
then a * vvx in W3 by A1,ZMODUL01:29;
then C3: v in W3 by C2,ZMODUL01:29;
vvx in W2 by CX,ZMODUL01:94;
then a * vvx in W2 by ZMODUL01:37;
then v in W2 by C2,ZMODUL01:29;
hence thesis by C3,ZMODUL01:94;
end;
hence thesis by ZMODUL01:44;
end;
then rank(a (*) (W1 /\ W2)) <= rank(W3 /\ W2) by ZMODUL05:2;
then rank(W1 /\ W2) <= rank(W3 /\ W2) by A1,ThRankS1;
hence thesis by A2,XXREAL_0:1;
end;
theorem
for V being torsion-free Z_Module,
W1, W2, W3 being finite-rank free Subspace of V,
a being Element of INT.Ring st a <> 0.INT.Ring & W3 = a (*) W1 holds
rank(W3 + W2) = rank(W1 + W2)
proof
let V be torsion-free Z_Module,
W1, W2, W3 be finite-rank free Subspace of V,
a be Element of INT.Ring such that
A1: a <> 0.INT.Ring & W3 = a (*) W1;
for v being Vector of V st v in W3 + W2 holds v in W1 + W2
proof
let v be Vector of V such that
B1: v in W3 + W2;
consider v1, v2 be Vector of V such that
B2: v1 in W3 & v2 in W2 & v = v1 + v2 by B1,ZMODUL01:92;
v1 in W1 by B2,A1;
hence thesis by B2,ZMODUL01:92;
end;
then W3 + W2 is Subspace of W1 + W2 by ZMODUL01:44;
then A2: rank(W3 + W2) <= rank(W1 + W2) by ZMODUL05:2;
reconsider aW = a (*) (W1 + W2) as finite-rank free Subspace of V
by ZMODUL01:42;
for v being Vector of V st v in a (*) (W1 + W2) holds v in W3 + W2
proof
let v be Vector of V such that
B1: v in a (*) (W1 + W2);
consider vx be Vector of (W1 + W2) such that
B2: v = a * vx by B1;
reconsider vvx = vx as Vector of V by ZMODUL01:25;
vvx in W1 + W2;
then consider v1, v2 be Vector of V such that
B3: v1 in W1 & v2 in W2 & vvx = v1 + v2 by ZMODUL01:92;
B4: v = a * vvx by B2,ZMODUL01:29
.= a * v1 + a * v2 by VECTSP_1:def 14,B3;
reconsider vv1 = v1 as Vector of W1 by B3;
a * vv1 in a * W1;
then B5: a * v1 in W3 by A1,ZMODUL01:29;
a * v2 in W2 by B3,ZMODUL01:37;
hence thesis by B4,B5,ZMODUL01:92;
end;
then aW is Subspace of W3 + W2 by ZMODUL01:44;
then rank(a (*) (W1 + W2)) <= rank(W3 + W2) by ZMODUL05:2;
then rank(W1 + W2) <= rank(W3 + W2) by A1,ThRankS1;
hence thesis by A2,XXREAL_0:1;
end;
theorem ThISRank2:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V,
I being Basis of W1
st (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
holds rank(W1 /\ W2) = rank(W1)
proof
let V be torsion-free Z_Module;
defpred P[Nat] means
for W1, W2 being finite-rank free Subspace of V,
I being Basis of W1
st (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
& rank(W1) = $1 holds
rank(W1 /\ W2) = rank(W1);
A1: P[0] by ThISRank1;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let W1, W2 be finite-rank free Subspace of V,
I be Basis of W1 such that
B2: (for v being Vector of V st v in I holds
(W1 /\ W2) /\ Lin{v} <> (0).V) & rank(W1) = n + 1;
card(I) > 0 by ZMODUL03:def 5,B2;
then I <> {}(the carrier of W1);
then consider u be object such that
B3: u in I by XBOOLE_0:7;
reconsider u as Vector of W1 by B3;
reconsider uu = u as Vector of V by ZMODUL01:25;
BX1: I is linearly-independent by VECTSP_7:def 3;
reconsider II = I as linearly-independent Subset of V
by ZMODUL03:15,VECTSP_7:def 3;
I \ {u} is linearly-independent by BX1,XBOOLE_1:36,ZMODUL02:56;
then reconsider Iu = I \ {u} as linearly-independent Subset of V
by ZMODUL03:15;
(Omega).W1 = Lin(I) by VECTSP_7:def 3
.= Lin(II) by ZMODUL03:20;
then BX2: (Omega).W1 = Lin(Iu) + Lin{uu} & Lin(Iu) /\ Lin{uu} = (0).V &
Lin(Iu) is free & Lin{uu} is free & uu <> 0.V by B3,ThLin8;
reconsider LIu = Lin(Iu) as finite-rank free Subspace of V;
B5: Iu is Basis of Lin(Iu) by ThLin7;
card(Iu) = card(I) - card{u} by B3,ZFMISC_1:31,CARD_2:44
.= rank(W1) - card{u} by ZMODUL03:def 5
.= n + 1 - 1 by B2,CARD_1:30
.= n;
then B6: rank(LIu) = n by B5,ZMODUL03:def 5;
B7X:for v being Vector of V st v in Iu holds
(Lin(Iu) /\ W2) /\ Lin{v} <> (0).V
proof
let v be Vector of V such that
C1: v in Iu;
v in I by C1,TARSKI:def 3,XBOOLE_1:36;
then (W1 /\ W2) /\ Lin{v} <> (0).V by B2;
then W1 /\ (W2 /\ Lin{v}) <> (0).V by ZMODUL01:104;
then C2: W2 /\ Lin{v} <> (0).V by ZMODUL01:107;
C3: v <> 0.V by C1,ZMODUL02:57;
C4: v in Lin{v} by ZMODUL02:65,ZFMISC_1:31;
v in LIu by C1,ZMODUL02:65;
then LIu /\ Lin{v} <> (0).V by C3,ZMODUL02:66,C4,ZMODUL01:94;
hence thesis by C2,LmISRank21;
end;
B8: (W1 /\ W2) /\ Lin{uu} <> (0).V by B2,B3;
(LIu /\ W2) + Lin{uu} is Subspace of (W1 /\ W2) + Lin{uu}
proof
for x being Vector of V st x in (LIu /\ W2) + Lin{uu} holds
x in (W1 /\ W2) + Lin{uu}
proof
let x be Vector of V such that
D1: x in (LIu /\ W2) + Lin{uu};
consider x1, x2 be Vector of V such that
D2: x1 in (LIu /\ W2) & x2 in Lin{uu} & x = x1 + x2
by D1,ZMODUL01:92;
D3: x1 in LIu & x1 in W2 by D2,ZMODUL01:94; then
x1 in (Omega).W1 by BX2,ZMODUL01:93;
then x1 in W1;
then x1 in (W1 /\ W2) by D3,ZMODUL01:94;
hence thesis by D2,ZMODUL01:92;
end;
hence thesis by ZMODUL01:44;
end;
then B10X: rank((LIu /\ W2) + Lin{uu}) <= rank((W1 /\ W2) + Lin{uu})
by ZMODUL05:2;
(LIu /\ Lin{uu}) /\ W2 = (0).V by ZMODUL01:107,BX2;
then (W2 /\ LIu) /\ Lin{uu} = (0).V by ZMODUL01:104;
then rank((LIu /\ W2) + Lin{uu}) = rank(LIu /\ W2) + rank(Lin{uu})
by ThRankDirectSum
.= rank(LIu /\ W2) + 1 by BX2,LmRank0a
.= rank(LIu) + 1 by B7X,B1,B5,B6;
then B11: rank(LIu) + 1 <= rank(W1 /\ W2) by B10X,B8,BX2,LmRank2;
B12: rank(W1) = rank((Omega).W1) by ZMODUL05:4
.= rank(LIu) + rank(Lin{uu}) by BX2,ThRankDirectSum
.= rank(LIu) + 1 by BX2,LmRank0a;
W1 /\ W2 is Subspace of W1 by ZMODUL01:105;
then rank(W1 /\ W2) <= rank(W1) by ZMODUL05:2;
hence thesis by B12,B11,XXREAL_0:1;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let W1, W2 be finite-rank free Subspace of V,
I be Basis of W1 such that
A4: for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V;
thus thesis by A4,A3;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V,
I being Basis of W1
st rank(W1 /\ W2) < rank(W1) holds
ex v being Vector of V st v in I & (W1 /\ W2) /\ Lin{v} = (0).V
by ThISRank2;
theorem LmISRank41:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V, I being Basis of W1
st rank(W1 /\ W2) = rank(W1) holds
(for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V, I be Basis of W1 such that
A1: rank(W1 /\ W2) = rank(W1);
assume ex v being Vector of V st v in I & (W1 /\ W2) /\ Lin{v} = (0).V;
then consider v be Vector of V such that
A2: v in I & (W1 /\ W2) /\ Lin{v} = (0).V;
reconsider II = I as linearly-independent Subset of V
by ZMODUL03:15,VECTSP_7:def 3;
A4X: (Omega).W1 = Lin(I) by VECTSP_7:def 3
.= Lin(II) by ZMODUL03:20;
then A4: (Omega).W1 = Lin(II \ {v}) + Lin{v} &
Lin(II \ {v}) /\ Lin{v} = (0).V &
Lin(II \ {v}) is free & Lin{v} is free & v <> 0.V by A2,ThLin8;
reconsider LIv = Lin(II \ {v}) as finite-rank free Subspace of V;
reconsider W1s = (Omega).W1, W2s = (Omega).W2
as strict finite-rank free Subspace of V by ZMODUL01:42;
rank(W1s) = rank((W1s /\ W2s) + W1s) by ZMODUL01:112
.= rank((W1 /\ W2) + W1s) by ZMODUL04:23;
then A6: rank(W1) = rank((W1 /\ W2) + W1s) by ZMODUL05:4;
(W1 /\ W2) + W1s = (W1 /\ W2) + (LIv + Lin{v}) by A4X,A2,ThLin8
.= ((W1 /\ W2) + Lin{v}) + LIv by ZMODUL01:96;
then (W1 /\ W2) + Lin{v} is Subspace of (W1 /\ W2) + W1s by ZMODUL01:97;
then A8: rank((W1 /\ W2) + Lin{v}) <= rank(W1) by A6,ZMODUL05:2;
rank((W1 /\ W2) + Lin{v}) = rank(W1 /\ W2) + rank(Lin{v})
by A2,ThRankDirectSum
.= rank(W1) + 1 by A1,A4,LmRank0a;
hence contradiction by A8,NAT_1:13;
end;
theorem LmISRank42:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V, I being Basis of W1
st (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
holds rank(W1 + W2) = rank(W2)
proof
let V be torsion-free Z_Module;
defpred P[Nat] means
for W1, W2 being finite-rank free Subspace of V, I being Basis of W1
st (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
& rank(W1) = $1 holds rank(W1 + W2) = rank(W2);
A1: P[0]
proof
let W1, W2 be finite-rank free Subspace of V,
I be Basis of W1 such that
B1: (for v being Vector of V st v in I holds
(W1 /\ W2) /\ Lin{v} <> (0).V) & rank(W1) = 0;
B2: (Omega).W1 = (0).W1 by B1,ZMODUL05:1
.= (0).V by ZMODUL01:51;
reconsider W1s = (Omega).W1, W2s = (Omega).W2
as strict finite-rank free Subspace of V by ZMODUL01:42;
thus rank(W1 + W2) = rank(W1s + W2s) by ZMODUL04:22
.= rank(W2s) by ZMODUL01:99,B2
.= rank(W2) by ZMODUL05:4;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let W1, W2 be finite-rank free Subspace of V,
I be Basis of W1 such that
B2: (for v being Vector of V st v in I holds
(W1 /\ W2) /\ Lin{v} <> (0).V) & rank(W1) = n+1;
card(I) > 0 by ZMODUL03:def 5,B2;
then I <> {}(the carrier of W1);
then consider u be object such that
B3: u in I by XBOOLE_0:7;
reconsider u as Vector of W1 by B3;
reconsider uu = u as Vector of V by ZMODUL01:25;
B4: I is linearly-independent by VECTSP_7:def 3;
reconsider II = I as linearly-independent Subset of V
by ZMODUL03:15,VECTSP_7:def 3;
I \ {u} is linearly-independent by B4,XBOOLE_1:36,ZMODUL02:56;
then reconsider Iu = I \ {u} as linearly-independent Subset of V
by ZMODUL03:15;
BX2X: (Omega).W1 = Lin(I) by VECTSP_7:def 3
.= Lin(II) by ZMODUL03:20;
then BX2: (Omega).W1 = Lin(Iu) + Lin{uu} & Lin(Iu) /\ Lin{uu} = (0).V &
Lin(Iu) is free & Lin{uu} is free & uu <> 0.V by B3,ThLin8;
reconsider LIu = Lin(Iu) as finite-rank free Subspace of V;
B5: Iu is Basis of Lin(Iu) by ThLin7;
card(Iu) = card(I) - card{u} by B3,ZFMISC_1:31,CARD_2:44
.= rank(W1) - card{u} by ZMODUL03:def 5
.= n + 1 - 1 by B2,CARD_1:30
.= n;
then B6: rank(LIu) = n by B5,ZMODUL03:def 5;
B7X: for v being Vector of V st v in Iu holds
(Lin(Iu) /\ W2) /\ Lin{v} <> (0).V
proof
let v be Vector of V such that
C1: v in Iu;
v in I by C1,TARSKI:def 3,XBOOLE_1:36;
then (W1 /\ W2) /\ Lin{v} <> (0).V by B2;
then W1 /\ (W2 /\ Lin{v}) <> (0).V by ZMODUL01:104;
then C2: W2 /\ Lin{v} <> (0).V by ZMODUL01:107;
C3: v <> 0.V by C1,ZMODUL02:57;
C4: v in Lin{v} by ZMODUL02:65,ZFMISC_1:31;
v in LIu by C1,ZMODUL02:65;
then LIu /\ Lin{v} <> (0).V by C3,ZMODUL02:66,C4,ZMODUL01:94;
hence thesis by C2,LmISRank21;
end;
(W1 /\ W2) /\ Lin{uu} = W1 /\ (W2 /\ Lin{uu}) by ZMODUL01:104;
then W2 /\ Lin{uu} <> (0).V by ZMODUL01:107,B2,B3;
then (LIu + W2) /\ Lin{uu} <> (0).V by ThIS1;
then B8: rank((LIu + W2) + Lin{uu}) = rank(LIu + W2) by BX2,LmRank2
.= rank(W2) by B7X,B1,B5,B6;
reconsider W1s = (Omega).W1, W2s = (Omega).W2
as strict finite-rank free Subspace of V by ZMODUL01:42;
B9: (Omega).W1s = W1s;
(LIu + W2) + Lin{uu} = (Lin{uu} + LIu) + W2 by ZMODUL01:96
.= W1s + W2 by BX2X,B3,ThLin8
.= W1s + W2s by B9,ZMODUL04:22
.= W1 + W2 by ZMODUL04:22;
hence thesis by B8;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let W1, W2 be finite-rank free Subspace of V,
I be Basis of W1 such that
A4: for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V;
set rk = rank(W1);
P[rk] by A3;
hence thesis by A4;
end;
theorem ThISRank4:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V
st rank(W1 /\ W2) = rank(W1) holds
rank(W1 + W2) = rank(W2)
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V such that
A1: rank(W1 /\ W2) = rank(W1);
set I = the Basis of W1;
for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V
by A1,LmISRank41;
hence thesis by LmISRank42;
end;
theorem VECT9Th26:
for G be Field, V be VectSp of G, A being Subset of V
st A is linearly-independent holds
A is Basis of Lin(A)
proof
let G be Field, V be VectSp of G;
let A be Subset of V such that
A1: A is linearly-independent;
set W = Lin(A);
for x being object st x in A holds x in the carrier of W
by STRUCT_0:def 5,VECTSP_7:8;
then reconsider B = A as linearly-independent Subset of W
by A1,VECTSP_9:12,TARSKI:def 3;
W = Lin(B) by VECTSP_9:17;
hence thesis by VECTSP_7:def 3;
end;
theorem LmISRank501:
for V being Mult-cancelable finite-rank free Z_Module,
W1, W2 be finite-rank free Subspace of V holds
rank(W1 + W2) + rank(W1 /\ W2) = rank(W1) + rank(W2)
proof
let V be Mult-cancelable finite-rank free Z_Module,
W1, W2 be finite-rank free Subspace of V;
consider I1 being finite Subset of V such that
P1: I1 is finite Subset of W1
& I1 is linearly-independent
& Lin(I1) = (Omega).W1 & card(I1) = rank(W1) by LmFree2;
reconsider I1 as linearly-independent Subset of V by P1;
reconsider I10 = I1 as Basis of Lin(I1) by ThLin7;
consider I2 being finite Subset of V such that
P2: I2 is finite Subset of W2 & I2 is linearly-independent
& Lin(I2) = (Omega).W2 & card(I2) = rank(W2) by LmFree2;
reconsider I2 as linearly-independent Subset of V by P2;
reconsider I20 = I2 as Basis of Lin(I2) by ThLin7;
consider I1I2 being finite Subset of V such that
P3: I1I2 is finite Subset of W1 + W2
& I1I2 is linearly-independent
& Lin(I1I2) = (Omega).(W1 + W2)
& card(I1I2) = rank(W1 + W2) by LmFree2;
reconsider I1I2 as linearly-independent Subset of V by P3;
reconsider I1I20 = I1I2 as Basis of Lin(I1I2) by ThLin7;
consider I12 being finite Subset of V such that
P4: I12 is finite Subset of W1/\ W2
& I12 is linearly-independent
& Lin(I12) = (Omega).(W1 /\ W2) & card(I12) = rank(W1 /\ W2) by LmFree2;
set Iq1 = (MorphsZQ(V)).:I1;
set Iq2 = (MorphsZQ(V)).:I2;
set IIq12 = (MorphsZQ(V)).:I1I2;
set Iq12 = (MorphsZQ(V)).:I12;
reconsider Iq10 = Iq1 as Basis of Lin(Iq1) by ZMODUL04:11,VECT9Th26;
reconsider Iq20 = Iq2 as Basis of Lin(Iq2) by ZMODUL04:11,VECT9Th26;
reconsider IIq120 = IIq12 as Basis of Lin(IIq12) by ZMODUL04:11,VECT9Th26;
reconsider Iq120 = Iq12 as Basis of Lin(Iq12) by P4,ZMODUL04:11,VECT9Th26;
R1: dim Lin(Iq1) = card(Iq1) by VECTSP_9:26,ZMODUL04:11;
R2: dim Lin(Iq2) = card(Iq2) by VECTSP_9:26,ZMODUL04:11;
R3: dim Lin(IIq12) = card(IIq12) by VECTSP_9:26,ZMODUL04:11;
R4: dim Lin(Iq12) = card(Iq12) by P4,VECTSP_9:26,ZMODUL04:11;
Z0: (MorphsZQ(V)) is one-to-one by ZMODUL04:def 6;
S2: dom (MorphsZQ(V)) = the carrier of V by FUNCT_2:def 1;
D1: dim Lin(Iq1) = rank W1 by P1,S2,CARD_1:5,Z0,CARD_1:33,R1;
D2: dim Lin(Iq2) = rank W2 by P2,CARD_1:5,Z0,CARD_1:33,S2,R2;
D3: dim Lin(IIq12) = rank(W1 + W2) by P3,CARD_1:5,Z0,CARD_1:33,S2,R3;
D4: dim Lin(Iq12) = rank (W1 /\ W2) by P4,CARD_1:5,Z0,CARD_1:33,S2,R4;
for v be Vector of Z_MQ_VectSp(V) holds
v in Lin(Iq1) + Lin(Iq2) iff v in Lin(IIq12)
proof
let v be Vector of Z_MQ_VectSp(V);
hereby
assume v in Lin(Iq1) + Lin(Iq2);
then consider v1, v2 be Vector of Z_MQ_VectSp(V) such that
PP1: v1 in Lin(Iq1) & v2 in Lin(Iq2) & v = v1 + v2 by VECTSP_5:1;
consider lq1 be Linear_Combination of Iq1 such that
PP2: v1 = Sum(lq1) by VECTSP_7:7,PP1;
consider lq2 be Linear_Combination of Iq2 such that
PP3: v2 = Sum(lq2) by VECTSP_7:7,PP1;
consider m1 be Element of INT.Ring, a1 be Element of F_Rat,
l1 be Linear_Combination of I1 such that
PP4: m1 <> 0 & m1 = a1 & l1 = (a1 * lq1) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq1) = Carrier(l1) by ZMODUL04:9;
PP5: a1*v1 = (MorphsZQ(V)).(Sum(l1)) by PP4,ZMODUL04:10,PP2;
consider m2 be Element of INT.Ring, a2 be Element of F_Rat,
l2 be Linear_Combination of I2 such that
PP6: m2 <> 0 & m2 = a2 & l2 = (a2 * lq2) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq2) = Carrier(l2) by ZMODUL04:9;
PP7: a2*v2 = (MorphsZQ(V)).(Sum(l2)) by PP6,ZMODUL04:10,PP3;
PP8: (a1*a2)*v1 = a2*(a1*v1) by VECTSP_1:def 16
.= (MorphsZQ(V)).(m2*Sum(l1)) by PP6,ZMODUL04:def 6,PP5;
PP9: (a1*a2)*v2 = a1*(a2*v2) by VECTSP_1:def 16
.= (MorphsZQ(V)).(m1*Sum(l2)) by PP4,ZMODUL04:def 6,PP7;
PP10: (a1*a2)*(v1+v2) = (a1*a2)*v1 + (a1*a2)*v2 by VECTSP_1:def 14
.= (MorphsZQ(V)).(m2*Sum(l1) + m1*Sum(l2)) by ZMODUL04:def 6,PP8,PP9;
Sum(l1) in (Omega).W1 by P1,ZMODUL02:64;
then Sum(l1) in W1;
then
PP11: m2*Sum(l1) in W1 by ZMODUL01:37;
Sum(l2) in Lin(I2) by ZMODUL02:64;
then Sum(l2) in W2 by P2;
then m1*Sum(l2) in W2 by ZMODUL01:37;
then consider l12 be Linear_Combination of I1I2 such that
PP13: m2*Sum(l1) + m1*Sum(l2) = Sum(l12)
by ZMODUL02:64,P3,PP11,ZMODUL01:92;
reconsider r1 = 1 as Element of F_Rat;
reconsider i1 = 1 as Element of INT.Ring;
consider lq12 be Linear_Combination of IIq12 such that
PP14: l12 = lq12*(MorphsZQ(V))
& Carrier(lq12) = (MorphsZQ(V)).:(Carrier(l12)) by ZMODUL04:12;
r1 = 1.(F_Rat);
then l12 = (r1*lq12)*(MorphsZQ(V)) & 0 <> i1 & r1 = i1
by PP14; then
Y1: r1*(Sum(lq12)) = (MorphsZQ(V)).(Sum(l12)) by ZMODUL04:10;
reconsider ra1 = a1, ra2 = a2 as Rational;
Y3: (ra1*ra2)"*(ra1*ra2) = 1 by XCMPLX_0:def 7,PP4,PP6;
(a1*a2)" = (ra1*ra2)" by GAUSSINT:15,PP4,PP6; then
Y2: (a1*a2)"*(a1*a2) = 1.(F_Rat) by Y3;
X1X: r1*(Sum(lq12)) = 1.(F_Rat) * (Sum(lq12))
.= Sum(lq12);
(a1*a2)"*((a1*a2)*(v1+v2)) = ((a1*a2)"*(a1*a2)) *(v1+v2)
by VECTSP_1:def 16
.= v1 + v2 by Y2;
hence v in Lin(IIq12)
by X1X,PP1,VECTSP_4:21,VECTSP_7:7,PP13,PP10,Y1;
end;
assume v in Lin(IIq12);
then consider lq12 be Linear_Combination of IIq12 such that
PP2: v = Sum(lq12) by VECTSP_7:7;
consider m12 be Element of INT.Ring, a12 be Element of F_Rat,
l12 be Linear_Combination of I1I2 such that
PP4: m12 <> 0 & m12 = a12 & l12 = (a12 * lq12) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq12) = Carrier(l12) by ZMODUL04:9;
PP5: a12*v = (MorphsZQ(V)).(Sum(l12)) by PP4,ZMODUL04:10,PP2;
consider v1, v2 be Vector of V such that
PP1: v1 in W1 & v2 in W2 & Sum(l12) = v1 + v2
by ZMODUL01:92,P3,ZMODUL02:64;
v1 in (Omega).W1 by PP1;
then consider l1 be Linear_Combination of I1 such that
PP13: v1 = Sum(l1) by ZMODUL02:64,P1;
v2 in (Omega).W2 by PP1;
then consider l2 be Linear_Combination of I2 such that
PP14: v2 = Sum(l2) by ZMODUL02:64,P2;
Y1: a12*v = (MorphsZQ(V)).(Sum(l1)) + (MorphsZQ(V)).(Sum(l2))
by ZMODUL04:def 6,PP1,PP5,PP13,PP14;
consider lq1 be Linear_Combination of Iq1 such that
PP15: l1 = lq1*(MorphsZQ(V))
& Carrier(lq1) = (MorphsZQ(V)).:(Carrier(l1)) by ZMODUL04:12;
consider lq2 be Linear_Combination of Iq2 such that
PP16: l2 = lq2*(MorphsZQ(V))
& Carrier(lq2) = (MorphsZQ(V)).:(Carrier(l2)) by ZMODUL04:12;
Y3: Sum(lq2) = (MorphsZQ(V)).(Sum(l2)) by PP16,ZMODUL04:7;
Y4: a12*v = Sum(lq1) + Sum(lq2) by Y1,PP15,ZMODUL04:7,Y3;
reconsider w1 = Sum(lq1) as Vector of Z_MQ_VectSp(V);
reconsider w2 = Sum(lq2) as Vector of Z_MQ_VectSp(V);
w1 in Lin(Iq1) & w2 in Lin(Iq2) by VECTSP_7:7; then
Y5: a12*v in Lin(Iq1) + Lin(Iq2) by Y4,VECTSP_5:1;
reconsider ra12 = a12 as Rational;
Y7: (ra12)"*(ra12) = 1 by XCMPLX_0:def 7,PP4;
(a12)" = (ra12)" by PP4,GAUSSINT:15; then
Y8: (a12)"*(a12) = 1.(F_Rat) by Y7;
(a12)"*((a12)*v) in Lin(Iq1) + Lin(Iq2) by Y5,VECTSP_4:21;
then 1.(F_Rat )*v in Lin(Iq1) + Lin(Iq2) by Y8,VECTSP_1:def 16;
hence v in Lin(Iq1) + Lin(Iq2);
end;
then
E1: Lin(Iq1) + Lin(Iq2) = Lin(IIq12) by VECTSP_4:30;
for v be Vector of Z_MQ_VectSp(V) holds
v in Lin(Iq1) /\ Lin(Iq2) iff v in Lin(Iq12)
proof
let v be Vector of Z_MQ_VectSp(V);
hereby
assume v in Lin(Iq1) /\ Lin(Iq2);
then
PP1: v in Lin(Iq1) & v in Lin(Iq2) by VECTSP_5:3;
consider lq1 be Linear_Combination of Iq1 such that
PP2: v = Sum(lq1) by VECTSP_7:7,PP1;
consider lq2 be Linear_Combination of Iq2 such that
PP3: v = Sum(lq2) by VECTSP_7:7,PP1;
consider m1 be Element of INT.Ring, a1 be Element of F_Rat,
l1 be Linear_Combination of I1 such that
PP4: m1 <> 0 & m1 = a1 & l1 = (a1 * lq1) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq1) = Carrier(l1) by ZMODUL04:9;
PP5:a1*v = (MorphsZQ(V)).(Sum(l1)) by PP4,ZMODUL04:10,PP2;
consider m2 be Element of INT.Ring, a2 be Element of F_Rat,
l2 be Linear_Combination of I2 such that
PP6: m2 <> 0 & m2 = a2 & l2 = (a2 * lq2) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq2) = Carrier(l2) by ZMODUL04:9;
PP7: a2*v = (MorphsZQ(V)).(Sum(l2)) by PP6,ZMODUL04:10,PP3;
PP8: (a1*a2)*v = a2*(a1*v) by VECTSP_1:def 16
.= (MorphsZQ(V)).(m2*Sum(l1)) by PP6,ZMODUL04:def 6,PP5;
PP9: (a1*a2)*v = a1*(a2*v) by VECTSP_1:def 16
.= (MorphsZQ(V)).(m1*Sum(l2)) by PP4,ZMODUL04:def 6,PP7;
MorphsZQ(V) is one-to-one by ZMODUL04:def 6;
then
PP10: m1*Sum(l2) = m2*Sum(l1) by FUNCT_2:19,PP8,PP9;
Sum(l1) in Lin(I1) by ZMODUL02:64;
then Sum(l1) in W1 by P1;
then
PP11: m2*Sum(l1) in W1 by ZMODUL01:37;
Sum(l2) in (Omega).W2 by P2,ZMODUL02:64;
then Sum(l2) in W2;
then m1*Sum(l2) in W2 by ZMODUL01:37;
then consider l12 be Linear_Combination of I12 such that
PP13: m2*Sum(l1) = Sum(l12) by ZMODUL02:64,P4,PP10,PP11,ZMODUL01:94;
reconsider r1 = 1 as Element of F_Rat;
reconsider i1 = 1 as Element of INT.Ring;
consider lq12 be Linear_Combination of Iq12 such that
PP14: l12 = lq12*(MorphsZQ(V))
& Carrier(lq12) = (MorphsZQ(V)).:(Carrier(l12)) by ZMODUL04:12;
r1 = 1.(F_Rat);
then l12 = (r1*lq12)*(MorphsZQ(V)) & 0 <> i1 & r1 = i1
by PP14; then
Y1: r1*(Sum(lq12)) = (MorphsZQ(V)).(Sum(l12)) by ZMODUL04:10;
reconsider ra1 = a1, ra2 = a2 as Rational;
Y3: (ra1*ra2)"*(ra1*ra2) = 1 by XCMPLX_0:def 7,PP4,PP6;
(a1*a2)" = (ra1*ra2)" by PP4,PP6,GAUSSINT:15; then
Y2: (a1*a2)"*(a1*a2) = 1.(F_Rat) by Y3;
X1X: r1*(Sum(lq12)) = 1.(F_Rat) * (Sum(lq12))
.= Sum(lq12);
(a1*a2)"*((a1*a2)* v)= ((a1*a2)"*(a1*a2)) * v by VECTSP_1:def 16
.= v by Y2;
hence v in Lin(Iq12) by X1X,VECTSP_4:21,VECTSP_7:7,PP8,PP13,Y1;
end;
assume v in Lin(Iq12);
then consider lq12 be Linear_Combination of Iq12 such that
PP2: v = Sum(lq12) by VECTSP_7:7;
consider m12 be Element of INT.Ring, a12 be Element of F_Rat,
l12 be Linear_Combination of I12 such that
PP4: m12 <> 0 & m12 = a12 & l12 = (a12 * lq12) *(MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq12) = Carrier(l12) by ZMODUL04:9;
PP5: a12*v = (MorphsZQ(V)).(Sum(l12)) by PP4,ZMODUL04:10,PP2;
Sum(l12) in (Omega).(W1 /\ W2) by P4,ZMODUL02:64;
then
PP1: Sum(l12) in W1 & Sum(l12) in W2 by ZMODUL01:94;
Sum(l12) in (Omega).W1 by PP1;
then consider l1 be Linear_Combination of I1 such that
PP13: Sum(l12) = Sum(l1) by ZMODUL02:64,P1;
Sum(l12) in (Omega).W2 by PP1;
then consider l2 be Linear_Combination of I2 such that
PP14: Sum(l12) = Sum(l2) by ZMODUL02:64,P2;
consider lq1 be Linear_Combination of Iq1 such that
PP15: l1 = lq1*(MorphsZQ(V))
& Carrier(lq1) = (MorphsZQ(V)).:(Carrier(l1)) by ZMODUL04:12;
consider lq2 be Linear_Combination of Iq2 such that
PP16: l2 = lq2*(MorphsZQ(V))
& Carrier(lq2) = (MorphsZQ(V)).:(Carrier(l2)) by ZMODUL04:12;
Y4: a12*v = Sum(lq1) & a12*v = Sum(lq2)
by PP5,PP13,PP14,PP15,PP16,ZMODUL04:7;
reconsider w1 = Sum(lq1) as Vector of Z_MQ_VectSp(V);
reconsider w2 = Sum(lq2) as Vector of Z_MQ_VectSp(V);
w1 in Lin(Iq1) & w2 in Lin(Iq2) by VECTSP_7:7; then
Y5: a12*v in Lin(Iq1) /\ Lin(Iq2) by Y4,VECTSP_5:3;
reconsider ra12 = a12 as Rational;
Y7: (ra12)"*(ra12) = 1 by XCMPLX_0:def 7,PP4;
(a12)" = (ra12)" by PP4,GAUSSINT:15; then
Y8: (a12)"*(a12) = 1.(F_Rat) by Y7;
(a12)"*((a12)*v) in Lin(Iq1) /\ Lin(Iq2) by Y5,VECTSP_4:21;
then ((a12)"*(a12))*v in Lin(Iq1) /\ Lin(Iq2) by VECTSP_1:def 16;
hence v in Lin(Iq1) /\ Lin(Iq2) by Y8;
end; then
Lin(Iq1) /\ Lin(Iq2) = Lin(Iq12) by VECTSP_4:30;
hence thesis by VECTSP_9:32,E1,D1,D2,D3,D4;
end;
theorem LmISRank51X:
for V being torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V holds
rank(W1 + W2) + rank(W1 /\ W2) = rank(W1) + rank(W2)
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V;
set W1W2 = W1 + W2;
reconsider W10 = W1 as finite-rank free Subspace of W1W2
by ZMODUL01:97;
reconsider W20 = W2 as finite-rank free Subspace of W1W2
by ZMODUL01:97;
R0: rank(W10+W20) + rank(W10 /\ W20) = rank(W10) + rank(W20)
by LmISRank501;
SB1: W10 + W20 is strict Subspace of V by ZMODUL01:42;
for v be Vector of V holds v in W10+W20 iff v in W1+W2
proof
let v be Vector of V;
hereby
assume v in (W10 + W20);
then consider v1, v2 be Vector of W1W2 such that
S11: v1 in W10 & v2 in W20 & v = v1 + v2 by ZMODUL01:92;
thus v in W1 + W2 by S11;
end;
assume v in W1 + W2;
then consider v1, v2 be Vector of V such that
S11: v1 in W1 & v2 in W2 & v = v1 + v2 by ZMODUL01:92;
v1 in the carrier of W10 & v2 in the carrier of W20 by S11;
then reconsider v11 = v1, v22 = v2 as Vector of W1W2 by ZMODUL01:25;
v11+v22 = v1 + v2 by ZMODUL01:28;
hence v in (W10+W20) by S11,ZMODUL01:92;
end;
then
R1: rank(W10 + W20) = rank(W1 + W2) by SB1,ZMODUL01:46;
SB2: W10/\ W20 is strict Subspace of V by ZMODUL01:42;
for v be Vector of V holds v in W10 /\ W20 iff v in W1 /\ W2
proof
let v be Vector of V;
hereby
assume X1: v in (W10 /\ W20);
then reconsider v0 = v as Vector of W10 /\ W20;
v0 in W10 & v0 in W20 by X1,ZMODUL01:94;
hence v in (W1/\ W2) by ZMODUL01:94;
end;
assume X1:v in (W1 /\ W2);
then reconsider v0 = v as Vector of W1 /\ W2;
v in W1 & v in W2 by X1,ZMODUL01:94;
hence v in (W10 /\ W20) by ZMODUL01:94;
end;
hence thesis by R1,R0,SB2,ZMODUL01:46;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V
st rank(W1 + W2) = rank(W2) holds
rank(W1 /\ W2) = rank(W1)
proof
let V be torsion-free Z_Module ,
W1, W2 be finite-rank free Subspace of V;
assume rank(W1 + W2) = rank(W2); then
rank(W2) + rank(W1 /\ W2) = rank(W1) + rank(W2) by LmISRank51X;
hence thesis;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V, v being Vector of V
st v <> 0.V & W1 /\ Lin{v} = (0).V & (W1 + W2) /\ Lin{v} = (0).V holds
rank((W1 + Lin{v}) /\ W2) = rank(W1 /\ W2)
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V,
v be Vector of V such that
A1: v <> 0.V & W1 /\ Lin{v} = (0).V & (W1 + W2) /\ Lin{v} = (0).V;
for u being Vector of V st u in (W1 /\ W2) holds
u in (W1 + Lin{v}) /\ W2
proof
let u be Vector of V such that
B1: u in (W1 /\ W2);
u in W1 & u in W2 by B1,ZMODUL01:94;
then u in W1 + Lin{v} & u in W2 by ZMODUL01:93;
hence thesis by ZMODUL01:94;
end;
then (W1 /\ W2) is Subspace of (W1 + Lin{v}) /\ W2 by ZMODUL01:44;
then A2: rank((W1 + Lin{v}) /\ W2) >= rank(W1 /\ W2) by ZMODUL05:2;
assume AS: rank((W1 + Lin{v}) /\ W2) <> rank(W1 /\ W2);
ex u being Vector of V st u in (W1 + Lin{v}) /\ W2 &
not u in W1 /\ W2
proof
assume for u being Vector of V st u in (W1 + Lin{v}) /\ W2
holds u in W1 /\ W2;
then (W1 + Lin{v}) /\ W2 is Subspace of W1 /\ W2 by ZMODUL01:44;
then rank((W1 + Lin{v}) /\ W2) <= rank(W1 /\ W2) by ZMODUL05:2;
hence contradiction by AS,A2,XXREAL_0:1;
end;
then consider u be Vector of V such that
A4: u in (W1 + Lin{v}) /\ W2 & not u in W1 /\ W2;
u in W1 + Lin{v} by A4,ZMODUL01:94;
then consider u1, u2 be Vector of V such that
A5: u1 in W1 & u2 in Lin{v} & u = u1 + u2 by ZMODUL01:92;
A6: u in W2 by A4,ZMODUL01:94;
A7: u2 <> 0.V by A4,A5,A6,ZMODUL01:94;
A8: -u1 in W1 by A5,ZMODUL01:38;
u - u1 = u2 + (u1 - u1) by RLVECT_1:28,A5
.= u2 + 0.V by RLVECT_1:15
.= u2;
then u2 in W1 + W2 by A6,A8,ZMODUL01:92;
hence contradiction by A1,A7,ZMODUL02:66,A5,ZMODUL01:94;
end;
theorem LmRank41:
for V being torsion-free Z_Module, W being finite-rank free Subspace of V,
v being Vector of V st v <> 0.V & W /\ Lin{v} <> (0).V holds
rank(W /\ Lin{v}) = 1
proof
let V be torsion-free Z_Module, W be finite-rank free Subspace of V,
v be Vector of V such that
A1: v <> 0.V & W /\ Lin{v} <> (0).V;
A2: rank(Lin{v}) = 1 by A1,LmRank0a;
A3: W /\ Lin{v} is Subspace of Lin{v} by ZMODUL01:105;
rank(W /\ Lin{v}) <> 0
proof
assume rank(W /\ Lin{v}) = 0;
then (Omega).(W /\ Lin{v}) = (0).(W /\ Lin{v}) by ZMODUL05:1
.= (0).V by ZMODUL01:51;
hence contradiction by A1;
end;
hence rank(W /\ Lin{v}) = 1 by A3,NAT_1:25,ZMODUL05:2,A2;
end;
theorem LmSumMod4:
for V being torsion-free Z_Module, W being finite-rank free Subspace of V,
v being Vector of V
st v <> 0.V & W /\ Lin{v} <> (0).V
holds
ex u being Vector of V st u <> 0.V & W /\ Lin{v} = Lin{u}
proof
let V be torsion-free Z_Module, W be finite-rank free Subspace of V,
v be Vector of V such that
A1: v <> 0.V & W /\ Lin{v} <> (0).V;
rank(W /\ Lin{v}) = 1 by A1,LmRank41;
then consider uu be Vector of W /\ Lin{v} such that
A2: uu <> 0.(W /\ Lin{v}) & (Omega).(W /\ Lin{v}) = Lin{uu} by ZMODUL05:5;
reconsider u = uu as Vector of V by ZMODUL01:25;
A3: u <> 0.V by A2,ZMODUL01:26;
(Omega).(W /\ Lin{v}) = Lin{u} by A2,ZMODUL03:20;
hence thesis by A3;
end;
theorem LmRank421:
for V being torsion-free Z_Module, W being finite-rank free Subspace of V,
u, v being Vector of V st W /\ Lin{v} = (0).V &
(W + Lin{u}) /\ Lin{v} <> (0).V
holds W /\ Lin{u} = (0).V
proof
let V be torsion-free Z_Module, W be finite-rank free Subspace of V,
u, v be Vector of V such that
A1: W /\ Lin{v} = (0).V & (W + Lin{u}) /\ Lin{v} <> (0).V;
consider x be Vector of V such that
A2: x in (W + Lin{u}) /\ Lin{v} & x <> 0.V by A1,ZMODUL04:24;
x in W + Lin{u} by A2,ZMODUL01:94;
then consider x1, x2 be Vector of V such that
A3: x1 in W & x2 in Lin{u} & x = x1 + x2 by ZMODUL01:92;
consider i be Element of INT.Ring such that
A5: x2 = i*u by A3,ThLin1;
assume W /\ Lin{u} <> (0).V;
then consider y be Vector of V such that
A7: y in W /\ Lin{u} & y <> 0.V by ZMODUL04:24;
y in Lin{u} by A7,ZMODUL01:94;
then consider j be Element of INT.Ring such that
A8: y = j*u by ThLin1;
A9: j*x1 in W by A3,ZMODUL01:37;
A10: j*x2 = (j*i)*u by VECTSP_1:def 16,A5
.= i*y by A8,VECTSP_1:def 16;
y in W by A7,ZMODUL01:94;
then j*x2 in W by A10,ZMODUL01:37;
then j*x1 + j*x2 in W by A9,ZMODUL01:36;
then A11: j*x in W by A3,VECTSP_1:def 14;
x in Lin{v} by A2,ZMODUL01:94;
then j*x in Lin{v} by ZMODUL01:37;
then A12: j*x in W /\ Lin{v} by A11,ZMODUL01:94;
j <> 0.INT.Ring by A7,A8,ZMODUL01:1;
hence contradiction by A1,A12,ZMODUL02:66,A2,ZMODUL01:def 7;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V, v being Vector of V
st rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V holds
W2 /\ Lin{v} <> (0).V
proof
let V be torsion-free Z_Module;
defpred P[Nat] means
for W1, W2 being finite-rank free Subspace of V, v being Vector of V
st rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V
& rank(W1) = $1 holds W2 /\ Lin{v} <> (0).V;
A1: P[0]
proof
let W1, W2 be finite-rank free Subspace of V, v be Vector of V;
assume
B1: rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V
& rank(W1) = 0; then
B2: (Omega).W1 = (0).W1 by ZMODUL05:1
.= (0).V by ZMODUL01:51;
reconsider WW2 = (Omega).W2 as strict Subspace of V by ZMODUL01:42;
B3: W1 + W2 = (0).V + WW2 by B2,ZMODUL04:22
.= WW2 by ZMODUL01:99;
(Omega).Lin{v} = Lin{v};
hence thesis by B3,ZMODUL04:23,B1;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let W1, W2 be finite-rank free Subspace of V, v be Vector of V;
assume
B2: rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V
& rank(W1) = n+1; then
consider I be finite Subset of V such that
B3: I is finite Subset of W1 &
I is linearly-independent & Lin(I) = (Omega).W1
& card(I) = n+1 by LmFree2;
BX1: I is Basis of W1
proof
reconsider II = I as Subset of W1 by B3;
(Omega).W1 = Lin(II) by ZMODUL03:20,B3;
hence thesis by VECTSP_7:def 3,B3,ZMODUL03:16;
end;
I is non empty by B3;
then consider u be object such that
B4: u in I by XBOOLE_0:def 1;
reconsider u as Vector of V by B4;
B5: (Omega).W1 = Lin(I \ {u}) + Lin{u} & u <> 0.V by B3,B4,ThLin8;
set Iu = I \ {u};
{u} is Subset of I by B4,SUBSET_1:41;
then B7: card(Iu) = n+1 - card({u}) by B3,CARD_2:44
.= n+1 - 1 by CARD_1:30
.= n;
reconsider Iu as finite Subset of V;
B8: Iu is linearly-independent by B3,XBOOLE_1:36,ZMODUL02:56;
reconsider LIu = Lin(Iu) as strict finite-rank free Subspace of V;
BX2: Iu is Basis of LIu by B8,ThLin7;
C1: for v being Vector of V st v in I holds W2 /\ Lin{v} <> (0).V
proof
let v be Vector of V such that
D1: v in I;
(W1 /\ W2) /\ Lin{v} = W1 /\ (W2 /\ Lin{v}) by ZMODUL01:104;
hence (W2 /\ Lin{v}) <> (0).V by ZMODUL01:107,B2,BX1,D1,LmISRank41;
end;
B10: rank(LIu /\ W2) = rank(LIu)
proof
C2: for v being Vector of V st v in Iu holds
W2 /\ Lin{v} <> (0).V by C1,ZFMISC_1:56;
for v being Vector of V st v in Iu holds
(LIu /\ W2) /\ Lin{v} <> (0).V
proof
let v be Vector of V such that
D1: v in Iu;
v in LIu & v in Lin{v} by D1,ZMODUL02:65,ZFMISC_1:31;
then D2: v in LIu /\ Lin{v} by ZMODUL01:94;
consider iv be Vector of V such that
D3: iv in W2 /\ Lin{v} & iv <> 0.V by ZMODUL04:24,C2,D1;
iv in Lin{v} by D3,ZMODUL01:94;
then consider i be Element of INT.Ring such that
D4: iv = i * v by ThLin1;
D5: iv in LIu /\ Lin{v} by D2,D4,ZMODUL01:37;
iv in W2 by D3,ZMODUL01:94;
then W2 /\ (LIu /\ Lin{v}) <> (0).V by D3,ZMODUL02:66,D5,ZMODUL01:94;
hence thesis by ZMODUL01:104;
end;
hence thesis by BX2,ThISRank2;
end;
(LIu + W2) /\ Lin{v} <> (0).V
proof
assume C1: (LIu + W2) /\ Lin{v} = (0).V;
reconsider WW1 = (Omega).W1 as strict Subspace of V by ZMODUL01:42;
reconsider WW2 = (Omega).W2 as strict Subspace of V by ZMODUL01:42;
C2: (Omega).(LIu + Lin{u}) = LIu + Lin{u};
C3: (LIu + W2) + Lin{u} = W2 + (LIu + Lin{u}) by ZMODUL01:96
.= WW2 + (LIu + Lin{u}) by C2,ZMODUL04:22
.= WW2 + WW1 by B3,B4,ThLin8
.= W2 + W1 by ZMODUL04:22;
then (LIu + W2) /\ Lin{u} = (0).V by C1,LmRank421,B2;
then C4: rank((LIu + W2) + Lin{u}) = rank(LIu + W2) + rank(Lin{u})
by ThRankDirectSum
.= rank(W2) + rank(Lin{u}) by B10,ThISRank4
.= rank(W2) + 1 by B5,LmRank0a;
rank((LIu + W2) + Lin{u}) = rank(W2) by B2,ThISRank4,C3;
hence contradiction by C4;
end;
hence thesis by B1,B10,B7,ZMODUL03:def 5,BX2;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let W1, W2 be finite-rank free Subspace of V, v be Vector of V;
assume rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V;
hence thesis by A3;
end;
theorem ThRankS5:
for V being torsion-free Z_Module,
W1, W2, W3 being finite-rank free Subspace of V
st rank(W1 + W2) = rank(W2) & W3 is Subspace of W1
holds rank(W3 + W2) = rank(W2)
proof
let V be torsion-free Z_Module,
W1, W2, W3 be finite-rank free Subspace of V such that
A1: rank(W1 + W2) = rank(W2) & W3 is Subspace of W1;
for v being Vector of V st v in W3 + W2 holds v in W1 + W2
proof
let v be Vector of V such that
B1: v in W3 + W2;
consider v1, v2 be Vector of V such that
B2: v1 in W3 & v2 in W2 & v = v1 + v2 by B1,ZMODUL01:92;
v1 in W1 by A1,B2,ZMODUL01:23;
hence thesis by B2,ZMODUL01:92;
end;
then W3 + W2 is Subspace of W1 + W2 by ZMODUL01:44;
then A2: rank(W3 + W2) <= rank(W1 + W2) by ZMODUL05:2;
W2 is Subspace of W3 + W2 by ZMODUL01:97;
then rank(W2) <= rank(W3 + W2) by ZMODUL05:2;
hence thesis by A1,A2,XXREAL_0:1;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V, I being Basis of W1
st rank(W1 + W2) = rank(W2)
holds (for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Subspace of V, I being Basis of W1 such that
A1: rank(W1 + W2) = rank(W2);
thus
for v being Vector of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V
proof
let v be Vector of V such that
C1: v in I;
reconsider II = I as linearly-independent Subset of V
by ZMODUL03:15,VECTSP_7:def 3;
v in II by C1;
then C2: v <> 0.V by ZMODUL02:57;
C3: W1 /\ Lin{v} <> (0).V
proof
D1: v in W1 by C1;
D2: v in Lin{v} by ZMODUL02:65,ZFMISC_1:31;
v in II by C1;
then v <> 0.V by ZMODUL02:57;
hence thesis by D2,ZMODUL02:66,D1,ZMODUL01:94;
end;
W2 /\ Lin{v} <> (0).V
proof
Lin{v} is Subspace of Lin(II) by ZMODUL02:70,C1,ZFMISC_1:31;
then Lin{v} is Subspace of Lin(I) by ZMODUL03:20;
then Lin{v} is Subspace of W1 by ZMODUL01:42;
then D1: rank(Lin{v} + W2) = rank(W2) by A1,ThRankS5;
assume W2 /\ Lin{v} = (0).V;
then rank(Lin{v} + W2) = rank(Lin{v}) + rank(W2) by ThRankDirectSum
.= rank(W2) + 1 by C2,LmRank0a;
hence contradiction by D1;
end;
hence thesis by C3,LmISRank21;
end;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace of V
st rank(W1 /\ W2) = rank(W1)
holds ex a being Element of INT.Ring st a (*) W1 is Subspace of W2
proof
let V be torsion-free Z_Module;
defpred P[Nat] means
for W1, W2 being finite-rank free Subspace of V
st rank(W1 /\ W2) = rank(W1) & rank(W1) = $1
holds ex a being Element of INT.Ring st a (*) W1 is Subspace of W2;
A1: P[0]
proof
let W1, W2 be finite-rank free Subspace of V such that
B1: rank(W1 /\ W2) = rank(W1) & rank(W1) = 0;
(Omega).W1 = (0).W1 by B1,ZMODUL05:1;
then B2: (Omega).W1 is Subspace of W2 by ZMODUL01:55;
take 1.INT.Ring;
thus thesis by B2,Th1V;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let W1, W2 be finite-rank free Subspace of V such that
B2: rank(W1 /\ W2) = rank(W1) & rank(W1) = n+1;
set I = the Basis of W1;
card(I) > 0 by ZMODUL03:def 5,B2;
then I <> {}(the carrier of W1);
then consider u be object such that
B3: u in I by XBOOLE_0:7;
reconsider u as Vector of W1 by B3;
reconsider uu = u as Vector of V by ZMODUL01:25;
B4: I is linearly-independent by VECTSP_7:def 3;
reconsider II = I as linearly-independent Subset of V
by ZMODUL03:15,VECTSP_7:def 3;
I \ {u} is linearly-independent by B4,XBOOLE_1:36,ZMODUL02:56;
then reconsider Iu = I \ {u} as linearly-independent Subset of V
by ZMODUL03:15;
(Omega).W1 = Lin(I) by VECTSP_7:def 3
.= Lin(II) by ZMODUL03:20;
then B5: (Omega).W1 = Lin(Iu) + Lin{uu} & Lin(Iu) /\ Lin{uu} = (0).V &
Lin(Iu) is free & Lin{uu} is free & uu <> 0.V by B3,ThLin8;
reconsider LIu = Lin(Iu) as finite-rank free Subspace of V;
B6: Iu is Basis of LIu by ThLin7;
B7: card(Iu) = card(I) - card{u} by B3,ZFMISC_1:31,CARD_2:44
.= rank(W1) - card{u} by ZMODUL03:def 5
.= n + 1 - 1 by B2,CARD_1:30
.= n;
for v being Vector of V st v in Iu holds
(Lin(Iu) /\ W2) /\ Lin{v} <> (0).V
proof
let v be Vector of V such that
C1: v in Iu;
v in I by C1,TARSKI:def 3,XBOOLE_1:36;
then (W1 /\ W2) /\ Lin{v} <> (0).V by B2,LmISRank41;
then W1 /\ (W2 /\ Lin{v}) <> (0).V by ZMODUL01:104;
then C2: W2 /\ Lin{v} <> (0).V by ZMODUL01:107;
C3: v <> 0.V by C1,ZMODUL02:57;
C4: v in Lin{v} by ZMODUL02:65,ZFMISC_1:31;
v in LIu by C1,ZMODUL02:65;
then LIu /\ Lin{v} <> (0).V by C3,ZMODUL02:66,C4,ZMODUL01:94;
hence thesis by C2,LmISRank21;
end;
then rank(LIu /\ W2) = rank(LIu) by B6,ThISRank2;
then consider a be Element of INT.Ring such that
B9: a (*) LIu is Subspace of W2 by B1,B7,B6,ZMODUL03:def 5;
W2 /\ Lin{uu} <> (0).V
proof
assume W2 /\ Lin{uu} = (0).V;
then (W1 /\ W2) /\ Lin{uu} = W1 /\ (0).V by ZMODUL01:104
.= (0).V by ZMODUL01:107;
hence contradiction by B3,B2,LmISRank41;
end;
then consider iu being Vector of V such that
B10: iu <> 0.V & W2 /\ Lin{uu} = Lin{iu} by B5,LmSumMod4;
B14: iu in Lin{iu} by ZMODUL02:65,ZFMISC_1:31;
then iu in Lin{uu} by B10,ZMODUL01:94;
then consider i be Element of INT.Ring such that
B11: iu = i * uu by ThLin1;
B12: (i * a) (*) W1 is Subspace of W2
proof
CX: (i * a) (*) W1 is Subspace of V by ZMODUL01:42;
for v being Vector of V st v in (i * a) (*) W1 holds v in W2
proof
let v be Vector of V such that
C1: v in (i * a) (*) W1;
consider vw be Vector of W1 such that
C2: v = (i * a) * vw by C1;
reconsider vvw = vw as Vector of V by ZMODUL01:25;
vvw in (Omega).W1;
then consider vw1, vw2 be Vector of V such that
C3: vw1 in LIu & vw2 in Lin{uu} & vvw = vw1 + vw2 by B5,ZMODUL01:92;
C4: v = (i * a) * vvw by C2,ZMODUL01:29
.= (i * a) * vw1 + (i * a) * vw2 by VECTSP_1:def 14,C3
.= a * (i * vw1) + (i * a) * vw2 by VECTSP_1:def 16
.= a * (i * vw1) + a * (i * vw2) by VECTSP_1:def 16;
consider i2 be Element of INT.Ring such that
C5: vw2 = i2 * uu by C3,ThLin1;
C6: i * vw2 = (i * i2) * uu by VECTSP_1:def 16,C5
.= i2 * iu by B11,VECTSP_1:def 16;
iu in W2 by B10,B14,ZMODUL01:94;
then i * vw2 in W2 by C6,ZMODUL01:37;
then C7: a * (i * vw2) in W2 by ZMODUL01:37;
C8: a (*) LIu is Subspace of V by ZMODUL01:42;
i * vw1 in LIu by C3,ZMODUL01:37;
then reconsider ivw1 = i * vw1 as Vector of LIu;
a * ivw1 in a * LIu;
then a * (i * vw1) in a (*) LIu by ZMODUL01:29;
then a * (i * vw1) in W2 by B9,C8,ZMODUL01:23;
hence thesis by C4,C7,ZMODUL01:36;
end;
hence thesis by CX,ZMODUL01:44;
end;
take i*a;
thus thesis by B12;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let W1, W2 be finite-rank free Subspace of V;
assume rank(W1 /\ W2) = rank(W1);
hence thesis by A3;
end;