let p be prime Element of INT.Ring; for V being free Z_Module
for I being Subset 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
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
let V be free Z_Module; for I being Subset 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
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
let I be Subset 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
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
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 for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ )
assume
IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I }
; for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
defpred S1[ Nat] means for s being FinSequence of V st len s = $1 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ;
A1:
S1[ 0 ]
proof
let s be
FinSequence of
V;
( len s = 0 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) implies ZMtoMQV (V,p,(Sum s)) in Lin IQ )
assume that A2:
len s = 0
and
for
i being
Element of
NAT st
i in dom s holds
ex
si being
Vector of
V st
(
si = s . i &
ZMtoMQV (
V,
p,
si)
in Lin IQ )
;
ZMtoMQV (V,p,(Sum s)) in Lin IQ
s = <*> the
carrier of
V
by A2;
then
Sum s = 0. V
by RLVECT_1:43;
then
ZMtoMQV (
V,
p,
(Sum s))
= 0. (Z_MQ_VectSp (V,p))
by Th27;
hence
ZMtoMQV (
V,
p,
(Sum s))
in Lin IQ
by VECTSP_4:17;
verum
end;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
now for s being FinSequence of V st len s = k + 1 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQlet s be
FinSequence of
V;
( len s = k + 1 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) implies ZMtoMQV (V,p,(Sum s)) in Lin IQ )assume that A5:
len s = k + 1
and A6:
for
i being
Element of
NAT st
i in dom s holds
ex
si being
Vector of
V st
(
si = s . i &
ZMtoMQV (
V,
p,
si)
in Lin IQ )
;
ZMtoMQV (V,p,(Sum s)) in Lin IQreconsider s1 =
s | k as
FinSequence of
V ;
A7:
dom s = Seg (k + 1)
by A5, FINSEQ_1:def 3;
A8:
len s1 = k
by A5, FINSEQ_1:59, NAT_1:11;
A9:
dom s1 =
Seg (len s1)
by FINSEQ_1:def 3
.=
Seg k
by A5, FINSEQ_1:59, NAT_1:11
;
then A10:
s1 = s | (dom s1)
by FINSEQ_1:def 15;
s . (len s) in rng s
by A5, A7, FINSEQ_1:4, FUNCT_1:3;
then reconsider vs =
s . (len s) as
Element of
V ;
A11:
len s1 = k
by A5, FINSEQ_1:59, NAT_1:11;
A12:
for
i being
Element of
NAT st
i in dom s1 holds
ex
si being
Vector of
V st
(
si = s1 . i &
ZMtoMQV (
V,
p,
si)
in Lin IQ )
proof
let i be
Element of
NAT ;
( i in dom s1 implies ex si being Vector of V st
( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ ) )
assume A13:
i in dom s1
;
ex si being Vector of V st
( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ )
Seg k c= Seg (k + 1)
by FINSEQ_1:5, NAT_1:11;
then consider si being
Vector of
V such that A14:
(
si = s . i &
ZMtoMQV (
V,
p,
si)
in Lin IQ )
by A6, A9, A7, A13;
take
si
;
( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ )
thus
si = s1 . i
by A10, A13, A14, FUNCT_1:49;
ZMtoMQV (V,p,si) in Lin IQ
thus
ZMtoMQV (
V,
p,
si)
in Lin IQ
by A14;
verum
end; A15:
ZMtoMQV (
V,
p,
(Sum s1))
in Lin IQ
by A4, A11, A12;
consider ssi being
Vector of
V such that A16:
(
ssi = s . (len s) &
ZMtoMQV (
V,
p,
ssi)
in Lin IQ )
by A5, A6, A7, FINSEQ_1:4;
ZMtoMQV (
V,
p,
(Sum s)) =
ZMtoMQV (
V,
p,
((Sum s1) + vs))
by A5, A10, A8, RLVECT_1:38
.=
(ZMtoMQV (V,p,(Sum s1))) + (ZMtoMQV (V,p,vs))
by Th28
;
hence
ZMtoMQV (
V,
p,
(Sum s))
in Lin IQ
by A15, A16, VECTSP_4:20;
verum end;
hence
S1[
k + 1]
;
verum
end;
A17:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A3);
now for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQlet s be
FinSequence of
V;
( ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) implies ZMtoMQV (V,p,(Sum s)) in Lin IQ )assume A18:
for
i being
Element of
NAT st
i in dom s holds
ex
si being
Vector of
V st
(
si = s . i &
ZMtoMQV (
V,
p,
si)
in Lin IQ )
;
ZMtoMQV (V,p,(Sum s)) in Lin IQ
len s = len s
;
hence
ZMtoMQV (
V,
p,
(Sum s))
in Lin IQ
by A17, A18;
verum end;
hence
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
; verum