let V be Z_Module; :: thesis: for I being finite Subset of V
for W being Submodule of V st ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
let I be finite Subset of V; :: thesis: for W being Submodule of V st ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
let W be Submodule of V; :: thesis: ( ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) implies ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) ) )
defpred S₁[ Nat] means for I being finite Subset of V st card I = $1 & ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) );
P1: S₁[ 0 ]

proof

let I be finite Subset of V; :: thesis: ( card I = 0 & ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) implies ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) ) )
assume that
A0: card I = 0 and
for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ; :: thesis: ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
reconsider a = 1. INT.Ring as Element of INT.Ring ;
take a ; :: thesis: ( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
thus a <> 0. INT.Ring ; :: thesis: for v being VECTOR of V st v in I holds
a * v in W
thus for v being VECTOR of V st v in I holds
a * v in W by A0; :: thesis: verum

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
let I be finite Subset of V; :: thesis: ( card I = n + 1 & ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) implies ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) ) )
assume that
A0: card I = n + 1 and
A1: for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ; :: thesis: ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
not I is empty by A0;
then consider u being object such that
B3: u in I by XBOOLE_0:def 1;
reconsider u = u as VECTOR of V by B3;
set Iu = I \ {u};
{u} is Subset of I by B3, SUBSET_1:41;
then B6: card (I \ {u}) = (n + 1) - (card {u}) by A0, CARD_2:44
.= (n + 1) - 1 by CARD_1:30
.= n ;
reconsider Iu = I \ {u} as finite Subset of V ;
for v being VECTOR of V st v in Iu holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W )

proof

let v be VECTOR of V; :: thesis: ( v in Iu implies ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) )
assume v in Iu ; :: thesis: ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W )
then ( v in I & not v in {u} ) by XBOOLE_0:def 5;
hence ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) by A1; :: thesis: verum

end;

then consider b being Element of INT.Ring such that
A3: b <> 0. INT.Ring and
A4: for v being VECTOR of V st v in Iu holds
b * v in W by B1, B6;
consider au being Element of INT.Ring such that
A5: au <> 0. INT.Ring and
A6: au * u in W by A1, B3;
set a = au * b;
take au * b ; :: thesis: ( au * b <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
(au * b) * v in W ) )
thus au * b <> 0. INT.Ring by A3, A5; :: thesis: for v being VECTOR of V st v in I holds
(au * b) * v in W
thus for v being VECTOR of V st v in I holds
(au * b) * v in W :: thesis: verum

proof

let v be VECTOR of V; :: thesis: ( v in I implies (au * b) * v in W )
assume D1: v in I ; :: thesis: (au * b) * v in W

per cases ( v = u or v <> u ) ;

suppose v = u ; :: thesis: (au * b) * v in W

then (au * b) * v = (b * au) * u
.= b * (au * u) by VECTSP_1:def 16 ;
hence (au * b) * v in W by A6, ZMODUL01:37; :: thesis: verum

end;

suppose v <> u ; :: thesis: (au * b) * v in W

then D3: b * v in W by A4, D1, ZFMISC_1:56;
(au * b) * v = au * (b * v) by VECTSP_1:def 16;
hence (au * b) * v in W by D3, ZMODUL01:37; :: thesis: verum

end;

end;

end;

end;

X1: for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
assume X2: for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ; :: thesis: ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )
card I is Nat ;
hence ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) ) by X1, X2; :: thesis: verum