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
proof
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;
hence IQ is Basis of (Z_MQ_VectSp V) by AS0, X1, VECTSP_4:32, VECTSP_7:def 3; :: thesis: verum