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; :: thesis: for W being Subspace of V st rank V = 0 holds
W is free

let W be Subspace of V; :: thesis: ( rank V = 0 implies W is free )
assume B1: rank V = 0 ; :: thesis: 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 ;
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 ;
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
.= Lin II by ;
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 ;
then W is free by VECTSP_7:def 4;
hence W is free ; :: thesis: verum
end;
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume B1: S1[n] ; :: thesis: S1[n + 1]
let V be free finite-rank Z_Module; :: thesis: for W being Subspace of V st rank V = n + 1 holds
W is free

let W be Subspace of V; :: thesis: ( rank V = n + 1 implies W is free )
assume B2: rank V = n + 1 ; :: thesis: W is free
set I = the Basis of V;
B3: card the Basis of V = n + 1 by ;
card the Basis of V > 0 by ;
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 ;
then B5: card ( the Basis of V \ {v}) = (n + 1) - () by
.= (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 ;
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 ;
then reconsider IIv = the Basis of V \ {v} as linearly-independent Subset of VVv by ;
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 ;
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 ;
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
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } or b in INT )
assume CX1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis:
consider l being Linear_Combination of the Basis of V such that
CX2: ( l . v = b & Sum l in W ) by CX1;
thus b in INT by CX2; :: thesis: verum
end;
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 }
proof
let b1, b2 be Element of INT ; :: thesis: ( 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 } implies b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } )
assume C1: ( 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 } ) ; :: thesis: b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
set bb1 = b1;
set bb2 = b2;
consider l1 being Linear_Combination of the Basis of V such that
C3: ( l1 . v = b1 & Sum l1 in W ) by C1;
consider l2 being Linear_Combination of the Basis of V such that
C4: ( l2 . v = b2 & Sum l2 in W ) by C1;
(Sum l1) + (Sum l2) = Sum (l1 + l2) by ZMODUL02:52;
then C5: Sum (l1 + l2) in W by ;
l1 + l2 is Linear_Combination of the Basis of V by ZMODUL02:27;
then (l1 + l2) . v in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by C5;
then (l1 . v) + (l2 . v) in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by VECTSP_6:22;
then b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by C3, C4;
hence b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis: verum
end;
B17: 0 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
proof
set wv = the Element of (W /\ (Lin ( the Basis of V \ {v})));
the Element of (W /\ (Lin ( the Basis of V \ {v}))) in WWv ;
then consider lwv being Linear_Combination of the Basis of V \ {v} such that
C2: the Element of (W /\ (Lin ( the Basis of V \ {v}))) = Sum lwv by ;
Carrier lwv c= the Basis of V \ {v} by VECTSP_6:def 4;
then not v in Carrier lwv by ZFMISC_1:56;
then C4: lwv . v = 0 ;
the Element of (W /\ (Lin ( the Basis of V \ {v}))) in (Lin ( the Basis of V \ {v})) /\ W ;
then C5: the Element of (W /\ (Lin ( the Basis of V \ {v}))) in W by VECTSP_5:3;
lwv is Linear_Combination of the Basis of V by ;
hence 0 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by C2, C4, C5; :: thesis: verum
end;
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 }
proof
let b be Element of INT ; :: thesis: ( b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } implies - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } )
assume C1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
consider l being Linear_Combination of the Basis of V such that
C2: ( l . v = b & Sum l in W ) by C1;
- (Sum l) in W by ;
then C3: Sum (- l) in W by ZMODUL02:54;
consider bm being Element of INT.Ring such that
C4: bm = (- l) . v ;
reconsider bb = b as Element of INT.Ring ;
bm = - bb by ;
then C5: bm = - b ;
- l is Linear_Combination of the Basis of V by ZMODUL02:38;
hence - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by C3, C4, C5; :: thesis: verum
end;
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 }
proof
let b be Element of INT ; :: thesis: ( b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } implies 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 } )
assume C1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis: 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 }
defpred S2[ Integer] means \$1 * b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ;
C2: S2[ 0 ] by B17;
C3: for i being Integer st S2[i] holds
( S2[i - 1] & S2[i + 1] )
proof
let i be Integer; :: thesis: ( S2[i] implies ( S2[i - 1] & S2[i + 1] ) )
assume D1: S2[i] ; :: thesis: ( S2[i - 1] & S2[i + 1] )
D3: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by ;
( i * b is Element of INT & - b is Element of INT ) by INT_1:def 2;
then (i * b) + (- b) in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B16, D1, D3;
hence S2[i - 1] ; :: thesis: S2[i + 1]
i * b is Element of INT by INT_1:def 2;
then (i * b) + b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B16, C1, D1;
hence S2[i + 1] ; :: thesis: verum
end;
for i being Integer holds S2[i] from INT_1:sch 4(C2, C3);
hence 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 } ; :: thesis: verum
end;
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 ) )
proof
C2: not { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT is empty by ;
C5: { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT c= NAT by XBOOLE_1:17;
set BPN = ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ ;
per cases ) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ = {} or ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ <> {} ) ;
suppose ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ = {} ; :: thesis: 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 D1: { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT = by ;
D2: for b being object st b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } holds
b = 0
proof
let b be object ; :: thesis: ( b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } implies b = 0 )
assume E1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis: b = 0
reconsider bb = b as Element of INT by ;
assume E2: b <> 0 ; :: thesis: contradiction
per cases then ( bb > 0 or bb < 0 ) ;
suppose bb > 0 ; :: thesis: contradiction
then bb in NAT by INT_1:3;
then bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by ;
hence contradiction by D1, E2, TARSKI:def 1; :: thesis: verum
end;
suppose bb < 0 ; :: thesis: contradiction
then F1: - bb in NAT by INT_1:3;
- bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by ;
then - bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by ;
hence contradiction by D1, E2, TARSKI:def 1; :: thesis: verum
end;
end;
end;
set p = 0 ;
reconsider p = 0 as Element of INT by INT_1:def 2;
take p ; :: thesis: ( 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 ) )

thus ( 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 ) ) by ; :: thesis: verum
end;
suppose ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ <> {} ; :: thesis: 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 reconsider BPN = ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ as non empty Subset of NAT by ;
set p = min* BPN;
D1: min* BPN in BPN by NAT_1:def 1;
then D2: min* BPN in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by XBOOLE_0:def 4;
D4: ( min* BPN <> 0 & min* BPN is Element of NAT ) by ;
D5: 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 } /\ NAT holds
min* BPN divides b
proof
let b be Element of INT ; :: thesis: ( b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT implies min* BPN divides b )
assume E1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT ; :: thesis: min* BPN divides b
assume E2: not min* BPN divides b ; :: thesis: contradiction
set r = b mod (min* BPN);
reconsider r = b mod (min* BPN) as Element of NAT by ;
E3: r <> 0 by ;
E4: r in BPN
proof
set q = b div (min* BPN);
reconsider q = b div (min* BPN) as Element of INT by INT_1:def 2;
F1: b = (q * (min* BPN)) + r by ;
F2: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by ;
F3: q * (min* BPN) is Element of INT by INT_1:def 2;
min* BPN is Element of INT by INT_1:def 2;
then F5: - (q * (min* BPN)) in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B18, B19, D2, F3;
- (q * (min* BPN)) is Element of INT by INT_1:def 2;
then b + (- (q * (min* BPN))) in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B16, F2, F5;
then r in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by ;
hence r in BPN by ; :: thesis: verum
end;
r < min* BPN by ;
hence contradiction by E4, NAT_1:def 1; :: thesis: verum
end;
D6: 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
min* BPN divides b
proof
let b be Element of INT ; :: thesis: ( b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } implies min* BPN divides b )
assume E1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis: min* BPN divides b
assume E2: not min* BPN divides b ; :: thesis: contradiction
per cases ( b >= 0 or b < 0 ) ;
suppose b >= 0 ; :: thesis: contradiction
then b in NAT by INT_1:3;
then b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by ;
hence contradiction by D5, E2; :: thesis: verum
end;
suppose b < 0 ; :: thesis: contradiction
then F1: - b in NAT by INT_1:3;
- b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by ;
then F2: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by ;
- b is Element of INT by INT_1:def 2;
hence contradiction by D5, E2, F2, INT_2:10; :: thesis: verum
end;
end;
end;
reconsider p = min* BPN as Element of INT by INT_1:def 1;
take p ; :: thesis: ( 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 ) )

thus ( 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 ) ) by ; :: thesis: verum
end;
end;
end;
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 ; :: thesis: 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 ;
suppose p = 0. INT.Ring ; :: thesis: 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 ;
for w being Vector of V st w in W holds
w in Lin ( the Basis of V \ {v})
proof
let w be Vector of V; :: thesis: ( w in W implies w in Lin ( the Basis of V \ {v}) )
assume D1: w in W ; :: thesis: w in Lin ( the Basis of V \ {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;
then w in Lin the Basis of V ;
then consider lw being Linear_Combination of the Basis of V such that
D2: w = Sum lw by ZMODUL02:64;
lw . v in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by D1, D2;
then not v in Carrier lw by ;
then Carrier lw c= the Basis of V \ {v} by ;
then lw is Linear_Combination of the Basis of V \ {v} by VECTSP_6:def 4;
hence w in Lin ( the Basis of V \ {v}) by ; :: thesis: verum
end;
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 ;
reconsider IwsV = Iws as linearly-independent Subset of V by ;
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 ;
then IwsW is base by VECTSP_7:def 3;
hence W is free by VECTSP_7:def 4; :: thesis: verum
end;
suppose C1: p <> 0. INT.Ring ; :: thesis: 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}
proof
for u being object st u in Carrier lv holds
u in {v}
proof
assume ex u being object st
( u in Carrier lv & not u in {v} ) ; :: thesis: contradiction
then consider u being Vector of V such that
D1: ( u in Carrier lv & not u in {v} ) ;
u <> v by ;
then lv . u = 0 by C3;
hence contradiction by D1, ZMODUL02:8; :: thesis: verum
end;
then D2: Carrier lv c= {v} by TARSKI:def 3;
v in Carrier lv by C3;
then {v} c= Carrier lv by ZFMISC_1:31;
hence Carrier lv = {v} by D2; :: thesis: verum
end;
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 ;
lv is Linear_Combination of {v} by ;
then pp * lv is Linear_Combination of {v} by ZMODUL02:31;
then C6: pp * v in Lin {v} by ;
C17: v <> 0. V by ;
C8: not pp * v in Lin ( the Basis of V \ {v})
proof
assume pp * v in Lin ( the Basis of V \ {v}) ; :: thesis: contradiction
then pp * v in (Lin ( the Basis of V \ {v})) /\ () by ;
then pp * v in (0). V by ;
hence contradiction by C1, C17, ZMODUL01:def 7, ZMODUL02:66; :: thesis: verum
end;
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 ;
then reconsider lpv = pp * lv as Linear_Combination of the Basis of V by ;
D3: Sum lvpv = Sum (lwpv - lpv) by ;
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 ;
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 ;
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; :: thesis: verum
end;
reconsider wpv = Sum lwpv as Vector of V ;
set Iw = Iwv \/ {wpv};
C10: wpv <> 0. V
proof
assume wpv = 0. V ; :: thesis: contradiction
then - (- (pp * v)) in Lin ( the Basis of V \ {v}) by ;
hence contradiction by C8; :: thesis: verum
end;
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
proof
assume wpv in Iwv ; :: thesis: contradiction
then wpv in WWv ;
then D2: wpv in Lin ( the Basis of V \ {v}) by ZMODUL01:23;
wpv - ((Sum lwpv) - (pp * v)) = (wpv - wpv) + (pp * v) by RLVECT_1:29
.= (0. V) + (pp * v) by RLVECT_1:15
.= pp * v ;
hence contradiction by C8, C9, D2, ZMODUL01:39; :: thesis: verum
end;
C12: (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = WXv + Xwpv
proof
D1: Iwv /\ {wpv} = {} by ;
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})); :: thesis: 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 ;
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 ;
set x1 = Sum lx1;
set x2 = Sum lx2;
Sum lx1 in WXv by ;
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 ;
take xx1 ; :: thesis: 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 ; :: thesis: ( xx1 in WXv & xx2 in Xwpv & x = xx1 + xx2 )
thus ( xx1 in WXv & xx2 in Xwpv & x = xx1 + xx2 ) by ; :: thesis: verum
end;
hence (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = WXv + Xwpv by ZMODUL01:133; :: thesis: verum
end;
C15: {wpv} is linearly-independent by ;
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})) ; :: thesis: 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 ;
x in Lin {wpv} by ;
then consider lx being Linear_Combination of {wpv} such that
D5: x = Sum lx by ZMODUL02:64;
x in V by ;
then reconsider xx = x as Vector of V ;
x in WWv by ;
then D9: x in Lin ( the Basis of V \ {v}) by ZMODUL01:23;
D6: x = (lx . wpv) * wpv by ;
D7: lx . wpv <> 0
proof
assume lx . wpv = 0 ; :: thesis: contradiction
then x = 0. V by
.= 0. ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) by ZMODUL01:26 ;
hence contradiction by D2; :: thesis: verum
end;
((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
.= ((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 ;
then D10: ((lx . wpv) * pp) * v in Lin ( the Basis of V \ {v}) by ;
D11: Sum (((lx . wpv) * pp) * lv) = ((lx . wpv) * pp) * ((lv . v) * v) by
.= ((lx . wpv) * pp) * v by ;
lv is Linear_Combination of {v} by ;
then ((lx . wpv) * pp) * lv is Linear_Combination of {v} by ZMODUL02:31;
then ((lx . wpv) * pp) * v in Lin {v} by ;
then ((lx . wpv) * pp) * v in (Lin ( the Basis of V \ {v})) /\ () by ;
then ((lx . wpv) * pp) * v in (0). V by ;
hence contradiction by C1, C17, D7, ZMODUL01:def 7, ZMODUL02:66; :: thesis: verum
end;
then C17: (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) is free by ;
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; :: thesis: ( x in W iff x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )
hereby :: thesis: ( x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) implies x in W )
assume D1: x in W ; :: thesis: 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 ;
reconsider y = y as Element of INT.Ring by Lem1;
y * wpv in W by ;
then E3: x - (y * wpv) in W by ;
x - (y * wpv) in Lin ( the Basis of V \ {v})
proof
F2: y * wpv = Sum (y * lwpv) by ZMODUL02:53;
(lx - (y * lwpv)) . v = (lx . v) - ((y * lwpv) . v) by ZMODUL02:39
.= (pp * y) - (y * (lwpv . v)) by
.= 0 by C2 ;
then F3: not v in Carrier (lx - (y * lwpv)) by ZMODUL02:8;
y * lwpv is Linear_Combination of the Basis of V by ZMODUL02:31;
then lx - (y * lwpv) is Linear_Combination of the Basis of V by ZMODUL02:41;
then Carrier (lx - (y * lwpv)) c= the Basis of V \ {v} by ;
then reconsider lxy = lx - (y * lwpv) as Linear_Combination of the Basis of V \ {v} by VECTSP_6:def 4;
x - (y * wpv) = Sum lxy by ;
hence x - (y * wpv) in Lin ( the Basis of V \ {v}) by ZMODUL02:64; :: thesis: verum
end;
then E4: x - (y * wpv) in W /\ (Lin ( the Basis of V \ {v})) by ;
wpv in {wpv} by TARSKI:def 1;
then E5: y * wpv in Lin {wpv} by ;
(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 ; :: thesis: verum
end;
assume D1: x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) ; :: thesis: 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 ;
then (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) is Subspace of W by ;
hence x in W by ; :: thesis: 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 ;
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 ;
reconsider IwsV = Iws as linearly-independent Subset of V by ;
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 ;
then IwsW is base by VECTSP_7:def 3;
hence W is free by VECTSP_7:def 4; :: thesis: verum
end;
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; :: thesis: for W being Subspace of V holds W is free
let W be Subspace of V; :: thesis: W is free
set n = rank V;
S1[ rank V] by A3;
hence W is free ; :: thesis: verum