let p be prime Element of INT.Ring; for V being free Z_Module
for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
IQ is Basis of (Z_MQ_VectSp (V,p))
let V be free Z_Module; for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
IQ is Basis of (Z_MQ_VectSp (V,p))
let I be Basis of V; for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
IQ is Basis of (Z_MQ_VectSp (V,p))
let IQ be Subset of (Z_MQ_VectSp (V,p)); ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies IQ is Basis of (Z_MQ_VectSp (V,p)) )
assume A1:
IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I }
; IQ is Basis of (Z_MQ_VectSp (V,p))
A2:
IQ is linearly-independent
by Th32, A1;
for vq being Element of (Z_MQ_VectSp (V,p)) holds vq in Lin IQ
proof
let vq be
Element of
(Z_MQ_VectSp (V,p));
vq in Lin IQ
consider v being
Vector of
V such that A3:
vq = ZMtoMQV (
V,
p,
v)
by Th22;
I is
base
;
then
Lin I = ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #)
;
then consider l being
Linear_Combination of
I such that A4:
v = Sum l
by STRUCT_0:def 5, ZMODUL02:64;
thus
vq in Lin IQ
by A1, A4, A3, Th34;
verum
end;
then
Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)
by VECTSP_4:32;
then
IQ is base
by A2;
hence
IQ is Basis of (Z_MQ_VectSp (V,p))
; verum