let V be torsion-free Z_Module; for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) holds
rank (W1 + W2) = rank W2
defpred S1[ Nat] means for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = $1 holds
rank (W1 + W2) = rank W2;
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 I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = n + 1 holds
rank (W1 + W2) = rank W2let I be
Basis of
W1;
( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = n + 1 implies rank (W1 + W2) = rank W2 )
assume B2:
( ( for
v being
Vector of
V st
v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) &
rank W1 = n + 1 )
;
rank (W1 + W2) = rank W2
card I > 0
by ZMODUL03:def 5, B2;
then
I <> {} the
carrier of
W1
;
then consider u being
object such that B3:
u in I
by XBOOLE_0:7;
reconsider u =
u as
Vector of
W1 by B3;
reconsider uu =
u as
Vector of
V by ZMODUL01:25;
B4:
I is
linearly-independent
by VECTSP_7:def 3;
reconsider II =
I as
linearly-independent Subset of
V by ZMODUL03:15, VECTSP_7:def 3;
I \ {u} is
linearly-independent
by B4, XBOOLE_1:36, ZMODUL02:56;
then reconsider Iu =
I \ {u} as
linearly-independent Subset of
V by ZMODUL03:15;
BX2X:
(Omega). W1 =
Lin I
by VECTSP_7:def 3
.=
Lin II
by ZMODUL03:20
;
then BX2:
(
(Omega). W1 = (Lin Iu) + (Lin {uu}) &
(Lin Iu) /\ (Lin {uu}) = (0). V &
Lin Iu is
free &
Lin {uu} is
free &
uu <> 0. V )
by B3, ThLin8;
reconsider LIu =
Lin Iu as
free finite-rank Subspace of
V ;
B5:
Iu is
Basis of
(Lin Iu)
by ThLin7;
card Iu =
(card I) - (card {u})
by B3, ZFMISC_1:31, CARD_2:44
.=
(rank W1) - (card {u})
by ZMODUL03:def 5
.=
(n + 1) - 1
by B2, CARD_1:30
.=
n
;
then B6:
rank LIu = n
by B5, ZMODUL03:def 5;
B7X:
for
v being
Vector of
V st
v in Iu holds
((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V
(W1 /\ W2) /\ (Lin {uu}) = W1 /\ (W2 /\ (Lin {uu}))
by ZMODUL01:104;
then
W2 /\ (Lin {uu}) <> (0). V
by ZMODUL01:107, B2, B3;
then
(LIu + W2) /\ (Lin {uu}) <> (0). V
by ThIS1;
then B8:
rank ((LIu + W2) + (Lin {uu})) =
rank (LIu + W2)
by BX2, LmRank2
.=
rank W2
by B7X, B1, B5, B6
;
reconsider W1s =
(Omega). W1,
W2s =
(Omega). W2 as
strict free finite-rank Subspace of
V by ZMODUL01:42;
B9:
(Omega). W1s = W1s
;
(LIu + W2) + (Lin {uu}) =
((Lin {uu}) + LIu) + W2
by ZMODUL01:96
.=
W1s + W2
by BX2X, B3, ThLin8
.=
W1s + W2s
by B9, ZMODUL04:22
.=
W1 + W2
by ZMODUL04:22
;
hence
rank (W1 + W2) = rank W2
by B8;
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 I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) holds
rank (W1 + W2) = rank W2
let I be Basis of W1; ( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) implies rank (W1 + W2) = rank W2 )
assume A4:
for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
; rank (W1 + W2) = rank W2
set rk = rank W1;
S1[ rank W1]
by A3;
hence
rank (W1 + W2) = rank W2
by A4; verum