:: Affine Independence in Vector Spaces :: by Karol P\c{a}k :: :: Received December 18, 2009 :: Copyright (c) 2009-2016 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-unitalnon 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{}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 by RLVECT_1:17; 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 by RLVECT_1:17 .=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 c0.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,RLVECT_1:18; 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: 01-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)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;