defpred S_{1}[ 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: S_{1}[ 0 ]
_{1}[m] holds

S_{1}[m + 1]
_{1}[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;

S_{1}[ rank V]
by A3;

hence W is free ; :: thesis: verum

for W being Subspace of V st rank V = $1 holds

W is free ;

A1: S

proof

A2:
for m being Nat st S
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 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 ; :: thesis: verum

end;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 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 ; :: thesis: verum

S

proof

A3:
for m being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume B1: S_{1}[n]
; :: thesis: S_{1}[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 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

b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }

- b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }

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 }

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 ) )

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

B24: for w being Vector of V holds

( w in Ws iff w in W ) ;

end;assume B1: S

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 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

proof

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
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: b in INT

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;assume CX1: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ; :: thesis: b in INT

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

b1 + b2 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }

proof

B17:
0 in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }
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 C3, C4, ZMODUL01:36;

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;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 C3, C4, ZMODUL01:36;

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

proof

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
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 ZMODUL01:23, ZMODUL02:64;

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 XBOOLE_1:36, ZMODUL02:10;

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;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 ZMODUL01:23, ZMODUL02:64;

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 XBOOLE_1:36, ZMODUL02:10;

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

- b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W }

proof

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
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 C2, ZMODUL01:38;

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 C2, C4, VECTSP_6:36;

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;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 C2, ZMODUL01:38;

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 C2, C4, VECTSP_6:36;

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

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

set BP = { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT;
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 S_{2}[ Integer] means $1 * b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } ;

C2: S_{2}[ 0 ]
by B17;

C3: for i being Integer st S_{2}[i] holds

( S_{2}[i - 1] & S_{2}[i + 1] )
_{2}[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;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 S

C2: S

C3: for i being Integer st S

( S

proof

for i being Integer holds S
let i be Integer; :: thesis: ( S_{2}[i] implies ( S_{2}[i - 1] & S_{2}[i + 1] ) )

assume D1: S_{2}[i]
; :: thesis: ( S_{2}[i - 1] & S_{2}[i + 1] )

D3: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B18, C1;

( 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 S_{2}[i - 1]
; :: thesis: S_{2}[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 S_{2}[i + 1]
; :: thesis: verum

end;assume D1: S

D3: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B18, C1;

( 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 S

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 S

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

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

then consider p being Element of INT such that
C2:
not { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT is empty
by B17, XBOOLE_0:def 4;

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) \ {0};

end;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) \ {0};

per cases
( ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ {0} = {} or ( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ {0} <> {} )
;

end;

suppose
( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ {0} = {}
; :: 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 ) )

( 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 = {0}
by C2, ZFMISC_1:58;

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

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 B17, D2; :: thesis: verum

end;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

set p = 0 ;
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 B15, E1;

assume E2: b <> 0 ; :: thesis: contradiction

end;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 B15, E1;

assume E2: b <> 0 ; :: thesis: contradiction

per cases then
( bb > 0 or bb < 0 )
;

end;

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 E1, XBOOLE_0:def 4;

hence contradiction by D1, E2, TARSKI:def 1; :: thesis: verum

end;then bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by E1, XBOOLE_0:def 4;

hence contradiction by D1, E2, TARSKI:def 1; :: thesis: verum

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 B18, E1;

then - bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by F1, XBOOLE_0:def 4;

hence contradiction by D1, E2, TARSKI:def 1; :: thesis: verum

end;- bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B18, E1;

then - bb in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by F1, XBOOLE_0:def 4;

hence contradiction by D1, E2, TARSKI:def 1; :: thesis: verum

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 B17, D2; :: thesis: verum

suppose
( { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT) \ {0} <> {}
; :: 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 ) )

( 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) \ {0} as non empty Subset of NAT by C5, XBOOLE_1:1;

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 D1, ZFMISC_1:56;

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

min* BPN divides b

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 D1, D6, XBOOLE_0:def 4; :: thesis: verum

end;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 D1, ZFMISC_1:56;

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

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
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 INT_1:3, INT_1:57;

E3: r <> 0 by D4, E2, INT_1:62;

E4: r in BPN

hence contradiction by E4, NAT_1:def 1; :: thesis: verum

end;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 INT_1:3, INT_1:57;

E3: r <> 0 by D4, E2, INT_1:62;

E4: r in BPN

proof

r < min* BPN
by D4, INT_1:58;
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 D4, INT_1:59;

F2: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by E1, XBOOLE_0:def 4;

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 F1, XBOOLE_0:def 4;

hence r in BPN by E3, ZFMISC_1:56; :: thesis: verum

end;reconsider q = b div (min* BPN) as Element of INT by INT_1:def 2;

F1: b = (q * (min* BPN)) + r by D4, INT_1:59;

F2: b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by E1, XBOOLE_0:def 4;

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 F1, XBOOLE_0:def 4;

hence r in BPN by E3, ZFMISC_1:56; :: thesis: verum

hence contradiction by E4, NAT_1:def 1; :: thesis: verum

min* BPN divides b

proof

reconsider p = min* BPN as Element of INT by INT_1:def 1;
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

end;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 )
;

end;

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 E1, XBOOLE_0:def 4;

hence contradiction by D5, E2; :: thesis: verum

end;then b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by E1, XBOOLE_0:def 4;

hence contradiction by D5, E2; :: thesis: verum

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 B18, E1;

then F2: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by F1, XBOOLE_0:def 4;

- b is Element of INT by INT_1:def 2;

hence contradiction by D5, E2, F2, INT_2:10; :: thesis: verum

end;- b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } by B18, E1;

then F2: - b in { (l . v) where l is Linear_Combination of the Basis of V : Sum l in W } /\ NAT by F1, XBOOLE_0:def 4;

- b is Element of INT by INT_1:def 2;

hence contradiction by D5, E2, F2, INT_2:10; :: thesis: verum

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 D1, D6, XBOOLE_0:def 4; :: thesis: verum

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

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 ;
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; :: thesis: verum

end;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; :: thesis: verum

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 )
;

end;

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 B21, INT_2:3;

for w being Vector of V st w in W holds

w in Lin ( the Basis of V \ {v})

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; :: thesis: verum

end;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})

proof

then
for w being Vector of V st w in Ws holds
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 C2, ZMODUL02:8;

then Carrier lw c= the Basis of V \ {v} by ZFMISC_1:34, VECTSP_6:def 4;

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 D2, ZMODUL02:64; :: thesis: verum

end;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 C2, ZMODUL02:8;

then Carrier lw c= the Basis of V \ {v} by ZFMISC_1:34, VECTSP_6:def 4;

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 D2, ZMODUL02:64; :: thesis: verum

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; :: thesis: verum

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}

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})

set Iw = Iwv \/ {wpv};

C10: wpv <> 0. V

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

WXv /\ Xwpv = (0). ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}))

for x being Vector of V holds

( x in W iff x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )

( 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; :: thesis: verum

end;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

then C18:
Sum lv = (lv . v) * v
by ZMODUL02:24;
for u being object st u in Carrier lv holds

u in {v}

v in Carrier lv by C3;

then {v} c= Carrier lv by ZFMISC_1:31;

hence Carrier lv = {v} by D2; :: thesis: verum

end;u in {v}

proof

then D2:
Carrier lv c= {v}
by TARSKI:def 3;
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 D1, TARSKI:def 1;

then lv . u = 0 by C3;

hence contradiction by D1, ZMODUL02:8; :: thesis: verum

end;( 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 D1, TARSKI:def 1;

then lv . u = 0 by C3;

hence contradiction by D1, ZMODUL02:8; :: thesis: verum

v in Carrier lv by C3;

then {v} c= Carrier lv by ZFMISC_1:31;

hence Carrier lv = {v} by D2; :: thesis: verum

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})

proof

C9:
(Sum lwpv) - (pp * v) in Lin ( the Basis of V \ {v})
assume
pp * v in Lin ( the Basis of V \ {v})
; :: thesis: contradiction

then pp * v in (Lin ( the Basis of V \ {v})) /\ (Lin {v}) by C6, VECTSP_5:3;

then pp * v in (0). V by B13, VECTSP_5:def 4;

hence contradiction by C1, C17, ZMODUL01:def 7, ZMODUL02:66; :: thesis: verum

end;then pp * v in (Lin ( the Basis of V \ {v})) /\ (Lin {v}) by C6, VECTSP_5:3;

then pp * v in (0). V by B13, VECTSP_5:def 4;

hence contradiction by C1, C17, ZMODUL01:def 7, ZMODUL02:66; :: thesis: verum

proof

reconsider wpv = Sum lwpv as Vector 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;

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; :: thesis: verum

end;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; :: thesis: verum

set Iw = Iwv \/ {wpv};

C10: wpv <> 0. V

proof

set WX = (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv});
assume
wpv = 0. V
; :: thesis: contradiction

then - (- (pp * v)) in Lin ( the Basis of V \ {v}) by C9, ZMODUL01:38;

hence contradiction by C8; :: thesis: verum

end;then - (- (pp * v)) in Lin ( the Basis of V \ {v}) by C9, ZMODUL01:38;

hence contradiction by C8; :: thesis: verum

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

C12:
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = WXv + Xwpv
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;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

proof

C15:
{wpv} is linearly-independent
by C10, ZMODUL02:59;
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 )

end;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

hence
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) = WXv + Xwpv
by ZMODUL01:133; :: thesis: verum
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 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 ; :: 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 E1, E5, ZMODUL01:28, ZMODUL02:64; :: thesis: verum

end;( 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 ; :: 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 E1, E5, ZMODUL01:28, ZMODUL02:64; :: thesis: verum

WXv /\ Xwpv = (0). ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}))

proof

then C17:
(W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) is free
by C12, C15, FRdsX, VECTSP_5:def 4;
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 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

.= 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; :: thesis: verum

end;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

proof

((Sum lwpv) - (pp * v)) + (pp * v) =
wpv - ((pp * v) - (pp * v))
by RLVECT_1:29
assume
lx . wpv = 0
; :: thesis: contradiction

then x = 0. V by D6, ZMODUL01:1

.= 0. ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) by ZMODUL01:26 ;

hence contradiction by D2; :: thesis: verum

end;then x = 0. V by D6, ZMODUL01:1

.= 0. ((W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})) by ZMODUL01:26 ;

hence contradiction by D2; :: thesis: verum

.= 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; :: thesis: verum

for x being Vector of V holds

( x in W iff x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )

proof

then
for x being Vector of V holds
let x be Vector of V; :: thesis: ( x in W iff x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) )

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; :: thesis: verum

end;hereby :: thesis: ( x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv}) implies x in W )

assume D1:
x in (W /\ (Lin ( the Basis of V \ {v}))) + (Lin {wpv})
; :: thesis: x in Wassume 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 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})

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; :: thesis: verum

end;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})

proof

then E4:
x - (y * wpv) in W /\ (Lin ( the Basis of V \ {v}))
by E3, VECTSP_5:3;
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 D4, VECTSP_6:def 9

.= 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 F3, ZFMISC_1:34, VECTSP_6:def 4;

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 D2, F2, ZMODUL02:55;

hence x - (y * wpv) in Lin ( the Basis of V \ {v}) by ZMODUL02:64; :: thesis: verum

end;(lx - (y * lwpv)) . v = (lx . v) - ((y * lwpv) . v) by ZMODUL02:39

.= (pp * y) - (y * (lwpv . v)) by D4, VECTSP_6:def 9

.= 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 F3, ZFMISC_1:34, VECTSP_6:def 4;

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 D2, F2, ZMODUL02:55;

hence x - (y * wpv) in Lin ( the Basis of V \ {v}) by ZMODUL02:64; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum

( 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; :: thesis: verum

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;

S

hence W is free ; :: thesis: verum