:: Affine Independence in Vector Spaces
:: by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-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 ALGSTR_0, ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CONVEX1, CONVEX2,
CONVEX3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2,
MONOID_0, ORDERS_1, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3,
RUSUB_4, SEMI_AF1, SETFAM_1, SUBSET_1, TARSKI, CLASSES1, SUPINF_2,
RLVECT_5, REAL_1, NUMBERS, NAT_1, CARD_3, XXREAL_0, STRUCT_0, ZFMISC_1,
RLAFFIN1, ORDINAL1, ORDINAL4, PARTFUN1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDERS_1, CARD_1, NUMBERS,
XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FINSET_1, SETFAM_1, DOMAIN_1,
ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, STRUCT_0,
FINSEQ_2, FINSEQ_3, FINSEQOP, CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2,
RLVECT_3, RLVECT_5, RLSUB_1, RLSUB_2, RUSUB_4, CONVEX1, CONVEX2, CONVEX3;
constructors BINOP_1, BINOP_2, CLASSES1, CONVEX1, CONVEX3, FINSEQOP, FINSOP_1,
MATRLIN, ORDERS_1, REALSET1, REAL_1, RLVECT_3, RLVECT_5, RVSUM_1,
RLSUB_2, RUSUB_5, SETWISEO, RELSET_1;
registrations BINOP_2, CARD_1, CONVEX1, FINSET_1, FINSEQ_2, FUNCT_1, FUNCT_2,
NAT_1, NUMBERS, RELAT_1, RLVECT_1, RLVECT_3, RUSUB_4, STRUCT_0, SUBSET_1,
VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, RLVECT_5, RELSET_1, RLVECT_2,
ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions CONVEX1, RLVECT_3, RUSUB_4, TARSKI, XBOOLE_0;
equalities CONVEX1, FINSEQ_1, RLVECT_2, RUSUB_4, RVSUM_1, STRUCT_0, SUBSET_1,
XBOOLE_0;
expansions CONVEX1, FINSEQ_1, RLVECT_2, RLVECT_3, RUSUB_4, STRUCT_0, TARSKI,
XBOOLE_0;
theorems CARD_2, CONVEX1, CONVEX3, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, FINSEQOP, FINSET_1, FINSOP_1, FUNCT_1, FUNCT_2, MATRPROB,
NAT_1, ORDERS_1, ORDINAL1, PARTFUN1, RELAT_1, RFINSEQ, RLTOPSP1,
RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_4, RLVECT_5, RLSUB_1, RLSUB_2,
RUSUB_4, RVSUM_1, SETFAM_1, STIRL2_1, TARSKI, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ZFMISC_1, CARD_1;
schemes FRAENKEL, FUNCT_1, FUNCT_2, NAT_1, TREES_2, XFAMILY;
begin :: Preliminaries
reserve x,y for set,
r,s for Real,
S for non empty addLoopStr,
LS,LS1,LS2 for Linear_Combination of S,
G for Abelian add-associative right_zeroed right_complementable
non empty addLoopStr,
LG,LG1,LG2 for Linear_Combination of G,
g,h for Element of G,
RLS for non empty RLSStruct,
R for vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct,
AR for Subset of R,
LR,LR1,LR2 for Linear_Combination of R,
V for RealLinearSpace,
v,v1,v2,w,p for VECTOR of V,
A,B for Subset of V,
F1,F2 for Subset-Family of V,
L,L1,L2 for Linear_Combination of V;
registration
let RLS;
let A be empty Subset of RLS;
cluster conv A -> empty;
coherence
proof
A=the empty convex Subset of RLS;
then A in Convex-Family A by CONVEX1:def 4;
hence thesis by SETFAM_1:4;
end;
end;
Lm1: for A be Subset of RLS holds A c=conv A
proof
let A be Subset of RLS;
let x be object;
assume A1: x in A;
A2: now let y;
assume y in Convex-Family A;
then A c=y by CONVEX1:def 4;
hence x in y by A1;
end;
[#]RLS is convex;
then [#]RLS in Convex-Family A by CONVEX1:def 4;
hence thesis by A2,SETFAM_1:def 1;
end;
registration let RLS;
let A be non empty Subset of RLS;
cluster conv A -> non empty;
coherence
proof
A c=conv A by Lm1;
hence thesis;
end;
end;
theorem
for v be Element of R holds conv {v} = {v}
proof
let v be Element of R;
{v} is convex
proof
let u1,u2 be VECTOR of R,r;
assume that
0<r and
r<1;
assume that
A1: u1 in {v} and
A2: u2 in {v};
u1=v & u2=v by A1,A2,TARSKI:def 1;
then r*u1+(1-r)*u2=(r+(1-r))*u1 by RLVECT_1:def 6
.=u1 by RLVECT_1:def 8;
hence thesis by A1;
end;
then conv{v}c={v} by CONVEX1:30;
hence thesis by ZFMISC_1:33;
end;
theorem
for A be Subset of RLS holds A c= conv A by Lm1;
theorem Th3:
for A,B be Subset of RLS st A c= B holds conv A c= conv B
proof
let A,B be Subset of RLS such that
A1: A c=B;
A2: Convex-Family B c=Convex-Family A
proof
let x be object;
assume A3: x in Convex-Family B;
then reconsider X=x as Subset of RLS;
B c=X by A3,CONVEX1:def 4;
then A4: A c=X by A1;
X is convex by A3,CONVEX1:def 4;
hence thesis by A4,CONVEX1:def 4;
end;
[#]RLS is convex;
then [#]RLS in Convex-Family B by CONVEX1:def 4;
then A5: meet(Convex-Family A)c=meet(Convex-Family B) by A2,SETFAM_1:6;
let y be object;
assume y in conv A;
hence thesis by A5;
end;
theorem
for S,A be Subset of RLS st A c= conv S holds conv S = conv(S\/A)
proof
let S,A be Subset of RLS such that
A1: A c=conv S;
thus conv S c=conv(S\/A) by Th3,XBOOLE_1:7;
S c=conv S by Lm1;
then S\/A c=conv S by A1,XBOOLE_1:8;
hence thesis by CONVEX1:30;
end;
Lm2: for V be add-associative right_zeroed right_complementable
non empty addLoopStr
for A,B be Subset of V for v be Element of V holds
(v+A)\(v+B)=v+(A\B)
proof
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let A,B be Subset of V;
let v be Element of V;
hereby let x be object;
assume A1: x in (v+A)\(v+B);
then x in v+A by XBOOLE_0:def 5;
then consider w be Element of V such that
A2: x=v+w and
A3: w in A;
not x in v+B by A1,XBOOLE_0:def 5;
then not w in B by A2;
then w in A\B by A3,XBOOLE_0:def 5;
hence x in v+(A\B) by A2;
end;
let x be object;
assume x in v+(A\B);
then consider w be Element of V such that
A4: x=v+w and
A5: w in A\B;
A6: not x in v+B
proof
assume x in v+B;
then consider s be Element of V such that
A7: x=v+s and
A8: s in B;
s=w by A4,A7,RLVECT_1:8;
hence thesis by A5,A8,XBOOLE_0:def 5;
end;
w in A by A5,XBOOLE_0:def 5;
then x in v+A by A4;
hence thesis by A6,XBOOLE_0:def 5;
end;
Lm3: for v,w be Element of S holds{v+w}=v+{w}
proof
let p,q be Element of S;
hereby let x be object;
assume x in {p+q};
then A1: x=p+q by TARSKI:def 1;
q in {q} by TARSKI:def 1;
hence x in p+{q} by A1;
end;
let x be object;
assume x in p+{q};
then consider v be Element of S such that
A2: x=p+v and
A3: v in {q};
v=q by A3,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th5:
for V be add-associative non empty addLoopStr
for A be Subset of V for v,w be Element of V
holds (v+w)+A = v+(w+A)
proof
let V be add-associative non empty addLoopStr;
let A be Subset of V;
let v,w be Element of V;
set vw=v+w;
thus vw+A c=v+(w+A)
proof
let x be object;
assume x in vw+A;
then consider s be Element of V such that
A1: x=vw+s & s in A;
w+s in w+A & x=v+(w+s) by A1,RLVECT_1:def 3;
hence thesis;
end;
let x be object;
assume x in v+(w+A);
then consider s be Element of V such that
A2: x=v+s and
A3: s in w+A;
consider r be Element of V such that
A4: s=w+r and
A5: r in A by A3;
x=vw+r by A2,A4,RLVECT_1:def 3;
hence thesis by A5;
end;
theorem Th6:
for V be Abelian right_zeroed non empty addLoopStr for A be Subset of V
holds 0.V + A = A
proof
let V be Abelian right_zeroed non empty addLoopStr;
let A be Subset of V;
thus 0.V+A c=A
proof
let x be object;
assume x in 0.V+A;
then ex s be Element of V st x=0.V+s & s in A;
hence thesis by RLVECT_1:def 4;
end;
let x be object;
assume A1: x in A;
then reconsider v=x as Element of V;
0.V+v=v by RLVECT_1:def 4;
hence thesis by A1;
end;
Lm4: for V be non empty addLoopStr
for A be Subset of V for v be Element of V holds card (v+A) c= card A
proof
let V be non empty addLoopStr;
let A be Subset of V;
let v be Element of V;
deffunc F(Element of V)=v+$1;
card {F(w) where w is Element of V:w in A} c= card A from TREES_2:sch 2;
hence thesis;
end;
theorem Th7:
for A be Subset of G holds card A = card (g+A)
proof
let A be Subset of G;
-g+(g+A) = (-g+g)+A by Th5
.= 0.G+A by RLVECT_1:5
.= A by Th6;
then A1: card A c= card(g+A) by Lm4;
card(g+A) c= card A by Lm4;
hence thesis by A1;
end;
theorem Th8:
for v be Element of S holds v + {}S = {}S
proof
let v be Element of S;
assume v+{}S<>{}S;
then consider x being object such that
A1: x in v+{}S by XBOOLE_0:def 1;
ex w be Element of S st x=v+w & w in {}S by A1;
hence contradiction;
end;
theorem Th9:
for A,B be Subset of RLS st A c= B holds r*A c= r*B
proof
let A,B be Subset of RLS such that
A1: A c=B;
let x be object;
assume x in r*A;
then ex v be Element of RLS st x=r*v & v in A;
hence thesis by A1;
end;
theorem Th10:
(r*s)* AR = r * (s*AR)
proof
set rs=r*s;
hereby let x be object;
assume x in rs*AR;
then consider v be Element of R such that
A1: x=rs*v & v in AR;
s*v in s*AR & x=r*(s*v) by A1,RLVECT_1:def 7;
hence x in r*(s*AR);
end;
let x be object;
assume x in r*(s*AR);
then consider v be Element of R such that
A2: x=r*v and
A3: v in s*AR;
consider w be Element of R such that
A4: v=s*w and
A5: w in AR by A3;
rs*w=x by A2,A4,RLVECT_1:def 7;
hence thesis by A5;
end;
theorem Th11:
1 * AR = AR
proof
hereby let x be object;
assume x in 1*AR;
then ex v be Element of R st x=1*v & v in AR;
hence x in AR by RLVECT_1:def 8;
end;
let x be object such that
A1: x in AR;
reconsider v=x as Element of R by A1;
x=1*v by RLVECT_1:def 8;
hence thesis by A1;
end;
theorem Th12:
0 * A c= {0.V}
proof
let x be object;
assume x in 0*A;
then ex v be Element of V st x=0*v & v in A;
then x=0.V by RLVECT_1:10;
hence thesis by TARSKI:def 1;
end;
theorem Th13:
for F be FinSequence of S holds (LS1+LS2) * F = (LS1*F) + (LS2*F)
proof
let p be FinSequence of S;
A1: len(LS1*p)=len p by FINSEQ_2:33;
A2: len(LS2*p)=len p by FINSEQ_2:33;
then reconsider L1p=LS1*p,L2p=LS2*p as Element of len p-tuples_on REAL
by A1,FINSEQ_2:92;
A3: len((LS1+LS2)*p)=len p by FINSEQ_2:33;
A4: now let k be Nat;
assume A5: 1<=k & k<=len p;
then k in dom((LS1+LS2)*p) by A3,FINSEQ_3:25;
then A6: ((LS1+LS2)*p).k=(LS1+LS2).(p.k) by FUNCT_1:12;
k in dom L1p by A1,A5,FINSEQ_3:25;
then A7: p.k in dom LS1 & L1p.k=LS1.(p.k) by FUNCT_1:11,12;
k in dom L2p by A2,A5,FINSEQ_3:25;
then A8: L2p.k=LS2.(p.k) by FUNCT_1:12;
dom LS1=the carrier of S by FUNCT_2:def 1;
hence ((LS1+LS2)*p).k = L1p.k+L2p.k by A6,A8,A7,RLVECT_2:def 10
.= (L1p+L2p).k by RVSUM_1:11;
end;
len(L1p+L2p)=len p by CARD_1:def 7;
hence thesis by A3,A4;
end;
theorem Th14:
for F be FinSequence of V holds (r*L) * F = r * (L*F)
proof
let p be FinSequence of V;
A1: len((r*L)*p)=len p by FINSEQ_2:33;
A2: len(L*p)=len p by FINSEQ_2:33;
then reconsider rLp=(r*L)*p,Lp=L*p as Element of len p-tuples_on REAL
by A1,FINSEQ_2:92;
A3: now let k be Nat;
assume A4: 1<=k & k<=len p;
then k in dom Lp by A2,FINSEQ_3:25;
then A5: Lp.k=L.(p.k) & p.k in dom L by FUNCT_1:11,12;
k in dom rLp by A1,A4,FINSEQ_3:25;
then A6: rLp.k=(r*L).(p.k) by FUNCT_1:12;
(r*Lp).k=r*(Lp.k) & dom L=the carrier of V
by FUNCT_2:def 1,RVSUM_1:44;
hence rLp.k=(r*Lp).k by A5,A6,RLVECT_2:def 11;
end;
len(r*Lp)=len p by CARD_1:def 7;
hence thesis by A1,A3;
end;
theorem Th15:
A is linearly-independent & A c= B & Lin B = V implies
ex I be linearly-independent Subset of V st A c= I & I c= B & Lin I = V
proof
assume that
A1: A is linearly-independent & A c=B and
A2: Lin B =V;
defpred P[set] means
(ex I be Subset of V st I=$1 & A c=I & I c=B & I is linearly-independent);
consider Q be set such that
A3: for Z be set holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XFAMILY:sch 1;
A4: now let Z be set;
assume that
A5: Z<>{} and
A6: Z c=Q and
A7: Z is c=-linear;
set W=union Z;
W c=the carrier of V
proof
let x be object;
assume x in W;
then consider X be set such that
A8: x in X and
A9: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A3,A6,A9;
hence thesis by A8;
end;
then reconsider W as Subset of V;
set y=the Element of Z;
y in Q by A5,A6;
then A10: ex I being Subset of V st I=y & A c=I & I c=B & I is
linearly-independent by A3;
A11: W is linearly-independent
proof
deffunc F(object)={D where D is Subset of V:$1 in D & D in Z};
let l be Linear_Combination of W;
assume that
A12: Sum(l)=0.V and
A13: Carrier(l)<>{};
consider f being Function such that
A14: dom f=Carrier(l) and
A15: for x be object st x in Carrier(l) holds f.x=F(x)
from FUNCT_1:sch 3;
reconsider M=rng f as non empty set by A13,A14,RELAT_1:42;
A16: now assume{} in M;
then consider x be object such that
A17: x in dom f and
A18: f.x={} by FUNCT_1:def 3;
Carrier(l)c=W by RLVECT_2:def 6;
then consider X be set such that
A19: x in X and
A20: X in Z by A14,A17,TARSKI:def 4;
reconsider X as Subset of V by A3,A6,A20;
X in {D where D is Subset of V:x in D & D in Z} by A19,A20;
hence contradiction by A14,A15,A17,A18;
end;
set F = the Choice_Function of M;
set S=rng F;
A21: F is Function of M, union M by A16,ORDERS_1:90;
the Element of M in M;
then A22: union M<>{} by A16,ORDERS_1:6;
then A23: dom F=M by FUNCT_2:def 1,A21;
A24: now let X be set;
assume X in S;
then consider x be object such that
A25: x in dom F and
A26: F.x=X by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
consider y be object such that
A27: y in dom f & f.y=x by A23,A25,FUNCT_1:def 3;
A28: x={D where D is Subset of V:y in D & D in Z} by A14,A15,A27;
X in x by A16,A23,A25,A26,ORDERS_1:89;
then ex D be Subset of V st D=X & y in D & D in Z by A28;
hence X in Z;
end;
A29: now let X,Y be set;
assume X in S & Y in S;
then X in Z & Y in Z by A24;
then X,Y are_c=-comparable by A7,ORDINAL1:def 8;
hence X c=Y or Y c=X;
end;
dom F is finite by A14,A23,FINSET_1:8;
then S is finite by FINSET_1:8;
then union S in S by A22,A29,CARD_2:62,A21;
then union S in Z by A24;
then consider I be Subset of V such that
A30: I=union S and
A c=I and
I c=B and
A31: I is linearly-independent by A3,A6;
Carrier(l) c= union S
proof
let x be object;
assume A32: x in Carrier(l);
then A33: f.x={D where D is Subset of V:x in D & D in Z} by A15;
A34: f.x in M by A14,A32,FUNCT_1:def 3;
then F.(f.x) in f.x by A16,ORDERS_1:89;
then A35: ex D be Subset of V st F.(f.x)=D & x in D & D in Z
by A33;
F.(f.x) in S by A23,A34,FUNCT_1:def 3;
hence thesis by A35,TARSKI:def 4;
end;
then l is Linear_Combination of I by A30,RLVECT_2:def 6;
hence thesis by A12,A13,A31;
end;
A36: W c=B
proof
let x be object;
assume x in W;
then consider X be set such that
A37: x in X and
A38: X in Z by TARSKI:def 4;
ex I be Subset of V st I=X & A c=I & I c=B &
I is linearly-independent by A3,A6,A38;
hence thesis by A37;
end;
y c=W by A5,ZFMISC_1:74;
then A c=W by A10;
hence union Z in Q by A3,A11,A36;
end;
Q<>{} by A1,A3;
then consider X be set such that
A39: X in Q and
A40: for Z be set st Z in Q & Z<>X holds not X c=Z by A4,ORDERS_1:67;
consider I be Subset of V such that
A41: I=X and
A42: A c=I and
A43: I c=B and
A44: I is linearly-independent by A3,A39;
reconsider I as linearly-independent Subset of V by A44;
take I;
thus A c=I & I c=B by A42,A43;
assume A45: Lin(I)<>V;
now assume A46: for v st v in B holds v in Lin(I);
now let v;
assume v in Lin(B);
then consider l be Linear_Combination of B such that
A47: v = Sum(l) by RLVECT_3:14;
Carrier(l) c= the carrier of Lin(I)
proof
let x be object;
assume A48: x in Carrier(l);
then reconsider a=x as VECTOR of V;
Carrier(l)c=B by RLVECT_2:def 6;
then a in Lin(I) by A46,A48;
hence thesis;
end;
then reconsider l as Linear_Combination of Up Lin I
by RLVECT_2:def 6;
Sum(l)=v by A47;
then v in Lin(Up Lin I) by RLVECT_3:14;
hence v in Lin(I) by RLVECT_3:18;
end;
then Lin(B) is Subspace of Lin(I) by RLSUB_1:29;
hence contradiction by A2,A45,RLSUB_1:26;
end;
then consider v such that
A49: v in B and
A50: not v in Lin(I);
A51: not v in I by A50,RLVECT_3:15;
{v}c=B by A49,ZFMISC_1:31;
then A52: I\/{v}c=B by A43,XBOOLE_1:8;
v in {v} by TARSKI:def 1;
then A53: v in I\/{v} by XBOOLE_0:def 3;
A54: I\/{v} is linearly-independent
proof
let l be Linear_Combination of I\/{v};
assume A55: Sum(l)=0.V;
per cases;
suppose v in Carrier(l);
then A56: -l.v<>0 by RLVECT_2:19;
deffunc G(VECTOR of V)=In(0,REAL);
deffunc F(VECTOR of V)=l.$1;
consider f be Function of the carrier of V,REAL such that
A57: f.v=In(0,REAL) and
A58: for u be Element of V st u<>v holds f.u=F(u)
from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V,REAL)
by FUNCT_2:8;
now let u be Element of V;
assume not u in Carrier(l)\{v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u=0 & u<>v or u=v by TARSKI:def 1;
hence f.u=0 by A57,A58;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier(f) c= I
proof
let x be object;
assume x in Carrier(f);
then consider u be Element of V such that
A59: u=x and
A60: f.u<>0;
f.u=l.u by A57,A58,A60;
then Carrier(l)c=I\/{v} & u in Carrier(l) by A60,RLVECT_2:def 6;
then u in I or u in {v} by XBOOLE_0:def 3;
hence thesis by A57,A59,A60,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of I by RLVECT_2:def 6;
consider g be Function of the carrier of V,REAL such that
A61: g.v=-l.v and
A62: for u be Element of V st u<>v holds g.u=G(u)
from FUNCT_2:sch 6;
reconsider g as Element of Funcs(the carrier of V,REAL)
by FUNCT_2:8;
now let u be Element of V;
assume not u in {v};
then u<>v by TARSKI:def 1;
hence g.u=0 by A62;
end;
then reconsider g as Linear_Combination of V by RLVECT_2:def 3;
Carrier(g)c={v}
proof
let x be object;
assume x in Carrier(g);
then ex u be Element of V st x=u & g.u<>0;
then x=v by A62;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of{v} by RLVECT_2:def 6;
A63: Sum(g)=(-l.v)*v by A61,RLVECT_2:32;
now let u be Element of V;
now per cases;
suppose A64: v=u;
thus(f-g).u=f.u-g.u by RLVECT_2:54
.=l.u by A57,A61,A64;
end;
suppose A65: v<>u;
thus(f-g).u=f.u-g.u by RLVECT_2:54
.=l.u-g.u by A58,A65
.=l.u-0 by A62,A65
.=l.u;
end;
end;
hence (f-g).u=l.u;
end;
then f-g=l;
then 0.V=Sum(f)-Sum(g) by A55,RLVECT_3:4;
then Sum(f)=0.V+Sum(g) by RLSUB_2:61
.=(-l.v)*v by A63;
then A66: (-l.v)*v in Lin(I) by RLVECT_3:14;
(-l.v)"*((-l.v)*v)=(-l.v)"*(-l.v)*v by RLVECT_1:def 7
.=1*v by A56,XCMPLX_0:def 7
.=v by RLVECT_1:def 8;
hence thesis by A50,A66,RLSUB_1:21;
end;
suppose A67: not v in Carrier(l);
Carrier(l)c=I
proof
let x be object;
assume A68: x in Carrier(l);
Carrier(l)c=I\/{v} by RLVECT_2:def 6;
then x in I or x in {v} by A68,XBOOLE_0:def 3;
hence thesis by A67,A68,TARSKI:def 1;
end;
then l is Linear_Combination of I by RLVECT_2:def 6;
hence thesis by A55,RLVECT_3:def 1;
end;
end;
A c=I\/{v} by A42,XBOOLE_1:10;
then I\/{v} in Q by A3,A52,A54;
hence contradiction by A40,A41,A51,A53,XBOOLE_1:7;
end;
begin :: Two Transformations of Linear Combinations
definition
let G,LG,g;
func g + LG -> Linear_Combination of G means :Def1:
it.h = LG.(h-g);
existence
proof
deffunc G(Element of G)=g+$1;
set vC={G(h):h in Carrier LG};
A1: vC c=the carrier of G
proof
let x be object;
assume x in vC;
then ex h st x=G(h) & h in Carrier LG;
hence thesis;
end;
A2: Carrier LG is finite;
vC is finite from FRAENKEL:sch 21(A2);
then reconsider vC as finite Subset of G by A1;
deffunc F(Element of G)=LG.($1-g);
consider f be Function of the carrier of G,REAL such that
A3: for h holds f.h=F(h) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of G,REAL) by FUNCT_2:8;
now let h;
assume A4: not h in vC;
assume f.h<>0;
then LG.(h-g)<>0 by A3;
then A5: h-g in Carrier LG;
g+(h-g) = (h+-g)+g by RLVECT_1:def 11
.= h+(g+-g) by RLVECT_1:def 3
.= h+0.G by RLVECT_1:def 10
.= h;
hence contradiction by A4,A5;
end;
then reconsider f as Linear_Combination of G by RLVECT_2:def 3;
take f;
thus thesis by A3;
end;
uniqueness
proof
let L1,L2 be Linear_Combination of G such that
A6: for h holds L1.h=LG.(h-g) and
A7: for h holds L2.h=LG.(h-g);
now let h;
thus L1.h = LG.(h-g) by A6
.= L2.h by A7;
end;
hence thesis;
end;
end;
theorem Th16:
Carrier (g+LG) = g + Carrier LG
proof
thus Carrier(g+LG)c=g+Carrier LG
proof
let x be object such that
A1: x in Carrier(g+LG);
reconsider w=x as Element of G by A1;
A2: (g+LG).w <>0 by A1,RLVECT_2:19;
A3: g+(w-g) = (w+-g)+g by RLVECT_1:def 11
.= w+(g+-g) by RLVECT_1:def 3
.= w+0.G by RLVECT_1:def 10
.= w;
(g+LG).w=LG.(w-g) by Def1;
then w-g in Carrier LG by A2;
hence thesis by A3;
end;
let x be object;
assume x in g+Carrier LG;
then consider w be Element of G such that
A4: x=g+w and
A5: w in Carrier LG;
g+w-g = g+w+-g by RLVECT_1:def 11
.= (-g+g)+w by RLVECT_1:def 3
.= 0.G+w by RLVECT_1:5
.= w;
then A6: (g+LG).(g+w)=LG.w by Def1;
LG.w<>0 by A5,RLVECT_2:19;
hence thesis by A4,A6;
end;
theorem Th17:
g + (LG1+LG2) = (g+LG1) + (g+LG2)
proof
now let h;
thus(g+(LG1+LG2)).h = (LG1+LG2).(h-g) by Def1
.= LG1.(h-g)+LG2.(h-g) by RLVECT_2:def 10
.=(g+LG1).h+LG2.(h-g) by Def1
.=(g+LG1).h+(g+LG2).h by Def1
.=((g+LG1)+(g+LG2)).h by RLVECT_2:def 10;
end;
hence thesis;
end;
theorem
v + (r*L) = r * (v+L)
proof
now let w;
thus(v+(r*L)).w = (r*L).(w-v) by Def1
.= r*(L.(w-v)) by RLVECT_2:def 11
.= r*((v+L).w) by Def1
.= (r*(v+L)).w by RLVECT_2:def 11;
end;
hence thesis;
end;
theorem Th19:
g + (h+LG) = (g+h) + LG
proof
now let s be Element of G;
thus(g+(h+LG)).s = (h+LG).(s-g) by Def1
.= LG.(s-g-h) by Def1
.= LG.(s-(g+h)) by RLVECT_1:27
.= ((g+h)+LG).s by Def1;
end;
hence thesis;
end;
theorem Th20:
g + ZeroLC G = ZeroLC G
proof
Carrier ZeroLC(G)={}G by RLVECT_2:def 5;
then {}G = g+Carrier ZeroLC(G) by Th8
.= Carrier(g+ZeroLC(G)) by Th16;
hence thesis by RLVECT_2:def 5;
end;
theorem Th21:
0.G + LG = LG
proof
now let g;
thus(0.G+LG).g = LG.(g-0.G) by Def1
.= LG.g;
end;
hence thesis;
end;
definition
let R,LR; let r be Real;
func r (*) LR -> Linear_Combination of R means :Def2:
for v be Element of R holds it.v = LR.(r"*v) if r<>0 otherwise
it = ZeroLC R;
existence
proof
now deffunc F(Element of R)=LR.(r"*$1);
deffunc G(Element of R)=r*$1;
consider f being Function of the carrier of R,REAL such that
A1: for v being Element of R holds f.v=F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of R,REAL) by FUNCT_2:8;
assume A2: r<>0;
A3: now let v be Element of R;
assume A4: not v in r*Carrier LR;
A5: f.v=LR.(r"*v) by A1;
A6: r*(r"*v) = (r*r")*v by RLVECT_1:def 7
.= 1*v by A2,XCMPLX_0:def 7
.= v by RLVECT_1:def 8;
assume f.v<>0;
then r"*v in Carrier LR by A5;
hence contradiction by A4,A6;
end;
A7: Carrier LR is finite;
{G(w) where w is Element of R:w in Carrier LR} is finite
from FRAENKEL:sch 21(A7);
then reconsider f as Linear_Combination of R by A3,RLVECT_2:def 3;
take f;
let v be Element of R;
f.v=LR.(r"*v) by A1;
hence thesis by A1;
end;
hence thesis;
end;
uniqueness
proof
now let L1,L2 be Linear_Combination of R such that
A8: for v be Element of R holds L1.v=LR.(r"*v) and
A9: for v be Element of R holds L2.v=LR.(r"*v);
now let v be Element of R;
thus L1.v = LR.(r"*v) by A8
.= L2.v by A9;
end;
hence L1=L2;
end;
hence thesis;
end;
consistency;
end;
theorem Th22:
Carrier (r(*)LR) c= r*Carrier LR
proof
let x be object such that
A1: x in Carrier(r(*)LR);
reconsider v=x as Element of R by A1;
A2: (r(*)LR).v<>0 by A1,RLVECT_2:19;
(0 qua Real)(*)LR=ZeroLC(R) by Def2;
then A3: r<>0 by A1,RLVECT_2:def 5;
then (r(*)LR).v=LR.(r"*v) by Def2;
then A4: r"*v in Carrier LR by A2;
r*(r"*v) = (r*r")*v by RLVECT_1:def 7
.= 1*v by A3,XCMPLX_0:def 7
.= v by RLVECT_1:def 8;
hence thesis by A4;
end;
theorem Th23:
r <> 0 implies Carrier (r(*)LR) = r * Carrier LR
proof
assume A1: r<>0;
thus Carrier(r(*)LR)c=r*Carrier LR by Th22;
let x be object;
assume x in r*Carrier LR;
then consider v be Element of R such that
A2: x=r*v and
A3: v in Carrier LR;
r"*(r*v) = (r"*r)*v by RLVECT_1:def 7
.= 1*v by A1,XCMPLX_0:def 7
.= v by RLVECT_1:def 8;
then A4: LR.v=(r(*)LR).x by A1,A2,Def2;
LR.v<>0 by A3,RLVECT_2:19;
hence thesis by A2,A4;
end;
theorem Th24:
r (*) (LR1+LR2) = (r(*)LR1) + (r(*)LR2)
proof
per cases;
suppose A1: r = 0;
set Z=ZeroLC(R);
A2: now let v be Element of R;
thus (Z+Z).v = Z.v+Z.v by RLVECT_2:def 10
.= Z.v+0 by RLVECT_2:20
.= Z.v;
end;
thus r(*)(LR1+LR2) = Z by A1,Def2
.= Z+Z by A2
.= (r(*)LR1)+Z by A1,Def2
.= (r(*)LR1)+(r(*)LR2) by A1,Def2;
end;
suppose A3: r<>0;
now let v be Element of R;
thus(r(*)(LR1+LR2)).v = (LR1+LR2).(r"*v) by A3,Def2
.= LR1.(r"*v)+LR2.(r"*v) by RLVECT_2:def 10
.= (r(*)LR1).v+LR2.(r"*v) by A3,Def2
.= (r(*)LR1).v+(r(*)LR2).v by A3,Def2
.= ((r(*)LR1)+(r(*)LR2)).v by RLVECT_2:def 10;
end;
hence thesis;
end;
end;
theorem
r * (s(*)L) = s (*) (r*L)
proof
per cases;
suppose A1: s=0;
hence r*(s(*)L) = r*ZeroLC(V) by Def2
.= r*(0*L) by RLVECT_2:43
.= (r*0)*L by RLVECT_2:47
.= ZeroLC(V) by RLVECT_2:43
.= s(*)(r*L) by A1,Def2;
end;
suppose A2: s<>0;
now let v;
thus(r*(s(*)L)).v = r*((s(*)L).v) by RLVECT_2:def 11
.= r*(L.(s"*v)) by A2,Def2
.= (r*L).(s"*v) by RLVECT_2:def 11
.= (s(*)(r*L)).v by A2,Def2;
end;
hence thesis;
end;
end;
theorem Th26:
r (*) ZeroLC(R) = ZeroLC R
proof
per cases;
suppose r=0;
hence thesis by Def2;
end;
suppose A1: r<>0;
now let v be Element of R;
thus(r(*)ZeroLC(R)).v = ZeroLC(R).(r"*v) by A1,Def2
.= 0 by RLVECT_2:20
.= ZeroLC(R).v by RLVECT_2:20;
end;
hence thesis;
end;
end;
theorem Th27:
r(*)(s(*)LR)=(r*s)(*)LR
proof
per cases;
suppose A1: r=0 or s=0;
then (r*s)(*)LR=ZeroLC(R) by Def2;
hence thesis by A1,Def2,Th26;
end;
suppose A2: r<>0 & s<>0;
now let v be Element of R;
thus(r(*)(s(*)LR)).v = (s(*)LR).(r"*v) by A2,Def2
.= LR.(s"*(r"*v)) by A2,Def2
.= LR.((s"*r")*v) by RLVECT_1:def 7
.= LR.((r*s)"*v) by XCMPLX_1:204
.= ((r*s)(*)LR).v by A2,Def2;
end;
hence thesis;
end;
end;
theorem Th28:
1 (*) LR = LR
proof
now let v be Element of R;
thus(1(*)LR).v = LR.(1"*v) by Def2
.= LR.v by RLVECT_1:def 8;
end;
hence thesis;
end;
begin :: The Sum of Coefficients of a Linear Combination
definition
let S,LS;
func sum LS -> Real means :Def3:
ex F be FinSequence of S st
F is one-to-one & rng F = Carrier LS & it = Sum (LS*F);
existence
proof
consider p be FinSequence such that
A1: rng p=Carrier LS and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of S by A1,FINSEQ_1:def 4;
take Sum(LS*p);
thus thesis by A1,A2;
end;
uniqueness
proof
let S1,S2 be Real;
given F1 be FinSequence of S such that
A3: F1 is one-to-one and
A4: rng F1=Carrier LS and
A5: S1=Sum(LS*F1);
A6: dom(F1")=Carrier LS by A3,A4,FUNCT_1:33;
A7: len F1=card Carrier LS by A3,A4,FINSEQ_4:62;
given F2 be FinSequence of S such that
A8: F2 is one-to-one and
A9: rng F2=Carrier LS and
A10: S2=Sum(LS*F2);
set F12=(F1")*F2;
dom F2=Seg len F2 & len F2=card Carrier LS
by A8,A9,FINSEQ_1:def 3,FINSEQ_4:62;
then A11: dom F12=Seg len F1 by A6,A7,A9,RELAT_1:27;
dom F1=Seg len F1 by FINSEQ_1:def 3;
then rng(F1")=Seg len F1 by A3,FUNCT_1:33;
then A12: rng F12=Seg len F1 by A6,A9,RELAT_1:28;
then reconsider F12 as Function of Seg len F1,Seg len F1 by A11,FUNCT_2:1;
A13: F12 is onto by A12,FUNCT_2:def 3;
len(LS*F1)=len F1 by FINSEQ_2:33;
then dom(LS*F1)=Seg len F1 by FINSEQ_1:def 3;
then reconsider F12 as Permutation of dom(LS*F1) by A3,A8,A13;
LS*F1*F12 = LS*(F1*F12) by RELAT_1:36
.= LS*((F1*F1")*F2) by RELAT_1:36
.= LS*((id Carrier LS)*F2) by A3,A4,FUNCT_1:39
.= LS*F2 by A9,RELAT_1:53;
hence S1=S2 by A5,A10,FINSOP_1:7;
end;
end;
theorem Th29:
for F be FinSequence of S st Carrier LS misses rng F holds Sum (LS*F) = 0
proof
let F be FinSequence of S such that
A1: Carrier LS misses rng F;
set LF=LS*F;
set LF0=len LF|->(0 qua Real);
A2: now let k be Nat;
assume A3: 1<=k & k<=len LF;
A4: k in dom LF by A3,FINSEQ_3:25;
then k in dom F by FUNCT_1:11;
then F.k in rng F by FUNCT_1:def 3;
then A5: dom LS=the carrier of S & not F.k in Carrier LS
by A1,FUNCT_2:def 1,XBOOLE_0:3;
LF.k=LS.(F.k) & F.k in dom LS by A4,FUNCT_1:11,12;
hence LF.k=LF0.k by A5;
end;
len LF0=len LF by CARD_1:def 7;
then LF=LF0 by A2;
hence thesis by RVSUM_1:81;
end;
theorem Th30:
for F be FinSequence of S st F is one-to-one & Carrier LS c= rng F
holds sum LS = Sum (LS*F)
proof
let F be FinSequence of S such that
A1: F is one-to-one and
A2: Carrier LS c=rng F;
consider G be FinSequence of S such that
A3: G is one-to-one and
A4: rng G=Carrier LS and
A5: sum LS=Sum(LS*G) by Def3;
reconsider R=rng G as Subset of rng F by A2,A4;
reconsider FR=F-R,FR1=F-R` as FinSequence of S by FINSEQ_3:86;
consider p be Permutation of dom F such that
A6: F*p=(F-R`)^(F-R) by FINSEQ_3:115;
rng F\R` = R`` .= R;
then A7: rng FR1=R by FINSEQ_3:65;
FR1 is one-to-one by A1,FINSEQ_3:87;
then FR1,G are_fiberwise_equipotent by A3,A7,RFINSEQ:26;
then consider q be Permutation of dom G such that
A8: FR1=G*q by RFINSEQ:4;
len(LS*G)=len G by FINSEQ_2:33;
then A9: dom G=dom(LS*G) by FINSEQ_3:29;
(LS*G)*q=LS*FR1 by A8,RELAT_1:36;
then A10: sum LS=Sum(LS*FR1) by A5,A9,FINSOP_1:7;
len(LS*F)=len F by FINSEQ_2:33;
then A11: dom F=dom(LS*F) by FINSEQ_3:29;
rng F\R=rng FR by FINSEQ_3:65;
then rng FR misses Carrier LS by A4,XBOOLE_1:79;
then A12: LS*(FR1^FR)=(LS*FR1)^(LS*FR) & Sum(LS*FR)=0 by Th29,FINSEQOP:9;
(LS*F)*p=LS*(FR1^FR) by A6,RELAT_1:36;
hence Sum(LS*F) = Sum(LS*(FR1^FR)) by A11,FINSOP_1:7
.= sum LS+0 by A10,A12,RVSUM_1:75
.= sum LS;
end;
theorem Th31:
sum ZeroLC S = 0
proof
consider F be FinSequence of S such that
F is one-to-one and
A1: rng F=Carrier (ZeroLC S) and
A2: sum ZeroLC S = Sum((ZeroLC S)*F) by Def3;
F={} by A1,RLVECT_2:def 5;
hence thesis by A2,RVSUM_1:72;
end;
theorem Th32:
for v be Element of S st Carrier LS c= {v} holds sum LS = LS.v
proof
let v be Element of S;
consider p be FinSequence such that
A1: rng p={v} and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of S by A1,FINSEQ_1:def 4;
dom LS=the carrier of S & p=<*v*> by A1,A2,FINSEQ_3:97,FUNCT_2:def 1;
then A3: LS*p=<*LS.v*> by FINSEQ_2:34;
assume Carrier LS c={v};
hence sum LS = Sum(LS*p) by A1,A2,Th30
.= LS.v by A3,RVSUM_1:73;
end;
theorem
for v1,v2 be Element of S st
Carrier LS c= {v1,v2} & v1 <> v2 holds sum LS = LS.v1 + LS.v2
proof
let v1,v2 be Element of S;
consider p be FinSequence such that
A1: rng p={v1,v2} and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of S by A1,FINSEQ_1:def 4;
assume that
A3: Carrier LS c={v1,v2} and
A4: v1<>v2;
A5: dom LS=the carrier of S by FUNCT_2:def 1;
A6: Sum<*LS.v1*>=LS.v1 by RVSUM_1:73;
p=<*v1,v2*> or p=<*v2,v1*> by A1,A2,A4,FINSEQ_3:99;
then LS*p=<*LS.v1,LS.v2*> or LS*p=<*LS.v2,LS.v1*> by A5,FINSEQ_2:125;
then Sum(LS*p)=LS.v1+LS.v2 or Sum(LS*p)=LS.v2+LS.v1 by A6,RVSUM_1:74,76;
hence thesis by A1,A2,A3,Th30;
end;
theorem Th34:
sum (LS1+LS2) = sum LS1 + sum LS2
proof
set C1=Carrier LS1;
set C2=Carrier LS2;
consider p112 be FinSequence such that
A1: rng p112=C1\C2 and
A2: p112 is one-to-one by FINSEQ_4:58;
consider p12 be FinSequence such that
A3: rng p12=C1/\C2 and
A4: p12 is one-to-one by FINSEQ_4:58;
consider p211 be FinSequence such that
A5: rng p211=C2\C1 and
A6: p211 is one-to-one by FINSEQ_4:58;
reconsider p112,p12,p211 as FinSequence of S by A1,A3,A5,FINSEQ_1:def 4;
C1\C2 misses C1/\C2 by XBOOLE_1:89;
then A7: p112^p12 is one-to-one by A1,A2,A3,A4,FINSEQ_3:91;
set p1=p112^p12;
A8: rng p1 = C1\C2\/C1/\C2 by A1,A3,FINSEQ_1:31
.= C1 by XBOOLE_1:51;
then A9: rng(p112^p12^p211) = C1\/(C2\C1) by A5,FINSEQ_1:31
.= C1\/C2 by XBOOLE_1:39;
set p2=p12^p211;
A10: rng p2 = C1/\C2\/(C2\C1) by A3,A5,FINSEQ_1:31
.= C2 by XBOOLE_1:51;
set pp=p1^p211;
pp=p112^p2 by FINSEQ_1:32;
then A11: LS2*pp=(LS2*p112)^(LS2*p2) by FINSEQOP:9;
C2\C1 misses C1/\C2 by XBOOLE_1:89;
then A12: p12^p211 is one-to-one by A3,A4,A5,A6,FINSEQ_3:91;
C2 misses C1\C2 by XBOOLE_1:79;
then Sum(LS2*p112)=0 by A1,Th29;
then A13: Sum(LS2*pp) = 0+Sum(LS2*p2) by A11,RVSUM_1:75
.= sum LS2 by A10,A12,Def3;
len(LS1*pp)=len pp & len(LS2*pp)=len pp by FINSEQ_2:33;
then reconsider L1p=LS1*pp,L2p=LS2*pp as Element of len pp-tuples_on REAL
by FINSEQ_2:92;
A14: (LS1+LS2)*pp=L1p+L2p by Th13;
A15: C1 misses C2\C1 by XBOOLE_1:79;
then LS1*pp=(LS1*p1)^(LS1*p211) & Sum(LS1*p211)=0 by A5,Th29,FINSEQOP:9;
then A16: Sum(LS1*pp) = Sum(LS1*p1)+0 by RVSUM_1:75
.= sum LS1 by A7,A8,Def3;
A17: Carrier(LS1+LS2)c=C1\/C2
proof
let x be object;
assume x in Carrier(LS1+LS2);
then consider u be Element of S such that
A18: x=u and
A19: (LS1+LS2).u<>0;
(LS1+LS2).u=LS1.u+LS2.u by RLVECT_2:def 10;
then LS1.u<>0 or LS2.u<>0 by A19;
then x in C1 or x in C2 by A18;
hence thesis by XBOOLE_0:def 3;
end;
p112^p12^p211 is one-to-one by A5,A6,A7,A8,A15,FINSEQ_3:91;
hence sum(LS1+LS2) = Sum(L1p+L2p) by A9,A14,A17,Th30
.= sum LS1+sum LS2 by A13,A16,RVSUM_1:89;
end;
theorem Th35:
sum (r * L) = r * sum L
proof
consider F be FinSequence of V such that
A1: F is one-to-one and
A2: rng F=Carrier L and
A3: sum L=Sum(L*F) by Def3;
L is Linear_Combination of Carrier L by RLVECT_2:def 6;
then r*L is Linear_Combination of Carrier L by RLVECT_2:44;
then A4: Carrier(r*L)c=rng F by A2,RLVECT_2:def 6;
thus r*sum L = Sum(r*(L*F)) by A3,RVSUM_1:87
.= Sum((r*L)*F) by Th14
.= sum(r*L) by A1,A4,Th30;
end;
theorem Th36:
sum (L1-L2) =sum L1 - sum L2
proof
thus sum(L1-L2) = sum(L1)+sum((-1)*L2) by Th34
.= sum(L1)+(-1)*sum(L2) by Th35
.= sum(L1)-sum(L2);
end;
theorem Th37:
sum LG = sum (g+LG)
proof
set gL=g+LG;
deffunc F(Element of G)=$1+g;
consider f be Function of the carrier of G,the carrier of G such that
A1: for h holds f.h=F(h) from FUNCT_2:sch 4;
consider F be FinSequence of G such that
A2: F is one-to-one and
A3: rng F=Carrier LG and
A4: sum LG=Sum(LG*F) by Def3;
A5: len(f*F)=len F by FINSEQ_2:33;
A6: len(LG*F)=len F by FINSEQ_2:33;
A7: len(gL*(f*F))=len(f*F) by FINSEQ_2:33;
A8: now let k be Nat;
assume A9: 1<=k & k<=len F;
then k in dom F by FINSEQ_3:25;
then A10: F/.k=F.k by PARTFUN1:def 6;
k in dom(LG*F) by A6,A9,FINSEQ_3:25;
then A11: (LG*F).k=LG.(F.k) by FUNCT_1:12;
k in dom(gL*(f*F)) by A5,A7,A9,FINSEQ_3:25;
then A12: (gL*(f*F)).k=gL.((f*F).k) by FUNCT_1:12;
k in dom(f*F) by A5,A9,FINSEQ_3:25;
then (f*F).k=f.(F.k) by FUNCT_1:12;
then (f*F).k=F/.k+g by A1,A10;
hence (gL*(f*F)).k = LG.(F/.k+g-g) by A12,Def1
.= LG.(F/.k+g+-g) by RLVECT_1:def 11
.= LG.(F/.k+(g+-g)) by RLVECT_1:def 3
.= LG.(F/.k+0.G) by RLVECT_1:def 10
.= (LG*F).k by A10,A11;
end;
now let x1,x2 be object such that
A13: x1 in dom(f*F) and
A14: x2 in dom(f*F) and
A15: (f*F).x1=(f*F).x2;
A16: f.(F/.x1)=F/.x1+g by A1;
A17: x1 in dom F by A13,FUNCT_1:11;
then A18: F.x1=F/.x1 by PARTFUN1:def 6;
A19: x2 in dom F by A14,FUNCT_1:11;
then A20: F.x2=F/.x2 by PARTFUN1:def 6;
(f*F).x1=f.(F.x1) & (f*F).x2=f.(F.x2) by A13,A14,FUNCT_1:12;
then F/.x1+g=F/.x2+g by A1,A15,A16,A18,A20;
then F/.x1=F/.x2 by RLVECT_1:8;
hence x1=x2 by A2,A17,A18,A19,A20,FUNCT_1:def 4;
end;
then A21: f*F is one-to-one by FUNCT_1:def 4;
Carrier gL c=rng(f*F)
proof
let x be object;
assume x in Carrier gL;
then x in g+Carrier LG by Th16;
then consider h such that
A22: x=g+h and
A23: h in Carrier LG;
consider y being object such that
A24: y in dom F and
A25: F.y=h by A3,A23,FUNCT_1:def 3;
A26: f.(F.y)=x by A1,A22,A25;
dom f=the carrier of G by FUNCT_2:def 1;
then A27: y in dom(f*F) by A24,A25,FUNCT_1:11;
then (f*F).y in rng(f*F) by FUNCT_1:def 3;
hence thesis by A26,A27,FUNCT_1:12;
end;
then sum gL=Sum(gL*(f*F)) by A21,Th30;
hence thesis by A4,A5,A6,A7,A8,FINSEQ_1:14;
end;
theorem Th38:
r <> 0 implies sum LR = sum (r(*)LR)
proof
set rL=r(*)LR;
deffunc F(Element of R)=r*$1;
consider f be Function of the carrier of R,the carrier of R such that
A1: for v be Element of R holds f.v=F(v) from FUNCT_2:sch 4;
consider F be FinSequence of R such that
A2: F is one-to-one and
A3: rng F=Carrier LR and
A4: sum LR=Sum(LR*F) by Def3;
assume A5: r<>0;
now let x1,x2 be object such that
A6: x1 in dom(f*F) and
A7: x2 in dom(f*F) and
A8: (f*F).x1=(f*F).x2;
A9: f.(F/.x1)=r*F/.x1 by A1;
A10: x1 in dom F by A6,FUNCT_1:11;
then A11: F.x1=F/.x1 by PARTFUN1:def 6;
A12: x2 in dom F by A7,FUNCT_1:11;
then A13: F.x2=F/.x2 by PARTFUN1:def 6;
(f*F).x1=f.(F.x1) & (f*F).x2=f.(F.x2) by A6,A7,FUNCT_1:12;
then A14: r*F/.x1=r*F/.x2 by A1,A8,A9,A11,A13;
F/.x1 = 1*F/.x1 by RLVECT_1:def 8
.= (r"*r)*F/.x1 by A5,XCMPLX_0:def 7
.= r"*(r*F/.x2) by A14,RLVECT_1:def 7
.= (r"*r)*F/.x2 by RLVECT_1:def 7
.= 1*F/.x2 by A5,XCMPLX_0:def 7
.= F/.x2 by RLVECT_1:def 8;
hence x1 = x2 by A2,A10,A11,A12,A13,FUNCT_1:def 4;
end;
then A15: f*F is one-to-one by FUNCT_1:def 4;
A16: len(LR*F)=len F by FINSEQ_2:33;
A17: len(f*F)=len F by FINSEQ_2:33;
A18: len(rL*(f*F))=len(f*F) by FINSEQ_2:33;
now let k be Nat;
assume A19: 1<=k & k<=len F;
then k in dom F by FINSEQ_3:25;
then A20: F/.k=F.k by PARTFUN1:def 6;
k in dom(LR*F) by A16,A19,FINSEQ_3:25;
then A21: (LR*F).k=LR.(F.k) by FUNCT_1:12;
k in dom(f*F) by A17,A19,FINSEQ_3:25;
then A22: (f*F).k=f.(F.k) by FUNCT_1:12;
k in dom(rL*(f*F)) by A17,A18,A19,FINSEQ_3:25;
then (rL*(f*F)).k=rL.((f*F).k) by FUNCT_1:12;
hence (rL*(f*F)).k = rL.(r*F/.k) by A1,A20,A22
.= LR.(r"*(r*(F/.k))) by A5,Def2
.= LR.((r"*r)*F/.k) by RLVECT_1:def 7
.= LR.(1*F/.k) by A5,XCMPLX_0:def 7
.= (LR*F).k by A20,A21,RLVECT_1:def 8;
end;
then A23: LR*F=rL*(f*F) by A16,A17,A18;
Carrier rL c=rng(f*F)
proof
let x be object;
assume x in Carrier rL;
then x in r*Carrier LR by A5,Th23;
then consider v be Element of R such that
A24: x=r*v and
A25: v in Carrier LR;
consider y be object such that
A26: y in dom F and
A27: F.y=v by A3,A25,FUNCT_1:def 3;
A28: f.v=x by A1,A24;
A29: dom F=dom(f*F) by A17,FINSEQ_3:29;
then (f*F).y=f.v by A26,A27,FUNCT_1:12;
hence thesis by A26,A28,A29,FUNCT_1:def 3;
end;
hence thesis by A4,A15,A23,Th30;
end;
theorem Th39:
Sum (v + L) = (sum L)*v + Sum L
proof
defpred P[Nat] means
for L be Linear_Combination of V st card Carrier L<=$1 holds
Sum(v+L)=(sum L)*v+Sum L;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: P[n];
let L be Linear_Combination of V such that
A3: card Carrier L<=n+1;
per cases by A3,NAT_1:8;
suppose card Carrier L<=n;
hence thesis by A2;
end;
suppose A4: card Carrier L=n+1;
then Carrier L is non empty;
then consider w be object such that
A5: w in Carrier L;
reconsider w as Element of V by A5;
A6: card(Carrier L\{w})=n by A4,A5,STIRL2_1:55;
consider Lw be Linear_Combination of{w} such that
A7: Lw.w=L.w by RLVECT_4:37;
set LLw=L-Lw;
LLw.w = L.w-Lw.w by RLVECT_2:54
.= 0 by A7;
then A8: not w in Carrier LLw by RLVECT_2:19;
A9: Carrier Lw c={w} by RLVECT_2:def 6;
then A10: Carrier LLw c=Carrier L\/Carrier Lw &
Carrier L\/Carrier Lw c= Carrier L\/{w} by RLVECT_2:55,XBOOLE_1:9;
Carrier L\/{w}=Carrier L by A5,ZFMISC_1:40;
then Carrier LLw c=Carrier L by A10;
then card Carrier LLw<=n by A8,A6,NAT_1:43,ZFMISC_1:34;
then A11: Sum(v+LLw)=(sum LLw)*v+Sum LLw by A2;
A12: LLw+Lw = L+(Lw-Lw) by RLVECT_2:40
.= L+ZeroLC(V) by RLVECT_2:57
.=L by RLVECT_2:41;
then A13: Sum L = Sum LLw+Sum Lw by RLVECT_3:1
.= Sum LLw+Lw.w*w by RLVECT_2:32;
v+Carrier Lw c= v+{w} by A9,RLTOPSP1:8;
then v+Carrier Lw c={v+w} by Lm3;
then Carrier(v+Lw)c={v+w} by Th16;
then v+Lw is Linear_Combination of{v+w} by RLVECT_2:def 6;
then A14: Sum(v+Lw) = (v+Lw).(v+w)*(v+w) by RLVECT_2:32
.= Lw.(v+w-v)*(v+w) by Def1
.= Lw.w*(v+w) by RLVECT_4:1;
A15: sum L = sum LLw+sum Lw by A12,Th34
.= sum LLw+Lw.w by A9,Th32;
v+L=(v+LLw)+(v+Lw) by A12,Th17;
hence Sum(v+L) = Sum(v+LLw)+Sum(v+Lw) by RLVECT_3:1
.= (sum LLw)*v+Sum LLw+(Lw.w*v+Lw.w*w)
by A11,A14,RLVECT_1:def 5
.= (sum LLw)*v+Sum LLw+Lw.w*v+Lw.w*w by RLVECT_1:def 3
.= (sum LLw)*v+Lw.w*v+Sum LLw+Lw.w*w by RLVECT_1:def 3
.= sum L*v+Sum LLw+Lw.w*w by A15,RLVECT_1:def 6
.= sum L*v+Sum L by A13,RLVECT_1:def 3;
end;
end;
A16: P[0 qua Nat]
proof
let L be Linear_Combination of V;
assume card Carrier L<=0;
then A17: Carrier L={}V;
then A18: L=ZeroLC(V) & Sum L=0.V by RLVECT_2:34,def 5;
v+Carrier L={} by A17,Th8;
then Carrier(v+L)={} by Th16;
hence Sum(v+L) = 0.V by RLVECT_2:34
.= 0.V+0.V
.= (sum L)*v+Sum L by A18,Th31,RLVECT_1:10;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A16,A1);
then P[card Carrier L];
hence thesis;
end;
theorem Th40:
Sum (r(*)L) = r * Sum L
proof
defpred P[Nat] means
for L be Linear_Combination of V st card Carrier L<=$1 holds Sum(r(*)L)=r*
Sum L;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: P[n];
let L be Linear_Combination of V such that
A3: card Carrier L<=n+1;
per cases;
suppose r=0;
then r(*)L=ZeroLC(V) & r*Sum L=0.V by Def2,RLVECT_1:10;
hence thesis by RLVECT_2:30;
end;
suppose A4: r<>0;
per cases by A3,NAT_1:8;
suppose card Carrier L<=n;
hence thesis by A2;
end;
suppose A5: card Carrier L=n+1;
then Carrier L<>{};
then consider p be object such that
A6: p in Carrier L by XBOOLE_0:def 1;
reconsider p as Element of V by A6;
A7: card(Carrier L\{p})=n by A5,A6,STIRL2_1:55;
consider Lp be Linear_Combination of{p} such that
A8: Lp.p=L.p by RLVECT_4:37;
set LLp=L-Lp;
LLp.p = L.p-Lp.p by RLVECT_2:54
.= 0 by A8;
then A9: not p in Carrier LLp by RLVECT_2:19;
A10: Carrier Lp c={p} by RLVECT_2:def 6;
then A11: Carrier LLp c=Carrier L\/Carrier Lp &
Carrier L\/Carrier Lp c= Carrier L\/{p} by RLVECT_2:55,XBOOLE_1:9;
r*Carrier Lp c={r*p}
proof
let x be object;
assume x in r*Carrier Lp;
then consider w be Element of V such that
A12: x=r*w and
A13: w in Carrier Lp;
w=p by A10,A13,TARSKI:def 1;
hence thesis by A12,TARSKI:def 1;
end;
then Carrier(r(*)Lp)c={r*p} by A4,Th23;
then r(*)Lp is Linear_Combination of{r*p} by RLVECT_2:def 6;
then A14: Sum(r(*)Lp)=(r(*)Lp).(r*p)*(r*p) by RLVECT_2:32
.=Lp.(r"*(r*p))*(r*p) by A4,Def2
.=Lp.((r"*r)*p)*(r*p) by RLVECT_1:def 7
.=Lp.(1*p)*(r*p) by A4,XCMPLX_0:def 7
.=Lp.p*(r*p) by RLVECT_1:def 8;
A15: LLp+Lp=L+(Lp-Lp) by RLVECT_2:40
.=L+ZeroLC(V) by RLVECT_2:57
.=L by RLVECT_2:41;
then A16: Sum L=Sum LLp+Sum Lp by RLVECT_3:1
.=Sum LLp+Lp.p*p by RLVECT_2:32;
Carrier L\/{p}=Carrier L by A6,ZFMISC_1:40;
then Carrier LLp c=Carrier L by A11;
then card Carrier LLp<=n by A9,A7,NAT_1:43,ZFMISC_1:34;
then A17: Sum(r(*)LLp)=r*Sum LLp by A2;
r(*)L=(r(*)LLp)+(r(*)Lp) by A15,Th24;
hence Sum(r(*)L)=Sum(r(*)LLp)+Sum(r(*)Lp) by RLVECT_3:1
.=r*Sum LLp+(Lp.p*r)*p by A14,A17,RLVECT_1:def 7
.=r*Sum LLp+r*(Lp.p*p) by RLVECT_1:def 7
.=r*Sum L by A16,RLVECT_1:def 5;
end;
end;
end;
A18: P[0 qua Nat]
proof
let L;
assume card Carrier L<=0;
then Carrier L={};
then A19: L=ZeroLC(V) by RLVECT_2:def 5;
then r*0.V=0.V & Sum L=0.V by RLVECT_2:30;
hence thesis by A19,Th26;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A18,A1);
then P[card Carrier L];
hence thesis;
end;
begin :: Affine Independence of Vectors
definition
let V,A;
attr A is affinely-independent means
A is empty or ex v st v in A & -v + A\{0.V} is linearly-independent;
end;
registration
let V;
cluster empty -> affinely-independent for Subset of V;
coherence;
let v;
cluster {v} -> affinely-independent for Subset of V;
coherence
proof
{v} is affinely-independent
proof
assume{v} is non empty;
take v;
thus v in {v} by TARSKI:def 1;
-v+v=0.V by RLVECT_1:5;
then -v+{v}={0.V} by Lm3;
then -v+{v}\{0.V}={}(the carrier of V) by XBOOLE_1:37;
hence thesis by RLVECT_3:7;
end;
hence thesis;
end;
let w;
cluster {v,w} -> affinely-independent for Subset of V;
coherence
proof
per cases;
suppose v=w;
then {v,w}={w} by ENUMSET1:29;
hence thesis;
end;
suppose A1: v<>w;
-v+{v,w}c={-v+w,0.V}
proof
let x be object;
assume x in -v+{v,w};
then consider r be Element of V such that
A2: x=-v+r and
A3: r in {v,w};
per cases by A3,TARSKI:def 2;
suppose r=v;
then x=0.V by A2,RLVECT_1:5;
hence thesis by TARSKI:def 2;
end;
suppose r=w;
hence thesis by A2,TARSKI:def 2;
end;
end;
then A4: -v+{v,w}\{0.V}c={-v+w,0.V}\{0.V} by XBOOLE_1:33;
--v=v;
then A5: w+-v<>0.V by A1,RLVECT_1:6;
then A6: {-v+w} is linearly-independent by RLVECT_3:8;
{v,w} is affinely-independent
proof
assume{v,w} is non empty;
take v;
thus v in {v,w} by TARSKI:def 2;
0.V in {0.V} & not-v+w in {0.V} by A5,TARSKI:def 1;
then -v+{v,w}\{0.V}c={-v+w} by A4,ZFMISC_1:62;
hence thesis by A6,RLVECT_3:5;
end;
hence thesis;
end;
end;
end;
registration
let V;
cluster 1-element affinely-independent for Subset of V;
existence
proof
take {the Element of V};
thus thesis;
end;
end;
Lm5: for A st A is affinely-independent
for L be Linear_Combination of A st Sum L=0.V & sum L=0
holds Carrier L={}
proof
let A;
assume A1: A is affinely-independent;
let L be Linear_Combination of A such that
A2: Sum L=0.V and
A3: sum L=0;
per cases;
suppose A is empty;
then Carrier L c={} by RLVECT_2:def 6;
hence thesis;
end;
suppose A is non empty;
then consider p be VECTOR of V such that
A4: p in A and
A5: (-p+A)\{0.V} is linearly-independent by A1;
A6: A\/{p}=A by A4,ZFMISC_1:40;
consider Lp be Linear_Combination of{p} such that
A7: Lp.p=L.p by RLVECT_4:37;
set LLp=L-Lp;
(-p+LLp).(0.V)=LLp.(0.V-(-p)) by Def1
.=LLp.(-(-p)) by RLVECT_1:14
.=LLp.p
.=L.p-Lp.p by RLVECT_2:54
.=0 by A7;
then A8: not 0.V in Carrier(-p+LLp) by RLVECT_2:19;
A9: Carrier Lp c={p} by RLVECT_2:def 6;
then A10: Carrier Lp={p} or Carrier Lp={} by ZFMISC_1:33;
Carrier L c=A by RLVECT_2:def 6;
then Carrier LLp c=Carrier L\/Carrier Lp &
Carrier L\/Carrier Lp c=A\/{p} by A9,RLVECT_2:55,XBOOLE_1:13;
then A11: Carrier LLp c=A by A6;
Carrier(-p+LLp)=-p+Carrier LLp by Th16;
then Carrier(-p+LLp)c=-p+A by A11,RLTOPSP1:8;
then Carrier(-p+LLp)c=(-p+A)\{0.V} by A8,ZFMISC_1:34;
then A12: -p+LLp is Linear_Combination of(-p+A)\{0.V} by RLVECT_2:def 6;
A13: LLp+Lp=L+(Lp-Lp) by RLVECT_2:40
.=L+ZeroLC(V) by RLVECT_2:57
.=L by RLVECT_2:41;
A14: Sum(-p+Lp)=(sum Lp)*(-p)+Sum Lp by Th39
.=(sum Lp)*(-p)+Lp.p*p by RLVECT_2:32
.=Lp.p*(-p)+Lp.p*p by A9,Th32
.=Lp.p*(-p+p) by RLVECT_1:def 5
.=Lp.p*0.V by RLVECT_1:5
.=0.V;
Sum(-p+L)=(sum L)*(-p)+Sum L by Th39
.=0.V+0.V by A2,A3,RLVECT_1:10
.=0.V;
then 0.V=Sum((-p+LLp)+(-p+Lp)) by A13,Th17
.=Sum(-p+LLp)+0.V by A14,RLVECT_3:1
.=Sum(-p+LLp);
then {}=Carrier(-p+LLp) by A5,A12;
then A15: ZeroLC(V)=-p+LLp by RLVECT_2:def 5;
A16: LLp=0.V+LLp by Th21
.=(p+-p)+LLp by RLVECT_1:5
.=p+(-p+LLp) by Th19
.=ZeroLC(V) by A15,Th20;
then sum LLp=0 by Th31;
then 0=0+sum Lp by A3,A13,Th34
.=0+Lp.p by A9,Th32;
then not p in Carrier Lp by RLVECT_2:19;
then Carrier LLp\/Carrier Lp={} by A10,A16,RLVECT_2:def 5,TARSKI:def 1;
then Carrier L c={} by A13,RLVECT_2:37;
hence thesis;
end;
end;
Lm6: for A st for L be Linear_Combination of A st Sum L=0.V & sum L=0 holds
Carrier L={} for p be VECTOR of V st p in A holds(-p+A)\{0.V} is
linearly-independent
proof
let A such that
A1: for L be Linear_Combination of A st Sum L=0.V & sum L=0 holds Carrier L=
{};
let p be Element of V such that
A2: p in A;
set pA=-p+A,pA0=(-p+A)\{0.V};
-p+p=0.V by RLVECT_1:5;
then 0.V in pA by A2;
then A3: pA0\/{0.V}=pA by ZFMISC_1:116;
let L be Linear_Combination of pA0 such that
A4: Sum L=0.V;
reconsider sL=-(sum L) as Real;
consider Lp be Linear_Combination of{0.V} such that
A5: Lp.0.V=sL by RLVECT_4:37;
set LLp=L+Lp;
set pLLp=p+LLp;
A6: Carrier Lp c={0.V} by RLVECT_2:def 6;
A7: p+pA=(p+-p)+A by Th5
.=0.V+A by RLVECT_1:5
.=A by Th6;
A8: Carrier pLLp=p+Carrier LLp by Th16;
A9: Carrier L c=pA0 by RLVECT_2:def 6;
then Carrier LLp c=Carrier L\/Carrier Lp & Carrier L\/Carrier Lp c=pA0\/{0.V}
by A6,RLVECT_2:37,XBOOLE_1:13;
then Carrier LLp c=pA by A3;
then Carrier pLLp c=A by A7,A8,RLTOPSP1:8;
then A10: pLLp is Linear_Combination of A by RLVECT_2:def 6;
A11: sum pLLp=sum LLp by Th37;
A12: sum LLp=sum L+sum Lp by Th34
.=sum L+sL by A5,A6,Th32
.=0;
then Sum pLLp=0*p+Sum LLp by Th39
.=0.V+Sum LLp by RLVECT_1:10
.=Sum LLp
.=Sum L+Sum Lp by RLVECT_3:1
.=Sum Lp by A4
.=Lp.0.V*0.V by RLVECT_2:32
.=0.V;
then Carrier pLLp={} by A1,A10,A11,A12;
then A13: pLLp=ZeroLC(V) by RLVECT_2:def 5;
A14: LLp=0.V+LLp by Th21
.=(-p+p)+LLp by RLVECT_1:5
.=-p+ZeroLC(V) by A13,Th19
.=ZeroLC(V) by Th20;
assume Carrier L<>{};
then consider v be object such that
A15: v in Carrier L by XBOOLE_0:def 1;
reconsider v as Element of V by A15;
not v in Carrier Lp by A6,A9,A15,XBOOLE_0:def 5;
then Lp.v=0;
then L.v+0=LLp.v by RLVECT_2:def 10
.=0 by A14,RLVECT_2:20;
hence contradiction by A15,RLVECT_2:19;
end;
theorem Th41:
A is affinely-independent iff for v st v in A holds
-v + A\{0.V} is linearly-independent
proof
hereby assume A is affinely-independent;
then for L be Linear_Combination of A st Sum L=0.V & sum L=0 holds Carrier L
={} by Lm5;
hence for v st v in A holds(-v+A)\{0.V} is linearly-independent by Lm6;
end;
assume A1: for v st v in A holds(-v+A)\{0.V} is linearly-independent;
assume A is non empty;
then consider v be object such that
A2: v in A;
reconsider v as Element of V by A2;
take v;
thus thesis by A1,A2;
end;
theorem Th42:
A is affinely-independent iff
for L be Linear_Combination of A st Sum L = 0.V & sum L = 0
holds Carrier L = {}
proof
thus A is affinely-independent implies for L be Linear_Combination of A st
Sum L=0.V & sum L=0 holds Carrier L={} by Lm5;
assume for L be Linear_Combination of A st Sum L=0.V & sum L=0 holds Carrier
L={};
then for p be VECTOR of V st p in A holds(-p+A)\{0.V} is linearly-independent
by Lm6;
hence thesis by Th41;
end;
theorem Th43:
A is affinely-independent & B c= A implies B is affinely-independent
proof
assume that
A1: A is affinely-independent and
A2: B c=A;
now let L be Linear_Combination of B such that
A3: Sum L=0.V & sum L=0;
L is Linear_Combination of A by A2,RLVECT_2:21;
hence Carrier L={} by A1,A3,Th42;
end;
hence thesis by Th42;
end;
registration
let V;
cluster linearly-independent -> affinely-independent for Subset of V;
coherence
proof
let A;
assume A is linearly-independent;
then for L be Linear_Combination of A st Sum L=0.V & sum L=0 holds Carrier L=
{};
hence thesis by Th42;
end;
end;
reserve I for affinely-independent Subset of V;
registration
let V,I,v;
cluster v + I -> affinely-independent;
coherence
proof
set vI=v+I;
now let L be Linear_Combination of vI such that
A1: Sum L=0.V and
A2: sum L=0;
set vL=-v+L;
A3: sum vL=0 by A2,Th37;
A4: Carrier vL=-v+Carrier L & Carrier L c=vI by Th16,RLVECT_2:def 6;
-v+vI=(-v+v)+I by Th5
.=0.V+I by RLVECT_1:5
.=I by Th6;
then Carrier vL c=I by A4,RLTOPSP1:8;
then A5: vL is Linear_Combination of I by RLVECT_2:def 6;
Sum vL=0*(-v)+0.V by A1,A2,Th39
.=0.V+0.V by RLVECT_1:10
.=0.V;
then Carrier vL={} by A3,A5,Th42;
then A6: vL=ZeroLC(V) by RLVECT_2:def 5;
L=0.V+L by Th21
.=(v+-v)+L by RLVECT_1:5
.=v+ZeroLC(V) by A6,Th19
.=ZeroLC(V) by Th20;
hence Carrier L={} by RLVECT_2:def 5;
end;
hence thesis by Th42;
end;
end;
theorem
v+A is affinely-independent implies A is affinely-independent
proof
assume A1: v+A is affinely-independent;
-v+(v+A)=(-v+v)+A by Th5
.=0.V+A by RLVECT_1:5
.=A by Th6;
hence thesis by A1;
end;
registration
let V,I,r;
cluster r*I -> affinely-independent;
coherence
proof
per cases;
suppose r=0;
then r*I c={0.V} by Th12;
then r*I={}V or r*I={0.V} by ZFMISC_1:33;
hence thesis;
end;
suppose A1: r<>0;
now let L be Linear_Combination of r*I such that
A2: Sum L=0.V and
A3: sum L=0;
set rL=r"(*)L;
A4: Sum rL=r"*0.V by A2,Th40
.=0.V;
A5: Carrier rL=r"*Carrier L & Carrier L c=r*I by A1,Th23,RLVECT_2:def 6;
r"*(r*I)=(r"*r)*I by Th10
.=1*I by A1,XCMPLX_0:def 7
.=I by Th11;
then Carrier rL c=I by A5,Th9;
then A6: rL is Linear_Combination of I by RLVECT_2:def 6;
sum rL=0 by A1,A3,Th38;
then Carrier rL={} by A4,A6,Th42;
then A7: rL=ZeroLC(V) by RLVECT_2:def 5;
L=1(*)L by Th28
.=(r*r")(*)L by A1,XCMPLX_0:def 7
.=r(*)ZeroLC(V) by A7,Th27
.=ZeroLC(V) by Th26;
hence Carrier L={} by RLVECT_2:def 5;
end;
hence thesis by Th42;
end;
end;
end;
theorem
r * A is affinely-independent & r <> 0 implies A is affinely-independent
proof
assume that
A1: r*A is affinely-independent and
A2: r<>0;
r"*(r*A)=(r"*r)*A by Th10
.=1*A by A2,XCMPLX_0:def 7
.=A by Th11;
hence thesis by A1;
end;
theorem Th46:
0.V in A implies
(A is affinely-independent iff A \ {0.V} is linearly-independent)
proof
assume A1: 0.V in A;
A2: -0.V+A=0.V+A
.=A by Th6;
hence A is affinely-independent implies A\{0.V} is linearly-independent by A1
,Th41;
assume A\{0.V} is linearly-independent;
hence thesis by A1,A2;
end;
definition
let V;
let F be Subset-Family of V;
attr F is affinely-independent means
A in F implies A is affinely-independent;
end;
registration
let V;
cluster empty -> affinely-independent for Subset-Family of V;
coherence;
let I;
cluster {I} -> affinely-independent for Subset-Family of V;
coherence
by TARSKI:def 1;
end;
registration
let V;
cluster empty affinely-independent for Subset-Family of V;
existence
proof
take{}bool the carrier of V;
thus thesis;
end;
cluster non empty affinely-independent for Subset-Family of V;
existence
proof
take{the affinely-independent Subset of V};
thus thesis;
end;
end;
theorem
F1 is affinely-independent & F2 is affinely-independent implies
F1 \/ F2 is affinely-independent
proof
assume A1: F1 is affinely-independent & F2 is affinely-independent;
let A;
assume A in F1\/F2;
then A in F1 or A in F2 by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem
F1 c= F2 & F2 is affinely-independent implies F1 is affinely-independent;
begin :: Affine Hull
definition
let RLS;
let A be Subset of RLS;
func Affin A -> Subset of RLS equals
meet {B where B is Affine Subset of RLS : A c= B};
coherence
proof
set BB={B where B is Affine Subset of RLS:A c=B};
BB c=bool[#]RLS
proof
let x be object;
assume x in BB;
then ex B be Affine Subset of RLS st x=B & A c=B;
hence thesis;
end;
then reconsider BB as Subset-Family of RLS;
meet BB is Subset of RLS;
hence thesis;
end;
end;
registration
let RLS;
let A be Subset of RLS;
cluster Affin A -> Affine;
coherence
proof
set BB={B where B is Affine Subset of RLS:A c=B};
let v1,v2 be Element of RLS;
let r be Real;
assume that
A1: v1 in Affin A and
A2: v2 in Affin A;
A3: now let Y be set;
assume A4: Y in BB;
then consider B be Affine Subset of RLS such that
A5: Y=B and
A c=B;
v1 in B & v2 in B by A1,A2,A4,A5,SETFAM_1:def 1;
hence (1-r)*v1+r*v2 in Y by A5,RUSUB_4:def 4;
end;
BB<>{} by A1,SETFAM_1:def 1;
hence thesis by A3,SETFAM_1:def 1;
end;
end;
Lm7: for V be non empty RLSStruct for A be Subset of V holds A c= Affin A
proof
let V be non empty RLSStruct;
let A be Subset of V;
set BB={B where B is Affine Subset of V:A c=B};
A1: now let Y be set;
assume Y in BB;
then ex B be Affine Subset of V st Y=B & A c=B;
hence A c=Y;
end;
[#]V is Affine;
then [#]V in BB;
hence thesis by A1,SETFAM_1:5;
end;
Lm8: for V be non empty RLSStruct for A be Affine Subset of V holds A=Affin A
proof
let V be non empty RLSStruct;
let A be Affine Subset of V;
set BB={B where B is Affine Subset of V:A c=B};
A in BB;
then A1: Affin A c=A by SETFAM_1:3;
A c=Affin A by Lm7;
hence thesis by A1;
end;
registration
let RLS;
let A be empty Subset of RLS;
cluster Affin A -> empty;
coherence
proof
{}RLS is Affine;
hence thesis by Lm8;
end;
end;
registration
let RLS;
let A be non empty Subset of RLS;
cluster Affin A -> non empty;
coherence
proof
A c=Affin A by Lm7;
hence thesis;
end;
end;
theorem
for A be Subset of RLS holds A c= Affin A by Lm7;
theorem
for A be Affine Subset of RLS holds A = Affin A by Lm8;
theorem Th51:
for A,B be Subset of RLS st A c= B & B is Affine holds Affin A c= B
proof
let A,B be Subset of RLS;
assume A c=B & B is Affine;
then B in {C where C is Affine Subset of RLS:A c=C};
hence thesis by SETFAM_1:3;
end;
theorem Th52:
for A,B be Subset of RLS st A c= B holds Affin A c= Affin B
proof
let A,B be Subset of RLS;
assume A1: A c=B;
B c=Affin B by Lm7;
then A c=Affin B by A1;
hence thesis by Th51;
end;
theorem Th53:
Affin (v+A) = v + Affin A
proof
v+A c=v+Affin A by Lm7,RLTOPSP1:8;
then A1: Affin(v+A)c=v+Affin A by Th51,RUSUB_4:31;
-v+(v+A)=(-v+v)+A by Th5
.=0.V+A by RLVECT_1:5
.=A by Th6;
then A c=-v+Affin(v+A) by Lm7,RLTOPSP1:8;
then A2: Affin A c=-v+Affin(v+A) by Th51,RUSUB_4:31;
v+(-v+Affin(v+A))=(v+-v)+Affin(v+A) by Th5
.=0.V+Affin(v+A) by RLVECT_1:5
.=Affin(v+A) by Th6;
then v+Affin A c=Affin(v+A) by A2,RLTOPSP1:8;
hence thesis by A1;
end;
theorem Th54:
AR is Affine implies r * AR is Affine
proof
assume A1: AR is Affine;
let v1,v2 be VECTOR of R,s;
assume v1 in r*AR;
then consider w1 be Element of R such that
A2: v1=r*w1 and
A3: w1 in AR;
assume v2 in r*AR;
then consider w2 be Element of R such that
A4: v2=r*w2 and
A5: w2 in AR;
A6: (1-s)*w1+s*w2 in AR by A1,A3,A5;
A7: (1-s)*(r*w1)=((1-s)*r)*w1 by RLVECT_1:def 7
.=r*((1-s)*w1) by RLVECT_1:def 7;
s*(r*w2)=(s*r)*w2 by RLVECT_1:def 7
.=r*(s*w2) by RLVECT_1:def 7;
then (1-s)*v1+s*v2=r*((1-s)*w1+s*w2) by A2,A4,A7,RLVECT_1:def 5;
hence thesis by A6;
end;
theorem Th55:
r <> 0 implies Affin (r*AR) = r * Affin AR
proof
assume A1: r<>0;
r"*(r*AR)=(r"*r)*AR by Th10
.=1*AR by A1,XCMPLX_0:def 7
.=AR by Th11;
then AR c=r"*Affin(r*AR) by Lm7,Th9;
then A2: Affin AR c=r"*Affin(r*AR) by Th51,Th54;
r*AR c=r*Affin AR by Lm7,Th9;
then A3: Affin(r*AR)c=r*Affin AR by Th51,Th54;
r*(r"*Affin(r*AR))=(r*r")*Affin(r*AR) by Th10
.=1*Affin(r*AR) by A1,XCMPLX_0:def 7
.=Affin(r*AR) by Th11;
then r*Affin AR c=Affin(r*AR) by A2,Th9;
hence thesis by A3;
end;
theorem
Affin (r*A) = r * Affin A
proof
per cases;
suppose A1: r=0;
then A2: r*Affin A c={0.V} by Th12;
A3: r*Affin A c=r*A
proof
let x be object;
assume A4: x in r*Affin A;
then ex v be Element of V st x=r*v & v in Affin A;
then A is non empty;
then consider v be object such that
A5: v in A;
reconsider v as Element of V by A5;
A6: r*v in r*A by A5;
x=0.V by A2,A4,TARSKI:def 1;
hence thesis by A1,A6,RLVECT_1:10;
end;
r*A c={0.V} by A1,Th12;
then A7: r*A is empty or r*A={0.V} by ZFMISC_1:33;
{0.V} is Affine by RUSUB_4:23;
then A8: Affin(r*A)=r*A by A7,Lm8;
r*A c=r*Affin A by Lm7,Th9;
hence thesis by A3,A8;
end;
suppose r<>0;
hence thesis by Th55;
end;
end;
theorem Th57:
v in Affin A implies Affin A = v + Up Lin (-v+A)
proof
set vA=-v+A;
set BB={B where B is Affine Subset of V:vA c=B};
A1: -v+A c=Up(Lin(-v+A))
proof
let x be object;
assume x in -v+A;
then x in Lin(-v+A) by RLVECT_3:15;
hence thesis;
end;
Up(Lin vA) is Affine by RUSUB_4:24;
then A2: Up(Lin vA) in BB by A1;
then A3: Affin vA c=Up(Lin vA) by SETFAM_1:3;
assume v in Affin A;
then -v+v in -v+Affin A;
then A4: 0.V in -v+Affin A by RLVECT_1:5;
now let Y be set;
A5: Affin vA=-v+Affin A by Th53;
assume Y in BB;
then consider B be Affine Subset of V such that
A6: Y=B and
A7: vA c=B;
A8: Lin vA is Subspace of Lin B by A7,RLVECT_3:20;
Affin vA c=B by A7,Th51;
then B=the carrier of Lin B by A4,A5,RUSUB_4:26;
hence Up(Lin vA)c=Y by A6,A8,RLSUB_1:def 2;
end;
then Up(Lin(-v+A))c=Affin vA by A2,SETFAM_1:5;
then Up(Lin(-v+A))=Affin vA by A3;
hence v+Up(Lin(-v+A))=v+(-v+Affin A) by Th53
.=(v+-v)+Affin A by Th5
.=0.V+Affin A by RLVECT_1:5
.=Affin A by Th6;
end;
Lm9: Lin(A\/{0.V})=Lin A
proof
{0.V}=the carrier of(0).V by RLSUB_1:def 3;
then Lin{0.V}=(0).V by RLVECT_3:18;
hence Lin(A\/{0.V})=(Lin A)+(0).V by RLVECT_3:22
.=Lin A by RLSUB_2:9;
end;
theorem Th58:
A is affinely-independent iff for B st B c= A & Affin A = Affin B holds A = B
proof
hereby assume A1: A is affinely-independent;
let B;
assume that
A2: B c=A and
A3: Affin A=Affin B;
assume A<>B;
then B c<A by A2;
then consider p be object such that
A4: p in A and
A5: not p in B by XBOOLE_0:6;
reconsider p as Element of V by A4;
A6: A\{p}c=Affin(A\{p}) by Lm7;
B is non empty by A3,A4;
then consider q be object such that
A7: q in B;
reconsider q as Element of V by A7;
-(-q)=q;
then A8: -q+p<>0.V by A5,A7,RLVECT_1:def 10;
set qA0=(-q+A)\{0.V};
-q+p in -q+A by A4;
then A9: -q+p in qA0 by A8,ZFMISC_1:56;
qA0 is linearly-independent by A1,A2,A7,Th41;
then A10: not-q+p in Lin(qA0\{-q+p}) by A9,RLVECT_5:17;
A11: q+(-q+p)=q+-q+p by RLVECT_1:def 3
.=0.V+p by RLVECT_1:5
.=p;
-q+q=0.V by RLVECT_1:5;
then 0.V in -q+A by A2,A7;
then A12: 0.V in -q+A\{-q+p} by A8,ZFMISC_1:56;
(-q+A)\{0.V}\{-q+p}=(-q+A)\({0.V}\/{-q+p}) by XBOOLE_1:41
.=(-q+A)\{-q+p}\{0.V} by XBOOLE_1:41;
then A13: Lin(qA0\{-q+p})=Lin(((-q+A)\{-q+p}\{0.V})\/{0.V}) by Lm9
.=Lin((-q+A)\{-q+p}) by A12,ZFMISC_1:116
.=Lin((-q+A)\(-q+{p})) by Lm3
.=Lin(-q+(A\{p})) by Lm2;
q in A\{p} by A2,A5,A7,ZFMISC_1:56;
then A14: Affin(A\{p})=q+Up Lin(qA0\{-q+p}) by A6,A13,Th57;
A15: not p in Affin(A\{p})
proof
assume p in Affin(A\{p});
then consider v be Element of V such that
A16: p=q+v and
A17: v in Up Lin(qA0\{-q+p}) by A14;
-q+p=v by A11,A16,RLVECT_1:8;
hence thesis by A10,A17;
end;
B c=A\{p} by A2,A5,ZFMISC_1:34;
then A18: Affin B c=Affin(A\{p}) by Th52;
Affin(A\{p})c=Affin A by Th52,XBOOLE_1:36;
then A19: Affin A=Affin(A\{p}) by A3,A18;
A c=Affin A by Lm7;
hence contradiction by A4,A15,A19;
end;
assume A20: for B st B c=A & Affin A=Affin B holds A=B;
assume A is non affinely-independent;
then consider p be Element of V such that
A21: p in A and
A22: (-p+A)\{0.V} is non linearly-independent by Th41;
set L=Lin((-p+A)\{0.V});
(-p+A)\{0.V}c=the carrier of L
proof
let x be object;
assume x in (-p+A)\{0.V};
then x in L by RLVECT_3:15;
hence thesis;
end;
then reconsider pA0=(-p+A)\{0.V} as Subset of L;
-p+p=0.V by RLVECT_1:5;
then A23: 0.V in -p+A by A21;
then A24: pA0\/{0.V}=-p+A by ZFMISC_1:116;
Lin(pA0)=L by RLVECT_5:20;
then consider b be Subset of L such that
A25: b c=pA0 and
A26: b is linearly-independent and
A27: Lin(b)=L by RLVECT_3:25;
reconsider B=b as linearly-independent Subset of V by A26,RLVECT_5:14;
A28: B\/{0.V}c=pA0\/{0.V} by A25,XBOOLE_1:9;
0.V in {0.V} by TARSKI:def 1;
then p+0.V=p & 0.V in B\/{0.V} by XBOOLE_0:def 3;
then A29: p in p+(B\/{0.V});
A30: p+(B\/{0.V})c=Affin(p+(B\/{0.V})) by Lm7;
A31: p+(-p+A)=(p+-p)+A by Th5
.=0.V+A by RLVECT_1:5
.=A by Th6;
A32: -p+(p+(B\/{0.V}))=(-p+p)+(B\/{0.V}) by Th5
.=0.V+(B\/{0.V}) by RLVECT_1:5
.=B\/{0.V} by Th6;
A c=Affin A by Lm7;
then Affin A=p+Up Lin(-p+A) by A21,Th57
.=p+Up Lin((-p+A)\{0.V}\/{0.V}) by A23,ZFMISC_1:116
.=p+Up L by Lm9
.=p+Up Lin(B) by A27,RLVECT_5:20
.=p+Up Lin(-p+(p+(B\/{0.V}))) by A32,Lm9
.=Affin(p+(B\/{0.V})) by A29,A30,Th57;
then pA0=(B\/{0.V})\{0.V} by A20,A24,A28,A31,A32,RLTOPSP1:8
.=B by RLVECT_3:6,ZFMISC_1:117;
hence contradiction by A22;
end;
theorem Th59:
Affin A = {Sum L where L is Linear_Combination of A : sum L=1}
proof
set S={Sum L where L is Linear_Combination of A:sum L=1};
per cases;
suppose A1: A is empty;
assume Affin A<>S;
then S is non empty by A1;
then consider x being object such that
A2: x in S;
consider L be Linear_Combination of A such that
x=Sum L and
A3: sum L=1 by A2;
A={}(the carrier of V) by A1;
then L=ZeroLC(V) by RLVECT_2:23;
hence thesis by A3,Th31;
end;
suppose A is non empty;
then consider p be object such that
A4: p in A;
reconsider p as Element of V by A4;
A c=Affin A by Lm7;
then A5: Affin A=p+Up Lin(-p+A) by A4,Th57;
thus Affin A c=S
proof
let x be object;
assume x in Affin A;
then consider v such that
A6: x=p+v and
A7: v in Up Lin(-p+A) by A5;
v in Lin(-p+A) by A7;
then consider L be Linear_Combination of-p+A such that
A8: Sum L=v by RLVECT_3:14;
set pL=p+L;
consider Lp be Linear_Combination of{0.V} such that
A9: Lp.0.V=1-sum L by RLVECT_4:37;
set pLL=p+(L+Lp);
set pLp=p+Lp;
A10: Carrier Lp c={0.V} by RLVECT_2:def 6;
then A11: p+Carrier Lp c=p+{0.V} by RLTOPSP1:8;
A12: Carrier pL=p+Carrier L & Carrier L c=-p+A by Th16,RLVECT_2:def 6;
p+(-p+A)=(p+-p)+A by Th5
.=0.V+A by RLVECT_1:5
.=A by Th6;
then A13: Carrier pL c=A by A12,RLTOPSP1:8;
A14: Carrier(pL+pLp)c=Carrier pL\/Carrier pLp & pLL=pL+pLp by Th17,
RLVECT_2:37;
Carrier pLp=p+Carrier Lp & p+{0.V}={p+0.V} by Lm3,Th16;
then Carrier pLp c={p} by A11;
then Carrier pL\/Carrier pLp c=A\/{p} by A13,XBOOLE_1:13;
then Carrier pLL c=A\/{p} by A14;
then Carrier pLL c=A by A4,ZFMISC_1:40;
then A15: pLL is Linear_Combination of A by RLVECT_2:def 6;
A16: sum pLL=sum(L+Lp) by Th37;
A17: sum(L+Lp)=sum L+sum Lp by Th34
.=sum L+(1-sum L) by A9,A10,Th32
.=1;
then Sum pLL=1*p+Sum(L+Lp) by Th39
.=1*p+(v+Sum Lp) by A8,RLVECT_3:1
.=1*p+(v+Lp.0.V*0.V) by RLVECT_2:32
.=1*p+(v+0.V)
.=p+(v+0.V) by RLVECT_1:def 8
.=x by A6;
hence thesis by A15,A16,A17;
end;
let x be object;
assume x in S;
then consider L be Linear_Combination of A such that
A18: Sum L=x and
A19: sum L=1;
set pL=-p+L;
Carrier L c=A by RLVECT_2:def 6;
then A20: -p+Carrier L c=-p+A by RLTOPSP1:8;
-p+Carrier L=Carrier pL by Th16;
then pL is Linear_Combination of-p+A by A20,RLVECT_2:def 6;
then Sum pL in Lin(-p+A) by RLVECT_3:14;
then A21: Sum pL in Up Lin(-p+A);
p+Sum pL=p+(1*(-p)+Sum L) by A19,Th39
.=p+(-p+Sum L) by RLVECT_1:def 8
.=(p+-p)+Sum L by RLVECT_1:def 3
.=0.V+Sum L by RLVECT_1:5
.=x by A18;
hence thesis by A5,A21;
end;
end;
theorem Th60:
I c=A implies ex Ia be affinely-independent Subset of V st
I c= Ia & Ia c= A & Affin Ia = Affin A
proof
assume A1: I c=A;
A2: A c=Affin A by Lm7;
per cases;
suppose A3: I is empty;
per cases;
suppose A4: A is empty;
take I;
thus thesis by A3,A4;
end;
suppose A is non empty;
then consider p be object such that
A5: p in A;
reconsider p as Element of V by A5;
set L=Lin(-p+A);
-p+A c=[#]L
proof
let x be object;
assume x in -p+A;
then x in Lin(-p+A) by RLVECT_3:15;
hence thesis;
end;
then reconsider pA=-p+A as Subset of L;
L=Lin(pA) by RLVECT_5:20;
then consider Ia be Subset of L such that
A6: Ia c=pA and
A7: Ia is linearly-independent and
A8: Lin(Ia)=L by RLVECT_3:25;
[#]L c=[#]V by RLSUB_1:def 2;
then reconsider IA=Ia as Subset of V by XBOOLE_1:1;
set IA0=IA\/{0.V};
not 0.V in IA by A7,RLVECT_3:6,RLVECT_5:14;
then A9: IA0\{0.V}=IA by ZFMISC_1:117;
0.V in {0.V} by TARSKI:def 1;
then A10: 0.V in IA0 by XBOOLE_0:def 3;
IA is linearly-independent by A7,RLVECT_5:14;
then IA0 is affinely-independent by A9,A10,Th46;
then reconsider pIA0=p+IA0 as affinely-independent Subset of V;
take pIA0;
thus I c=pIA0 by A3;
thus pIA0 c=A
proof
let x be object;
assume x in pIA0;
then consider v such that
A11: x=p+v and
A12: v in IA0;
per cases by A12,XBOOLE_0:def 3;
suppose v in IA;
then v in {-p+w:w in A} by A6;
then consider w such that
A13: v=-p+w and
A14: w in A;
x=(p+-p)+w by A11,A13,RLVECT_1:def 3
.=0.V+w by RLVECT_1:5
.=w;
hence thesis by A14;
end;
suppose v in {0.V};
then v=0.V by TARSKI:def 1;
hence thesis by A5,A11;
end;
end;
A15: pIA0 c=Affin pIA0 by Lm7;
A16: -p+pIA0=(-p+p)+IA0 by Th5
.=0.V+IA0 by RLVECT_1:5
.=IA0 by Th6;
p+0.V=p;
then p in pIA0 by A10;
hence Affin pIA0=p+Up Lin(IA0) by A15,A16,Th57
.=p+Up Lin(IA) by Lm9
.=p+Up L by A8,RLVECT_5:20
.=Affin A by A2,A5,Th57;
end;
end;
suppose I is non empty;
then consider p be object such that
A17: p in I;
reconsider p as Element of V by A17;
A18: (-p+I)\{0.V} is linearly-independent by A17,Th41;
A19: -p+I c=-p+A by A1,RLTOPSP1:8;
set L=Lin(-p+A);
A20: -p+I\{0.V}c=-p+I by XBOOLE_1:36;
A21: -p+A c=Up L
proof
let x be object;
assume x in -p+A;
then x in L by RLVECT_3:15;
hence thesis;
end;
then -p+I c=Up L by A19;
then reconsider pI0=-p+I\{0.V},pA=-p+A as Subset of L by A20,A21,XBOOLE_1:1;
L=Lin(pA) & pI0 c=pA by A19,A20,RLVECT_5:20;
then consider i be linearly-independent Subset of L such that
A22: pI0 c=i and
A23: i c=pA and
A24: Lin(i)=L by A18,Th15,RLVECT_5:15;
reconsider Ia=i as linearly-independent Subset of V by RLVECT_5:14;
set I0=Ia\/{0.V};
A25: 0.V in {0.V} by TARSKI:def 1;
not 0.V in Ia by RLVECT_3:6;
then I0\{0.V}=Ia & 0.V in I0 by A25,XBOOLE_0:def 3,ZFMISC_1:117;
then I0 is affinely-independent by Th46;
then reconsider pI0=p+I0 as affinely-independent Subset of V;
take pI0;
A26: -p+p=0.V by RLVECT_1:5;
then A27: p+(-p+I)=0.V+I by Th5
.=I by Th6;
0.V in {-p+v where v is Element of V:v in I} by A17,A26;
then (-p+I\{0.V})\/{0.V}=-p+I by ZFMISC_1:116;
then A28: -p+I c=I0 by A22,XBOOLE_1:9;
hence I c=pI0 by A27,RLTOPSP1:8;
p+(-p+I)c=pI0 by A28,RLTOPSP1:8;
then A29: p in pI0 by A17,A27;
thus pI0 c=A
proof
let x be object;
assume x in pI0;
then consider v such that
A30: x=p+v and
A31: v in I0;
per cases by A31,XBOOLE_0:def 3;
suppose v in Ia;
then v in {-p+w:w in A} by A23;
then consider w such that
A32: v=-p+w and
A33: w in A;
x=(p+-p)+w by A30,A32,RLVECT_1:def 3
.=0.V+w by RLVECT_1:5
.=w;
hence thesis by A33;
end;
suppose v in {0.V};
then v=0.V by TARSKI:def 1;
then x=p by A30;
hence thesis by A1,A17;
end;
end;
A34: pI0 c=Affin pI0 by Lm7;
A35: p in A by A1,A17;
-p+pI0=0.V+I0 by A26,Th5
.=I0 by Th6;
hence Affin pI0=p+Up Lin(I0) by A29,A34,Th57
.=p+Up Lin(Ia) by Lm9
.=p+Up L by A24,RLVECT_5:20
.=Affin A by A2,A35,Th57;
end;
end;
theorem
for A,B be finite Subset of V st
A is affinely-independent & Affin A = Affin B & card B <= card A
holds B is affinely-independent
proof
let A,B be finite Subset of V;
assume that
A1: A is affinely-independent and
A2: Affin A=Affin B and
A3: card B<=card A;
per cases;
suppose A is empty;
then B is empty by A3,XXREAL_0:1;
hence thesis;
end;
suppose A is non empty;
then consider p be object such that
A4: p in A;
card A>0 by A4;
then reconsider n=(card A)-1 as Element of NAT by NAT_1:20;
A5: A c=Affin A by Lm7;
reconsider p as Element of V by A4;
set L=Lin(-p+A);
{}V c=B;
then consider Ia be affinely-independent Subset of V such that
{}V c=Ia and
A6: Ia c=B and
A7: Affin Ia=Affin B by Th60;
Ia is non empty by A2,A4,A7;
then consider q be object such that
A8: q in Ia;
-p+A c=[#]L
proof
let x be object;
assume x in -p+A;
then x in Lin(-p+A) by RLVECT_3:15;
hence thesis;
end;
then reconsider pA=-p+A as Subset of L;
-p+A\{0.V} is linearly-independent by A1,A4,Th41;
then A9: pA\{0.V} is linearly-independent by RLVECT_5:15;
-p+p=0.V by RLVECT_1:5;
then A10: 0.V in pA by A4;
then L=Lin(((-p+A)\{0.V})\/{0.V}) by ZFMISC_1:116
.=Lin(-p+A\{0.V}) by Lm9
.=Lin(pA\{0.V}) by RLVECT_5:20;
then A11: pA\{0.V} is Basis of L by A9,RLVECT_3:def 3;
reconsider IA=Ia as finite set by A6;
A12: Ia c=Affin Ia by Lm7;
reconsider q as Element of V by A8;
p+L=p+Up L by RUSUB_4:30
.=Affin A by A4,A5,Th57
.=q+Up Lin(-q+Ia) by A2,A7,A8,A12,Th57
.=q+Lin(-q+Ia) by RUSUB_4:30;
then A13: L=Lin(-q+Ia) by RLSUB_1:69;
set qI=-q+Ia;
A14: qI c=[#]Lin(-q+Ia)
proof
let x be object;
assume x in qI;
then x in Lin(-q+Ia) by RLVECT_3:15;
hence thesis;
end;
card pA=n+1 by Th7;
then A15: card(pA\{0.V})=n by A10,STIRL2_1:55;
then pA\{0.V} is finite;
then A16: L is finite-dimensional by A11,RLVECT_5:def 1;
reconsider qI as Subset of Lin(-q+Ia) by A14;
-q+Ia\{0.V} is linearly-independent by A8,Th41;
then A17: qI\{0.V} is linearly-independent by RLVECT_5:15;
-q+q=0.V by RLVECT_1:5;
then A18: 0.V in qI by A8;
then Lin(-q+Ia)=Lin(((-q+Ia)\{0.V})\/{0.V}) by ZFMISC_1:116
.=Lin(-q+Ia\{0.V}) by Lm9
.=Lin(qI\{0.V}) by RLVECT_5:20;
then qI\{0.V} is Basis of Lin(-q+Ia) by A17,RLVECT_3:def 3;
then A19: card(qI\{0.V})=n by A11,A13,A15,A16,RLVECT_5:25;
then (not 0.V in qI\{0.V}) & qI\{0.V} is finite by ZFMISC_1:56;
then A20: n+1=card((qI\{0.V})\/{0.V}) by A19,CARD_2:41
.=card qI by A18,ZFMISC_1:116
.=card Ia by Th7;
card IA<=card B by A6,NAT_1:43;
hence thesis by A3,A6,A20,CARD_2:102,XXREAL_0:1;
end;
end;
theorem Th62:
L is convex iff sum L = 1 & for v holds 0 <= L.v
proof
hereby assume L is convex;
then consider F be FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F=Carrier L and
A3: ex f be FinSequence of REAL st len f=len F & Sum(f)=1 & for n be Nat st
n in dom f holds f.n=L.(F.n) & f.n>=0;
consider f be FinSequence of REAL such that
A4: len f=len F and
A5: Sum(f)=1 and
A6: for n be Nat st n in dom f holds f.n=L.(F.n) & f.n>=0 by A3;
A7: len(L*F)=len F by FINSEQ_2:33;
now let k be Nat;
assume A8: 1<=k & k<=len F;
then k in dom f by A4,FINSEQ_3:25;
then A9: f.k=L.(F.k) by A6;
k in dom(L*F) by A7,A8,FINSEQ_3:25;
hence (L*F).k=f.k by A9,FUNCT_1:12;
end;
then L*F=f by A4,A7;
hence sum L=1 by A1,A2,A5,Def3;
let v be Element of V;
per cases;
suppose v in Carrier L;
then consider n be object such that
A10: n in dom F and
A11: F.n=v by A2,FUNCT_1:def 3;
A12: dom f=dom F by A4,FINSEQ_3:29;
then f.n=L.(F.n) by A6,A10;
hence L.v>=0 by A6,A10,A11,A12;
end;
suppose not v in Carrier L;
hence L.v>=0;
end;
end;
assume sum L=1;
then consider F be FinSequence of V such that
A13: F is one-to-one & rng F=Carrier L and
A14: 1=Sum(L*F) by Def3;
assume A15: for v be Element of V holds L.v>=0;
now take F;
thus F is one-to-one & rng F=Carrier L by A13;
take f=L*F;
thus len f=len F & Sum f=1 by A14,FINSEQ_2:33;
then A16: dom F=dom f by FINSEQ_3:29;
let n be Nat;
assume A17: n in dom f;
then A18: f.n=L.(F.n) by FUNCT_1:12;
F.n=F/.n by A16,A17,PARTFUN1:def 6;
hence f.n=L.(F.n) & f.n>=0 by A15,A18;
end;
hence thesis;
end;
theorem Th63:
L is convex implies L.x <= 1
proof
assume A1: L is convex;
then sum L=1 by Th62;
then consider F be FinSequence of V such that
F is one-to-one and
A2: rng F=Carrier L and
A3: 1=Sum(L*F) by Def3;
assume A4: L.x>1;
then x in dom L by FUNCT_1:def 2;
then reconsider v=x as Element of V by FUNCT_2:def 1;
v in Carrier L by A4;
then consider n be object such that
A5: n in dom F and
A6: F.n=v by A2,FUNCT_1:def 3;
len(L*F)=len F by FINSEQ_2:33;
then A7: dom(L*F)=dom F by FINSEQ_3:29;
A8: now let i be Nat;
assume i in dom(L*F);
then (L*F).i=L.(F.i) & F.i=F/.i by A7,FUNCT_1:12,PARTFUN1:def 6;
hence (L*F).i>=0 by A1,Th62;
end;
reconsider n as Nat by A5;
(L*F).n=L.x by A5,A6,A7,FUNCT_1:12;
hence contradiction by A3,A4,A5,A7,A8,MATRPROB:5;
end;
reconsider jj=1 as Real;
theorem Th64:
L is convex & L.x = 1 implies Carrier L = {x}
proof
assume that
A1: L is convex and
A2: L.x=1;
x in dom L by A2,FUNCT_1:def 2;
then reconsider v=x as Element of V by FUNCT_2:def 1;
consider K be Linear_Combination of{v} such that
A3: K.v=jj by RLVECT_4:37;
set LK=L-K;
A4: Carrier K c={v} by RLVECT_2:def 6;
sum LK=sum L-sum K by Th36
.=sum L-1 by A3,A4,Th32
.=1-1 by A1,Th62
.=0;
then consider F be FinSequence of V such that
F is one-to-one and
A5: rng F=Carrier LK and
A6: 0=Sum(LK*F) by Def3;
len(LK*F)=len F by FINSEQ_2:33;
then A7: dom(LK*F)=dom F by FINSEQ_3:29;
A8: for i be Nat st i in dom(LK*F) holds 0<=(LK*F).i
proof
let i be Nat;
assume A9: i in dom(LK*F);
then A10: (LK*F).i=LK.(F.i) by FUNCT_1:12;
A11: F.i in Carrier LK by A5,A7,A9,FUNCT_1:def 3;
then A12: LK.(F.i)=L.(F.i)-K.(F.i) by RLVECT_2:54;
per cases;
suppose F.i=v;
hence thesis by A2,A3,A9,A12,FUNCT_1:12;
end;
suppose F.i<>v;
then not F.i in Carrier K by A4,TARSKI:def 1;
then K.(F.i)=0 by A11;
hence thesis by A1,A10,A11,A12,Th62;
end;
end;
Carrier LK={}
proof
assume Carrier LK<>{};
then consider p be object such that
A13: p in Carrier LK by XBOOLE_0:def 1;
reconsider p as Element of V by A13;
consider i be object such that
A14: i in dom F and
A15: F.i=p by A5,A13,FUNCT_1:def 3;
reconsider i as Nat by A14;
(LK*F).i>0
proof
A16: LK.p=L.p-K.p by RLVECT_2:54;
per cases;
suppose p=v;
then LK.p=1-1 by A2,A3,RLVECT_2:54;
hence thesis by A13,RLVECT_2:19;
end;
suppose p<>v;
then not p in Carrier K by A4,TARSKI:def 1;
then K.p=0;
then A17: LK.p>=0 by A1,A16,Th62;
LK.p<>0 by A13,RLVECT_2:19;
hence thesis by A7,A14,A15,A17,FUNCT_1:12;
end;
end;
hence thesis by A6,A7,A8,A14,RVSUM_1:85;
end;
then ZeroLC(V)=L+(-K) by RLVECT_2:def 5;
then A18: -K=-L by RLVECT_2:50;
A19: v in Carrier L by A2;
-(-L)=L by RLVECT_2:53;
then K=L by A18,RLVECT_2:53;
hence thesis by A4,A19,ZFMISC_1:33;
end;
theorem Th65:
conv A c= Affin A
proof
let x be object;
assume A1: x in conv A;
then reconsider A1=A as non empty Subset of V;
conv(A1)={Sum(L) where L is Convex_Combination of A1:L in ConvexComb(V)}
by CONVEX3:5;
then consider L be Convex_Combination of A1 such that
A2: Sum L=x and
L in ConvexComb(V) by A1;
sum L=1 by Th62;
then x in {Sum K where K is Linear_Combination of A:sum K=1} by A2;
hence thesis by Th59;
end;
theorem
x in conv A & (conv A)\{x} is convex implies x in A
proof
assume that
A1: x in conv A and
A2: (conv A)\{x} is convex;
reconsider A1=A as non empty Subset of V by A1;
A3: conv(A1)={Sum(L) where L is Convex_Combination of A1:L in ConvexComb(V)}
by CONVEX3:5;
assume A4: not x in A;
consider L be Convex_Combination of A1 such that
A5: Sum L=x and
L in ConvexComb(V) by A1,A3;
set C=Carrier L;
A6: C c=A1 by RLVECT_2:def 6;
C<>{} by CONVEX1:21;
then consider p be object such that
A7: p in C by XBOOLE_0:def 1;
reconsider p as Element of V by A7;
A8: sum L=1 by Th62;
C\{p}<>{}
proof
assume A9: C\{p}={};
then C={p} by A7,ZFMISC_1:58;
then A10: L.p=1 by A8,Th32;
Sum L=L.p*p by A7,A9,RLVECT_2:35,ZFMISC_1:58;
then x=p by A5,A10,RLVECT_1:def 8;
hence thesis by A4,A6,A7;
end;
then consider q be object such that
A11: q in C\{p} by XBOOLE_0:def 1;
reconsider q as Element of V by A11;
A12: q in C by A11,XBOOLE_0:def 5;
then L.q<>0 by RLVECT_2:19;
then A13: L.q>0 by Th62;
reconsider mm=min(L.p,L.q) as Real;
consider Lq be Linear_Combination of{q} such that
A14: Lq.q=mm by RLVECT_4:37;
A15: p<>q by A11,ZFMISC_1:56;
then A16: p-q<>0.V by RLVECT_1:21;
A17: Carrier Lq c={q} by RLVECT_2:def 6;
{q}c=A by A6,A12,ZFMISC_1:31;
then Carrier Lq c=A by A17;
then A18: Lq is Linear_Combination of A by RLVECT_2:def 6;
consider Lp be Linear_Combination of{p} such that
A19: Lp.p=mm by RLVECT_4:37;
A20: Carrier Lp c={p} by RLVECT_2:def 6;
{p}c=A by A6,A7,ZFMISC_1:31;
then Carrier Lp c=A by A20;
then Lp is Linear_Combination of A by RLVECT_2:def 6;
then A21: Lp-Lq is Linear_Combination of A by A18,RLVECT_2:56;
then -(Lp-Lq) is Linear_Combination of A by RLVECT_2:52;
then reconsider Lpq=L+(Lp-Lq),L1pq=L-(Lp-Lq) as Linear_Combination of A1
by A21,RLVECT_2:38;
A22: Sum L1pq=Sum L-Sum(Lp-Lq) by RLVECT_3:4
.=Sum L+-Sum(Lp-Lq) by RLVECT_1:def 11;
L.p<>0 by A7,RLVECT_2:19;
then L.p>0 by Th62;
then A23: mm>0 by A13,XXREAL_0:15;
A24: for v holds L1pq.v>=0
proof
let v;
A25: L1pq.v=L.v-(Lp-Lq).v by RLVECT_2:54
.=L.v-(Lp.v-Lq.v) by RLVECT_2:54;
A26: L.v>=0 by Th62;
per cases;
suppose A27: v=q;
then not v in Carrier Lp by A15,A20,TARSKI:def 1;
then Lp.v=0;
hence thesis by A23,A14,A25,A26,A27;
end;
suppose A28: v=p;
L.p>=mm by XXREAL_0:17;
then A29: L.p-mm>=mm-mm by XREAL_1:9;
not v in Carrier Lq by A15,A17,A28,TARSKI:def 1;
then Lq.v=0;
hence thesis by A19,A25,A28,A29;
end;
suppose A30: v<>p & v<>q;
then not v in Carrier Lq by A17,TARSKI:def 1;
then A31: Lq.v=0;
not v in Carrier Lp by A20,A30,TARSKI:def 1;
then Lp.v=0;
hence thesis by A25,A31,Th62;
end;
end;
Sum(Lp-Lq)=(Sum Lp)-(Sum Lq) by RLVECT_3:4
.=mm*p-Sum Lq by A19,RLVECT_2:32
.=mm*p-mm*q by A14,RLVECT_2:32
.=mm*(p-q) by RLVECT_1:34;
then A32: Sum(Lp-Lq)<>0.V by A23,A16,RLVECT_1:11;
A33: sum(Lp-Lq)=(sum Lp)-sum Lq by Th36
.=mm-sum Lq by A19,A20,Th32
.=mm-mm by A14,A17,Th32
.=0;
A34: for v holds Lpq.v>=0
proof
let v;
A35: Lpq.v=L.v+(Lp-Lq).v by RLVECT_2:def 10
.=L.v+(Lp.v-Lq.v) by RLVECT_2:54;
A36: L.v>=0 by Th62;
per cases;
suppose A37: v=p;
then not v in Carrier Lq by A15,A17,TARSKI:def 1;
then Lpq.v=L.v+(mm-0) by A19,A35,A37;
hence thesis by A23,A36;
end;
suppose A38: v=q;
L.q>=mm by XXREAL_0:17;
then A39: L.q-mm>=mm-mm by XREAL_1:9;
not v in Carrier Lp by A15,A20,A38,TARSKI:def 1;
then Lp.v=0;
hence thesis by A14,A35,A38,A39;
end;
suppose A40: v<>p & v<>q;
then not v in Carrier Lq by A17,TARSKI:def 1;
then A41: Lq.v=0;
not v in Carrier Lp by A20,A40,TARSKI:def 1;
then Lp.v=0;
hence thesis by A35,A41,Th62;
end;
end;
sum L1pq=sum L-sum(Lp-Lq) by Th36
.=1+0 by A33,Th62;
then A42: L1pq is convex by A24,Th62;
then L1pq in ConvexComb(V) by CONVEX3:def 1;
then A43: Sum L1pq in conv(A1) by A3,A42;
sum Lpq=sum L+sum(Lp-Lq) by Th34
.=1+0 by A33,Th62;
then A44: Lpq is convex by A34,Th62;
then Lpq in ConvexComb(V) by CONVEX3:def 1;
then A45: Sum Lpq in conv(A) by A3,A44;
0.V=-0.V;
then -Sum(Lp-Lq)<>0.V by A32;
then Sum L1pq<>x by A5,A22,RLVECT_1:9;
then A46: Sum L1pq in conv(A)\{x} by A43,ZFMISC_1:56;
Sum Lpq=Sum L+Sum(Lp-Lq) by RLVECT_3:1;
then Sum Lpq<>x by A5,A32,RLVECT_1:9;
then A47: Sum Lpq in conv(A)\{x} by A45,ZFMISC_1:56;
(1/2)*Sum Lpq+(1-1/2)*Sum L1pq=(1/2)*(Sum L+Sum(Lp-Lq))+(1/2)*(Sum L+-Sum(Lp-
Lq)) by A22,RLVECT_3:1
.=(1/2)*Sum L+(1/2)*Sum(Lp-Lq)+(1/2)*(Sum L+-Sum(Lp-Lq)) by RLVECT_1:def 5
.=(1/2)*Sum L+(1/2)*Sum(Lp-Lq)+((1/2)*(Sum L)+(1/2)*(-Sum(Lp-Lq))) by
RLVECT_1:def 5
.=(1/2)*Sum L+((1/2)*Sum(Lp-Lq)+((1/2)*(-Sum(Lp-Lq))+(1/2)*(Sum L))) by
RLVECT_1:def 3
.=(1/2)*Sum L+((1/2)*Sum(Lp-Lq)+(1/2)*(-Sum(Lp-Lq))+(1/2)*(Sum L)) by
RLVECT_1:def 3
.=(1/2)*Sum L+((1/2)*(Sum(Lp-Lq)+(-Sum(Lp-Lq)))+(1/2)*(Sum L)) by
RLVECT_1:def 5
.=(1/2)*Sum L+((1/2)*0.V+(1/2)*(Sum L)) by RLVECT_1:5
.=(1/2)*Sum L+(0.V+(1/2)*(Sum L))
.=(1/2)*Sum L+(1/2)*(Sum L)
.=(1/2+1/2)*Sum L by RLVECT_1:def 6
.=Sum L by RLVECT_1:def 8;
then Sum L in (conv A)\{x} by A2,A46,A47;
hence contradiction by A5,ZFMISC_1:56;
end;
theorem Th67:
Affin conv A = Affin A
proof
thus Affin conv A c=Affin A by Th51,Th65;
let x be object;
assume x in Affin A;
then x in {Sum L where L is Linear_Combination of A:sum L=1} by Th59;
then consider L be Linear_Combination of A such that
A1: x=Sum L and
A2: sum L=1;
reconsider K=L as Linear_Combination of conv A by Lm1,RLVECT_2:21;
Sum K in {Sum M where M is Linear_Combination of conv A:sum M=1} by A2;
hence thesis by A1,Th59;
end;
theorem
conv A c= conv B implies Affin A c= Affin B
proof
Affin conv A=Affin A & Affin conv B=Affin B by Th67;
hence thesis by Th52;
end;
theorem Th69:
for A,B be Subset of RLS st A c= Affin B holds Affin (A\/B) = Affin B
proof
let A,B be Subset of RLS such that
A1: A c=Affin B;
set AB={C where C is Affine Subset of RLS:A\/B c=C};
B c=Affin B by Lm7;
then A\/B c=Affin B by A1,XBOOLE_1:8;
then Affin B in AB;
then A2: Affin(A\/B)c=Affin B by SETFAM_1:3;
Affin B c=Affin(A\/B) by Th52,XBOOLE_1:7;
hence thesis by A2;
end;
begin :: Barycentric Coordinates
definition
let V;
let A such that
A1: A is affinely-independent;
let x be object such that
A2: x in Affin A;
func x |-- A -> Linear_Combination of A means :Def7:
Sum it = x & sum it = 1;
existence
proof
Affin A={Sum L where L is Linear_Combination of A:sum L=1} by Th59;
hence thesis by A2;
end;
uniqueness
proof
let L1,L2 be Linear_Combination of A such that
A3: Sum L1=x and
A4: sum L1=1 and
A5: Sum L2=x and
A6: sum L2=1;
A7: Sum(L1-L2)=Sum L1-Sum L1 by A3,A5,RLVECT_3:4
.=0.V by RLVECT_1:15;
A8: L1-L2 is Linear_Combination of A by RLVECT_2:56;
sum(L1-L2)=1-1 by A4,A6,Th36
.=0;
then Carrier(L1-L2)={} by A1,A7,A8,Th42;
then ZeroLC(V)=L1+(-L2) by RLVECT_2:def 5;
then A9: -L2=-L1 by RLVECT_2:50;
L1=-(-L1) by RLVECT_2:53;
hence thesis by A9,RLVECT_2:53;
end;
end;
theorem Th70:
v1 in Affin I & v2 in Affin I implies
((1-r)*v1+r*v2) |-- I = (1-r) * (v1|--I) + r * (v2|--I)
proof
assume that
A1: v1 in Affin I and
A2: v2 in Affin I;
set rv12=(1-r)*v1+r*v2;
A3: rv12 in Affin I by A1,A2,RUSUB_4:def 4;
(1-r)*(v1|--I) is Linear_Combination of I & r*(v2|--I) is Linear_Combination
of I by RLVECT_2:44;
then A4: (1-r)*(v1|--I)+r*(v2|--I) is Linear_Combination of I by RLVECT_2:38;
A5: Sum((1-r)*(v1|--I)+r*(v2|--I))=Sum((1-r)*(v1|--I))+Sum(r*(v2|--I)) by
RLVECT_3:1
.=(1-r)*Sum(v1|--I)+Sum(r*(v2|--I)) by RLVECT_3:2
.=(1-r)*Sum(v1|--I)+r*Sum(v2|--I) by RLVECT_3:2
.=(1-r)*v1+r*Sum(v2|--I) by A1,Def7
.=rv12 by A2,Def7;
sum((1-r)*(v1|--I)+r*(v2|--I))=sum((1-r)*(v1|--I))+sum(r*(v2|--I)) by Th34
.=(1-r)*sum(v1|--I)+sum(r*(v2|--I)) by Th35
.=(1-r)*sum(v1|--I)+r*sum(v2|--I) by Th35
.=(1-r)*1+r*sum(v2|--I) by A1,Def7
.=(1-r)*1+r*1 by A2,Def7
.=1;
hence thesis by A3,A4,A5,Def7;
end;
theorem Th71:
x in conv I implies x|--I is convex & 0 <= (x|--I).v & (x|--I).v <= 1
proof
assume A1: x in conv I;
then reconsider I1=I as non empty Subset of V;
conv(I1)={Sum(L) where L is Convex_Combination of I1:L in ConvexComb(V)}
by CONVEX3:5;
then consider L be Convex_Combination of I1 such that
A2: Sum L=x and
L in ConvexComb(V) by A1;
conv I c=Affin I & sum L=1 by Th62,Th65;
then L=x|--I by A1,A2,Def7;
hence thesis by Th62,Th63;
end;
theorem Th72:
x in conv I implies ((x|--I).y = 1 iff x = y & x in I)
proof
assume A1: x in conv I;
then reconsider v=x as Element of V;
hereby assume A2: (x|--I).y=1;
x|--I is convex by A1,Th71;
then A3: Carrier(x|--I)={y} by A2,Th64;
y in {y} by TARSKI:def 1;
then reconsider v=y as Element of V by A3;
conv I c=Affin I by Th65;
hence A4: x=Sum(x|--I) by A1,Def7
.=(x|--I).v*v by A3,RLVECT_2:35
.=y by A2,RLVECT_1:def 8;
Carrier(x|--I)c=I & v in Carrier(x|--I) by A2,RLVECT_2:def 6;
hence x in I by A4;
end;
assume that
A5: x=y and
A6: x in I;
consider L be Linear_Combination of{v} such that
A7: L.v=jj by RLVECT_4:37;
Carrier L c={v} by RLVECT_2:def 6;
then A8: sum L=1 by A7,Th32;
A9: I c=Affin I by Lm7;
{v}c=I by A6,ZFMISC_1:31;
then A10: L is Linear_Combination of I by RLVECT_2:21;
Sum L=1*v by A7,RLVECT_2:32
.=v by RLVECT_1:def 8;
hence thesis by A5,A6,A7,A8,A9,A10,Def7;
end;
theorem Th73:
for I st x in Affin I & for v st v in I holds 0 <= (x|--I).v
holds x in conv I
proof
let I such that
A1: x in Affin I and
A2: for v st v in I holds 0<=(x|--I).v;
set xI=x|--I;
A3: Sum xI=x by A1,Def7;
reconsider I1=I as non empty Subset of V by A1;
A4: for v holds 0<=xI.v
proof
let v;
A5: v in Carrier xI or not v in Carrier xI;
Carrier xI c=I by RLVECT_2:def 6;
hence thesis by A2,A5;
end;
sum xI=1 by A1,Def7;
then A6: xI is convex by A4,Th62;
then conv(I1)={Sum(L) where L is Convex_Combination of I1:L in ConvexComb(V)}
& xI in ConvexComb(V) by CONVEX3:5,def 1;
hence thesis by A3,A6;
end;
theorem
x in I implies (conv I)\{x} is convex
proof
assume A1: x in I;
then reconsider X=x as Element of V;
A2: conv I c=Affin I by Th65;
now let v1,v2,r;
set rv12=r*v1+(1-r)*v2;
assume that
A3: 0<r and
A4: r<1;
assume that
A5: v1 in (conv I)\{x} and
A6: v2 in (conv I)\{x};
A7: 1-r>1-1 by A4,XREAL_1:10;
A8: v2 in conv I by A6,ZFMISC_1:56;
then A9: (v2|--I).X<=1 by Th71;
A10: v1 in conv I by A5,ZFMISC_1:56;
then A11: (v1|--I).X<=1 by Th71;
A12: rv12|--I=(1-r)*(v2|--I)+r*(v1|--I) by A2,A10,A8,Th70;
A13: now let w;
assume w in I;
A14: (rv12|--I).w=((1-r)*(v2|--I)).w+(r*(v1|--I)).w by A12,RLVECT_2:def 10
.=(1-r)*((v2|--I).w)+(r*(v1|--I)).w by RLVECT_2:def 11
.=(1-r)*((v2|--I).w)+r*((v1|--I).w) by RLVECT_2:def 11;
(v2|--I).w>=0 & (v1|--I).w>=0 by A10,A8,Th71;
hence 0<=(rv12|--I).w by A3,A7,A14;
end;
rv12 in Affin I by A2,A10,A8,RUSUB_4:def 4;
then A15: rv12 in conv I by A13,Th73;
v1<>x by A5,ZFMISC_1:56;
then (v1|--I).X<>1 by A10,Th72;
then (v1|--I).X<1 by A11,XXREAL_0:1;
then A16: r*((v1|--I).X)<r*1 by A3,XREAL_1:68;
v2<>x by A6,ZFMISC_1:56;
then (v2|--I).X<>1 by A8,Th72;
then (v2|--I).X<1 by A9,XXREAL_0:1;
then (1-r)*((v2|--I).X)<(1-r)*1 by A7,XREAL_1:68;
then A17: (1-r)*((v2|--I).X)+r*((v1|--I).X)<(1-r)*1+r*1 by A16,XREAL_1:8;
(rv12|--I).X=((1-r)*(v2|--I)).X+(r*(v1|--I)).X by A12,RLVECT_2:def 10
.=(1-r)*((v2|--I).X)+(r*(v1|--I)).X by RLVECT_2:def 11
.=(1-r)*((v2|--I).X)+r*((v1|--I).X) by RLVECT_2:def 11;
then rv12<>X by A1,A15,A17,Th72;
hence rv12 in (conv I)\{x} by A15,ZFMISC_1:56;
end;
hence thesis;
end;
theorem Th75:
for B st x in Affin I & for y st y in B holds (x|--I).y = 0
holds x in Affin(I\B) & x |-- I = x |-- (I\B)
proof
let B such that
A1: x in Affin I and
A2: for y st y in B holds(x|--I).y=0;
A3: Affin I={Sum L where L is Linear_Combination of I:sum L=1} by Th59;
A4: I\B is affinely-independent by Th43,XBOOLE_1:36;
consider L be Linear_Combination of I such that
A5: x=Sum L & sum L=1 by A1,A3;
A6: x|--I=L by A1,A5,Def7;
Carrier L c=I\B
proof
A7: Carrier L c=I by RLVECT_2:def 6;
let y be object such that
A8: y in Carrier L;
assume not y in I\B;
then y in B by A7,A8,XBOOLE_0:def 5;
then L.y=0 by A2,A6;
hence thesis by A8,RLVECT_2:19;
end;
then A9: L is Linear_Combination of I\B by RLVECT_2:def 6;
then x in {Sum K where K is Linear_Combination of I\B:sum K=1} by A5;
then x in Affin(I\B) by Th59;
hence thesis by A4,A5,A6,A9,Def7;
end;
theorem
for B st x in conv I & for y st y in B holds (x|--I).y = 0
holds x in conv (I\B)
proof
let B such that
A1: x in conv I and
A2: for y st y in B holds(x|--I).y=0;
set IB=I\B;
A3: conv I c=Affin I by Th65;
then x|--I=x|--IB by A1,A2,Th75;
then A4: for v st v in IB holds 0<=(x|--IB).v by A1,Th71;
A5: IB is affinely-independent by Th43,XBOOLE_1:36;
x in Affin IB by A1,A2,A3,Th75;
hence thesis by A4,A5,Th73;
end;
theorem Th77:
B c= I & x in Affin B implies x |-- B = x |-- I
proof
assume that
A1: B c=I and
A2: x in Affin B;
B is affinely-independent by A1,Th43;
then A3: Sum(x|--B)=x & sum(x|--B)=1 by A2,Def7;
Affin B c=Affin I & x|--B is Linear_Combination of I by A1,Th52,RLVECT_2:21;
hence thesis by A2,A3,Def7;
end;
theorem Th78:
v1 in Affin A & v2 in Affin A & r+s = 1 implies r*v1 + s*v2 in Affin A
proof
A1: Affin A={Sum L where L is Linear_Combination of A:sum L=1} by Th59;
assume v1 in Affin A;
then consider L1 be Linear_Combination of A such that
A2: v1=Sum L1 and
A3: sum L1=1 by A1;
assume v2 in Affin A;
then consider L2 be Linear_Combination of A such that
A4: v2=Sum L2 and
A5: sum L2=1 by A1;
A6: Sum(r*L1+s*L2)=Sum(r*L1)+Sum(s*L2) by RLVECT_3:1
.=r*Sum L1+Sum(s*L2) by RLVECT_3:2
.=r*v1+s*v2 by A2,A4,RLVECT_3:2;
r*L1 is Linear_Combination of A & s*L2 is Linear_Combination of A by
RLVECT_2:44;
then A7: r*L1+s*L2 is Linear_Combination of A by RLVECT_2:38;
assume A8: r+s=1;
sum(r*L1+s*L2)=sum(r*L1)+sum(s*L2) by Th34
.=r*sum L1+sum(s*L2) by Th35
.=r*1+s*1 by A3,A5,Th35
.=1 by A8;
hence thesis by A1,A7,A6;
end;
theorem Th79:
for A,B be finite Subset of V st
A is affinely-independent & Affin A c= Affin B
holds card A <= card B
proof
let A,B be finite Subset of V such that
A1: A is affinely-independent and
A2: Affin A c=Affin B;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A is non empty;
then consider p be object such that
A3: p in A;
reconsider p as Element of V by A3;
A4: A c=Affin A by Lm7;
then A5: p in Affin A by A3;
set LA=Lin(-p+A);
A6: card A=card(-p+A) by Th7;
{}V c=B;
then consider Ib be affinely-independent Subset of V such that
{}V c=Ib and
A7: Ib c=B and
A8: Affin Ib=Affin B by Th60;
Ib is non empty by A2,A3,A8;
then consider q be object such that
A9: q in Ib;
reconsider q as Element of V by A9;
set LI=Lin(-q+Ib);
A10: card Ib=card(-q+Ib) by Th7;
-q+Ib c=the carrier of LI
proof
let x be object;
assume x in -q+Ib;
then x in LI by RLVECT_3:15;
hence thesis;
end;
then reconsider qI=-q+Ib as finite Subset of LI by A7,A10;
-q+q=0.V by RLVECT_1:5;
then A11: 0.V in qI by A9;
then A12: Lin(-q+Ib)=Lin(((-q+Ib)\{0.V})\/{0.V}) by ZFMISC_1:116
.=Lin(-q+Ib\{0.V}) by Lm9
.=Lin(qI\{0.V}) by RLVECT_5:20;
A13: -q+Ib\{0.V} is linearly-independent by A9,Th41;
then qI\{0.V} is linearly-independent by RLVECT_5:15;
then qI\{0.V} is Basis of LI by A12,RLVECT_3:def 3;
then reconsider LI as finite-dimensional Subspace of V by RLVECT_5:def 1;
A14: Ib c=Affin Ib by Lm7;
then A15: Affin Ib=q+Up LI by A9,Th57;
A16: Affin A=p+Up LA by A3,A4,Th57;
-p+A c=the carrier of LI
proof
let x be object;
A17: 2+-1=1;
2*q+(-1)*p=(1+1)*q+(-1)*p .=1*q+1*q+(-1)*p by RLVECT_1:def 6
.=1*q+1*q+-p by RLVECT_1:16
.=1*q+q+-p by RLVECT_1:def 8
.=q+q+-p by RLVECT_1:def 8
.=q+q-p by RLVECT_1:def 11
.=(q-p)+q by RLVECT_1:28;
then q+Up LI=q+LI & (q-p)+q in q+Up LI by A2,A8,A5,A9,A14,A15,A17,Th78,
RUSUB_4:30;
then A18: q-p in LI by RLSUB_1:61;
assume x in -p+A;
then A19: x in LA by RLVECT_3:15;
then x in V by RLSUB_1:9;
then reconsider w=x as Element of V;
w in Up LA by A19;
then p+w in Affin A by A16;
then p+w in q+Up LI by A2,A8,A15;
then consider u be Element of V such that
A20: p+w=q+u and
A21: u in Up LI;
A22: w=q+u-p by A20,RLVECT_4:1
.=q+(u-p) by RLVECT_1:28
.=u-(p-q) by RLVECT_1:29
.=u+-(p-q) by RLVECT_1:def 11
.=u+(q+-p) by RLVECT_1:33
.=u+(q-p) by RLVECT_1:def 11;
u in LI by A21;
then w in LI by A18,A22,RLSUB_1:20;
hence thesis;
end;
then reconsider LA as Subspace of LI by RLVECT_5:19;
-p+A c=the carrier of LA
proof
let x be object;
assume x in -p+A;
then x in LA by RLVECT_3:15;
hence thesis;
end;
then reconsider pA=-p+A as finite Subset of LA by A6;
-p+p=0.V by RLVECT_1:5;
then A23: 0.V in pA by A3;
then A24: {0.V}c=pA by ZFMISC_1:31;
A25: -p+A\{0.V} is linearly-independent by A1,A3,Th41;
A26: card{0.V}=1 by CARD_1:30;
A27: {0.V}c=qI by A11,ZFMISC_1:31;
A28: dim LI=card(qI\{0.V}) by A13,A12,RLVECT_5:15,29
.=card qI-1 by A27,A26,CARD_2:44;
Lin(-p+A)=Lin(((-p+A)\{0.V})\/{0.V}) by A23,ZFMISC_1:116
.=Lin(-p+A\{0.V}) by Lm9
.=Lin(pA\{0.V}) by RLVECT_5:20;
then dim LA=card(pA\{0.V}) by A25,RLVECT_5:15,29
.=card A-1 by A6,A26,A24,CARD_2:44;
then card A-1<=card qI-1 by A28,RLVECT_5:28;
then A29: card A<=card qI by XREAL_1:9;
card qI<=card B by A7,A10,NAT_1:43;
hence thesis by A29,XXREAL_0:2;
end;
end;
theorem
for A,B be finite Subset of V st
A is affinely-independent & Affin A c= Affin B & card A = card B
holds B is affinely-independent
proof
let A,B be finite Subset of V such that
A1: A is affinely-independent & Affin A c=Affin B & card A=card B;
{}V c=B;
then consider Ib be affinely-independent Subset of V such that
{}V c=Ib and
A2: Ib c=B and
A3: Affin Ib=Affin B by Th60;
reconsider IB=Ib as finite Subset of V by A2;
A4: card IB<=card B by A3,Th79;
card B<=card IB by A1,A3,Th79;
hence thesis by A2,A4,CARD_2:102,XXREAL_0:1;
end;
theorem
L1.v <> L2.v implies ((r*L1+(1-r)*L2).v = s iff r = (L2.v-s)/(L2.v-L1.v))
proof
set u1=L1.v,u2=L2.v;
A1: (r*L1+(1-r)*L2).v=(r*L1).v+((1-r)*L2).v by RLVECT_2:def 10
.=r*u1+((1-r)*L2).v by RLVECT_2:def 11
.=r*u1+(-r+1)*u2 by RLVECT_2:def 11
.=r*(u1-u2)+u2;
assume A2: u1<>u2;
then A3: u1-u2<>0;
A4: u2-u1<>0 by A2;
hereby assume(r*L1+(1-r)*L2).v=s;
then r*(u2-u1)=(u2-s)*1 by A1;
then r/1=(u2-s)/(u2-u1) by A4,XCMPLX_1:94;
hence r=(u2-s)/(u2-u1);
end;
assume r=(u2-s)/(u2-u1);
hence (r*L1+(1-r)*L2).v=(u2-s)/(-(u1-u2))*(u1-u2)+u2 by A1
.=(-(u2-s))/(u1-u2)*(u1-u2)+u2 by XCMPLX_1:192
.=-(u2-s)+u2 by A3,XCMPLX_1:87
.=s;
end;
theorem
A\/{v} is affinely-independent iff
A is affinely-independent & (v in A or not v in Affin A)
proof
set Av=A\/{v};
v in {v} by TARSKI:def 1;
then A1: v in Av by XBOOLE_0:def 3;
A2: A c=Av by XBOOLE_1:7;
hereby assume A3: Av is affinely-independent;
hence A is affinely-independent by Th43,XBOOLE_1:7;
v in Affin A implies v in A
proof
assume v in Affin A;
then {v}c=Affin A by ZFMISC_1:31;
then Affin Av=Affin A by Th69;
hence thesis by A2,A1,A3,Th58;
end;
hence v in A or not v in Affin A;
end;
assume that
A4: A is affinely-independent and
A5: v in A or not v in Affin A;
per cases by A5;
suppose v in A;
hence thesis by A4,ZFMISC_1:40;
end;
suppose A6: not v in Affin A & not v in A;
consider I be affinely-independent Subset of V such that
A7: A c=I and
A8: I c=Av and
A9: Affin I=Affin Av by A2,A4,Th60;
assume A10: not Av is affinely-independent;
not v in I
proof
assume v in I;
then {v}c=I by ZFMISC_1:31;
hence contradiction by A7,A10,Th43,XBOOLE_1:8;
end;
then A11: I c=Av\{v} by A8,ZFMISC_1:34;
A12: Av c=Affin Av by Lm7;
Av\{v}=A by A6,ZFMISC_1:117;
then I=A by A7,A11;
hence contradiction by A1,A6,A9,A12;
end;
end;
theorem
not w in Affin A & v1 in A & v2 in A & r<>1 & r*w + (1-r)*v1 = s*w + (1-s)*v2
implies r = s & v1 = v2
proof
assume that
A1: (not w in Affin A) & v1 in A & v2 in A and
A2: r<>1 and
A3: r*w+(1-r)*v1=s*w+(1-s)*v2;
r*w=r*w+0.V
.=r*w+((1-r)*v1-(1-r)*v1) by RLVECT_1:15
.=(s*w+(1-s)*v2)-(1-r)*v1 by A3,RLVECT_1:28
.=((1-s)*v2-(1-r)*v1)+s*w by RLVECT_1:28;
then r*w-s*w=(1-s)*v2-(1-r)*v1 by RLVECT_4:1;
then A4: (r-s)*w=(1-s)*v2-(1-r)*v1 by RLVECT_1:35;
A5: A c=Affin A by Lm7;
per cases;
suppose r<>s;
then A6: r-s<>0;
A7: 1/(r-s)*(1-s)=(r-s-(r-1))/(r-s) by XCMPLX_1:99
.=(r-s)/(r-s)-(r-1)/(r-s) by XCMPLX_1:120
.=1-(r-1)/(r-s) by A6,XCMPLX_1:60;
A8: -(1/(r-s)*(1-r))=-((1-r)/(r-s)) by XCMPLX_1:99
.=(-(1-r))/(r-s) by XCMPLX_1:187;
1=(r-s)*(1/(r-s)) by A6,XCMPLX_1:106;
then w=(1/(r-s)*(r-s))*w by RLVECT_1:def 8
.=1/(r-s)*((r-s)*w) by RLVECT_1:def 7
.=1/(r-s)*((1-s)*v2)-1/(r-s)*((1-r)*v1) by A4,RLVECT_1:34
.=(1/(r-s)*(1-s))*v2-1/(r-s)*((1-r)*v1) by RLVECT_1:def 7
.=(1/(r-s)*(1-s))*v2-(1/(r-s)*(1-r))*v1 by RLVECT_1:def 7
.=(1/(r-s)*(1-s))*v2+-(1/(r-s)*(1-r))*v1 by RLVECT_1:def 11
.=(1-(r-1)/(r-s))*v2+((r-1)/(r-s))*v1 by A7,A8,RLVECT_4:3;
hence thesis by A1,A5,RUSUB_4:def 4;
end;
suppose A9: r=s;
A10: 1-r<>0 by A2;
(1-r)*v1=(1-r)*v2 by A3,A9,RLVECT_1:8;
hence thesis by A9,A10,RLVECT_1:36;
end;
end;
theorem
v in I & w in Affin I & p in Affin(I\{v}) & w = r*v + (1-r)*p
implies r = (w|--I).v
proof
assume that
A1: v in I and
w in Affin I and
A2: p in Affin(I\{v}) and
A3: w=r*v+(1-r)*p;
A4: I c=conv I by CONVEX1:41;
Carrier(p|--(I\{v}))c=I\{v} by RLVECT_2:def 6;
then not v in Carrier(p|--(I\{v})) by ZFMISC_1:56;
then A5: (p|--(I\{v})).v=0;
I\{v}c=I by XBOOLE_1:36;
then Affin(I\{v})c=Affin I & I c=Affin I by Lm7,Th52;
hence (w|--I).v=((1-r)*(p|--I)+r*(v|--I)).v by A1,A2,A3,Th70
.=((1-r)*(p|--I)).v+(r*(v|--I)).v by RLVECT_2:def 10
.=((1-r)*(p|--I)).v+r*((v|--I).v) by RLVECT_2:def 11
.=(1-r)*((p|--I).v)+r*((v|--I).v) by RLVECT_2:def 11
.=(1-r)*((p|--I).v)+r*1 by A1,A4,Th72
.=(1-r)*((p|--(I\{v})).v)+r*1 by A2,Th77,XBOOLE_1:36
.=r by A5;
end;