let V be torsion-free Z_Module; for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V holds
W2 /\ (Lin {v}) <> (0). V
defpred S1[ Nat] means for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = $1 holds
W2 /\ (Lin {v}) <> (0). V;
A1:
S1[ 0 ]
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 W1,
W2 be
free finite-rank Subspace of
V;
for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = n + 1 holds
W2 /\ (Lin {v}) <> (0). Vlet v be
Vector of
V;
( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = n + 1 implies W2 /\ (Lin {v}) <> (0). V )
assume B2:
(
rank (W1 /\ W2) = rank W1 &
(W1 + W2) /\ (Lin {v}) <> (0). V &
rank W1 = n + 1 )
;
W2 /\ (Lin {v}) <> (0). V
then consider I being
finite Subset of
V such that B3:
(
I is
finite Subset of
W1 &
I is
linearly-independent &
Lin I = (Omega). W1 &
card I = n + 1 )
by LmFree2;
BX1:
I is
Basis of
W1
not
I is
empty
by B3;
then consider u being
object such that B4:
u in I
by XBOOLE_0:def 1;
reconsider u =
u as
Vector of
V by B4;
B5:
(
(Omega). W1 = (Lin (I \ {u})) + (Lin {u}) &
u <> 0. V )
by B3, B4, ThLin8;
set Iu =
I \ {u};
{u} is
Subset of
I
by B4, SUBSET_1:41;
then B7:
card (I \ {u}) =
(n + 1) - (card {u})
by B3, CARD_2:44
.=
(n + 1) - 1
by CARD_1:30
.=
n
;
reconsider Iu =
I \ {u} as
finite Subset of
V ;
B8:
Iu is
linearly-independent
by B3, XBOOLE_1:36, ZMODUL02:56;
reconsider LIu =
Lin Iu as
strict free finite-rank Subspace of
V ;
BX2:
Iu is
Basis of
LIu
by B8, ThLin7;
C1:
for
v being
Vector of
V st
v in I holds
W2 /\ (Lin {v}) <> (0). V
B10:
rank (LIu /\ W2) = rank LIu
proof
C2:
for
v being
Vector of
V st
v in Iu holds
W2 /\ (Lin {v}) <> (0). V
by C1, ZFMISC_1:56;
for
v being
Vector of
V st
v in Iu holds
(LIu /\ W2) /\ (Lin {v}) <> (0). V
proof
let v be
Vector of
V;
( v in Iu implies (LIu /\ W2) /\ (Lin {v}) <> (0). V )
assume D1:
v in Iu
;
(LIu /\ W2) /\ (Lin {v}) <> (0). V
(
v in LIu &
v in Lin {v} )
by D1, ZMODUL02:65, ZFMISC_1:31;
then D2:
v in LIu /\ (Lin {v})
by ZMODUL01:94;
consider iv being
Vector of
V such that D3:
(
iv in W2 /\ (Lin {v}) &
iv <> 0. V )
by ZMODUL04:24, C2, D1;
iv in Lin {v}
by D3, ZMODUL01:94;
then consider i being
Element of
INT.Ring such that D4:
iv = i * v
by ThLin1;
D5:
iv in LIu /\ (Lin {v})
by D2, D4, ZMODUL01:37;
iv in W2
by D3, ZMODUL01:94;
then
W2 /\ (LIu /\ (Lin {v})) <> (0). V
by D3, ZMODUL02:66, D5, ZMODUL01:94;
hence
(LIu /\ W2) /\ (Lin {v}) <> (0). V
by ZMODUL01:104;
verum
end;
hence
rank (LIu /\ W2) = rank LIu
by BX2, ThISRank2;
verum
end;
(LIu + W2) /\ (Lin {v}) <> (0). V
hence
W2 /\ (Lin {v}) <> (0). V
by B1, B10, B7, ZMODUL03:def 5, BX2;
verum
end;
A3:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let W1, W2 be free finite-rank Subspace of V; for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V holds
W2 /\ (Lin {v}) <> (0). V
let v be Vector of V; ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V implies W2 /\ (Lin {v}) <> (0). V )
assume
( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V )
; W2 /\ (Lin {v}) <> (0). V
hence
W2 /\ (Lin {v}) <> (0). V
by A3; verum