let V be 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) )
let Z be Submodule of DivisibleMod V; ( Z is finitely-generated iff ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V) )
hereby ( ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V) implies Z is finitely-generated )
assume AS:
Z is
finitely-generated
;
ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V)then reconsider ZX =
Z as
free Submodule of
DivisibleMod V ;
reconsider ZX =
ZX as
free finite-rank Submodule of
DivisibleMod V by AS;
defpred S1[
Nat]
means for
ZZ being
free finite-rank Submodule of
DivisibleMod V st
rank ZZ = $1 holds
ex
i being non
zero Integer ex
r being non
zero Element of
F_Rat st
(
ZZ is
Submodule of
EMbedding (
r,
V) &
r = 1
/ i );
B1:
S1[
0 ]
proof
let ZZ be
free finite-rank Submodule of
DivisibleMod V;
( rank ZZ = 0 implies ex i being non zero Integer ex r being non zero Element of F_Rat st
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i ) )
assume C0:
rank ZZ = 0
;
ex i being non zero Integer ex r being non zero Element of F_Rat st
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i )
reconsider i = 1 as non
zero Integer ;
reconsider r = 1
/ i as
Element of
F_Rat ;
not
r is
zero
;
then reconsider r = 1
/ i as non
zero Element of
F_Rat ;
C1:
EMbedding (
r,
V) is
Submodule of
DivisibleMod V
by ThDivisible3;
C2:
(Omega). ZZ =
(0). ZZ
by C0, ZMODUL05:1
.=
(0). (EMbedding (r,V))
by C1, ZMODUL01:52
;
take
i
;
ex r being non zero Element of F_Rat st
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i )
take
r
;
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i )
ZZ is
Submodule of
(Omega). ZZ
by VECTSP_4:41;
hence
(
ZZ is
Submodule of
EMbedding (
r,
V) &
r = 1
/ i )
by C2, ZMODUL01:42;
verum
end; B2:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume C1:
S1[
n]
;
S1[n + 1]
let ZZ be
free finite-rank Submodule of
DivisibleMod V;
( rank ZZ = n + 1 implies ex i being non zero Integer ex r being non zero Element of F_Rat st
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i ) )
assume C0:
rank ZZ = n + 1
;
ex i being non zero Integer ex r being non zero Element of F_Rat st
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i )
set I = the
Basis of
ZZ;
C2:
card the
Basis of
ZZ = n + 1
by C0, ZMODUL03:def 5;
then
the
Basis of
ZZ <> {}
;
then consider v being
object such that C3:
v in the
Basis of
ZZ
by XBOOLE_0:def 1;
reconsider v =
v as
Vector of
ZZ by C3;
C4:
ZZ is_the_direct_sum_of Lin ( the Basis of ZZ \ {v}),
Lin {v}
by C3, ZMODUL04:33;
C5:
card ( the Basis of ZZ \ {v}) =
(card the Basis of ZZ) - (card {v})
by C3, CARD_2:44, ZFMISC_1:31
.=
(card the Basis of ZZ) - 1
by CARD_1:30
.=
n
by C2
;
the
Basis of
ZZ is
linearly-independent
by VECTSP_7:def 3;
then
the
Basis of
ZZ \ {v} is
linearly-independent
by XBOOLE_1:36, ZMODUL02:56;
then C6:
rank (Lin ( the Basis of ZZ \ {v})) = n
by C5, ZMODUL05:3;
Lin ( the Basis of ZZ \ {v}) is
Submodule of
DivisibleMod V
by ZMODUL01:42;
then consider ix being non
zero Integer,
rx being non
zero Element of
F_Rat such that C7:
(
Lin ( the Basis of ZZ \ {v}) is
Submodule of
EMbedding (
rx,
V) &
rx = 1
/ ix )
by C1, C6;
ex
iy being non
zero Integer ex
ry being non
zero Element of
F_Rat st
(
Lin {v} is
Submodule of
EMbedding (
ry,
V) &
ry = 1
/ iy )
proof
reconsider vv =
v as
Vector of
(DivisibleMod V) by ZMODUL01:25;
consider iiy being
Element of
INT.Ring such that D1:
(
iiy <> 0. INT.Ring &
iiy * vv in EMbedding V )
by ThDM1;
reconsider iy =
iiy as
Integer ;
reconsider iy =
iy as non
zero Integer by D1;
reconsider ry = 1
/ iy as
Element of
F_Rat by RAT_1:def 1;
not
ry is
zero
;
then reconsider ry =
ry as non
zero Element of
F_Rat ;
take
iy
;
ex ry being non zero Element of F_Rat st
( Lin {v} is Submodule of EMbedding (ry,V) & ry = 1 / iy )
take
ry
;
( Lin {v} is Submodule of EMbedding (ry,V) & ry = 1 / iy )
reconsider ivv =
iiy * vv as
Vector of
(Z_MQ_VectSp V) by D1, SB01;
reconsider iv =
ivv as
Vector of
(DivisibleMod V) ;
consider T being
linear-transformation of
(EMbedding V),
(EMbedding (ry,V)) such that D7:
( ( for
v being
Element of
(Z_MQ_VectSp V) st
v in EMbedding V holds
T . v = ry * v ) &
T is
bijective )
by rSB03A;
consider y being
Vector of
(DivisibleMod V) such that D8:
(
iv = iiy * y &
ry * ivv = (1. INT.Ring) * y )
by ThDivisibleX2;
T . ivv =
ry * ivv
by D1, D7
.=
y
by D8, VECTSP_1:def 17
.=
vv
by D8, ZMODUL01:10
;
then D3:
vv in EMbedding (
ry,
V)
by D1, FUNCT_2:5;
D4:
EMbedding (
ry,
V) is
Submodule of
DivisibleMod V
by ThDivisible3;
D5:
for
x being
Vector of
(DivisibleMod V) st
x in Lin {v} holds
x in EMbedding (
ry,
V)
Lin {v} is
Submodule of
DivisibleMod V
by ZMODUL01:42;
hence
(
Lin {v} is
Submodule of
EMbedding (
ry,
V) &
ry = 1
/ iy )
by D4, D5, ZMODUL01:44;
verum
end;
then consider iy being non
zero Integer,
ry being non
zero Element of
F_Rat such that C8:
(
Lin {v} is
Submodule of
EMbedding (
ry,
V) &
ry = 1
/ iy )
;
reconsider i =
ix * iy as non
zero Integer ;
reconsider r = 1
/ i as
Element of
F_Rat by RAT_1:def 1;
not
r is
zero
;
then reconsider r =
r as non
zero Element of
F_Rat ;
take
i
;
ex r being non zero Element of F_Rat st
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i )
take
r
;
( ZZ is Submodule of EMbedding (r,V) & r = 1 / i )
r = rx / iy
by C7, XCMPLX_1:78;
then
EMbedding (
rx,
V) is
Submodule of
EMbedding (
r,
V)
by ThDivisible4;
then C9:
Lin ( the Basis of ZZ \ {v}) is
Submodule of
EMbedding (
r,
V)
by C7, ZMODUL01:42;
r = ry / ix
by C8, XCMPLX_1:78;
then
EMbedding (
ry,
V) is
Submodule of
EMbedding (
r,
V)
by ThDivisible4;
then C13:
Lin {v} is
Submodule of
EMbedding (
r,
V)
by C8, ZMODUL01:42;
reconsider LIv =
Lin ( the Basis of ZZ \ {v}),
Lv =
Lin {v} as
Submodule of
DivisibleMod V by ZMODUL01:42;
reconsider EMr =
EMbedding (
r,
V) as
Submodule of
DivisibleMod V by ThDivisible3;
C11:
LIv + Lv is
Submodule of
EMr
by C9, C13, ZMODUL02:76;
C12:
(Omega). ZZ is
Submodule of
EMbedding (
r,
V)
by C4, C11, ZMODUL06:31;
ZZ is
Submodule of
(Omega). ZZ
by VECTSP_4:41;
hence
(
ZZ is
Submodule of
EMbedding (
r,
V) &
r = 1
/ i )
by C12, ZMODUL01:42;
verum
end; B3:
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(B1, B2);
set n =
rank ZX;
S1[
rank ZX]
by B3;
then consider i being non
zero Integer,
r being non
zero Element of
F_Rat such that B4:
(
Z is
Submodule of
EMbedding (
r,
V) &
r = 1
/ i )
;
thus
ex
r being non
zero Element of
F_Rat st
Z is
Submodule of
EMbedding (
r,
V)
by B4;
verum
end;
given r being non zero Element of F_Rat such that B1:
Z is Submodule of EMbedding (r,V)
; Z is finitely-generated
thus
Z is finitely-generated
by B1; verum