let V be torsion-free Z_Module; for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
W + (Lin {v}) is free
defpred S1[ Nat] means for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = $1 + 1 holds
W + (Lin {v}) is free ;
A1:
S1[ 0 ]
proof
let W be
free finite-rank Subspace of
V;
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = 0 + 1 holds
W + (Lin {v}) is free let v be
Vector of
V;
( v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = 0 + 1 implies W + (Lin {v}) is free )
assume that B1:
(
v <> 0. V &
W /\ (Lin {v}) <> (0). V )
and B2:
rank W = 0 + 1
;
W + (Lin {v}) is free
ex
x being
Vector of
V st
(
x <> 0. V &
W + (Lin {v}) = Lin {x} )
proof
consider w being
Vector of
W such that C1:
(
w <> 0. W &
(Omega). W = Lin {w} )
by ZMODUL05:5, B2;
reconsider wv =
w as
Vector of
V by ZMODUL01:25;
C2:
(Omega). W = Lin {wv}
by C1, ZMODUL03:20;
C3:
(Omega). (Lin {v}) = Lin {v}
;
then C4:
W + (Lin {v}) = (Lin {wv}) + (Lin {v})
by C2, ZMODUL04:22;
C5:
(Lin {wv}) /\ (Lin {v}) <> (0). V
by B1, C2, C3, ZMODUL04:23;
wv <> 0. V
by C1, ZMODUL01:26;
hence
ex
x being
Vector of
V st
(
x <> 0. V &
W + (Lin {v}) = Lin {x} )
by B1, C4, C5, LmSumMod2;
verum
end;
then consider x being
Vector of
V such that B3:
(
x <> 0. V &
W + (Lin {v}) = Lin {x} )
;
thus
W + (Lin {v}) is
free
by B3;
verum
end;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume B1:
S1[
n]
;
S1[n + 1]
let W be
free finite-rank Subspace of
V;
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = (n + 1) + 1 holds
W + (Lin {v}) is free let v be
Vector of
V;
( v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = (n + 1) + 1 implies W + (Lin {v}) is free )
assume B2:
(
v <> 0. V &
W /\ (Lin {v}) <> (0). V &
rank W = (n + 1) + 1 )
;
W + (Lin {v}) is free
set I = the
Basis of
W;
B3:
card the
Basis of
W = n + 2
by B2, ZMODUL03:def 5;
then
the
Basis of
W <> {} the
carrier of
W
;
then consider w being
object such that B4:
w in the
Basis of
W
by XBOOLE_0:7;
reconsider w =
w as
Vector of
W by B4;
B5:
W is_the_direct_sum_of Lin ( the Basis of W \ {w}),
Lin {w}
by B4, ZMODUL04:33;
( the
Basis of
W c= the
carrier of
W & the
carrier of
W c= the
carrier of
V )
by VECTSP_4:def 2;
then
the
Basis of
W c= the
carrier of
V
;
then reconsider IV = the
Basis of
W as
finite Subset of
V ;
reconsider wv =
w as
Vector of
V by ZMODUL01:25;
B6:
Lin ( the Basis of W \ {w}) = Lin (IV \ {wv})
by ZMODUL03:20;
B7:
Lin {w} = Lin {wv}
by ZMODUL03:20;
then reconsider WLinIw =
Lin ( the Basis of W \ {w}),
WLinw =
Lin {w} as
Subspace of
(Lin (IV \ {wv})) + (Lin {wv}) by B6, ZMODUL01:97;
B8:
(Lin (IV \ {wv})) /\ (Lin {wv}) = (0). V
the
Basis of
W is
linearly-independent
by VECTSP_7:def 3;
then
the
Basis of
W \ {w} is
linearly-independent
by XBOOLE_1:36, ZMODUL02:56;
then B9:
IV \ {wv} is
linearly-independent
by ZMODUL03:15;
reconsider LinIw =
Lin (IV \ {wv}) as
free finite-rank Subspace of
V by B9;
reconsider IVwv =
IV \ {wv} as
Subset of
(Lin (IV \ {wv})) by ThLin4;
(Omega). (Lin (IV \ {wv})) = Lin IVwv
by ZMODUL03:20;
then B11:
IVwv is
Basis of
LinIw
by VECTSP_7:def 3, B9, ZMODUL03:16;
B12:
card ( the Basis of W \ {w}) =
(card the Basis of W) - (card {w})
by B4, ZFMISC_1:31, CARD_2:44
.=
(n + 2) - 1
by B3, CARD_1:30
.=
n + 1
;
B13:
rank LinIw = n + 1
by B12, B11, ZMODUL03:def 5;
B15:
(Lin (IV \ {wv})) + (Lin {v}) is
free
B16:
((Lin (IV \ {wv})) + (Lin {v})) + (Lin {wv}) is
free
B17:
(Omega). W = (Lin (IV \ {wv})) + (Lin {wv})
reconsider Ws =
(Omega). W as
strict Subspace of
V by ZMODUL01:42;
reconsider Linvs =
(Omega). (Lin {v}) as
strict Subspace of
V ;
((Lin (IV \ {wv})) + (Lin {v})) + (Lin {wv}) =
Ws + Linvs
by B17, ZMODUL01:96
.=
W + (Lin {v})
by ZMODUL04:22
;
hence
W + (Lin {v}) is
free
by B16;
verum
end;
A3:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let W be free finite-rank Subspace of V; for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
W + (Lin {v}) is free
let v be Vector of V; ( v <> 0. V & W /\ (Lin {v}) <> (0). V implies W + (Lin {v}) is free )
assume A4:
( v <> 0. V & W /\ (Lin {v}) <> (0). V )
; W + (Lin {v}) is free
set rk = rank W;
(rank W) - 1 is Nat
then reconsider rk1 = (rank W) - 1 as Nat ;
S1[rk1]
by A3;
hence
W + (Lin {v}) is free
by A4; verum