let V be torsion-free Z_Module; for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 holds
ex a being Element of INT.Ring st a (*) W1 is Subspace of W2
defpred S1[ Nat] means for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 & rank W1 = $1 holds
ex a being Element of INT.Ring st a (*) W1 is Subspace of 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;
( rank (W1 /\ W2) = rank W1 & rank W1 = n + 1 implies ex a being Element of INT.Ring st a (*) W1 is Subspace of W2 )
assume B2:
(
rank (W1 /\ W2) = rank W1 &
rank W1 = n + 1 )
;
ex a being Element of INT.Ring st a (*) W1 is Subspace of W2
set I = the
Basis of
W1;
card the
Basis of
W1 > 0
by ZMODUL03:def 5, B2;
then
the
Basis of
W1 <> {} the
carrier of
W1
;
then consider u being
object such that B3:
u in the
Basis of
W1
by XBOOLE_0:7;
reconsider u =
u as
Vector of
W1 by B3;
reconsider uu =
u as
Vector of
V by ZMODUL01:25;
B4:
the
Basis of
W1 is
linearly-independent
by VECTSP_7:def 3;
reconsider II = the
Basis of
W1 as
linearly-independent Subset of
V by ZMODUL03:15, VECTSP_7:def 3;
the
Basis of
W1 \ {u} is
linearly-independent
by B4, XBOOLE_1:36, ZMODUL02:56;
then reconsider Iu = the
Basis of
W1 \ {u} as
linearly-independent Subset of
V by ZMODUL03:15;
(Omega). W1 =
Lin the
Basis of
W1
by VECTSP_7:def 3
.=
Lin II
by ZMODUL03:20
;
then B5:
(
(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 ;
B6:
Iu is
Basis of
LIu
by ThLin7;
B7:
card Iu =
(card the Basis of W1) - (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
;
for
v being
Vector of
V st
v in Iu holds
((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V
proof
let v be
Vector of
V;
( v in Iu implies ((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V )
assume C1:
v in Iu
;
((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V
v in the
Basis of
W1
by C1, TARSKI:def 3, XBOOLE_1:36;
then
(W1 /\ W2) /\ (Lin {v}) <> (0). V
by B2, LmISRank41;
then
W1 /\ (W2 /\ (Lin {v})) <> (0). V
by ZMODUL01:104;
then C2:
W2 /\ (Lin {v}) <> (0). V
by ZMODUL01:107;
C3:
v <> 0. V
by C1, ZMODUL02:57;
C4:
v in Lin {v}
by ZMODUL02:65, ZFMISC_1:31;
v in LIu
by C1, ZMODUL02:65;
then
LIu /\ (Lin {v}) <> (0). V
by C3, ZMODUL02:66, C4, ZMODUL01:94;
hence
((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V
by C2, LmISRank21;
verum
end;
then
rank (LIu /\ W2) = rank LIu
by B6, ThISRank2;
then consider a being
Element of
INT.Ring such that B9:
a (*) LIu is
Subspace of
W2
by B1, B7, B6, ZMODUL03:def 5;
W2 /\ (Lin {uu}) <> (0). V
then consider iu being
Vector of
V such that B10:
(
iu <> 0. V &
W2 /\ (Lin {uu}) = Lin {iu} )
by B5, LmSumMod4;
B14:
iu in Lin {iu}
by ZMODUL02:65, ZFMISC_1:31;
then
iu in Lin {uu}
by B10, ZMODUL01:94;
then consider i being
Element of
INT.Ring such that B11:
iu = i * uu
by ThLin1;
B12:
(i * a) (*) W1 is
Subspace of
W2
proof
CX:
(i * a) (*) W1 is
Subspace of
V
by ZMODUL01:42;
for
v being
Vector of
V st
v in (i * a) (*) W1 holds
v in W2
proof
let v be
Vector of
V;
( v in (i * a) (*) W1 implies v in W2 )
assume C1:
v in (i * a) (*) W1
;
v in W2
consider vw being
Vector of
W1 such that C2:
v = (i * a) * vw
by C1;
reconsider vvw =
vw as
Vector of
V by ZMODUL01:25;
vvw in (Omega). W1
;
then consider vw1,
vw2 being
Vector of
V such that C3:
(
vw1 in LIu &
vw2 in Lin {uu} &
vvw = vw1 + vw2 )
by B5, ZMODUL01:92;
C4:
v =
(i * a) * vvw
by C2, ZMODUL01:29
.=
((i * a) * vw1) + ((i * a) * vw2)
by VECTSP_1:def 14, C3
.=
(a * (i * vw1)) + ((i * a) * vw2)
by VECTSP_1:def 16
.=
(a * (i * vw1)) + (a * (i * vw2))
by VECTSP_1:def 16
;
consider i2 being
Element of
INT.Ring such that C5:
vw2 = i2 * uu
by C3, ThLin1;
C6:
i * vw2 =
(i * i2) * uu
by VECTSP_1:def 16, C5
.=
i2 * iu
by B11, VECTSP_1:def 16
;
iu in W2
by B10, B14, ZMODUL01:94;
then
i * vw2 in W2
by C6, ZMODUL01:37;
then C7:
a * (i * vw2) in W2
by ZMODUL01:37;
C8:
a (*) LIu is
Subspace of
V
by ZMODUL01:42;
i * vw1 in LIu
by C3, ZMODUL01:37;
then reconsider ivw1 =
i * vw1 as
Vector of
LIu ;
a * ivw1 in a * LIu
;
then
a * (i * vw1) in a (*) LIu
by ZMODUL01:29;
then
a * (i * vw1) in W2
by B9, C8, ZMODUL01:23;
hence
v in W2
by C4, C7, ZMODUL01:36;
verum
end;
hence
(i * a) (*) W1 is
Subspace of
W2
by CX, ZMODUL01:44;
verum
end;
take
i * a
;
(i * a) (*) W1 is Subspace of W2
thus
(i * a) (*) W1 is
Subspace of
W2
by B12;
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; ( rank (W1 /\ W2) = rank W1 implies ex a being Element of INT.Ring st a (*) W1 is Subspace of W2 )
assume
rank (W1 /\ W2) = rank W1
; ex a being Element of INT.Ring st a (*) W1 is Subspace of W2
hence
ex a being Element of INT.Ring st a (*) W1 is Subspace of W2
by A3; verum