defpred S1[ Nat] means for V being free finite-rank Z_Module
for W being Subspace of V st rank V = $1 holds
W is free ;
A1:
S1[ 0 ]
proof
let V be
free finite-rank Z_Module;
for W being Subspace of V st rank V = 0 holds
W is free let W be
Subspace of
V;
( rank V = 0 implies W is free )
assume B1:
rank V = 0
;
W is free
set I = the
Basis of
V;
set sW =
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #);
B2:
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
= (Omega). W
;
B3:
card the
Basis of
V = 0
by B1, ZMODUL03:def 5;
then B31:
the
Basis of
V = {} the
carrier of
V
;
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #) =
Lin the
Basis of
V
by VECTSP_7:def 3
.=
(0). V
by B31, ZMODUL02:67
;
then
the
carrier of
V = {(0. V)}
by VECTSP_4:def 3;
then
the
carrier of
W c= {(0. V)}
by VECTSP_4:def 2;
then B5:
the
carrier of
W c= {(0. W)}
by ZMODUL01:26;
B6:
the
Basis of
V = {} the
carrier of
W
by B3;
then reconsider II = the
Basis of
V as
Subset of
W ;
II = {} the
carrier of
W
by B6;
then AA:
II is
linearly-independent
;
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #) =
(0). W
by B2, B5, XBOOLE_0:def 10, VECTSP_4:def 3
.=
Lin II
by B6, ZMODUL02:67
;
then
Lin II = ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
;
then
II is
base
by VECTSP_7:def 3, AA;
then
W is
free
by VECTSP_7:def 4;
hence
W is
free
;
verum
end;
A2:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume B1:
S1[
n]
;
S1[n + 1]
let V be
free finite-rank Z_Module;
for W being Subspace of V st rank V = n + 1 holds
W is free let W be
Subspace of
V;
( rank V = n + 1 implies W is free )
assume B2:
rank V = n + 1
;
W is free
set I = the
Basis of
V;
B3:
card the
Basis of
V = n + 1
by B2, ZMODUL03:def 5;
card the
Basis of
V > 0
by B2, ZMODUL03:def 5;
then
the
Basis of
V <> {}
;
then consider v being
object such that B4:
v in the
Basis of
V
by XBOOLE_0:7;
reconsider v =
v as
Vector of
V by B4;
set Iv = the
Basis of
V \ {v};
B22:
{v} is
Subset of the
Basis of
V
by B4, SUBSET_1:41;
then B5:
card ( the Basis of V \ {v}) =
(n + 1) - (card {v})
by B3, CARD_2:44
.=
(n + 1) - 1
by CARD_1:30
.=
n
;
the
Basis of
V is
linearly-independent
by VECTSP_7:def 3;
then B6:
the
Basis of
V \ {v} is
linearly-independent
by XBOOLE_1:36, ZMODUL02:56;
set Vv =
Lin ( the Basis of V \ {v});
reconsider VVv =
Lin ( the Basis of V \ {v}) as
free finite-rank Z_Module by B6;
for
x being
object st
x in the
Basis of
V \ {v} holds
x in the
carrier of
VVv
by STRUCT_0:def 5, ZMODUL02:65;
then reconsider IIv = the
Basis of
V \ {v} as
linearly-independent Subset of
VVv by B6, TARSKI:def 3, ZMODUL03:16;
Lin ( the Basis of V \ {v}) = Lin IIv
by ZMODUL03:20;
then
IIv is
Basis of
VVv
by VECTSP_7:def 3;
then B8:
rank VVv = n
by B5, ZMODUL03:def 5;
set Wv =
W /\ (Lin ( the Basis of V \ {v}));
reconsider WWv =
W /\ (Lin ( the Basis of V \ {v})) as
Subspace of
Lin ( the Basis of V \ {v}) by ZMODUL01:105;
reconsider WWv =
WWv as
free Subspace of
Lin ( the Basis of V \ {v}) by B1, B8;
set IIwv = the
Basis of
WWv;
the
carrier of
WWv c= the
carrier of
V
by VECTSP_4:def 2;
then reconsider Iwv = the
Basis of
WWv as
Subset of
V by XBOOLE_1:1;
B13:
V is_the_direct_sum_of Lin ( the Basis of V \ {v}),
Lin {v}
by B4, FRdsY;
set B =
{ (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ;
B15:
{ (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } c= INT
B16:
for
b1,
b2 being
Element of
INT st
b1 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } &
b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
B17:
0 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
B18:
for
b being
Element of
INT st
b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
- b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
B19:
for
b being
Element of
INT st
b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
for
i being
Element of
INT holds
i * b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
set BP =
{ (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT;
ex
p being
Element of
INT st
(
p in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } & ( for
b being
Element of
INT st
b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
p divides b ) )
then consider p being
Element of
INT such that B20:
p in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
and B21:
for
b being
Element of
INT st
b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
p divides b
;
reconsider pp =
p as
Element of
INT.Ring ;
set Ws =
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #);
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #) is
Subspace of
V
proof
C2:
the
carrier of
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
c= the
carrier of
V
by VECTSP_4:def 2;
C3:
0. ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #) =
0. W
.=
0. V
by ZMODUL01:26
;
C4:
the
addF of
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
= the
addF of
V || the
carrier of
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
by VECTSP_4:def 2;
the
lmult of
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
= the
lmult of
V | [:INT, the carrier of ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #):]
by VECTSP_4:def 2;
hence
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #) is
Subspace of
V
by C2, C3, C4, ZMODUL01:40;
verum
end;
then reconsider Ws =
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #) as
strict Subspace of
V ;
B24:
for
w being
Vector of
V holds
(
w in Ws iff
w in W )
;
per cases
( p = 0. INT.Ring or p <> 0. INT.Ring )
;
suppose
p = 0. INT.Ring
;
W is free then C2:
for
b being
Element of
INT st
b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
b = 0
by B21, INT_2:3;
for
w being
Vector of
V st
w in W holds
w in Lin ( the Basis of V \ {v})
then
for
w being
Vector of
V st
w in Ws holds
w in Lin ( the Basis of V \ {v})
by B24;
then C4:
Ws is
Subspace of
Lin ( the Basis of V \ {v})
by ZMODUL01:44;
Ws is
free
by B1, B8, C4;
then consider Iws being
Subset of
Ws such that c5:
Iws is
base
by VECTSP_7:def 4;
C5:
(
Iws is
linearly-independent &
Lin Iws = ModuleStr(# the
carrier of
Ws, the
addF of
Ws, the
ZeroF of
Ws, the
lmult of
Ws #) )
by c5, VECTSP_7:def 3;
reconsider IwsV =
Iws as
linearly-independent Subset of
V by C5, ZMODUL03:15;
reconsider IwsW =
IwsV as
linearly-independent Subset of
W by ZMODUL03:16;
Lin IwsW =
Lin IwsV
by ZMODUL03:20
.=
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
by C5, ZMODUL03:20
;
then
IwsW is
base
by VECTSP_7:def 3;
hence
W is
free
by VECTSP_7:def 4;
verum end; suppose C1:
p <> 0. INT.Ring
;
W is free consider lwpv being
Linear_Combination of the
Basis of
V such that C2:
(
lwpv . v = p &
Sum lwpv in W )
by B20;
set wpv =
Sum lwpv;
set vpv =
(Sum lwpv) - (pp * v);
consider lv being
Linear_Combination of
V such that C3:
(
lv . v = 1. INT.Ring & ( for
u being
Vector of
V st
v <> u holds
lv . u = 0. INT.Ring ) )
by ZMODUL03:1;
C4:
Carrier lv = {v}
then C18:
Sum lv = (lv . v) * v
by ZMODUL02:24;
then C5:
Sum (pp * lv) =
pp * ((lv . v) * v)
by ZMODUL02:53
.=
pp * v
by C3, VECTSP_1:def 17
;
lv is
Linear_Combination of
{v}
by C4, VECTSP_6:def 4;
then
pp * lv is
Linear_Combination of
{v}
by ZMODUL02:31;
then C6:
pp * v in Lin {v}
by C5, ZMODUL02:64;
C17:
v <> 0. V
by B22, ZMODUL02:56, VECTSP_7:def 3;
C8:
not
pp * v in Lin ( the Basis of V \ {v})
C9:
(Sum lwpv) - (pp * v) in Lin ( the Basis of V \ {v})
proof
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #)
= Lin the
Basis of
V
by VECTSP_7:def 3;
then
(Sum lwpv) - (pp * v) in Lin the
Basis of
V
;
then consider lvpv being
Linear_Combination of the
Basis of
V such that D2:
(Sum lwpv) - (pp * v) = Sum lvpv
by ZMODUL02:64;
Carrier (pp * lv) = {v}
by C1, C4, ZMODUL02:29;
then reconsider lpv =
pp * lv as
Linear_Combination of the
Basis of
V by B4, ZFMISC_1:31, VECTSP_6:def 4;
D3:
Sum lvpv = Sum (lwpv - lpv)
by C5, D2, ZMODUL02:55;
lwpv - lpv is
Linear_Combination of the
Basis of
V
by ZMODUL02:41;
then
(
Carrier lvpv c= the
Basis of
V &
Carrier (lwpv - lpv) c= the
Basis of
V )
by VECTSP_6:def 4;
then
lvpv = lwpv - lpv
by D3, VECTSP_7:def 3, ZMODUL03:3;
then lvpv . v =
(lwpv . v) - (lpv . v)
by ZMODUL02:39
.=
(lwpv . v) - (pp * (lv . v))
by VECTSP_6:def 9
.=
0
by C2, C3
;
then
not
v in Carrier lvpv
by ZMODUL02:8;
then
Carrier lvpv c= the
Basis of
V \ {v}
by ZFMISC_1:34, VECTSP_6:def 4;
then reconsider lvvpv =
lvpv as
Linear_Combination of the
Basis of
V \ {v} by VECTSP_6:def 4;
(Sum lwpv) - (pp * v) = Sum lvvpv
by D2;
hence
(Sum lwpv) - (pp * v) in Lin ( the Basis of V \ {v})
by ZMODUL02:64;
verum
end; reconsider wpv =
Sum lwpv as
Vector of
V ;
set Iw =
Iwv \/ {wpv};
C10:
wpv <> 0. V
set WX =
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv});
reconsider WXv =
WWv as
Subspace of
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) by ZMODUL01:97;
reconsider Xwpv =
Lin {wpv} as
Subspace of
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) by ZMODUL01:97;
C11:
not
wpv in Iwv
C12:
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = WXv + Xwpv
proof
D1:
Iwv /\ {wpv} = {}
by C11, XBOOLE_0:def 7, ZFMISC_1:50;
for
x being
Vector of
((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) ex
x1,
x2 being
Vector of
((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) st
(
x1 in WXv &
x2 in Xwpv &
x = x1 + x2 )
proof
let x be
Vector of
((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}));
ex x1, x2 being Vector of ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) st
( x1 in WXv & x2 in Xwpv & x = x1 + x2 )
E1:
W /\ (Lin ( the Basis of V \ {v})) =
Lin the
Basis of
WWv
by VECTSP_7:def 3
.=
Lin Iwv
by ZMODUL03:20
;
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = Lin (Iwv \/ {wpv})
by E1, ZMODUL02:72;
then
x in Lin (Iwv \/ {wpv})
;
then consider lx being
Linear_Combination of
Iwv \/ {wpv} such that E3:
x = Sum lx
by ZMODUL02:64;
consider lx1 being
Linear_Combination of
Iwv,
lx2 being
Linear_Combination of
{wpv} such that E4:
lx = lx1 + lx2
by D1, ThCarrier2;
set x1 =
Sum lx1;
set x2 =
Sum lx2;
Sum lx1 in WXv
by E1, ZMODUL02:64;
then
Sum lx1 in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})
by ZMODUL01:24;
then reconsider xx1 =
Sum lx1 as
Vector of
((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) ;
Sum lx2 in Xwpv
by ZMODUL02:64;
then
Sum lx2 in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})
by ZMODUL01:24;
then reconsider xx2 =
Sum lx2 as
Vector of
((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) ;
E5:
(Sum lx1) + (Sum lx2) = x
by E3, E4, ZMODUL02:52;
take
xx1
;
ex x2 being Vector of ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) st
( xx1 in WXv & x2 in Xwpv & x = xx1 + x2 )
take
xx2
;
( xx1 in WXv & xx2 in Xwpv & x = xx1 + xx2 )
thus
(
xx1 in WXv &
xx2 in Xwpv &
x = xx1 + xx2 )
by E1, E5, ZMODUL01:28, ZMODUL02:64;
verum
end;
hence
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = WXv + Xwpv
by ZMODUL01:133;
verum
end; C15:
{wpv} is
linearly-independent
by C10, ZMODUL02:59;
WXv /\ Xwpv = (0). ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}))
proof
assume
WXv /\ Xwpv <> (0). ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}))
;
contradiction
then consider x being
Vector of
((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) such that D2:
(
x in WXv /\ Xwpv &
x <> 0. ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) )
by Thn0V;
D3:
x in WXv
by D2, VECTSP_5:3;
x in Lin {wpv}
by D2, VECTSP_5:3;
then consider lx being
Linear_Combination of
{wpv} such that D5:
x = Sum lx
by ZMODUL02:64;
x in V
by D3, ZMODUL01:24;
then reconsider xx =
x as
Vector of
V ;
x in WWv
by D2, VECTSP_5:3;
then D9:
x in Lin ( the Basis of V \ {v})
by ZMODUL01:23;
D6:
x = (lx . wpv) * wpv
by D5, ZMODUL02:21;
D7:
lx . wpv <> 0
((Sum lwpv) - (pp * v)) + (pp * v) =
wpv - ((pp * v) - (pp * v))
by RLVECT_1:29
.=
wpv - (0. V)
by RLVECT_1:15
.=
wpv
;
then x =
((lx . wpv) * ((Sum lwpv) - (pp * v))) + ((lx . wpv) * (pp * v))
by D6, VECTSP_1:def 14
.=
((lx . wpv) * ((Sum lwpv) - (pp * v))) + (((lx . wpv) * pp) * v)
by VECTSP_1:def 16
;
then D8:
xx - ((lx . wpv) * ((Sum lwpv) - (pp * v))) =
(((lx . wpv) * pp) * v) + (((lx . wpv) * ((Sum lwpv) - (pp * v))) - ((lx . wpv) * ((Sum lwpv) - (pp * v))))
by RLVECT_1:28
.=
(((lx . wpv) * pp) * v) + (0. V)
by RLVECT_1:15
.=
((lx . wpv) * pp) * v
;
(lx . wpv) * ((Sum lwpv) - (pp * v)) in Lin ( the Basis of V \ {v})
by C9, ZMODUL01:37;
then D10:
((lx . wpv) * pp) * v in Lin ( the Basis of V \ {v})
by D8, D9, ZMODUL01:39;
D11:
Sum (((lx . wpv) * pp) * lv) =
((lx . wpv) * pp) * ((lv . v) * v)
by C18, ZMODUL02:53
.=
((lx . wpv) * pp) * v
by C3, VECTSP_1:def 17
;
lv is
Linear_Combination of
{v}
by C4, VECTSP_6:def 4;
then
((lx . wpv) * pp) * lv is
Linear_Combination of
{v}
by ZMODUL02:31;
then
((lx . wpv) * pp) * v in Lin {v}
by D11, ZMODUL02:64;
then
((lx . wpv) * pp) * v in (Lin ( the Basis of V \ {v})) /\ (Lin {v})
by D10, VECTSP_5:3;
then
((lx . wpv) * pp) * v in (0). V
by B13, VECTSP_5:def 4;
hence
contradiction
by C1, C17, D7, ZMODUL01:def 7, ZMODUL02:66;
verum
end; then C17:
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) is
free
by C12, C15, FRdsX, VECTSP_5:def 4;
for
x being
Vector of
V holds
(
x in W iff
x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )
proof
let x be
Vector of
V;
( x in W iff x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )
hereby ( x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) implies x in W )
assume D1:
x in W
;
x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #)
= Lin the
Basis of
V
by VECTSP_7:def 3;
then
x in Lin the
Basis of
V
;
then consider lx being
Linear_Combination of the
Basis of
V such that D2:
x = Sum lx
by ZMODUL02:64;
lx . v in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
by D1, D2;
then consider y being
Integer such that D4:
lx . v = p * y
by B21, INT_1:def 3;
reconsider y =
y as
Element of
INT.Ring by Lem1;
y * wpv in W
by C2, ZMODUL01:37;
then E3:
x - (y * wpv) in W
by D1, ZMODUL01:39;
x - (y * wpv) in Lin ( the Basis of V \ {v})
then E4:
x - (y * wpv) in W /\ (Lin ( the Basis of V \ {v}))
by E3, VECTSP_5:3;
wpv in {wpv}
by TARSKI:def 1;
then E5:
y * wpv in Lin {wpv}
by ZMODUL01:37, ZMODUL02:65;
(x - (y * wpv)) + (y * wpv) =
x - ((y * wpv) - (y * wpv))
by RLVECT_1:29
.=
x - (0. V)
by RLVECT_1:5
.=
x
;
hence
x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})
by E4, E5, VECTSP_5:1;
verum
end;
assume D1:
x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})
;
x in W
D2:
W /\ (Lin ( the Basis of V \ {v})) is
Subspace of
W
by ZMODUL01:105;
Lin {wpv} is
Subspace of
W
by C2, ZFMISC_1:31, ZMODUL03:19;
then
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) is
Subspace of
W
by D2, ZMODUL02:76;
hence
x in W
by D1, ZMODUL01:23;
verum
end; then
for
x being
Vector of
V holds
(
x in Ws iff
x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )
by B24;
then
Ws is
free
by C17, VECTSP_4:30;
then consider Iws being
Subset of
Ws such that c18:
Iws is
base
by VECTSP_7:def 4;
C18:
(
Iws is
linearly-independent &
Lin Iws = ModuleStr(# the
carrier of
Ws, the
addF of
Ws, the
ZeroF of
Ws, the
lmult of
Ws #) )
by VECTSP_7:def 3, c18;
reconsider IwsV =
Iws as
linearly-independent Subset of
V by C18, ZMODUL03:15;
reconsider IwsW =
IwsV as
linearly-independent Subset of
W by ZMODUL03:16;
Lin IwsW =
Lin IwsV
by ZMODUL03:20
.=
ModuleStr(# the
carrier of
W, the
addF of
W, the
ZeroF of
W, the
lmult of
W #)
by C18, ZMODUL03:20
;
then
IwsW is
base
by VECTSP_7:def 3;
hence
W is
free
by VECTSP_7:def 4;
verum end;
end;
A3:
for m being Nat holds S1[m]
from NAT_1:sch 2(A1, A2);
let V be free finite-rank Z_Module; for W being Subspace of V holds W is free
let W be Subspace of V; W is free
set n = rank V;
S1[ rank V]
by A3;
hence
W is free
; verum