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 W1
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 W1;
A1:
S1[ 0 ]
by ThISRank1;
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 W1let 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 W1 )
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 W1
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;
BX1:
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 BX1, XBOOLE_1:36, ZMODUL02:56;
then reconsider Iu =
I \ {u} as
linearly-independent Subset of
V by ZMODUL03:15;
(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
B8:
(W1 /\ W2) /\ (Lin {uu}) <> (0). V
by B2, B3;
(LIu /\ W2) + (Lin {uu}) is
Subspace of
(W1 /\ W2) + (Lin {uu})
then B10X:
rank ((LIu /\ W2) + (Lin {uu})) <= rank ((W1 /\ W2) + (Lin {uu}))
by ZMODUL05:2;
(LIu /\ (Lin {uu})) /\ W2 = (0). V
by ZMODUL01:107, BX2;
then
(W2 /\ LIu) /\ (Lin {uu}) = (0). V
by ZMODUL01:104;
then rank ((LIu /\ W2) + (Lin {uu})) =
(rank (LIu /\ W2)) + (rank (Lin {uu}))
by ThRankDirectSum
.=
(rank (LIu /\ W2)) + 1
by BX2, LmRank0a
.=
(rank LIu) + 1
by B7X, B1, B5, B6
;
then B11:
(rank LIu) + 1
<= rank (W1 /\ W2)
by B10X, B8, BX2, LmRank2;
B12:
rank W1 =
rank ((Omega). W1)
by ZMODUL05:4
.=
(rank LIu) + (rank (Lin {uu}))
by BX2, ThRankDirectSum
.=
(rank LIu) + 1
by BX2, LmRank0a
;
W1 /\ W2 is
Subspace of
W1
by ZMODUL01:105;
then
rank (W1 /\ W2) <= rank W1
by ZMODUL05:2;
hence
rank (W1 /\ W2) = rank W1
by B12, B11, XXREAL_0:1;
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 W1
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 W1 )
assume A4:
for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V
; rank (W1 /\ W2) = rank W1
thus
rank (W1 /\ W2) = rank W1
by A4, A3; verum