let V be free Z_Module; :: thesis: for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds

A is linearly-dependent

let I, A be finite Subset of V; :: thesis: ( I is Basis of V & (card I) + 1 = card A implies A is linearly-dependent )

assume AS: ( I is Basis of V & (card I) + 1 = card A ) ; :: thesis: A is linearly-dependent

reconsider IQ = (MorphsZQ V) .: I as Subset of (Z_MQ_VectSp V) ;

reconsider IQ = IQ as finite Subset of (Z_MQ_VectSp V) ;

P2: IQ is Basis of (Z_MQ_VectSp V) by AS, ThEQRZMV3D;

assume P31: not A is linearly-dependent ; :: thesis: contradiction

reconsider B = (MorphsZQ V) .: A as Subset of (Z_MQ_VectSp V) ;

reconsider B = B as finite Subset of (Z_MQ_VectSp V) ;

PP: ( IQ is linearly-independent & Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp V), the addF of (Z_MQ_VectSp V), the ZeroF of (Z_MQ_VectSp V), the lmult of (Z_MQ_VectSp V) #) ) by VECTSP_7:def 3, P2;

B is linearly-independent by P31, ThEQRZMV3C;

then P5: card B <= card IQ by VECTSP_9:19, PP;

card IQ = card I by ThEQRZMV3E;

then card A <= card I by P5, ThEQRZMV3E;

hence contradiction by AS, NAT_1:13; :: thesis: verum

A is linearly-dependent

let I, A be finite Subset of V; :: thesis: ( I is Basis of V & (card I) + 1 = card A implies A is linearly-dependent )

assume AS: ( I is Basis of V & (card I) + 1 = card A ) ; :: thesis: A is linearly-dependent

reconsider IQ = (MorphsZQ V) .: I as Subset of (Z_MQ_VectSp V) ;

reconsider IQ = IQ as finite Subset of (Z_MQ_VectSp V) ;

P2: IQ is Basis of (Z_MQ_VectSp V) by AS, ThEQRZMV3D;

assume P31: not A is linearly-dependent ; :: thesis: contradiction

reconsider B = (MorphsZQ V) .: A as Subset of (Z_MQ_VectSp V) ;

reconsider B = B as finite Subset of (Z_MQ_VectSp V) ;

PP: ( IQ is linearly-independent & Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp V), the addF of (Z_MQ_VectSp V), the ZeroF of (Z_MQ_VectSp V), the lmult of (Z_MQ_VectSp V) #) ) by VECTSP_7:def 3, P2;

B is linearly-independent by P31, ThEQRZMV3C;

then P5: card B <= card IQ by VECTSP_9:19, PP;

card IQ = card I by ThEQRZMV3E;

then card A <= card I by P5, ThEQRZMV3E;

hence contradiction by AS, NAT_1:13; :: thesis: verum