let V be non trivial torsion finitely-generated Z_Module; :: thesis: ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) )
defpred S1[ Nat] means for I being finite Subset of V st card I = $1 holds
ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) );
P1: S1[ 0 ]
proof
let I be finite Subset of V; :: thesis: ( card I = 0 implies ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) ) )
assume card I = 0 ; :: thesis: ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) )
then A2: I = {} the carrier of V ;
reconsider i = 1 as Element of INT.Ring ;
take i ; :: thesis: ( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) )
thus i <> 0 ; :: thesis: for v being Vector of V st v in Lin I holds
i * v = 0. V
thus for v being Vector of V st v in Lin I holds
i * v = 0. V :: thesis: verum
proof
let v be Vector of V; :: thesis: ( v in Lin I implies i * v = 0. V )
assume v in Lin I ; :: thesis: i * v = 0. V
then v in (0). V by A2, ZMODUL02:67;
then v in {(0. V)} by VECTSP_4:def 3;
then v = 0. V by TARSKI:def 1;
hence i * v = 0. V by ZMODUL01:1; :: thesis: verum
end;
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A0: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let I be finite Subset of V; :: thesis: ( card I = n + 1 implies ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) ) )
assume A1: card I = n + 1 ; :: thesis: ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) )
then I <> {} ;
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;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A3, ZFMISC_1:40 ;
then A4: Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;
A5: card (I \ {v}) = (card I) - (card {v}) by A3, CARD_2:44, ZFMISC_1:31
.= (card I) - 1 by CARD_1:30
.= n by A1 ;
reconsider J = I \ {v} as finite Subset of V ;
consider j being Element of INT.Ring such that
B8: ( j <> 0 & ( for v being Vector of V st v in Lin J holds
j * v = 0. V ) ) by A0, A5;
v is torsion by ZMODUL06:def 2;
then consider k being Element of INT.Ring such that
A8: ( k <> 0 & k * v = 0. V ) ;
reconsider i = j * k as Element of INT.Ring ;
take i ; :: thesis: ( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) )
thus i <> 0 by A8, B8; :: thesis: for v being Vector of V st v in Lin I holds
i * v = 0. V
thus for w being Vector of V st w in Lin I holds
i * w = 0. V :: thesis: verum
proof
let w be Vector of V; :: thesis: ( w in Lin I implies i * w = 0. V )
assume w in Lin I ; :: thesis: i * w = 0. V
then consider u1, u2 being Vector of V such that
A10: ( u1 in Lin (I \ {v}) & u2 in Lin {v} & w = u1 + u2 ) by A4, ZMODUL01:92;
consider iu2 being Element of INT.Ring such that
A11: u2 = iu2 * v by A10, ZMODUL06:19;
thus i * w = (i * u1) + (i * u2) by A10, VECTSP_1:def 14
.= (k * (j * u1)) + ((j * k) * u2) by VECTSP_1:def 16
.= (k * (0. V)) + ((j * k) * u2) by B8, A10
.= (k * (0. V)) + (j * (k * u2)) by VECTSP_1:def 16
.= (k * (0. V)) + (j * ((k * iu2) * v)) by A11, VECTSP_1:def 16
.= (k * (0. V)) + (j * (iu2 * (k * v))) by VECTSP_1:def 16
.= (0. V) + (j * (iu2 * (0. V))) by A8, ZMODUL01:1
.= (0. V) + (j * (0. V)) by ZMODUL01:1
.= 0. V by ZMODUL01:1 ; :: thesis: verum
end;
end;
end;
X1: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
 consider I being finite Subset of V such that
A1: Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by ZMODUL03:def 4;
card I is Nat ;
then consider i being Element of INT.Ring such that
X2: ( i <> 0 & ( for v being Vector of V st v in Lin I holds
i * v = 0. V ) ) by X1;
take i ; :: thesis: ( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) )
thus i <> 0 by X2; :: thesis: for v being Vector of V holds i * v = 0. V
thus for v being Vector of V holds i * v = 0. V :: thesis: verum
proof
let v be Vector of V; :: thesis: i * v = 0. V
v in Lin I by A1;
hence i * v = 0. V by X2; :: thesis: verum
end;