:: 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-2021 Association of Mizar Users

theorem Th1V: :: ZMODUL06:1

for R being commutative Ring
for V being LeftMod of R
for W being Subspace of V holds (1. R) (*) W = (Omega). W

proof end;

theorem :: ZMODUL06:2

for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Subspace of V holds W1 /\ W2 is Subspace of (W1 + W3) /\ W2

proof end;

theorem ThIS1: :: ZMODUL06:3

for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Subspace of V st W1 /\ W2 <> (0). V holds
(W1 + W3) /\ W2 <> (0). V

proof end;

theorem :: ZMODUL06:4

for V being Z_Module
for I, I1 being linearly-independent Subset of V st I1 c= I holds
(Lin (I \ I1)) /\ (Lin I1) = (0). V

proof end;

definition

let R be Ring;
let V be LeftMod of R;
let v be Vector of V;

attr v is torsion means :: ZMODUL06:def 1
ex i being Element of R st
( i <> 0. R & i * v = 0. V );

end;

:: deftheorem defines torsion ZMODUL06:def 1 :
for R being Ring
for V being LeftMod of R
for v being Vector of V holds
( v is torsion iff ex i being Element of R st
( i <> 0. R & i * v = 0. V ) );

ThTV1: for V being Z_Module holds 0. V is torsion

proof end;

registration

let V be Z_Module;

cluster 0. V -> torsion ;

coherence
0. V is torsion by ThTV1;

end;

theorem :: ZMODUL06:5

for V being Z_Module
for v, u being Vector of V st v is torsion & u is torsion holds
v + u is torsion

proof end;

theorem :: ZMODUL06:6

for V being Z_Module
for v being Vector of V st v is torsion holds
- v is torsion

proof end;

theorem :: ZMODUL06:7

for V being Z_Module
for v, u being Vector of V st v is torsion & u is torsion holds
v - u is torsion

proof end;

theorem :: ZMODUL06:8

for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring st v is torsion holds
i * v is torsion

proof end;

theorem ThTV6: :: ZMODUL06:9

for V being Z_Module
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
( v is torsion iff w is torsion )

proof end;

registration

let V be Z_Module;

cluster torsion for Element of the carrier of V;

correctness
existence
ex b₁ being Vector of V st b₁ is torsion ;

proof end;

end;

theorem :: ZMODUL06:10

for V being Z_Module
for v being Vector of V st not v is torsion holds
not - v is torsion

proof end;

theorem :: ZMODUL06:11

for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring st not v is torsion & i <> 0 holds
not i * v is torsion

proof end;

theorem ThnTV3: :: ZMODUL06:12

for V being Z_Module
for v being Vector of V holds
( not v is torsion iff {v} is linearly-independent )

proof end;

definition

let V be Z_Module;

attr V is torsion means :defTorsionModule: :: ZMODUL06:def 2
for v being Vector of V holds v is torsion ;

end;

:: deftheorem defTorsionModule defines torsion ZMODUL06:def 2 :
for V being Z_Module holds
( V is torsion iff for v being Vector of V holds v is torsion );

ThTZM: for V being Z_Module holds (0). V is torsion

proof end;

registration

let V be Z_Module;

cluster (0). V -> torsion ;

coherence
(0). V is torsion by ThTZM;

end;

registration

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() torsion for ModuleStr over INT.Ring ;

existence
ex b₁ being Z_Module st b₁ is torsion

proof end;

end;

theorem LMINTRNG1: :: ZMODUL06:13

for v being Element of INT.Ring
for v1 being Integer st v = v1 holds
for n being Nat holds (Nat-mult-left INT.Ring) . (n,v) = n * v1

proof end;

theorem LMINTRNG2: :: ZMODUL06:14

for x, v being Element of INT.Ring
for v1 being Integer st v = v1 holds
(Int-mult-left INT.Ring) . (x,v) = x * v1

proof end;

registration

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() non torsion for ModuleStr over INT.Ring ;

existence
not for b₁ being Z_Module holds b₁ is torsion

proof end;

end;

registration

let V be non torsion Z_Module;

cluster non torsion for Element of the carrier of V;

existence
not for b₁ being Vector of V holds b₁ is torsion by defTorsionModule;

end;

definition

let V be Z_Module;

attr V is torsion-free means :defTorsionFree: :: ZMODUL06:def 3
for v being Vector of V st v <> 0. V holds
not v is torsion ;

end;

:: deftheorem defTorsionFree defines torsion-free ZMODUL06:def 3 :
for V being Z_Module holds
( V is torsion-free iff for v being Vector of V st v <> 0. V holds
not v is torsion );

theorem ThMCTF: :: ZMODUL06:15

for V being Z_Module holds
( V is Mult-cancelable iff V is torsion-free )

proof end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Mult-cancelable -> Mult-cancelable torsion-free for ModuleStr over INT.Ring ;

coherence
for b₁ being Mult-cancelable Z_Module holds b₁ is torsion-free by ThMCTF;

end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed torsion-free -> Mult-cancelable torsion-free for ModuleStr over INT.Ring ;

coherence
for b₁ being torsion-free Z_Module holds b₁ is Mult-cancelable by ThMCTF;

end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free -> free torsion-free for ModuleStr over INT.Ring ;

coherence
for b₁ being free Z_Module holds b₁ is torsion-free ;

end;

registration

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() free torsion-free for ModuleStr over INT.Ring ;

existence
ex b₁ being Z_Module st
( b₁ is torsion-free & b₁ is free )

proof end;

end;

theorem :: ZMODUL06:16

for V being torsion-free Z_Module
for 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
for b₁ being Subspace of V holds b₁ is torsion-free

proof end;

end;

registration

let R be Ring;
let V be LeftMod of R;

cluster (0). V -> trivial ;

coherence
(0). V is trivial

proof end;

end;

registration

cluster non empty non trivial right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed torsion-free -> non trivial non torsion torsion-free for ModuleStr over INT.Ring ;

coherence
for b₁ being non trivial torsion-free Z_Module holds not b₁ is torsion

proof end;

end;

registration

let R be Ring;

cluster non empty trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() for ModuleStr over R;

existence
ex b₁ being LeftMod of R st b₁ is trivial

proof end;

end;

registration

let K be non empty non degenerated right_complementable associative distributive left_unital Abelian add-associative right_zeroed doubleLoopStr ;

cluster non empty non trivial right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for ModuleStr over K;

existence
ex b₁ being non trivial ModuleStr over K st
( b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is scalar-unital & b₁ is strict )

proof end;

end;

registration

let R be non degenerated Ring;
let V be non trivial LeftMod of R;

cluster non zero for Element of the carrier of V;

existence
not for b₁ being Vector of V holds b₁ is zero

proof end;

end;

theorem ThnTV4: :: ZMODUL06:17

for V being Z_Module
for v being Vector of V holds
( not v is torsion iff ( Lin {v} is free & v <> 0. V ) )

proof end;

registration

let V be non torsion Z_Module;
let v be non torsion Vector of V;

cluster Lin {v} -> free ;

coherence
Lin {v} is free by ThnTV4;

end;

theorem ThLIV1: :: ZMODUL06:18

for V being Z_Module
for A being Subset of V
for v being Vector of V st A is linearly-independent & v in A holds
not v is torsion

proof end;

theorem ThLin1: :: ZMODUL06:19

for V being Z_Module
for v being Vector of V
for u being object st u in Lin {v} holds
ex i being Element of INT.Ring st u = i * v

proof end;

theorem ThLin2: :: ZMODUL06:20

for V being Z_Module
for v being Vector of V holds v in Lin {v} by ZMODUL02:65, ZFMISC_1:31;

theorem :: ZMODUL06:21

for V being Z_Module
for v being Vector of V
for i being Element of INT.Ring holds i * v in Lin {v} by ZMODUL01:37, ThLin2;

ThLin4: for V being Z_Module
for A being Subset of V holds A is Subset of (Lin A)
by ZMODUL05:30;

theorem ThLin5: :: ZMODUL06:22

for R being Ring
for V being LeftMod of R holds Lin {(0. V)} = (0). V

proof end;

registration

let V be torsion-free Z_Module;
let v be Vector of V;

cluster Lin {v} -> free ;

coherence
Lin {v} is free

proof end;

end;

theorem :: ZMODUL06:23

for V being Z_Module
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 end;

ThLin7: for V being Z_Module
for A being linearly-independent Subset of V holds A is Basis of (Lin A)

proof end;

theorem ThLin8: :: ZMODUL06:24

for V being Z_Module
for W being free Subspace of V
for I being Subset of V
for 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 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 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 end;

theorem :: ZMODUL06:25

for V being Z_Module
for W being free Subspace of V ex A being Subset of V st
( A is Subset of W & A is linearly-independent & Lin A = (Omega). W )

proof end;

theorem LmFree2: :: ZMODUL06:26

for V being Z_Module
for W being free finite-rank Subspace of V 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 end;

theorem LmSumMod1: :: ZMODUL06:27

for V being torsion-free Z_Module
for v1, v2 being Vector of V st v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V holds
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) /\ (Lin {v2}) = Lin {u} )

proof end;

theorem LmSumMod2: :: ZMODUL06:28

for V being torsion-free Z_Module
for v1, v2 being Vector of V st v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V holds
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) + (Lin {v2}) = Lin {u} )

proof end;

theorem LmSumMod3: :: ZMODUL06:29

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for 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 end;

theorem LmSumModX: :: ZMODUL06:30

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
W + (Lin {v}) is free

proof end;

registration

let V be torsion-free Z_Module;
let v be Vector of V;
let W be free finite-rank Subspace of V;

cluster W + (Lin {v}) -> free ;

coherence
W + (Lin {v}) is free

proof 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
W + (Lin {v}) is finitely-generated

proof end;

end;

registration

let V be Z_Module;
let W1, W2 be finitely-generated Subspace of V;

cluster W1 + W2 -> finitely-generated ;

coherence
W1 + W2 is finitely-generated

proof end;

end;

theorem LMThSumMod2: :: ZMODUL06:31

for R being Ring
for V being LeftMod of R
for W being Subspace of V
for W1s, W2s being Subspace of W
for W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2

proof end;

registration

let V be torsion-free Z_Module;
let U1, U2 be free finite-rank Subspace of V;

cluster U1 + U2 -> free ;

correctness
coherence
U1 + U2 is free ;

proof end;

end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finitely-generated torsion-free -> free finitely-generated torsion-free for ModuleStr over INT.Ring ;

correctness
coherence
for b₁ being finitely-generated torsion-free Z_Module holds b₁ is free ;

proof end;

end;

theorem ThRankDirectSum: :: ZMODUL06:32

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st W1 /\ W2 = (0). V holds
rank (W1 + W2) = (rank W1) + (rank W2)

proof end;

theorem :: ZMODUL06:33

for V being free finite-rank Z_Module
for W1, W2 being free finite-rank Subspace of V st V is_the_direct_sum_of W1,W2 holds
rank V = (rank W1) + (rank W2)

proof end;

theorem ThISRank1: :: ZMODUL06:34

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V holds rank (W1 /\ W2) <= rank W1

proof end;

theorem LmRank0a: :: ZMODUL06:35

for V being torsion-free Z_Module
for v being Vector of V st v <> 0. V holds
rank (Lin {v}) = 1

proof end;

theorem :: ZMODUL06:36

for V being Z_Module holds rank ((0). V) = 0

proof end;

theorem LmRank1: :: ZMODUL06:37

for V being torsion-free Z_Module
for 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 end;

theorem LmRank2: :: ZMODUL06:38

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
rank (W + (Lin {v})) = rank W

proof end;

theorem LmISRank21: :: ZMODUL06:39

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st W1 /\ (Lin {v}) <> (0). V & W2 /\ (Lin {v}) <> (0). V holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V

proof end;

theorem ThTF3C: :: ZMODUL06:40

for R being Ring
for V, W being LeftMod of R
for T being linear-transformation of V,W
for A being Subset of V holds T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A))

proof end;

theorem HM0: :: ZMODUL06:41

for R being Ring
for X, Y being LeftMod of R
for L being linear-transformation of X,Y holds L . (0. X) = 0. Y

proof end;

theorem HM1: :: ZMODUL06:42

for R being Ring
for X, Y being LeftMod of R
for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )

proof end;

theorem :: ZMODUL06:43

for R being Ring
for X, Y being LeftMod of R
for l being Linear_Combination of X
for L being linear-transformation of X,Y st L is bijective holds
L @* l = l * (L ")

proof end;

theorem :: ZMODUL06:44

for R being Ring
for X, Y being LeftMod of R
for X0 being Subset of X
for L being linear-transformation of X,Y
for l being Linear_Combination of L .: X0 st X0 = the carrier of X & L is one-to-one holds
L # l = l * L

proof end;

HM4: for R being Ring
for X, Y being LeftMod of R
for A being Subset of X
for L being linear-transformation of X,Y st L is bijective & A is linearly-independent holds
L .: A is linearly-independent

proof end;

theorem HM6: :: ZMODUL06:45

for R being Ring
for X, Y being LeftMod of R
for A being Subset of X
for L being linear-transformation of X,Y st L is bijective holds
( A is linearly-independent iff L .: A is linearly-independent )

proof end;

theorem HM7: :: ZMODUL06:46

for R being Ring
for X, Y being LeftMod of R
for A being Subset of X
for T being linear-transformation of X,Y st T is bijective holds
T .: the carrier of (Lin A) = the carrier of (Lin (T .: A))

proof end;

theorem HM8: :: ZMODUL06:47

for R being Ring
for Y being LeftMod of R
for A being Subset of Y holds Lin A is strict Subspace of (Omega). Y

proof end;

HM9: for R being Ring
for X, Y being LeftMod of R
for T being linear-transformation of X,Y st T is bijective & X is free holds
Y is free

proof end;

theorem :: ZMODUL06:48

for R being Ring
for X, Y being LeftMod of R
for T being linear-transformation of X,Y st T is bijective holds
( X is free iff Y is free )

proof end;

HM11: for X, Y being free Z_Module
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y

proof end;

theorem HM12: :: ZMODUL06:49

for X, Y being free Z_Module
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective holds
( A is Basis of X iff T .: A is Basis of Y )

proof end;

HM13: for X, Y being free Z_Module
for T being linear-transformation of X,Y st T is bijective & X is finite-rank holds
Y is finite-rank

proof end;

theorem :: ZMODUL06:50

for X, Y being free Z_Module
for T being linear-transformation of X,Y st T is bijective holds
( X is finite-rank iff Y is finite-rank )

proof end;

theorem HM15: :: ZMODUL06:51

for X, Y being free finite-rank Z_Module
for T being linear-transformation of X,Y st T is bijective holds
rank X = rank Y

proof end;

theorem ThRankS1: :: ZMODUL06:52

for V being Z_Module
for W being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring holds
rank (a (*) W) = rank W

proof end;

theorem :: ZMODUL06:53

for V being Z_Module
for W1, W2, W3 being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 /\ W2) = rank (W1 /\ W2)

proof end;

theorem :: ZMODUL06:54

for V being torsion-free Z_Module
for W1, W2, W3 being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring & W3 = a (*) W1 holds
rank (W3 + W2) = rank (W1 + W2)

proof end;

theorem ThISRank2: :: ZMODUL06:55

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for 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 end;

theorem :: ZMODUL06:56

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for 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: :: ZMODUL06:57

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for 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 end;

theorem LmISRank42: :: ZMODUL06:58

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for 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 end;

theorem ThISRank4: :: ZMODUL06:59

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 holds
rank (W1 + W2) = rank W2

proof end;

theorem VECT9Th26: :: ZMODUL06:60

for G being Field
for V being VectSp of G
for A being Subset of V st A is linearly-independent holds
A is Basis of (Lin A)

proof end;

theorem LmISRank501: :: ZMODUL06:61

for V being free finite-rank Mult-cancelable Z_Module
for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)

proof end;

theorem LmISRank51X: :: ZMODUL06:62

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V holds (rank (W1 + W2)) + (rank (W1 /\ W2)) = (rank W1) + (rank W2)

proof end;

theorem :: ZMODUL06:63

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V st rank (W1 + W2) = rank W2 holds
rank (W1 /\ W2) = rank W1

proof end;

theorem :: ZMODUL06:64

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for 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 end;

theorem LmRank41: :: ZMODUL06:65

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
rank (W /\ (Lin {v})) = 1

proof end;

theorem LmSumMod4: :: ZMODUL06:66

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for 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 end;

theorem LmRank421: :: ZMODUL06:67

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for 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 end;

theorem :: ZMODUL06:68

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V holds
W2 /\ (Lin {v}) <> (0). V

proof end;

theorem ThRankS5: :: ZMODUL06:69

for V being torsion-free Z_Module
for W1, W2, W3 being free finite-rank Subspace of V st rank (W1 + W2) = rank W2 & W3 is Subspace of W1 holds
rank (W3 + W2) = rank W2

proof end;

theorem :: ZMODUL06:70

for V being torsion-free Z_Module
for W1, W2 being free finite-rank Subspace of V
for 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 end;

theorem :: ZMODUL06:71

for V being torsion-free Z_Module
for W1, W2 being free finite-rank 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 end;