let V be free Z_Module; :: thesis: for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds

IQ is Basis of (Z_MQ_VectSp V)

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds

IQ is Basis of (Z_MQ_VectSp V)

let IQ be Subset of (Z_MQ_VectSp V); :: thesis: ( IQ = (MorphsZQ V) .: I & I is Basis of V implies IQ is Basis of (Z_MQ_VectSp V) )

assume AS: ( IQ = (MorphsZQ V) .: I & I is Basis of V ) ; :: thesis: IQ is Basis of (Z_MQ_VectSp V)

then I is base ;

then X0: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;

X1: IQ is linearly-independent by AS, ThEQRZMV3C, VECTSP_7:def 3;

AS0: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by defZMQVSp;

for vq being Element of (Z_MQ_VectSp V) holds vq in Lin IQ

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds

IQ is Basis of (Z_MQ_VectSp V)

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds

IQ is Basis of (Z_MQ_VectSp V)

let IQ be Subset of (Z_MQ_VectSp V); :: thesis: ( IQ = (MorphsZQ V) .: I & I is Basis of V implies IQ is Basis of (Z_MQ_VectSp V) )

assume AS: ( IQ = (MorphsZQ V) .: I & I is Basis of V ) ; :: thesis: IQ is Basis of (Z_MQ_VectSp V)

then I is base ;

then X0: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;

X1: IQ is linearly-independent by AS, ThEQRZMV3C, VECTSP_7:def 3;

AS0: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by defZMQVSp;

for vq being Element of (Z_MQ_VectSp V) holds vq in Lin IQ

proof

hence
IQ is Basis of (Z_MQ_VectSp V)
by AS0, X1, VECTSP_4:32, VECTSP_7:def 3; :: thesis: verum
let vq be Element of (Z_MQ_VectSp V); :: thesis: vq in Lin IQ

consider i being Element of INT.Ring, v being Element of V such that

P3: ( i <> 0 & vq = Class ((EQRZM V),[v,i]) ) by AS0, LMEQRZM1;

v in Lin I by X0;

then consider l being Linear_Combination of I such that

P4: v = Sum l by ZMODUL02:64;

thus vq in Lin IQ by AS, P4, P3, ThQuotAX; :: thesis: verum

end;consider i being Element of INT.Ring, v being Element of V such that

P3: ( i <> 0 & vq = Class ((EQRZM V),[v,i]) ) by AS0, LMEQRZM1;

v in Lin I by X0;

then consider l being Linear_Combination of I such that

P4: v = Sum l by ZMODUL02:64;

thus vq in Lin IQ by AS, P4, P3, ThQuotAX; :: thesis: verum