let V be non trivial torsion-free finitely-generated Z_Module; not V is divisible
consider I being finite Subset of V such that
A1:
I is Basis of V
by ZMODUL03:def 3;
(Omega). V <> (0). V
;
then
Lin I <> (0). V
by A1, VECTSP_7:def 3;
then
I <> {} the carrier of V
by ZMODUL02:67;
then consider v being object such that
A3:
v in I
by XBOOLE_0:def 1;
reconsider v = v as Vector of V by A3;
A4:
( V is Submodule of V & I is linearly-independent & (Omega). V = Lin I )
by A1, ZMODUL01:32, VECTSP_7:def 3;
then A5:
( (Omega). V = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
by A3, ZMODUL06:24;
(I \ {v}) \/ {v} =
I \/ {v}
by XBOOLE_1:39
.=
I
by A3, XBOOLE_1:12, ZFMISC_1:31
;
then B3:
Lin I = (Lin (I \ {v})) + (Lin {v})
by ZMODUL02:72;
reconsider i2 = 2 as Element of INT.Ring by INT_1:def 2;
not v is divisible
proof
assume
v is
divisible
;
contradiction
then consider u being
Vector of
V such that C1:
i2 * u = v
;
u in Lin I
by A4;
then consider u1,
u2 being
Vector of
V such that C2:
(
u1 in Lin (I \ {v}) &
u2 in Lin {v} &
u = u1 + u2 )
by B3, ZMODUL01:92;
consider iu2 being
Element of
INT.Ring such that C3:
u2 = iu2 * v
by C2, ZMODUL06:19;
C4:
u1 <> 0. V
v =
(i2 * u1) + (i2 * u2)
by C1, C2, VECTSP_1:def 14
.=
(i2 * u1) + ((i2 * iu2) * v)
by C3, VECTSP_1:def 16
;
then v - ((i2 * iu2) * v) =
(i2 * u1) + (((i2 * iu2) * v) - ((i2 * iu2) * v))
by RLVECT_1:28
.=
(i2 * u1) + (0. V)
by RLVECT_1:15
.=
i2 * u1
;
then
((1. INT.Ring) * v) - ((i2 * iu2) * v) = i2 * u1
by VECTSP_1:def 17;
then C5:
((1. INT.Ring) - (i2 * iu2)) * v = i2 * u1
by ZMODUL01:9;
i2 <> 0. INT.Ring
;
then C6:
i2 * u1 <> 0. V
by C4, ZMODUL01:def 7;
C7:
i2 * u1 in Lin (I \ {v})
by C2, ZMODUL01:37;
((1. INT.Ring) - (i2 * iu2)) * v in Lin {v}
by ZMODUL06:21;
hence
contradiction
by A5, C5, C6, C7, ZMODUL01:94, ZMODUL02:66;
verum
end;
hence
not V is divisible
; verum