:: by Yuichi Futa and Yasunari Shidama

::

:: Received December 30, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

registration

let a, b be Element of F_Rat;

let x, y be Rational;

correctness

compatibility

( a = x & b = y implies a + b = x + y );

end;
let x, y be Rational;

correctness

compatibility

( a = x & b = y implies a + b = x + y );

proof end;

registration

let a, b be Element of F_Rat;

let x, y be Rational;

correctness

compatibility

( a = x & b = y implies a * b = x * y );

end;
let x, y be Rational;

correctness

compatibility

( a = x & b = y implies a * b = x * y );

proof end;

:: deftheorem defDivisibleVector defines divisible ZMODUL08:def 1 :

for V being Z_Module

for v being Vector of V holds

( v is divisible iff for a being Element of INT.Ring st a <> 0. INT.Ring holds

ex u being Vector of V st a * u = v );

for V being Z_Module

for v being Vector of V holds

( v is divisible iff for a being Element of INT.Ring st a <> 0. INT.Ring holds

ex u being Vector of V st a * u = v );

registration
end;

registration

let V be Z_Module;

correctness

existence

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

end;
correctness

existence

ex b

proof end;

theorem :: ZMODUL08:3

for V being Z_Module

for v being divisible Vector of V

for i being Element of INT.Ring holds i * v is divisible

for v being divisible Vector of V

for i being Element of INT.Ring holds i * v is divisible

proof end;

definition

let V be Z_Module;

end;
attr V is divisible means :defDivisibleModule: :: ZMODUL08:def 2

for v being Vector of V holds v is divisible ;

for v being Vector of V holds v is divisible ;

:: deftheorem defDivisibleModule defines divisible ZMODUL08:def 2 :

for V being Z_Module holds

( V is divisible iff for v being Vector of V holds v is divisible );

for V being Z_Module holds

( V is divisible iff for v being Vector of V holds v is divisible );

registration
end;

registration

existence

ex b_{1} being Z_Module st b_{1} is divisible ;

end;

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

correctness existence

ex b

proof end;

registration

let V be Z_Module;

existence

ex b_{1} being Submodule of V st b_{1} is divisible ;

end;
cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() divisible for Subspace of V;

correctness existence

ex b

proof end;

registration

existence

not for b_{1} being divisible Z_Module holds b_{1} is finitely-generated ;

end;

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() non finitely-generated divisible for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

LMLT12: addreal || INT = addint

proof end;

theorem :: ZMODUL08:5

ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) is Submodule of Rat-Module

proof end;

registration

existence

not for b_{1} being divisible Z_Module holds b_{1} is trivial ;

end;

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

correctness existence

not for b

proof end;

theorem LmFGND2: :: ZMODUL08:9

for V being Z_Module

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

not Lin {v} is divisible

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

not Lin {v} is divisible

proof end;

registration

let V be non trivial Z_Module;

let v be non zero Vector of V;

correctness

coherence

not Lin {v} is divisible ;

end;
let v be non zero Vector of V;

correctness

coherence

not Lin {v} is divisible ;

proof end;

registration

let V be non trivial Z_Module;

existence

not for b_{1} being Submodule of V holds b_{1} is divisible ;

end;
cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() non divisible for Subspace of V;

correctness existence

not for b

proof end;

theorem LmTM1: :: ZMODUL08:11

for V being non trivial torsion finitely-generated Z_Module ex i being Element of INT.Ring st

( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) )

( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) )

proof end;

theorem LmFGND41: :: ZMODUL08:12

for V being non trivial torsion finitely-generated Z_Module

for i being Element of INT.Ring st i <> 0 & ( for v being Vector of V holds i * v = 0. V ) holds

not V is divisible

for i being Element of INT.Ring st i <> 0 & ( for v being Vector of V holds i * v = 0. V ) holds

not V is divisible

proof end;

registration

existence

not for b_{1} being non trivial torsion finitely-generated Z_Module holds b_{1} is divisible ;

end;

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

correctness existence

not for b

proof end;

registration

coherence

for b_{1} being non trivial divisible Z_Module holds not b_{1} is finitely-generated ;

by ThFGND;

end;

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

correctness coherence

for b

by ThFGND;

registration

let V be non trivial non divisible Z_Module;

correctness

existence

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

end;
correctness

existence

not for b

proof end;

registration

let V be non trivial free finite-rank Z_Module;

correctness

coherence

not rank V is zero ;

end;
correctness

coherence

not rank V is zero ;

proof end;

theorem LmND1: :: ZMODUL08:15

for V being non trivial free Z_Module

for v being non zero Vector of V

for I being Basis of V ex L being Linear_Combination of I ex u being Vector of V st

( v = Sum L & u in I & L . u <> 0 )

for v being non zero Vector of V

for I being Basis of V ex L being Linear_Combination of I ex u being Vector of V st

( v = Sum L & u in I & L . u <> 0 )

proof end;

registration

coherence

for b_{1} being non trivial free Z_Module holds not b_{1} is divisible ;

end;

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

correctness coherence

for b

proof end;

theorem LmND2: :: ZMODUL08:17

for V being non trivial free Z_Module

for v being non zero Vector of V ex a being Element of INT.Ring st

( a in NAT & ( for b being Element of INT.Ring

for u being Vector of V st b > a holds

v <> b * u ) )

for v being non zero Vector of V ex a being Element of INT.Ring st

( a in NAT & ( for b being Element of INT.Ring

for u being Vector of V st b > a holds

v <> b * u ) )

proof end;

theorem :: ZMODUL08:18

for V being non trivial free Z_Module

for v being non zero Vector of V ex a being Element of INT.Ring ex u being Vector of V st

( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring

for w being Vector of V st b > a holds

v <> b * w ) )

for v being non zero Vector of V ex a being Element of INT.Ring ex u being Vector of V st

( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring

for w being Vector of V st b > a holds

v <> b * w ) )

proof end;

definition

let V be torsion-free Z_Module;

ex b_{1} being strict Z_Module st

( the carrier of b_{1} = rng (MorphsZQ V) & the ZeroF of b_{1} = zeroCoset V & the addF of b_{1} = (addCoset V) || (rng (MorphsZQ V)) & the lmult of b_{1} = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] )

for b_{1}, b_{2} being strict Z_Module st the carrier of b_{1} = rng (MorphsZQ V) & the ZeroF of b_{1} = zeroCoset V & the addF of b_{1} = (addCoset V) || (rng (MorphsZQ V)) & the lmult of b_{1} = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] & the carrier of b_{2} = rng (MorphsZQ V) & the ZeroF of b_{2} = zeroCoset V & the addF of b_{2} = (addCoset V) || (rng (MorphsZQ V)) & the lmult of b_{2} = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] holds

b_{1} = b_{2}
;

end;
func EMbedding V -> strict Z_Module means :defEmbedding: :: ZMODUL08:def 3

( the carrier of it = rng (MorphsZQ V) & the ZeroF of it = zeroCoset V & the addF of it = (addCoset V) || (rng (MorphsZQ V)) & the lmult of it = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] );

existence ( the carrier of it = rng (MorphsZQ V) & the ZeroF of it = zeroCoset V & the addF of it = (addCoset V) || (rng (MorphsZQ V)) & the lmult of it = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defEmbedding defines EMbedding ZMODUL08:def 3 :

for V being torsion-free Z_Module

for b_{2} being strict Z_Module holds

( b_{2} = EMbedding V iff ( the carrier of b_{2} = rng (MorphsZQ V) & the ZeroF of b_{2} = zeroCoset V & the addF of b_{2} = (addCoset V) || (rng (MorphsZQ V)) & the lmult of b_{2} = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] ) );

for V being torsion-free Z_Module

for b

( b

theorem SB01: :: ZMODUL08:19

for V being torsion-free Z_Module holds

( ( for x being Vector of (EMbedding V) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding V) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding V)

for v, w being Vector of (Z_MQ_VectSp V) st x = v & y = w holds

x + y = v + w ) & ( for i being Element of INT.Ring

for j being Element of F_Rat

for x being Vector of (EMbedding V)

for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds

i * x = j * v ) )

( ( for x being Vector of (EMbedding V) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding V) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding V)

for v, w being Vector of (Z_MQ_VectSp V) st x = v & y = w holds

x + y = v + w ) & ( for i being Element of INT.Ring

for j being Element of F_Rat

for x being Vector of (EMbedding V)

for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds

i * x = j * v ) )

proof end;

theorem SB02: :: ZMODUL08:20

for V being torsion-free Z_Module holds

( ( for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding V & w in EMbedding V holds

v + w in EMbedding V ) & ( for j being Element of F_Rat

for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds

j * v in EMbedding V ) )

( ( for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding V & w in EMbedding V holds

v + w in EMbedding V ) & ( for j being Element of F_Rat

for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds

j * v in EMbedding V ) )

proof end;

theorem SB03: :: ZMODUL08:21

for V being torsion-free Z_Module ex T being linear-transformation of V,(EMbedding V) st

( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((EQRZM V),[v,1]) ) )

( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((EQRZM V),[v,1]) ) )

proof end;

theorem :: ZMODUL08:22

for V being torsion-free Z_Module

for vv being Vector of (EMbedding V) ex v being Vector of V st (MorphsZQ V) . v = vv

for vv being Vector of (EMbedding V) ex v being Vector of V st (MorphsZQ V) . v = vv

proof end;

definition

let V be torsion-free Z_Module;

ex b_{1} being strict Z_Module st

( the carrier of b_{1} = Class (EQRZM V) & the ZeroF of b_{1} = zeroCoset V & the addF of b_{1} = addCoset V & the lmult of b_{1} = (lmultCoset V) | [:INT,(Class (EQRZM V)):] )

for b_{1}, b_{2} being strict Z_Module st the carrier of b_{1} = Class (EQRZM V) & the ZeroF of b_{1} = zeroCoset V & the addF of b_{1} = addCoset V & the lmult of b_{1} = (lmultCoset V) | [:INT,(Class (EQRZM V)):] & the carrier of b_{2} = Class (EQRZM V) & the ZeroF of b_{2} = zeroCoset V & the addF of b_{2} = addCoset V & the lmult of b_{2} = (lmultCoset V) | [:INT,(Class (EQRZM V)):] holds

b_{1} = b_{2}
;

end;
func DivisibleMod V -> strict Z_Module means :defDivisibleMod: :: ZMODUL08:def 4

( the carrier of it = Class (EQRZM V) & the ZeroF of it = zeroCoset V & the addF of it = addCoset V & the lmult of it = (lmultCoset V) | [:INT,(Class (EQRZM V)):] );

existence ( the carrier of it = Class (EQRZM V) & the ZeroF of it = zeroCoset V & the addF of it = addCoset V & the lmult of it = (lmultCoset V) | [:INT,(Class (EQRZM V)):] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defDivisibleMod defines DivisibleMod ZMODUL08:def 4 :

for V being torsion-free Z_Module

for b_{2} being strict Z_Module holds

( b_{2} = DivisibleMod V iff ( the carrier of b_{2} = Class (EQRZM V) & the ZeroF of b_{2} = zeroCoset V & the addF of b_{2} = addCoset V & the lmult of b_{2} = (lmultCoset V) | [:INT,(Class (EQRZM V)):] ) );

for V being torsion-free Z_Module

for b

( b

theorem ThDivisible1: :: ZMODUL08:23

for V being torsion-free Z_Module

for v being Vector of (DivisibleMod V)

for a being Element of INT.Ring st a <> 0 holds

ex u being Vector of (DivisibleMod V) st a * u = v

for v being Vector of (DivisibleMod V)

for a being Element of INT.Ring st a <> 0 holds

ex u being Vector of (DivisibleMod V) st a * u = v

proof end;

registration
end;

registration

let V be torsion-free finitely-generated Z_Module;

correctness

coherence

EMbedding V is finitely-generated ;

end;
correctness

coherence

EMbedding V is finitely-generated ;

proof end;

registration

let V be non trivial torsion-free Z_Module;

correctness

coherence

not EMbedding V is trivial ;

end;
correctness

coherence

not EMbedding V is trivial ;

proof end;

definition

let G be Field;

let V be VectSp of G;

let W be Subset of V;

let a be Element of G;

coherence

{ (a * u) where u is Vector of V : u in W } is Subset of V

end;
let V be VectSp of G;

let W be Subset of V;

let a be Element of G;

coherence

{ (a * u) where u is Vector of V : u in W } is Subset of V

proof end;

:: deftheorem defines * ZMODUL08:def 5 :

for G being Field

for V being VectSp of G

for W being Subset of V

for a being Element of G holds a * W = { (a * u) where u is Vector of V : u in W } ;

for G being Field

for V being VectSp of G

for W being Subset of V

for a being Element of G holds a * W = { (a * u) where u is Vector of V : u in W } ;

definition

let V be torsion-free Z_Module;

let r be Element of F_Rat;

ex b_{1} being strict Z_Module st

( the carrier of b_{1} = r * (rng (MorphsZQ V)) & the ZeroF of b_{1} = zeroCoset V & the addF of b_{1} = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of b_{1} = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] )

for b_{1}, b_{2} being strict Z_Module st the carrier of b_{1} = r * (rng (MorphsZQ V)) & the ZeroF of b_{1} = zeroCoset V & the addF of b_{1} = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of b_{1} = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] & the carrier of b_{2} = r * (rng (MorphsZQ V)) & the ZeroF of b_{2} = zeroCoset V & the addF of b_{2} = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of b_{2} = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] holds

b_{1} = b_{2}
;

end;
let r be Element of F_Rat;

func EMbedding (r,V) -> strict Z_Module means :defriV: :: ZMODUL08:def 6

( the carrier of it = r * (rng (MorphsZQ V)) & the ZeroF of it = zeroCoset V & the addF of it = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of it = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] );

existence ( the carrier of it = r * (rng (MorphsZQ V)) & the ZeroF of it = zeroCoset V & the addF of it = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of it = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defriV defines EMbedding ZMODUL08:def 6 :

for V being torsion-free Z_Module

for r being Element of F_Rat

for b_{3} being strict Z_Module holds

( b_{3} = EMbedding (r,V) iff ( the carrier of b_{3} = r * (rng (MorphsZQ V)) & the ZeroF of b_{3} = zeroCoset V & the addF of b_{3} = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of b_{3} = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] ) );

for V being torsion-free Z_Module

for r being Element of F_Rat

for b

( b

theorem rSB01: :: ZMODUL08:25

for V being torsion-free Z_Module

for r being Element of F_Rat holds

( ( for x being Vector of (EMbedding (r,V)) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding (r,V)) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding (r,V))

for v, w being Vector of (Z_MQ_VectSp V) st x = v & y = w holds

x + y = v + w ) & ( for i being Element of INT.Ring

for j being Element of F_Rat

for x being Vector of (EMbedding (r,V))

for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds

i * x = j * v ) )

for r being Element of F_Rat holds

( ( for x being Vector of (EMbedding (r,V)) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding (r,V)) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding (r,V))

for v, w being Vector of (Z_MQ_VectSp V) st x = v & y = w holds

x + y = v + w ) & ( for i being Element of INT.Ring

for j being Element of F_Rat

for x being Vector of (EMbedding (r,V))

for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds

i * x = j * v ) )

proof end;

theorem :: ZMODUL08:26

for V being torsion-free Z_Module

for r being Element of F_Rat holds

( ( for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding (r,V) & w in EMbedding (r,V) holds

v + w in EMbedding (r,V) ) & ( for j being Element of F_Rat

for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding (r,V) holds

j * v in EMbedding (r,V) ) )

for r being Element of F_Rat holds

( ( for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding (r,V) & w in EMbedding (r,V) holds

v + w in EMbedding (r,V) ) & ( for j being Element of F_Rat

for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding (r,V) holds

j * v in EMbedding (r,V) ) )

proof end;

theorem rSB03A: :: ZMODUL08:27

for V being torsion-free Z_Module

for r being Element of F_Rat st r <> 0. F_Rat holds

ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st

( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds

T . v = r * v ) & T is bijective )

for r being Element of F_Rat st r <> 0. F_Rat holds

ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st

( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds

T . v = r * v ) & T is bijective )

proof end;

theorem ThEM1: :: ZMODUL08:28

for V being torsion-free Z_Module

for v being Vector of V holds Class ((EQRZM V),[v,1]) in EMbedding V

for v being Vector of V holds Class ((EQRZM V),[v,1]) in EMbedding V

proof end;

theorem ThDM1: :: ZMODUL08:29

for V being torsion-free Z_Module

for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st

( a <> 0 & a * v in EMbedding V )

for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st

( a <> 0 & a * v in EMbedding V )

proof end;

registration
end;

registration
end;

theorem ThDivisibleX1: :: ZMODUL08:30

for V being torsion-free Z_Module holds

( ( for v being Vector of (Z_MQ_VectSp V) holds v is Vector of (DivisibleMod V) ) & ( for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) ) & 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) )

( ( for v being Vector of (Z_MQ_VectSp V) holds v is Vector of (DivisibleMod V) ) & ( for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) ) & 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) )

proof end;

theorem ThDivisibleX2: :: ZMODUL08:31

for V being torsion-free Z_Module holds

( ( for x, y being Vector of (DivisibleMod V)

for v, u being Vector of (Z_MQ_VectSp V) st x = v & y = u holds

x + y = v + u ) & ( for z being Vector of (DivisibleMod V)

for w being Vector of (Z_MQ_VectSp V)

for a being Element of INT.Ring

for aq being Element of F_Rat st z = w & a = aq holds

a * z = aq * w ) & ( for z being Vector of (DivisibleMod V)

for w being Vector of (Z_MQ_VectSp V)

for aq being Element of F_Rat

for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds

z = w ) & ( for x being Vector of (DivisibleMod V)

for v being Vector of (Z_MQ_VectSp V)

for r being Element of F_Rat

for m, n being Element of INT.Ring

for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds

ex y being Vector of (DivisibleMod V) st

( x = n * y & r * v = m * y ) ) )

( ( for x, y being Vector of (DivisibleMod V)

for v, u being Vector of (Z_MQ_VectSp V) st x = v & y = u holds

x + y = v + u ) & ( for z being Vector of (DivisibleMod V)

for w being Vector of (Z_MQ_VectSp V)

for a being Element of INT.Ring

for aq being Element of F_Rat st z = w & a = aq holds

a * z = aq * w ) & ( for z being Vector of (DivisibleMod V)

for w being Vector of (Z_MQ_VectSp V)

for aq being Element of F_Rat

for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds

z = w ) & ( for x being Vector of (DivisibleMod V)

for v being Vector of (Z_MQ_VectSp V)

for r being Element of F_Rat

for m, n being Element of INT.Ring

for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds

ex y being Vector of (DivisibleMod V) st

( x = n * y & r * v = m * y ) ) )

proof end;

theorem ThDivisible3: :: ZMODUL08:32

for V being torsion-free Z_Module

for r being Element of F_Rat holds EMbedding (r,V) is Submodule of DivisibleMod V

for r being Element of F_Rat holds EMbedding (r,V) is Submodule of DivisibleMod V

proof end;

registration

let V be torsion-free finitely-generated Z_Module;

let r be Element of F_Rat;

correctness

coherence

EMbedding (r,V) is finitely-generated ;

end;
let r be Element of F_Rat;

correctness

coherence

EMbedding (r,V) is finitely-generated ;

proof end;

registration

let V be non trivial torsion-free Z_Module;

let r be non zero Element of F_Rat;

correctness

coherence

not EMbedding (r,V) is trivial ;

end;
let r be non zero Element of F_Rat;

correctness

coherence

not EMbedding (r,V) is trivial ;

proof end;

registration

let V be torsion-free Z_Module;

let r be Element of F_Rat;

correctness

coherence

EMbedding (r,V) is torsion-free ;

by ThDivisible3;

end;
let r be Element of F_Rat;

correctness

coherence

EMbedding (r,V) is torsion-free ;

by ThDivisible3;

registration

let V be free Z_Module;

let r be non zero Element of F_Rat;

correctness

coherence

EMbedding (r,V) is free ;

end;
let r be non zero Element of F_Rat;

correctness

coherence

EMbedding (r,V) is free ;

proof end;

theorem :: ZMODUL08:33

for V being non trivial free Z_Module

for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st

( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds

not b * v in EMbedding V ) )

for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st

( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds

not b * v in EMbedding V ) )

proof end;

theorem ThRankrEM1: :: ZMODUL08:35

for V being free finite-rank Z_Module

for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank (EMbedding V)

for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank (EMbedding V)

proof end;

theorem :: ZMODUL08:36

for V being free finite-rank Z_Module

for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank V

for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank V

proof end;

registration

coherence

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

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 infinite torsion-free for ModuleStr over INT.Ring ;

correctness coherence

for b

proof end;

theorem :: ZMODUL08:37

for V being Z_Module ex A being Subset of V st

( A is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st

( a in NAT & a > 0 & a * v in Lin A ) ) )

( A is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st

( a in NAT & a > 0 & a * v in Lin A ) ) )

proof end;

theorem :: ZMODUL08:38

for V being non trivial torsion-free Z_Module

for v being non zero Vector of V

for A being Subset of V

for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds

ex L being Linear_Combination of A ex u being Vector of V st

( a * v = Sum L & u in A & L . u <> 0 )

for v being non zero Vector of V

for A being Subset of V

for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds

ex L being Linear_Combination of A ex u being Vector of V st

( a * v = Sum L & u in A & L . u <> 0 )

proof end;

theorem ThDivisible4: :: ZMODUL08:39

for V being torsion-free Z_Module

for i being non zero Integer

for r1, r2 being non zero Element of F_Rat st r2 = r1 / i holds

EMbedding (r1,V) is Submodule of EMbedding (r2,V)

for i being non zero Integer

for r1, r2 being non zero Element of F_Rat st r2 = r1 / i holds

EMbedding (r1,V) is Submodule of EMbedding (r2,V)

proof end;

theorem :: ZMODUL08:40

for V being free finite-rank Z_Module

for Z being Submodule of DivisibleMod V holds

( Z is finitely-generated iff ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V) )

for Z being Submodule of DivisibleMod V holds

( Z is finitely-generated iff ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V) )

proof end;