:: Formalization of Integral Linear Space
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REAL_1, SUBSET_1, NUMBERS, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2,
FINSEQ_1, STRUCT_0, FUNCT_1, XBOOLE_0, VALUED_1, ORDINAL4, ARYTM_3,
RELAT_1, PARTFUN1, NAT_1, INT_1, CARD_3, CARD_1, SUPINF_2, TARSKI,
FUNCT_2, ARYTM_1, RLVECT_3, RLVECT_X, XXREAL_0, VALUED_0, FUNCT_4,
FUNCOP_1, FINSEQ_2, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, VALUED_0, FINSEQ_1,
FINSEQ_2, STRUCT_0, RLVECT_1, RLSUB_1, RLVECT_2, RLVECT_3, RUSUB_4,
VFUNCT_1, BINOM;
constructors REALSET1, RLVECT_2, RLVECT_3, FUNCT_4, RUSUB_4, BINOP_2,
FUNCSDOM, TOPREALB, VFUNCT_1, BINOM, REAL_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FINSET_1, NUMBERS, STRUCT_0,
ORDINAL1, INT_1, XREAL_0, RLVECT_2, VALUED_0, FINSEQ_1, FINSEQ_2, CARD_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions RLVECT_2, TARSKI;
equalities RLVECT_2, RUSUB_4, FINSEQ_1;
expansions TARSKI, FINSEQ_1;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, RLSUB_1,
RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1,
STRUCT_0, PARTFUN1, RLVECT_3, INT_1, NUMBERS, NAT_1, XREAL_0, XXREAL_0,
ENUMSET1, RLVECT_4, VFUNCT_1, BINOM, FUNCOP_1, FINSEQ_5, FUNCT_4, CARD_1;
schemes FINSEQ_1, NAT_1, FUNCT_2, RLVECT_4;
begin :: 1. Preliminaries
reconsider z0=0 as Real;
deffunc H(object)=In(0,REAL);
theorem
for X be RealLinearSpace,
R1, R2 be FinSequence of X
st len R1 = len R2 holds Sum(R1+R2) = Sum(R1) + Sum(R2)
proof
let X be RealLinearSpace,
R1, R2 be FinSequence of X;
assume len R1 = len R2; then
dom R1 = dom R2 by FINSEQ_3:29;
hence thesis by BINOM:7;
end;
theorem
for X be RealLinearSpace,
R1, R2, R3 be FinSequence of X
st len R1 = len R2 & R3 = R1-R2 holds Sum(R3) = Sum(R1) - Sum(R2)
proof
let X be RealLinearSpace,
R1, R2, R3 be FinSequence of X;
assume A1: len R1 = len R2 & R3 = R1 - R2; then
A2: dom R1 = dom R2 by FINSEQ_3:29;
A3: dom R3 = dom R1 /\ dom R2 by A1,VFUNCT_1:def 2
.= dom R1 by A2; then
A4: len R3 = len R1 by FINSEQ_3:29;
for k be Nat st k in dom R1 holds R3.k = R1/.k - R2/.k
proof
let k be Nat;
assume A5: k in dom R1;
hence R3.k = R3/.k by A3,PARTFUN1:def 6
.= R1/.k - R2/.k by A1,A5,A3,VFUNCT_1:def 2;
end;
hence thesis by A1,A4,RLVECT_2:5;
end;
theorem Th3:
for X be RealLinearSpace,
R1, R2 be FinSequence of X,
a be Element of REAL st R2 = a(#)R1 holds Sum(R2) = a * Sum(R1)
proof
let X be RealLinearSpace,
R1, R2 be FinSequence of X,
a be Element of REAL;
assume A1: R2 = a(#)R1;
dom R2 = dom R1 by A1,VFUNCT_1:def 4; then
A2: len R2 = len R1 by FINSEQ_3:29;
for k be Nat st k in dom R1 holds R2.k = a * R1/.k
proof
let k be Nat;
assume k in dom R1; then
A3: k in dom R2 by A1,VFUNCT_1:def 4;
hence R2.k = R2/.k by PARTFUN1:def 6
.= a * R1/.k by A3,A1,VFUNCT_1:def 4;
end;
hence thesis by A2,RLVECT_2:3;
end;
begin :: 2. Integral Linear Space
reserve x,y for set;
reserve a,b for Real;
reserve i,j for Integer;
reserve V for RealLinearSpace;
reserve W1,W2,W3 for Subspace of V;
reserve v,v1,v2,v3,u,w,w1,w2,w3 for VECTOR of V;
reserve A,B,C for Subset of V;
reserve L,L1,L2 for Linear_Combination of V;
reserve l,l1,l2 for Linear_Combination of A;
definition let V,i,L;
func i * L -> Linear_Combination of V means :Def1:
for v holds it.v = i * L.v;
existence
proof
deffunc F(Element of V)= In(i * L.$1,REAL);
consider f being Function of the carrier of V, REAL such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let v be Element of V;
assume not v in Carrier(L);
then
A2: L.v = 0;
thus f.v = F(v) by A1
.= 0 by A2;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
take f;
let v;
f.v = F(v) by A1;
hence thesis;
end;
uniqueness
proof
let L1,L2;
assume that
A3: for v holds L1.v = i * L.v and
A4: for v holds L2.v = i * L.v;
let v;
thus L1.v = i * L.v by A3
.= L2.v by A4;
end;
end;
definition let V,A;
func Z_Lin(A) -> Subset of V equals
{Sum(l) : rng l c= INT};
correctness
proof
set A1 = {Sum(l) : rng l c= INT};
A1 c= the carrier of V
proof
let x be object;
assume x in A1;
then ex l st x = Sum(l) & rng l c= INT;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th4:
a = i implies a*l = i*l
proof
assume A1:a=i;
for v be VECTOR of V holds (i*l).v = a * l.v by A1,Def1;
hence thesis by RLVECT_2:def 11;
end;
theorem Th5:
rng l1 c= INT & rng l2 c= INT implies rng (l1+l2) c= INT
proof
assume A1: rng l1 c= INT & rng l2 c= INT;
let y be object;
assume A2:y in rng (l1+l2);
consider x be object such that
A3: x in the carrier of V & y=(l1+l2).x by A2,FUNCT_2:11;
reconsider z=x as VECTOR of V by A3;
l1.z in rng l1 by FUNCT_2:4; then
reconsider z1=l1.z as Integer by A1;
l2.z in rng l2 by FUNCT_2:4; then
reconsider z2=l2.z as Integer by A1;
(l1+l2).z = z1+ z2 by RLVECT_2:def 10;
hence y in INT by A3,INT_1:def 2;
end;
theorem Th6:
rng l c= INT implies rng (i*l) c= INT
proof
assume A1:rng l c= INT;
let y be object;
assume A2:y in rng (i*l);
consider x be object such that
A3: x in the carrier of V & y=(i*l).x by A2,FUNCT_2:11;
reconsider z=x as VECTOR of V by A3;
reconsider ii=i as Real;
l.z in rng l by FUNCT_2:4; then
reconsider z1=l.z as Integer by A1;
(i*l).z = (ii*l).z by Th4
.= i*z1 by RLVECT_2:def 11;
hence y in INT by A3,INT_1:def 2;
end;
theorem Th7:
rng (ZeroLC(V)) c= INT
proof
let y be object;
assume A1:y in rng (ZeroLC(V));
consider x be object such that
A2: x in the carrier of V & y=(ZeroLC(V)).x by A1,FUNCT_2:11;
reconsider z = x as VECTOR of V by A2;
ZeroLC(V).z = 0 by RLVECT_2:20;
hence y in INT by A2,NUMBERS:17;
end;
theorem Th8:
Z_Lin(A) c= the carrier of Lin(A)
proof
let x be object;
assume x in Z_Lin(A); then
consider l1 being Linear_Combination of A such that
A1: x = Sum(l1) & rng l1 c= INT;
x in Lin(A) by A1,RLVECT_3:14;
hence thesis by STRUCT_0:def 5;
end;
theorem Th9:
v in Z_Lin(A) & u in Z_Lin(A) implies v + u in Z_Lin(A)
proof
assume that
A1: v in Z_Lin(A) and
A2: u in Z_Lin(A);
consider l1 being Linear_Combination of A such that
A3: v = Sum(l1) & rng l1 c= INT by A1;
consider l2 being Linear_Combination of A such that
A4: u = Sum(l2) & rng l2 c= INT by A2;
reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38;
A5: rng f c= INT by A3,A4,Th5;
v + u = Sum(f) by A3,A4,RLVECT_3:1;
hence thesis by A5;
end;
theorem Th10:
v in Z_Lin(A) implies i*v in Z_Lin(A)
proof
assume v in Z_Lin(A);
then consider l such that
A1: v = Sum(l) & rng l c= INT;
reconsider a=i as Real;
A2: a*l=i*l by Th4; then
reconsider f = i * l as Linear_Combination of A by RLVECT_2:44;
A3: i * v = Sum(f) by A1,A2,RLVECT_3:2;
rng (i * l) c= INT by Th6,A1;
hence thesis by A3;
end;
theorem Th11:
0.V in Z_Lin(A)
proof
reconsider l = ZeroLC(V) as Linear_Combination of A by RLVECT_2:22;
A1: Sum(l) = 0.V by RLVECT_2:30;
rng l c= INT by Th7;
hence thesis by A1;
end;
theorem Th12:
x in A implies x in Z_Lin(A)
proof
assume
A1: x in A;
then reconsider v = x as VECTOR of V;
consider f being Function of the carrier of V, REAL such that
A2: f.v = In(1,REAL) and
A3: for u st u <> v holds f.u = H(u) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
ex T being finite Subset of V st for u st not u in T holds f.u = 0
proof
take T = {v};
let u;
assume not u in T;
then u <> v by TARSKI:def 1;
hence thesis by A3;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4: Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A5: x = u and
A6: f.u <> 0;
u = v by A3,A6;
hence thesis by A5,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;
A7: Sum(f) = f.v * v by RLVECT_2:32
.= v by A2,RLVECT_1:def 8;
{v} c= A by A1,ZFMISC_1:31;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
rng f c= INT
proof
let y be object;
assume A8:y in rng f;
consider x be object
such that A9: x in the carrier of V & y=f.x by A8,FUNCT_2:11;
reconsider z=x as VECTOR of V by A9;
per cases;
suppose z <> v; then
f.z = 0 by A3;
hence y in INT by A9,NUMBERS:17;
end;
suppose z = v;
hence y in INT by A2,A9,NUMBERS:17;
end;
end;
hence thesis by A7;
end;
theorem Th13:
A c= B implies Z_Lin(A) c= Z_Lin(B)
proof
assume
A1: A c= B;
let v be object;
assume v in Z_Lin(A);
then consider l such that
A2: v = Sum(l) & rng l c= INT;
reconsider l as Linear_Combination of B by A1,RLVECT_2:21;
Sum(l) = v by A2;
hence v in Z_Lin(B) by A2;
end;
theorem
Z_Lin(A \/ B) = Z_Lin(A) + Z_Lin(B)
proof
now
let v be object;
assume v in Z_Lin(A \/ B);
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) & rng l c= INT;
deffunc F(object)=l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred P[object] means $1 in C;
defpred D[object] means $1 in D;
A2: for x being object st x in the carrier of V
holds (P[x] implies F(x) in REAL) & (
not P[x ] implies H(x) in REAL) by XREAL_0:def 1;
consider f being Function of the carrier of V, REAL such that
A3: for x being object st x in the carrier of V
holds (P[x] implies f.x = F(x)) &
(not P[x] implies f.x = H(x)) from FUNCT_2:sch 5 (A2);
reconsider C as finite Subset of V;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
for u holds not u in C implies f.u = 0 by A3;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4: rng f c= INT
proof
let y be object;
assume A5:y in rng f;
consider x be object such that
A6: x in the carrier of V & y=f.x by A5,FUNCT_2:11;
reconsider z=x as VECTOR of V by A6;
per cases;
suppose not z in C; then
f.z = 0 by A3;
hence y in INT by A6,NUMBERS:17;
end;
suppose z in C; then
f.z = l.z by A3; then
f.z in rng l by FUNCT_2:4;
hence y in INT by A6,A1;
end;
end;
A7: Carrier(f) c= C
proof
let x be object;
assume x in Carrier(f); then
A8: ex u st x = u & f.u <> 0;
assume not x in C;
hence thesis by A3,A8;
end;
C c= A by XBOOLE_1:17;
then Carrier(f) c= A by A7;
then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
A9: for x being object st x in the carrier of V
holds (D[x] implies F(x) in REAL) & (
not D[x] implies H(x) in REAL) by XREAL_0:def 1;
consider g being Function of the carrier of V, REAL such that
A10: for x being object st x in the carrier of V
holds (D[x] implies g.x = F(x)) &
(not D[x] implies g.x = H(x)) from FUNCT_2:sch 5(A9);
reconsider D as finite Subset of V;
reconsider g as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
for u holds not u in D implies g.u = 0 by A10;
then reconsider g as Linear_Combination of V by RLVECT_2:def 3;
A11: rng g c= INT
proof
let y be object;
assume A12:y in rng g;
consider x be object
such that A13: x in the carrier of V & y=g.x by A12,FUNCT_2:11;
reconsider z=x as VECTOR of V by A13;
per cases;
suppose not z in D;
then g.z = 0 by A10;
hence y in INT by A13,NUMBERS:17;
end;
suppose z in D;
then g.z = l.z by A10;
then g.z in rng l by FUNCT_2:4;
hence y in INT by A13,A1;
end;
end;
A14: D c= B
proof
let x be object;
assume x in D; then
A15: x in Carrier(l) & not x in A by XBOOLE_0:def 5;
Carrier(l) c= A \/ B by RLVECT_2:def 6;
hence thesis by A15,XBOOLE_0:def 3;
end;
Carrier(g) c= D
proof
let x be object;
assume x in Carrier(g); then
A16: ex u st x = u & g.u <> 0;
assume not x in D;
hence thesis by A10,A16;
end;
then Carrier(g) c= B by A14;
then reconsider g as Linear_Combination of B by RLVECT_2:def 6;
l = f + g
proof
let v;
now
per cases;
suppose
A17: v in C;
A18: now
assume v in D;
then not v in A by XBOOLE_0:def 5;
hence contradiction by A17,XBOOLE_0:def 4;
end;
thus (f + g).v = f.v + g.v by RLVECT_2:def 10
.= l.v + g.v by A3,A17
.= l.v + z0 by A10,A18
.= l.v;
end;
suppose
A19: not v in C;
now
per cases;
suppose
A20: v in Carrier(l);
A21: now
assume not v in D;
then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
hence contradiction by A19,A20,XBOOLE_0:def 4;
end;
thus (f + g). v = f.v + g.v by RLVECT_2:def 10
.= z0 + g.v by A3,A19
.= l.v by A10,A21;
end;
suppose
A22: not v in Carrier(l); then
A23: not v in D by XBOOLE_0:def 5;
A24: not v in C by A22,XBOOLE_0:def 4;
thus (f + g).v = f.v + g.v by RLVECT_2:def 10
.= z0 + g.v by A3,A24
.= z0 + z0 by A10,A23
.= l.v by A22;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A25: v = Sum(f) + Sum(g) by A1,RLVECT_3:1;
Sum(f) in Z_Lin(A) & Sum(g) in Z_Lin(B) by A4,A11;
hence v in Z_Lin(A) + Z_Lin(B) by A25;
end;
then
A26: Z_Lin(A \/ B) c= Z_Lin(A) + Z_Lin(B);
A27: Z_Lin(A) c=Z_Lin(A \/ B) & Z_Lin(B) c= Z_Lin(A \/ B) by Th13,XBOOLE_1:7;
now let x be object;
assume x in Z_Lin(A) + Z_Lin(B); then
consider u,v be Element of V such that
A28:x=u+v & u in Z_Lin(A) & v in Z_Lin(B);
thus x in Z_Lin(A \/ B) by A28,A27,Th9;
end; then
Z_Lin(A) + Z_Lin(B) c= Z_Lin(A \/ B);
hence thesis by A26,XBOOLE_0:def 10;
end;
theorem
Z_Lin(A /\ B) c= Z_Lin(A) /\ Z_Lin(B)
proof
Z_Lin(A /\ B) c=Z_Lin(A) & Z_Lin(A /\ B) c=Z_Lin(B) by Th13,XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
theorem Th16:
x in Z_Lin{v} iff ex a be Integer st x = a * v
proof
thus x in Z_Lin{v} implies ex a be Integer st x = a * v
proof
assume x in Z_Lin{v};
then consider l being Linear_Combination of {v} such that
A1: x = Sum(l) & rng l c= INT;
A2: Sum(l) = l.v * v by RLVECT_2:32;
ex f being Function st l = f & dom f = the carrier of V
& rng f c= REAL by FUNCT_2:def 2; then
l.v in rng l by FUNCT_1:3;
hence thesis by A1,A2;
end;
given a0 be Integer such that
A3: x = a0 * v;
reconsider a=a0 as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V, REAL such that
A4: f.v = a and
A5: for z being VECTOR of V st z <> v holds f.z = H(z) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
A6:now
let z be VECTOR of V;
assume not z in {v};
then z <> v by TARSKI:def 1;
hence f.z = 0 by A5;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {v}
proof
let x be object;
assume
A7: x in Carrier f;
then f.x <> 0 by RLVECT_2:19;
then x = v by A5,A7;
hence thesis by TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;
A8:Sum(f) = x by A3,A4,RLVECT_2:32;
rng f c= INT
proof
let y be object;
assume A9:y in rng f;
consider x be object
such that A10: x in the carrier of V & y=f.x by A9,FUNCT_2:11;
reconsider z=x as VECTOR of V by A10;
per cases;
suppose not z in {v}; then
f.z = 0 by A6;
hence y in INT by A10,NUMBERS:17;
end;
suppose z in {v}; then
f.z = a0 by A4,TARSKI:def 1;
hence y in INT by A10,INT_1:def 2;
end;
end;
hence thesis by A8;
end;
theorem
v in Z_Lin{v}
proof
v in {v} by TARSKI:def 1;
hence thesis by Th12;
end;
theorem
x in v + Z_Lin{w} iff ex a be Integer st x = v + a * w
proof
thus x in v + Z_Lin{w} implies ex a be Integer st x = v + a * w
proof
assume x in v + Z_Lin{w};
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin{w};
ex a be Integer st u = a * w by A2,Th16;
hence thesis by A1;
end;
given a0 be Integer such that
A3: x = v + a0 * w;
a0 * w in Z_Lin{w} by Th16;
hence thesis by A3;
end;
theorem Th19:
x in Z_Lin{w1,w2} iff ex a,b be Integer st x = a * w1 + b * w2
proof
thus x in Z_Lin{w1,w2} implies ex a,b be Integer
st x = a * w1 + b * w2
proof
assume
A1: x in Z_Lin{w1,w2};
now
per cases;
suppose
w1 = w2;
then {w1,w2} = {w1} by ENUMSET1:29;
then consider a be Integer such that
A2: x = a * w1 by A1,Th16;
consider b be Integer such that
A3: b = 0;
x = a * w1 + 0.V by A2,RLVECT_1:4;
then x = a * w1 + b * w2 by A3,RLVECT_1:10;
hence thesis;
end;
suppose
A4: w1 <> w2;
consider l being Linear_Combination of {w1,w2} such that
A5: x = Sum(l) & rng l c= INT by A1;
A6: x = l.w1 * w1 + l.w2 * w2 by A4,A5,RLVECT_2:33;
ex f being Function st l = f & dom f = the carrier of V
& rng f c= REAL by FUNCT_2:def 2; then
l.w1 in rng l & l.w2 in rng l by FUNCT_1:3;
hence thesis by A5,A6;
end;
end;
hence thesis;
end;
given a0,b0 be Integer such that
A7: x = a0 * w1 + b0 * w2;
reconsider a=a0,b=b0 as Element of REAL by XREAL_0:def 1;
now
per cases;
suppose
A8: w1 = w2;
then x = (a + b) * w1 by A7,RLVECT_1:def 6;
then x in Z_Lin{w1} by Th16;
hence thesis by A8,ENUMSET1:29;
end;
suppose
A9: w1 <> w2;
consider f being Function of the carrier of V, REAL such that
A10: f.w1 = a & f.w2 = b and
A11: for u st u <> w1 & u <> w2 holds f.u = H(u) from FUNCT_2:sch 7(A9);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
A12: now
let u;
assume not u in {w1,w2};
then u <> w1 & u <> w2 by TARSKI:def 2;
hence f.u = 0 by A11;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {w1,w2}
proof
let x be object;
assume that
A13: x in Carrier f and
A14: not x in {w1,w2};
x <> w1 & x <> w2 by A14,TARSKI:def 2;
then f.x = 0 by A11,A13;
hence contradiction by A13,RLVECT_2:19;
end;
then reconsider f as Linear_Combination of {w1,w2} by RLVECT_2:def 6;
A15: x = Sum(f) by A7,A9,A10,RLVECT_2:33;
rng f c= INT
proof
let y be object;
assume A16:y in rng f;
consider x be object
such that A17: x in the carrier of V & y=f.x by A16,FUNCT_2:11;
reconsider v=x as VECTOR of V by A17;
per cases;
suppose not v in {w1,w2}; then
f.v = 0 by A12;
hence y in INT by A17,NUMBERS:17;
end;
suppose v in {w1,w2}; then
f.v = a0 or f.v = b0 by A10,TARSKI:def 2;
hence y in INT by A17,INT_1:def 2;
end;
end;
hence thesis by A15;
end;
end;
hence thesis;
end;
theorem
w1 in Z_Lin{w1,w2}
proof
w1 in {w1,w2} by TARSKI:def 2;
hence thesis by Th12;
end;
theorem
x in v + Z_Lin{w1,w2} iff ex a,b be Integer
st x = v + a * w1 + b * w2
proof
thus x in v + Z_Lin{w1,w2} implies
ex a,b be Integer st x = v + a * w1 + b * w2
proof
assume x in v + Z_Lin{w1,w2};
then consider u such that
A1: x = v + u and
A2: u in Z_Lin{w1,w2};
consider a,b be Integer such that
A3: u = a * w1 + b * w2 by A2,Th19;
take a,b;
thus thesis by A1,A3,RLVECT_1:def 3;
end;
given a,b be Integer such that
A4: x = v + a * w1 + b * w2;
a * w1 + b * w2 in Z_Lin{w1,w2} by Th19;
then v + (a * w1 + b * w2) in v + Z_Lin{w1,w2};
hence thesis by A4,RLVECT_1:def 3;
end;
theorem Th22:
x in Z_Lin{v1,v2,v3} iff ex a,b,c be Integer
st x = a * v1 + b * v2 + c * v3
proof
thus x in Z_Lin{v1,v2,v3} implies ex a,b,c be Integer
st x = a * v1 + b * v2 + c * v3
proof
assume
A1: x in Z_Lin{v1,v2,v3};
now
per cases;
suppose
A2: v1 <> v2 & v1 <> v3 & v2 <> v3;
consider l being Linear_Combination of {v1,v2,v3} such that
A3: x = Sum(l) & rng l c= INT by A1;
A4: x = l.v1 * v1 + l.v2 * v2 + l.v3 * v3 by A2,A3,RLVECT_4:6;
ex f being Function st l = f & dom f = the carrier of V
& rng f c= REAL by FUNCT_2:def 2; then
l.v1 in rng l & l.v2 in rng l & l.v3 in rng l by FUNCT_1:3;
hence thesis by A3,A4;
end;
suppose
v1 = v2 or v1 = v3 or v2 = v3; then
A5: {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {
v3,v3,v1} by ENUMSET1:30,59;
now
per cases by A5,ENUMSET1:30;
suppose
{v1,v2,v3} = {v1,v2};
then consider a,b be Integer such that
A6: x = a * v1 + b * v2 by A1,Th19;
consider c be Integer such that
A7: c = 0;
x = a * v1 + b * v2 + 0.V by A6,RLVECT_1:4
.= a * v1 + b * v2 + c * v3 by A7,RLVECT_1:10;
hence thesis;
end;
suppose
{v1,v2,v3} = {v1,v3};
then consider a,b be Integer such that
A8: x = a * v1 + b * v3 by A1,Th19;
consider c be Integer such that
A9: c = 0;
x = a * v1 + 0.V + b * v3 by A8,RLVECT_1:4
.= a * v1 + c * v2 + b * v3 by A9,RLVECT_1:10;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
given a0,b0,c0 be Integer such that
A10: x = a0 * v1 + b0 * v2 + c0 * v3;
reconsider a=a0, b=b0, c = c0 as Element of REAL by XREAL_0:def 1;
now
per cases;
suppose
A11: v1 = v2 or v1 = v3 or v2 = v3;
now
per cases by A11;
suppose v1 = v2;
then {v1,v2,v3} = {v1,v3} & x = (a + b) * v1 + c * v3 by A10,
ENUMSET1:30,RLVECT_1:def 6;
hence thesis by Th19;
end;
suppose
A12: v1 = v3; then
A13: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57
.= {v2,v1} by ENUMSET1:30;
x = b * v2 + (a * v1 + c * v1) by A10,A12,RLVECT_1:def 3
.= b * v2 + (a + c) * v1 by RLVECT_1:def 6;
hence thesis by A13,Th19;
end;
suppose
A14: v2 = v3;
then
A15: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59
.= {v1,v2} by ENUMSET1:30;
x = a * v1 + (b * v2 + c * v2) by A10,A14,RLVECT_1:def 3
.= a * v1 + (b + c) * v2 by RLVECT_1:def 6;
hence thesis by A15,Th19;
end;
end;
hence thesis;
end;
suppose
A16: v1 <> v2 & v1 <> v3 & v2 <> v3;
A17: v1 <> v3 by A16;
A18: v2 <> v3 by A16;
A19: v1 <> v2 by A16;
consider f being Function of the carrier of V,REAL such that
A20: f.v1 = a & f.v2 = b & f.v3 = c and
A21: for v st v <> v1 & v <> v2 & v <> v3 holds f.v = H(v) from
RLVECT_4:sch 1(A19,A17, A18);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
A22: now
let v;
assume
A23: not v in {v1,v2,v3};
then
A24: v <> v3 by ENUMSET1:def 1;
v <> v1 & v <> v2 by A23,ENUMSET1:def 1;
hence f.v = 0 by A21,A24;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {v1,v2,v3}
proof
let x be object;
assume that
A25: x in Carrier f and
A26: not x in {v1,v2,v3};
A27: x <> v3 by A26,ENUMSET1:def 1;
x <> v1 & x <> v2 by A26,ENUMSET1:def 1;
then f.x = 0 by A21,A25,A27;
hence thesis by A25,RLVECT_2:19;
end;
then reconsider f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 6;
A28: x = Sum(f) by A10,A16,A20,RLVECT_4:6;
rng f c= INT
proof
let y be object;
assume A29:y in rng f;
consider x be object
such that A30: x in the carrier of V & y=f.x by A29,FUNCT_2:11;
reconsider v=x as VECTOR of V by A30;
per cases;
suppose not v in {v1,v2,v3};
then f.v = 0 by A22;
hence y in INT by A30,NUMBERS:17;
end;
suppose v in {v1,v2,v3}; then
f.v = a0 or f.v = b0 or f.v = c0 by A20,ENUMSET1:def 1;
hence y in INT by A30,INT_1:def 2;
end;
end;
hence thesis by A28;
end;
end;
hence thesis;
end;
theorem
w1 in Z_Lin{w1,w2,w3} & w2 in Z_Lin{w1,w2,w3} & w3 in Z_Lin{w1,w2,w3}
proof
A1: w3 in {w1,w2,w3} by ENUMSET1:def 1;
w1 in {w1,w2,w3} & w2 in {w1,w2,w3} by ENUMSET1:def 1;
hence thesis by A1,Th12;
end;
theorem
x in v + Z_Lin{w1,w2,w3}
iff ex a,b,c be Integer st x = v + a * w1 + b * w2 + c * w3
proof
thus x in v + Z_Lin{w1,w2,w3} implies ex a,b,c be Integer
st x = v + a * w1 + b * w2 + c * w3
proof
assume x in v + Z_Lin{w1,w2,w3};
then consider u such that
A1: x = v + u and
A2: u in Z_Lin{w1,w2,w3};
consider a,b,c be Integer such that
A3: u = a * w1 + b * w2 + c * w3 by A2,Th22;
take a,b,c;
x = v + (a * w1 + b * w2) + c * w3 by A1,A3,RLVECT_1:def 3;
hence thesis by RLVECT_1:def 3;
end;
given a,b,c be Integer such that
A4: x = v + a * w1 + b * w2 + c * w3;
a * w1 + b * w2 + c * w3 in Z_Lin{w1,w2,w3} by Th22;
then v + (a * w1 + b * w2 + c * w3) in v + Z_Lin{w1,w2,w3};
then v + (a * w1 + b * w2) + c * w3 in v + Z_Lin{w1,w2,w3}
by RLVECT_1:def 3;
hence thesis by A4,RLVECT_1:def 3;
end;
Lm1:
for RS be RealLinearSpace,
X be Subset of RS,
g1,h1 be FinSequence of RS,
a1 be INT-valued FinSequence st
rng g1 c= X & len g1 =len h1 & len g1 = len a1 &
for i be Nat
st i in Seg (len g1) holds
h1/.i=(a1.i)*(g1/.i)
holds Sum(h1) in Z_Lin(X)
proof
let RS be RealLinearSpace, X be Subset of RS;
defpred P[Nat] means
for g,h be FinSequence of RS,
s be INT-valued FinSequence st
rng g c= X &
len g = $1 & len g = len h & len g = len s &
for i be Nat st i in Seg (len g) holds
h/.i=(s.i)*(g/.i) holds
Sum(h) in Z_Lin(X);
A1: P[0]
proof
let g,h be FinSequence of RS, s be INT-valued FinSequence;
set x = Sum(h);
assume A2:rng g c= X &
len g = 0 & len g = len h & len g = len s &
for i be Nat st i in Seg (len g) holds h/.i=(s.i)*(g/.i);
Sum(h) = Sum(<*> the carrier of RS) by A2,FINSEQ_1:20
.=0.RS by RLVECT_1:43;
hence x in Z_Lin(X) by Th11;
end;
A3: now let n be Nat;
assume A4: P[n];
now let g,h be FinSequence of RS,
s be INT-valued FinSequence, x be set;
assume A5: x=Sum(h) & rng g c= X &
len g = n+1 & len g = len h & len g = len s &
for i be Nat st i in Seg (len g) holds h/.i=(s.i)*(g/.i);
reconsider gn = g|n as FinSequence of RS;
reconsider hn = h|n as FinSequence of RS;
reconsider sn = s|n as real-valued FinSequence;
rng gn c= X & len gn = n & len gn = len hn & len gn = len sn &
for i be Nat st i in Seg (len gn) holds
hn/.i=(sn.i)*(gn/.i)
proof
rng gn c= rng g by RELAT_1:70;
then A6: rng gn c= X by A5;
A7: n <= len g by A5,NAT_1:11;
A8: n <= len h by A5,NAT_1:11;
A9: len hn = n by A5,FINSEQ_1:59,NAT_1:11;
A10: len sn = n by A5,FINSEQ_1:59,NAT_1:11;
for i be Nat st i in Seg (len gn) holds
hn/.i=(sn.i)*(gn/.i)
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose n <> 0;
then A11: n >= 1 by NAT_1:14;
let i be Nat;
assume i in Seg (len gn);
then A12: i in Seg (n) by A5,FINSEQ_1:59,NAT_1:11;
n in Seg (len g) by A7,A11;
then n in dom g by FINSEQ_1:def 3;
then A13: gn/.i = g/.i by A12,FINSEQ_4:71;
n in Seg (len h) by A8,A11;
then n in dom h by FINSEQ_1:def 3;
then A14: hn/.i = h/.i by A12,FINSEQ_4:71;
i <= n by A12,FINSEQ_1:1;
then sn.i = s.i by FINSEQ_3:112;
hence thesis by A5,A12,A13,A14,FINSEQ_2:8;
end;
end;
hence thesis by A6,A9,A10,A5,FINSEQ_1:59,NAT_1:11;
end; then
A15:Sum(hn) in Z_Lin(X) by A4;
A16: n+1 in Seg (len g) by A5,FINSEQ_1:4;
A17: h/.(n+1) = s.(n+1)*g/.(n+1) by A5,FINSEQ_1:4;
A18: h = hn ^ <* s.(n+1)*g/.(n+1) *> by A5,A17,FINSEQ_5:21;
A19: n+1 in dom g by A16,FINSEQ_1:def 3;
then g/.(n+1) = g.(n+1) by PARTFUN1:def 6;
then g/.(n+1) in rng g by A19,FUNCT_1:3;
then g/.(n+1) in Z_Lin(X) by A5,Th12; then
A20: s.(n+1)*(g/.(n+1)) in Z_Lin(X) by Th10;
Sum(h) = Sum(hn)+Sum(<* s.(n+1)*g/.(n+1) *>) by A18,RLVECT_1:41
.= Sum(hn)+ s.(n+1)*(g/.(n+1)) by RLVECT_1:44;
hence x in Z_Lin(X) by A5,A15,A20,Th9;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
Lm2:
for x be set st x in Z_Lin(A) holds
ex g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence
st x=Sum(h1) &
rng g1 c= A & len g1 =len h1 & len g1 = len a1 &
for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i)
proof
let x be set;
assume x in Z_Lin(A); then
consider z be Linear_Combination of A such that
A1: x=Sum(z) & rng z c= INT;
consider F be FinSequence of V such that
A2: F is one-to-one & rng F = Carrier(z) & Sum(z)
= Sum(z (#) F) by RLVECT_2:def 8;
A3: len (z (#) F) = len F &
for i be Nat st i in dom (z (#) F)
holds (z (#) F).i = z.(F/.i) * F/.i by RLVECT_2:def 7;
defpred P0[Nat,set] means $2=z.(F/.$1);
A4: now let k be Nat;
assume k in Seg (len F);
z.(F/.k) in rng z by FUNCT_2:4;
hence ex x being Element of INT st P0[k,x] by A1;
end;
consider u be FinSequence of INT such that
A5: dom u = Seg (len F)
& for i be Nat st i in Seg (len F) holds P0[i,u.i]
from FINSEQ_1:sch 5(A4);
A6: rng F c= A by A2,RLVECT_2:def 6;
A7: len F = len (z (#) F) by RLVECT_2:def 7;
A8: len F = len u by A5,FINSEQ_1:def 3;
now
let i be Nat;
assume A9: i in Seg (len F); then
A10: i in dom (z (#) F) by A3,FINSEQ_1:def 3;
hence (z (#) F)/.i = (z (#) F).i by PARTFUN1:def 6
.= z.(F/.i) * F/.i by A10,RLVECT_2:def 7
.=u.i * F/.i by A5,A9;
end;
hence thesis by A6,A7,A8,A1,A2;
end;
theorem
for x be set holds x in Z_Lin(A) iff
ex g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence
st x=Sum(h1) &
rng g1 c= A & len g1 =len h1 & len g1 = len a1 &
for i be Nat
st i in Seg (len g1) holds
h1/.i=(a1.i)*(g1/.i) by Lm1,Lm2;
registration
let D be non empty set, n be Nat;
cluster n-element D-valued for FinSequence;
existence
proof
take n |-> the Element of D;
thus thesis;
end;
end;
definition
let RS be RealLinearSpace;
let f be FinSequence of RS;
func Z_Lin(f) -> Subset of RS equals
{Sum(g) where g is (len f)-element FinSequence of RS :
ex a be (len f)-element INT-valued FinSequence
st for i be Nat st i in Seg (len f) holds g/.i=(a.i)*(f/.i)};
correctness
proof
now let x be object;
assume x in {Sum(g) where g is (len f)-element FinSequence of RS :
ex a be (len f)-element INT-valued FinSequence
st for i be Nat
st i in Seg (len f) holds
g/.i=(a.i)*(f/.i)}; then
ex g be (len f)-element FinSequence of RS st
x=Sum(g) & ex a be (len f)-element INT-valued FinSequence
st for i be Nat st i in Seg (len f) holds g/.i=(a.i)*(f/.i);
hence x in the carrier of RS;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th26:
for RS be RealLinearSpace,
f be FinSequence of RS,
x be set holds
x in Z_Lin(f) iff
ex g be (len f)-element FinSequence of RS,
a be (len f)-element INT-valued FinSequence st
x=Sum(g) & for i be Nat st i in Seg (len f) holds
g/.i=(a.i)*(f/.i)
proof
let RS be RealLinearSpace,
f be FinSequence of RS,
x be set;
hereby assume x in Z_Lin(f); then
consider g be (len f)-element FinSequence of RS such that
A1: x=Sum(g) & ex s be (len f)-element INT-valued FinSequence
st for i be Nat st i in Seg (len f) holds
g/.i=(s.i)*(f/.i);
consider s be (len f)-element INT-valued FinSequence such that
A2: for i be Nat st i in Seg (len f) holds g/.i=(s.i)*(f/.i) by A1;
take g,s;
thus x=Sum(g) & for i be Nat st i in Seg (len f) holds
g/.i=(s.i)*(f/.i) by A1,A2;
end;
assume ex g be (len f)-element FinSequence of RS,
a be (len f)-element INT-valued FinSequence st
x=Sum(g) & for i be Nat st i in Seg (len f) holds
g/.i=(a.i)*(f/.i);
hence x in Z_Lin(f);
end;
theorem Th27:
for RS be RealLinearSpace,
f be FinSequence of RS,
x, y being Element of RS,
a, b being Integer
st x in Z_Lin(f) & y in Z_Lin(f) holds
(a * x) + (b * y) in Z_Lin(f)
proof
let RS be RealLinearSpace;
let f be FinSequence of RS;
let x, y be Element of RS;
let a, b be Integer;
assume A1:x in Z_Lin(f) & y in Z_Lin(f);
consider g be (len f)-element FinSequence of RS,
s be (len f)-element INT-valued FinSequence such that
A2: x=Sum(g) &
for i be Nat st i in Seg (len f) holds
g/.i=(s.i)*(f/.i) by A1,Th26;
consider h be (len f)-element FinSequence of RS,
t be (len f)-element INT-valued FinSequence such that
A3: y=Sum(h) & for i be Nat st i in Seg (len f) holds
h/.i=(t.i)*(f/.i) by A1,Th26;
defpred P0[Nat,set] means $2=a*(s.$1) + b*(t.$1);
A4: for k be Nat st k in Seg (len f) holds
ex x being Element of INT st P0[k,x]
proof let k be Nat;
assume k in Seg (len f);
reconsider x = a*(s.k) + b*(t.k) as Element of INT by INT_1:def 2;
take x;
thus P0[k,x];
end;
consider u be FinSequence of INT such that
A5: dom u = Seg (len f)
& for i be Nat st i in Seg (len f) holds P0[i,u.i] from FINSEQ_1:sch 5(A4);
len u = len f by A5,FINSEQ_1:def 3;
then
reconsider u as (len f)-element INT-valued FinSequence by CARD_1:def 7;
defpred P1[Nat,set] means $2=a*g/.$1 + b*h/.$1;
A6: for k be Nat st k in Seg (len f) holds
ex x being Element of RS st P1[k,x];
consider w be FinSequence of RS such that
A7: dom w = Seg (len f)
& for i be Nat st i in Seg (len f) holds P1[i,w.i]
from FINSEQ_1:sch 5(A6);
len w = len f by A7,FINSEQ_1:def 3; then
reconsider w as (len f)-element FinSequence of RS by CARD_1:def 7;
A8: now let i be Nat;
assume A9: i in Seg (len f);
hence w/.i=w.i by A7,PARTFUN1:def 6
.=a*g/.i + b*h/.i by A7,A9;
end;
a in INT by INT_1:def 2;
then reconsider a0=a as Element of REAL by NUMBERS:15;
b in INT by INT_1:def 2;
then reconsider b0=b as Element of REAL by NUMBERS:15;
dom (a0(#)g) = dom g by VFUNCT_1:def 4
.= Seg (len g) by FINSEQ_1:def 3;
then
A10: a0(#)g is FinSequence-like;
rng (a0(#)g) c= the carrier of RS; then
reconsider ag = a0(#)g as FinSequence of RS by A10,FINSEQ_1:def 4;
dom (b0(#)h) = dom h by VFUNCT_1:def 4
.= Seg (len h) by FINSEQ_1:def 3;
then
A11: b0(#)h is FinSequence-like;
rng (b0(#)h) c= the carrier of RS;
then
reconsider bh = b0(#)h as FinSequence of RS by A11,FINSEQ_1:def 4;
A12: dom (a0(#)g) = dom g by VFUNCT_1:def 4
.=Seg (len g) by FINSEQ_1:def 3
.=Seg (len f) by CARD_1:def 7; then
A13: len ag = len f by FINSEQ_1:def 3;
A14: dom (b0(#)h) = dom h by VFUNCT_1:def 4
.=Seg (len h) by FINSEQ_1:def 3
.=Seg (len f) by CARD_1:def 7;
A15:now let i be Nat;
assume A16:i in dom ag;
hence w.i = a*g/.i + b*h/.i by A7,A12
.= ag/.i + b*h/.i by A16,VFUNCT_1:def 4
.= ag/.i + bh/.i by A16,A14,A12,VFUNCT_1:def 4;
end;
A17: len ag = len bh & len ag = len w by A7,A13,A14,FINSEQ_1:def 3;
A18: for i be Nat st i in Seg (len f) holds
w/.i=(u.i)*(f/.i)
proof
let i be Nat;
assume A19:i in Seg (len f);
hence w/.i=a*g/.i + b*h/.i by A8
.=a*((s.i)*(f/.i)) + b*h/.i by A19,A2
.=a*((s.i)*(f/.i)) + b*((t.i)*(f/.i)) by A19,A3
.=(a*(s.i))*(f/.i) + b*((t.i)*(f/.i)) by RLVECT_1:def 7
.=(a*(s.i))*(f/.i) + (b*(t.i))*(f/.i) by RLVECT_1:def 7
.= (a*(s.i) + b*(t.i))* (f/.i) by RLVECT_1:def 6
.= (u.i)*(f/.i) by A19,A5;
end;
(a * x) + (b * y) = Sum(ag) + (b * Sum(h)) by A2,A3,Th3
.= Sum(ag) + Sum(bh) by Th3
.= Sum(w) by A15,A17,RLVECT_2:2;
hence (a * x) + (b * y) in Z_Lin(f) by A18;
end;
theorem Th28:
for RS be RealLinearSpace,
f be FinSequence of RS st f = (Seg len f) --> 0.RS
holds Sum(f)=0.RS
proof
let RS be RealLinearSpace, f be FinSequence of RS;
assume A1:f = (Seg len f) --> 0.RS;
A2:now let k be Nat, v be Element of RS;
assume A3: k in dom f & v = f.k; then
k in Seg (len f) by FINSEQ_1:def 3; then
f.k = 0.RS by A1,FUNCOP_1:7;
hence f.k = -v by A3,RLVECT_1:12;
end;
len f = len f;
then Sum(f) = -Sum(f) by A2,RLVECT_1:40;
hence thesis by RLVECT_1:19;
end;
theorem Th29:
for RS be RealLinearSpace,
f be FinSequence of RS,
v be Element of RS ,i be Nat st i in Seg (len f)
& f = ( (Seg (len f)) --> 0.RS) +* ( {i} --> v)
holds Sum(f)=v
proof
let RS be RealLinearSpace, f be FinSequence of RS;
let v be Element of RS, i be Nat;
defpred P[Nat] means for g be FinSequence of RS
st len g = $1 & i in Seg (len g) &
g = ( (Seg (len g)) --> 0.RS) +* ( {i} --> v) holds Sum(g)=v;
A1: P[0];
A2: now let n be Nat;
assume A3: P[n];
now let f be FinSequence of RS;
assume A4: len f = n+1 & i in Seg (len f) &
f = ((Seg len f) --> 0.RS) +* ( {i} --> v);
reconsider g = f|n as FinSequence of RS;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A5: n+1 in dom f by A4,FINSEQ_1:def 3;
A6: len g = n by A4,FINSEQ_1:59,NAT_1:11;
f = (f|n) ^<*f.(n+1)*> by A4,FINSEQ_3:55
.=g ^<*f/.(n+1)*> by A5,PARTFUN1:def 6;
then
A7: Sum(f)=Sum(g)+Sum(<*f/.(n+1)*>) by RLVECT_1:41;
A8: dom ( {i} --> v) = {i} by FUNCOP_1:13;
let f1 be Function such that A9: f1 = (( Seg (len f)) --> 0.RS);
let f2 be Function such that A10: f2 = ( {i} --> v);
per cases;
suppose A11: i = n+1;
then dom f2 = {n+1} by A10,FUNCOP_1:13;
then g = f1|Seg(n) by A4,A9,A10,FINSEQ_3:14,FUNCT_4:72
.= ( ( Seg(len f) /\ Seg(n)) --> 0.RS) by A9,FUNCOP_1:12;
then A12: g = ( ( Seg (n)) --> 0.RS) by A4,FINSEQ_1:7,NAT_1:11;
A13: n+1 in {n+1} by ZFMISC_1:31;
then n+1 in dom f2 by A10,A11,FUNCOP_1:13;
then f.(n+1) = f2.(n+1) by A4,A10,FUNCT_4:13
.= v by A10,A11,A13,FUNCOP_1:7;
then A14: f/.(n+1) = v by A5,PARTFUN1:def 6;
Sum(g) = 0.RS by A6,A12,Th28;
hence Sum(f) = 0.RS + v by A7,A14,RLVECT_1:44
.= v by RLVECT_1:4;
end;
suppose A15: i <> n+1;
then i < n+1 or i > n+1 by XXREAL_0:1;
then 1 <= i & i <= n by A4,FINSEQ_1:1,NAT_1:13; then
A16: i in Seg (len g) by A6;
g = f1|Seg(n) +* f2|Seg(n) by A4,A9,A10,FUNCT_4:71
.= ( ( Seg(len f) /\ Seg(n)) --> 0.RS) +* f2|Seg(n) by A9,FUNCOP_1:12
.= ( ( Seg len g) --> 0.RS) +* f2|Seg(n) by A4,A6,FINSEQ_1:7,NAT_1:11
.= ( ( Seg len g) --> 0.RS) +*
({i} /\ Seg (n) --> v) by A10,FUNCOP_1:12; then
A17: g = ( (Seg (len g)) --> 0.RS)
+* ( {i} --> v) by A6,A16,ZFMISC_1:46;
not {n+1} c= dom f2 by A8,A10,A15,ZFMISC_1:3;
then not n+1 in dom f2 by ZFMISC_1:31;
then f.(n+1) = f1.(n+1) by A4,A9,A10,FUNCT_4:11
.= 0.RS by A4,A9,FINSEQ_1:4,FUNCOP_1:7;
then A18: f/.(n+1) = 0.RS by A5,PARTFUN1:def 6;
Sum(g) = v by A16,A17,A6,A3;
hence Sum(f) = v + 0.RS by A7,A18,RLVECT_1:44
.= v by RLVECT_1:4;
end;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th30:
for RS be RealLinearSpace,
f be FinSequence of RS,
i be Nat st i in Seg (len f) holds f/.i in Z_Lin(f)
proof
let RS be RealLinearSpace, f be FinSequence of RS;
let i be Nat;
assume A1: i in Seg (len f);
set s = ( (Seg len f) --> 0) +* ( {i} --> 1);
A2:dom s = Seg len f
proof
dom s = dom ((Seg (len f)) --> 0) \/ dom( {i} -->1) by FUNCT_4:def 1
.= (Seg (len f)) \/ dom( {i} -->1) by FUNCOP_1:13
.= (Seg (len f)) \/ {i} by FUNCOP_1:13;
hence thesis by A1,ZFMISC_1:40;
end; then
A3: s is FinSequence-like;
rng s c= INT by INT_1:def 2;
then
reconsider s as FinSequence of INT by A3,FINSEQ_1:def 4;
len s = len f by A2,FINSEQ_1:def 3; then
reconsider s as (len f)-element INT-valued FinSequence by CARD_1:def 7;
defpred Q[Nat,set] means $2=s.$1*f/.$1;
A6: for k be Nat st k in Seg (len f) holds
ex x being Element of RS st Q[k,x];
consider w be FinSequence of RS such that
A7: dom w = Seg len f & for i be Nat st i in Seg (len f) holds
Q[i,w.i] from FINSEQ_1:sch 5(A6);
A8:len w = len f by A7,FINSEQ_1:def 3;
then reconsider w as (len f)-element FinSequence of RS by CARD_1:def 7;
now let i be Nat;
assume A9: i in Seg len f;
hence w/.i=w.i by A7,PARTFUN1:def 6
.=s.i*f/.i by A7,A9;
end; then
A10:Sum(w) in Z_Lin(f);
A11:w = ( (Seg (len w)) --> 0.RS) +* ( {i} --> f/.i)
proof
consider w1 be Function such that A12: w1 = (( Seg (len f)) --> 0.RS);
A13: dom w1 = Seg (len f) by A12,FUNCOP_1:13;
consider w2 be Function such that A14: w2 = ( {i} --> f/.i);
A15: dom w2 = {i} by A14,FUNCOP_1:13;
consider ww be Function such that A16: ww = w1 +* w2;
A17: dom ww = Seg (len f) \/ {i} by A13,A15,A16,FUNCT_4:def 1
.= Seg (len f) by A1,ZFMISC_1:40; then
reconsider ww as FinSequence by FINSEQ_1:def 2;
rng w1 c= {0.RS} by A12,FUNCOP_1:13;
then A18: rng w1 c= (the carrier of RS) by XBOOLE_1:1;
rng w2 c= {f/.i} by A14,FUNCOP_1:13;
then A19: rng w2 c= (the carrier of RS) by XBOOLE_1:1;
A20: rng ww c= rng w1 \/ rng w2 by A16,FUNCT_4:17;
rng w1 \/ rng w2 c= (the carrier of RS) by A18,A19,XBOOLE_1:8;
then rng ww c= (the carrier of RS) by A20;
then
reconsider ww as FinSequence of RS by FINSEQ_1:def 4;
for j being Nat st j in dom w holds w/.j = ww/.j
proof
let j be Nat such that A21: j in dom w;
A22: dom({i} --> 1) ={i} by FUNCOP_1:13;
per cases;
suppose A23: j in dom w2;
then A24: j = i by A15,TARSKI:def 1;
then w/.j = w.i by A21,PARTFUN1:def 6;
then A25: w/.j = s.i*f/.i by A7,A21,A24;
A26:i in {i} by TARSKI:def 1;
then A27: s.i = ({i} --> 1).i by A22,FUNCT_4:13
.= 1 by A26,FUNCOP_1:7;
ww/.j = ww.j by A7,A17,A21,PARTFUN1:def 6
.= w2.j by A16,A23,FUNCT_4:13
.= f/.i by A14,A15,A23,FUNCOP_1:7;
hence thesis by A25,A27,RLVECT_1:def 8;
end;
suppose A28: not j in dom w2;
w/.j = w.j by A21,PARTFUN1:def 6;
then A29: w/.j = s.j*f/.j by A7,A21;
not j in dom({i} --> 1) by A15,A28;
then A30: s.j = ( (Seg (len f)) --> 0).j by FUNCT_4:11
.= 0 by A7,A21,FUNCOP_1:7;
ww/.j = ww.j by A7,A17,A21,PARTFUN1:def 6
.= w1.j by A16,A28,FUNCT_4:11
.= 0.RS by A7,A12,A21,FUNCOP_1:7;
hence thesis by A29,A30,RLVECT_1:10;
end;
end;
hence thesis by A7,A8,A12,A14,A16,A17,FINSEQ_5:12;
end;
i in Seg (len w) by A7,A1,FINSEQ_1:def 3;
hence f/.i in Z_Lin(f) by A10,A11,Th29;
end;
theorem Th31:
for RS be RealLinearSpace,
f be FinSequence of RS holds
rng f c= Z_Lin(f)
proof
let RS be RealLinearSpace, f be FinSequence of RS;
let y be object;
assume y in rng f; then
consider x be object such that
A1: x in dom f & y=f.x by FUNCT_1:def 3;
A2: x in Seg len f by A1,FINSEQ_1:def 3;
reconsider i=x as Nat by A1;
y=f/.i by A1,PARTFUN1:def 6;
hence y in Z_Lin(f) by A2,Th30;
end;
theorem Th32:
for RS be RealLinearSpace,
f be non empty FinSequence of RS,
g,h be FinSequence of RS,
s be INT-valued FinSequence
st rng g c= Z_Lin(f) &
len g = len s & len g = len h &
for i be Nat st i in Seg (len g) holds
h/.i=(s.i)*(g/.i) holds
Sum(h) in Z_Lin(f)
proof
let RS be RealLinearSpace,
f be non empty FinSequence of RS;
1<=1 & 1 <= len f by FINSEQ_1:20; then
1 in Seg (len f); then
A1:f/.1 in Z_Lin(f) by Th30;
reconsider z0=0 as Element of INT by NUMBERS:17;
reconsider z1=1 as Element of INT by NUMBERS:17;
z0 * (f/.1) + z0 * (f/.1) in Z_Lin(f) by Th27,A1; then
z0 * (f/.1) + 0.RS in Z_Lin(f) by RLVECT_1:10; then
A2: 0.RS + 0.RS in Z_Lin(f) by RLVECT_1:10;
defpred P[Nat] means
for g,h be FinSequence of RS,
s be INT-valued FinSequence
st rng g c= Z_Lin(f) &
len g = $1 & len g = len s & len g = len h &
for i be Nat st i in Seg (len g) holds
h/.i=(s.i)*(g/.i) holds
Sum(h) in Z_Lin(f);
A3: P[0]
proof
let g,h be FinSequence of RS, s be INT-valued FinSequence;
assume A4:rng g c= Z_Lin(f) &
len g = 0 & len g = len s & len g = len h &
for i be Nat st i in Seg (len g) holds
h/.i=(s.i)*(g/.i);
Sum(h)= Sum(<*> the carrier of RS) by A4,FINSEQ_1:20
.=0.RS by RLVECT_1:43;
hence Sum(h) in Z_Lin(f) by A2,RLVECT_1:4;
end;
A5:now let n be Nat;
assume A6: P[n];
now let g,h be FinSequence of RS,
s be INT-valued FinSequence;
assume A7:rng g c= Z_Lin(f) &
len g = n+1 & len g = len s & len g = len h &
for i be Nat st i in Seg (len g) holds h/.i=(s.i)*(g/.i);
reconsider gn = g|n as FinSequence of RS;
reconsider hn = h|n as FinSequence of RS;
reconsider sn = s|n as INT-valued FinSequence;
A8:rng gn c= Z_Lin(f) &
len gn = n & len gn = len sn & len gn = len hn &
for i be Nat st i in Seg (len gn) holds
hn/.i=(sn.i)*(gn/.i)
proof
A9: rng gn c= rng g by RELAT_1:70;
A10: n <= len g by A7,NAT_1:11;
A11: n <= len h by A7,NAT_1:11;
A12: len hn = n by A7,FINSEQ_1:59,NAT_1:11;
A13: len sn = n by A7,FINSEQ_1:59,NAT_1:11;
for i be Nat st i in Seg (len gn) holds hn/.i=(sn.i)*(gn/.i)
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose n <> 0;
then A14: n >= 1 by NAT_1:14;
let i be Nat;
assume i in Seg (len gn);
then A15: i in Seg (n) by A7,FINSEQ_1:59,NAT_1:11;
n in Seg (len g) by A10,A14;
then n in dom g by FINSEQ_1:def 3;
then A16: gn/.i = g/.i by A15,FINSEQ_4:71;
n in Seg (len h) by A11,A14;
then n in dom h by FINSEQ_1:def 3;
then A17: hn/.i = h/.i by A15,FINSEQ_4:71;
i <= n by A15,FINSEQ_1:1;
then sn.i = s.i by FINSEQ_3:112;
hence thesis by A7,A15,A16,A17,FINSEQ_2:8;
end;
end;
hence thesis by A9,A10,A12,A13,A7,FINSEQ_1:59;
end;
A18:Sum(hn) in Z_Lin(f) by A8,A6;
A19: n+1 in Seg (len g) by A7,FINSEQ_1:4;
A20: h/.(n+1) = s.(n+1)*g/.(n+1) by A7,FINSEQ_1:4;
A21: h = hn ^ <* s.(n+1)*g/.(n+1) *> by A7,A20,FINSEQ_5:21;
A22: n+1 in dom g by A19,FINSEQ_1:def 3;
then g/.(n+1) = g.(n+1) by PARTFUN1:def 6;
then g/.(n+1) in rng g by A22,FUNCT_1:3;
then
z1*s.(n+1)*(g/.(n+1)) + z0 * (g/.(n+1)) in Z_Lin(f) by A7,Th27;
then z1*s.(n+1)*(g/.(n+1)) + 0.RS in Z_Lin(f) by RLVECT_1:10;
then z1*s.(n+1)*(g/.(n+1)) in Z_Lin(f) by RLVECT_1:4;
then z1*Sum(hn)+z1* (s.(n+1)*(g/.(n+1))) in Z_Lin(f) by A18,Th27;
then
A23: z1*Sum(hn)+s.(n+1)*(g/.(n+1)) in Z_Lin(f) by RLVECT_1:def 8;
Sum(h) =Sum(hn)+Sum(<* s.(n+1)*(g/.(n+1)) *>) by A21,RLVECT_1:41
.=Sum(hn)+ s.(n+1)*(g/.(n+1)) by RLVECT_1:44;
hence Sum(h) in Z_Lin(f) by A23,RLVECT_1:def 8;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A5);
hence thesis;
end;
theorem
for RS be RealLinearSpace,
f be non empty FinSequence of RS holds
Z_Lin (rng f) = Z_Lin f
proof
let RS be RealLinearSpace,
f be non empty FinSequence of RS;
for x be object holds x in Z_Lin (rng f) iff x in Z_Lin f
proof
let x be object;
hereby assume x in Z_Lin (rng f); then
consider g,h be FinSequence of RS,
a be INT-valued FinSequence such that
A1:x=Sum(h) & rng g c= rng f & len g =len h & len g = len a &
for i be Nat st i in Seg (len g) holds
h/.i=(a.i)*(g/.i) by Lm2;
rng f c= Z_Lin f by Th31;
hence x in Z_Lin f by A1,Th32,XBOOLE_1:1;
end;
assume x in Z_Lin f;
then consider g be (len f)-element FinSequence of RS,
a be (len f)-element INT-valued FinSequence such that
A2: x=Sum(g) & for i be Nat st i in Seg (len f) holds
g/.i=(a.i)*(f/.i) by Th26;
len f =len g & len a = len f by CARD_1:def 7;
hence x in Z_Lin (rng f) by A2,Lm1;
end;
hence thesis by TARSKI:2;
end;
theorem Th34:
Lin Z_Lin A = Lin A
proof
for x be object st x in A holds x in Z_Lin(A) by Th12; then
A c= Z_Lin(A); then
A1: Lin(A) is Subspace of Lin(Z_Lin(A)) by RLVECT_3:20;
reconsider W = the carrier of Lin(A) as Subset of V by RLSUB_1:def 2;
Lin(Z_Lin A) is Subspace of Lin(W) by Th8,RLVECT_3:20; then
Lin(Z_Lin A) is Subspace of Lin(A) by RLVECT_3:18;
hence thesis by A1,RLSUB_1:26;
end;
theorem Th35:
for x be set, g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence st x=Sum(h1) &
rng g1 c= Z_Lin(A) & len g1 =len h1 & len g1 = len a1 &
for i be Nat st i in Seg (len g1) holds
h1/.i=(a1.i)*(g1/.i) holds x in Z_Lin(A)
proof
reconsider z0=0 as Element of INT by NUMBERS:17;
reconsider z1=1 as Element of INT by NUMBERS:17;
defpred P[Nat] means for x be set, g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence st x = Sum(h1) &
rng g1 c= Z_Lin(A) & len g1 = $1 & len g1 =len h1 & len g1 = len a1 &
for i be Nat st i in Seg (len g1) holds
h1/.i=(a1.i)*(g1/.i) holds x in Z_Lin(A);
A1: P[0]
proof
let x be set, g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence;
assume A2: x = Sum(h1) &
rng g1 c= Z_Lin(A) & len g1 = 0 & len g1 =len h1 & len g1 = len a1 &
for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i);
Sum(h1) = Sum(<*> the carrier of V) by A2,FINSEQ_1:20
.= 0.V by RLVECT_1:43;
hence x in Z_Lin(A) by A2,Th11;
end;
A3: now let n be Nat;
assume A4: P[n];
now let x be set, g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence;
assume A5: x = Sum(h1) &
rng g1 c= Z_Lin(A) & len g1 = n+1 & len g1 =len h1 & len g1 = len a1 &
for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i);
reconsider gn = g1|n as FinSequence of V;
reconsider hn = h1|n as FinSequence of V;
reconsider an = a1|n as INT-valued FinSequence;
A6:rng gn c= Z_Lin(A) &
len gn = n & len gn = len an & len gn = len hn &
for i be Nat st i in Seg (len gn) holds
hn/.i=(an.i)*(gn/.i)
proof
A7: rng gn c= rng g1 by RELAT_1:70;
A8: n <= len g1 by A5,NAT_1:11;
A9: n <= len h1 by A5,NAT_1:11;
A10: len hn = n by A5,FINSEQ_1:59,NAT_1:11;
A11: len an = n by A5,FINSEQ_1:59,NAT_1:11;
for i be Nat st i in Seg (len gn) holds
hn/.i=(an.i)*(gn/.i)
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose n <> 0;
then A12: n >= 1 by NAT_1:14;
let i be Nat;
assume i in Seg (len gn);
then A13: i in Seg (n) by A5,FINSEQ_1:59,NAT_1:11;
n in Seg (len g1) by A8,A12;
then n in dom g1 by FINSEQ_1:def 3;
then A14: gn/.i = g1/.i by A13,FINSEQ_4:71;
n in Seg (len h1) by A9,A12;
then n in dom h1 by FINSEQ_1:def 3;
then A15: hn/.i = h1/.i by A13,FINSEQ_4:71;
i <= n by A13,FINSEQ_1:1;
then an.i = a1.i by FINSEQ_3:112;
hence thesis by A5,A13,A14,A15,FINSEQ_2:8;
end;
end;
hence thesis by A5,A7,A8,A10,A11,FINSEQ_1:59;
end;
A16: n+1 in Seg (len g1) by A5,FINSEQ_1:4;
A17: h1/.(n+1) = a1.(n+1)*g1/.(n+1) by A5,FINSEQ_1:4;
A18: h1 = hn ^ <* a1.(n+1)*g1/.(n+1) *> by A5,A17,FINSEQ_5:21;
A19: n+1 in dom g1 by A16,FINSEQ_1:def 3; then
g1/.(n+1) = g1.(n+1) by PARTFUN1:def 6; then
g1/.(n+1) in rng g1 by A19,FUNCT_1:3; then
z1*a1.(n+1)*(g1/.(n+1)) in Z_Lin(A) &
z0*(g1/.(n+1)) in Z_Lin(A) by A5,Th10; then
z1*a1.(n+1)*(g1/.(n+1)) + z0*(g1/.(n+1)) in Z_Lin(A) by Th9; then
z1*a1.(n+1)*(g1/.(n+1)) + 0.V in Z_Lin(A) by RLVECT_1:10; then
A20: z1*(a1.(n+1))*(g1/.(n+1)) in Z_Lin(A) by RLVECT_1:4;
z1*Sum(hn) in Z_Lin(A) by A4,A6,Th10;
then A21: z1*Sum(hn)+z1*(a1.(n+1))*(g1/.(n+1)) in Z_Lin(A) by A20,Th9;
Sum(h1) =Sum(hn)+Sum(<* a1.(n+1)*(g1/.(n+1)) *>) by A18,RLVECT_1:41
.=Sum(hn)+ a1.(n+1)*(g1/.(n+1)) by RLVECT_1:44;
hence Sum(h1)in Z_Lin(A) by A21,RLVECT_1:def 8;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem
Z_Lin Z_Lin A = Z_Lin A
proof
for x be object st x in A holds x in Z_Lin(A) by Th12;
then A c= Z_Lin(A); then
A1: Z_Lin(A) c= Z_Lin( Z_Lin(A)) by Th13;
Z_Lin Z_Lin A c= Z_Lin(A)
proof
let x be object;
assume x in Z_Lin( Z_Lin(A));
then consider g1,h1 be FinSequence of V,
a1 be INT-valued FinSequence such that
A2: x=Sum(h1) &
rng g1 c= Z_Lin(A) & len g1 = len h1 & len g1 = len a1 &
for i be Nat st i in Seg (len g1) holds h1/.i=(a1.i)*(g1/.i) by Lm2;
thus x in Z_Lin(A) by A2,Th35;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
Z_Lin(A) = Z_Lin(B) implies Lin(A) = Lin(B)
proof
assume Z_Lin(A) = Z_Lin(B);
hence Lin(A) = Lin( Z_Lin(B)) by Th34
.= Lin(B) by Th34;
end;