:: by Yuichi Futa , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama

::

:: Received November 29, 2014

:: Copyright (c) 2014-2019 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

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

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

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

for I, I1 being linearly-independent Subset of V st I1 c= I holds

(Lin (I \ I1)) /\ (Lin I1) = (0). V

proof 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 ) );

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;

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

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

v + u 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

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

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 )

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;

correctness

existence

ex b_{1} being Vector of V st b_{1} is torsion ;

end;
correctness

existence

ex b

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

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 )

for v being Vector of V holds

( not v is torsion iff {v} is linearly-independent )

proof end;

definition

let V be Z_Module;

end;
attr V is torsion means :defTorsionModule: :: ZMODUL06:def 2

for v being Vector of V holds v is torsion ;

for v being Vector of V holds v is torsion ;

:: 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 );

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
end;

registration

ex b_{1} being Z_Module st b_{1} is torsion
end;

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

proof 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

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

for v1 being Integer st v = v1 holds

(Int-mult-left INT.Ring) . (x,v) = x * v1

proof end;

registration

not for b_{1} being Z_Module holds b_{1} is torsion
end;

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

proof end;

registration

let V be non torsion Z_Module;

existence

not for b_{1} being Vector of V holds b_{1} is torsion
by defTorsionModule;

end;
existence

not for b

definition

let V be Z_Module;

end;
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 ;

for v being Vector of V st v <> 0. V holds

not v is torsion ;

:: 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 );

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 );

registration

for b_{1} being Mult-cancelable Z_Module holds b_{1} is torsion-free
by ThMCTF;

end;

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

registration

for b_{1} being torsion-free Z_Module holds b_{1} is Mult-cancelable
by ThMCTF;

end;

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

registration

for b_{1} being free Z_Module holds b_{1} is torsion-free
;

end;

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

registration

ex b_{1} being Z_Module st

( b_{1} is torsion-free & b_{1} is free )
end;

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

( b

proof 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;

for v being Vector of V holds

( v is torsion iff v = 0. V ) by defTorsionFree;

registration

let V be torsion-free Z_Module;

coherence

for b_{1} being Subspace of V holds b_{1} is torsion-free

end;
coherence

for b

proof end;

registration

for b_{1} being non trivial torsion-free Z_Module holds not b_{1} is torsion
end;

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

proof end;

registration

let R be Ring;

ex b_{1} being LeftMod of R st b_{1} is trivial

end;
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

proof end;

registration

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

ex b_{1} being non trivial ModuleStr over K st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is strict )

end;
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

( b

proof end;

registration

let R be non degenerated Ring;

let V be non trivial LeftMod of R;

existence

not for b_{1} being Vector of V holds b_{1} is zero

end;
let V be non trivial LeftMod of R;

existence

not for b

proof 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 ) )

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;

coherence

Lin {v} is free by ThnTV4;

end;
let v be non torsion Vector of V;

coherence

Lin {v} is free by ThnTV4;

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

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

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 :: ZMODUL06:21

ThLin4: for V being Z_Module

for A being Subset of V holds A is Subset of (Lin A)

by ZMODUL05:30;

registration
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

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 )

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 )

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 )

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} )

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} )

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}) )

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

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;

coherence

W + (Lin {v}) is free

end;
let v be Vector of V;

let W be free finite-rank Subspace of V;

coherence

W + (Lin {v}) is free

proof end;

registration

let V be Z_Module;

let v be Vector of V;

let W be finitely-generated Subspace of V;

coherence

W + (Lin {v}) is finitely-generated

end;
let v be Vector of V;

let W be finitely-generated Subspace of V;

coherence

W + (Lin {v}) is finitely-generated

proof end;

registration

let V be Z_Module;

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

coherence

W1 + W2 is finitely-generated

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

coherence

W1 + W2 is finitely-generated

proof 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

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;

correctness

coherence

U1 + U2 is free ;

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

correctness

coherence

U1 + U2 is free ;

proof end;

registration

coherence

for b_{1} being finitely-generated torsion-free Z_Module holds b_{1} is free ;

end;

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

proof 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)

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)

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

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

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

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

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

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))

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

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 )

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 ")

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

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 )

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))

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

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 )

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 )

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 )

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

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

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)

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)

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

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

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

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

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

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)

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)

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)

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

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)

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

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} )

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

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

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

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

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

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;