:: CIRCLED1 semantic presentation begin Lm1: for V being non empty RLSStruct for M, N being Subset of V for x, y being VECTOR of V st x in M & y in N holds x - y in M - N proof let V be non empty RLSStruct ; ::_thesis: for M, N being Subset of V for x, y being VECTOR of V st x in M & y in N holds x - y in M - N let M, N be Subset of V; ::_thesis: for x, y being VECTOR of V st x in M & y in N holds x - y in M - N let x, y be VECTOR of V; ::_thesis: ( x in M & y in N implies x - y in M - N ) M - N = { (u - v) where u, v is VECTOR of V : ( u in M & v in N ) } by RUSUB_5:def_2; hence ( x in M & y in N implies x - y in M - N ) ; ::_thesis: verum end; theorem Th1: :: CIRCLED1:1 for V being RealLinearSpace for A, B being circled Subset of V holds A - B is circled proof let V be RealLinearSpace; ::_thesis: for A, B being circled Subset of V holds A - B is circled let A, B be circled Subset of V; ::_thesis: A - B is circled A1: A - B = { (u - v) where u, v is VECTOR of V : ( u in A & v in B ) } by RUSUB_5:def_2; let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( not abs r <= 1 or r * (A - B) c= A - B ) assume abs r <= 1 ; ::_thesis: r * (A - B) c= A - B then A2: ( r * A c= A & r * B c= B ) by RLTOPSP1:def_6; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (A - B) or x in A - B ) assume A3: x in r * (A - B) ; ::_thesis: x in A - B r * (A - B) = { (r * v) where v is VECTOR of V : v in A - B } by CONVEX1:def_1; then consider x9 being VECTOR of V such that A4: x = r * x9 and A5: x9 in A - B by A3; consider u, v being VECTOR of V such that A6: x9 = u - v and A7: ( u in A & v in B ) by A1, A5; A8: ( r * u in r * A & r * v in r * B ) by A7, RLTOPSP1:1; x = (r * u) - (r * v) by A4, A6, RLVECT_1:34; hence x in A - B by A2, A8, Lm1; ::_thesis: verum end; registration let V be RealLinearSpace; let M, N be circled Subset of V; clusterM - N -> circled ; coherence M - N is circled by Th1; end; definition let V be non empty RLSStruct ; let M be Subset of V; redefine attr M is circled means :Def1: :: CIRCLED1:def 1 for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M; compatibility ( M is circled iff for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M ) proof thus ( M is circled implies for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M ) ::_thesis: ( ( for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M ) implies M is circled ) proof assume A1: M is circled ; ::_thesis: for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M let u be VECTOR of V; ::_thesis: for r being Real st abs r <= 1 & u in M holds r * u in M let r be Real; ::_thesis: ( abs r <= 1 & u in M implies r * u in M ) assume abs r <= 1 ; ::_thesis: ( not u in M or r * u in M ) then A2: r * M c= M by A1, RLTOPSP1:def_6; assume u in M ; ::_thesis: r * u in M then r * u in r * M by RLTOPSP1:1; hence r * u in M by A2; ::_thesis: verum end; assume A3: for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M ; ::_thesis: M is circled let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( not abs r <= 1 or r * M c= M ) assume A4: abs r <= 1 ; ::_thesis: r * M c= M for x being Element of V st x in r * M holds x in M proof let x be Element of V; ::_thesis: ( x in r * M implies x in M ) assume x in r * M ; ::_thesis: x in M then consider u being Element of V such that A5: x = u and A6: u in r * M ; u in { (r * w) where w is Element of V : w in M } by A6, CONVEX1:def_1; then ex w1 being Element of V st ( u = r * w1 & w1 in M ) ; hence x in M by A3, A4, A5; ::_thesis: verum end; hence r * M c= M by SUBSET_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines circled CIRCLED1:def_1_:_ for V being non empty RLSStruct for M being Subset of V holds ( M is circled iff for u being VECTOR of V for r being Real st abs r <= 1 & u in M holds r * u in M ); theorem Th2: :: CIRCLED1:2 for V being RealLinearSpace for M being Subset of V for r being Real st M is circled holds r * M is circled proof let V be RealLinearSpace; ::_thesis: for M being Subset of V for r being Real st M is circled holds r * M is circled let M be Subset of V; ::_thesis: for r being Real st M is circled holds r * M is circled let r be Real; ::_thesis: ( M is circled implies r * M is circled ) assume A1: M is circled ; ::_thesis: r * M is circled for u being VECTOR of V for p being Real st abs p <= 1 & u in r * M holds p * u in r * M proof let u be VECTOR of V; ::_thesis: for p being Real st abs p <= 1 & u in r * M holds p * u in r * M let p be Real; ::_thesis: ( abs p <= 1 & u in r * M implies p * u in r * M ) assume that A2: abs p <= 1 and A3: u in r * M ; ::_thesis: p * u in r * M u in { (r * w) where w is Element of V : w in M } by A3, CONVEX1:def_1; then consider u9 being Element of V such that A4: u = r * u9 and A5: u9 in M ; A6: p * u = (r * p) * u9 by A4, RLVECT_1:def_7 .= r * (p * u9) by RLVECT_1:def_7 ; p * u9 in M by A1, A2, A5, Def1; hence p * u in r * M by A6, RLTOPSP1:1; ::_thesis: verum end; hence r * M is circled by Def1; ::_thesis: verum end; theorem Th3: :: CIRCLED1:3 for V being RealLinearSpace for M1, M2 being Subset of V for r1, r2 being Real st M1 is circled & M2 is circled holds (r1 * M1) + (r2 * M2) is circled proof let V be RealLinearSpace; ::_thesis: for M1, M2 being Subset of V for r1, r2 being Real st M1 is circled & M2 is circled holds (r1 * M1) + (r2 * M2) is circled let M1, M2 be Subset of V; ::_thesis: for r1, r2 being Real st M1 is circled & M2 is circled holds (r1 * M1) + (r2 * M2) is circled let r1, r2 be Real; ::_thesis: ( M1 is circled & M2 is circled implies (r1 * M1) + (r2 * M2) is circled ) assume that A1: M1 is circled and A2: M2 is circled ; ::_thesis: (r1 * M1) + (r2 * M2) is circled let u be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & u in (r1 * M1) + (r2 * M2) holds r * u in (r1 * M1) + (r2 * M2) let p be Real; ::_thesis: ( abs p <= 1 & u in (r1 * M1) + (r2 * M2) implies p * u in (r1 * M1) + (r2 * M2) ) assume that A3: abs p <= 1 and A4: u in (r1 * M1) + (r2 * M2) ; ::_thesis: p * u in (r1 * M1) + (r2 * M2) u in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A4, RUSUB_4:def_9; then consider u1, u2 being VECTOR of V such that A5: u = u1 + u2 and A6: u1 in r1 * M1 and A7: u2 in r2 * M2 ; u1 in { (r1 * x) where x is VECTOR of V : x in M1 } by A6, CONVEX1:def_1; then consider x1 being VECTOR of V such that A8: u1 = r1 * x1 and A9: x1 in M1 ; A10: p * u1 = (r1 * p) * x1 by A8, RLVECT_1:def_7 .= r1 * (p * x1) by RLVECT_1:def_7 ; u2 in { (r2 * x) where x is VECTOR of V : x in M2 } by A7, CONVEX1:def_1; then consider x2 being VECTOR of V such that A11: u2 = r2 * x2 and A12: x2 in M2 ; A13: p * u2 = (r2 * p) * x2 by A11, RLVECT_1:def_7 .= r2 * (p * x2) by RLVECT_1:def_7 ; p * x2 in M2 by A2, A3, A12, Def1; then A14: p * u2 in r2 * M2 by A13, RLTOPSP1:1; p * x1 in M1 by A1, A3, A9, Def1; then A15: p * u1 in r1 * M1 by A10, RLTOPSP1:1; p * (u1 + u2) = (p * u1) + (p * u2) by RLVECT_1:def_5; then p * (u1 + u2) in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A15, A14; hence p * u in (r1 * M1) + (r2 * M2) by A5, RUSUB_4:def_9; ::_thesis: verum end; theorem :: CIRCLED1:4 for V being RealLinearSpace for M1, M2, M3 being Subset of V for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled proof let V be RealLinearSpace; ::_thesis: for M1, M2, M3 being Subset of V for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled let M1, M2, M3 be Subset of V; ::_thesis: for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled let r1, r2, r3 be Real; ::_thesis: ( M1 is circled & M2 is circled & M3 is circled implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled ) assume that A1: ( M1 is circled & M2 is circled ) and A2: M3 is circled ; ::_thesis: ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled (r1 * M1) + (r2 * M2) is circled by A1, Th3; then (1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3) is circled by A2, Th3; hence ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled by CONVEX1:32; ::_thesis: verum end; theorem :: CIRCLED1:5 for V being RealLinearSpace holds Up ((0). V) is circled proof let V be RealLinearSpace; ::_thesis: Up ((0). V) is circled let u be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & u in Up ((0). V) holds r * u in Up ((0). V) let r be Real; ::_thesis: ( abs r <= 1 & u in Up ((0). V) implies r * u in Up ((0). V) ) assume that abs r <= 1 and A1: u in Up ((0). V) ; ::_thesis: r * u in Up ((0). V) u in the carrier of ((0). V) by A1, RUSUB_4:def_5; then u in {(0. V)} by RLSUB_1:def_3; then u = 0. V by TARSKI:def_1; then r * u = 0. V by RLVECT_1:10; then r * u in {(0. V)} by TARSKI:def_1; then r * u in the carrier of ((0). V) by RLSUB_1:def_3; hence r * u in Up ((0). V) by RUSUB_4:def_5; ::_thesis: verum end; theorem Th6: :: CIRCLED1:6 for V being RealLinearSpace holds Up ((Omega). V) is circled proof let V be RealLinearSpace; ::_thesis: Up ((Omega). V) is circled let u be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & u in Up ((Omega). V) holds r * u in Up ((Omega). V) let r be Real; ::_thesis: ( abs r <= 1 & u in Up ((Omega). V) implies r * u in Up ((Omega). V) ) (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) by RLSUB_1:def_4; then r * u in the carrier of ((Omega). V) ; hence ( abs r <= 1 & u in Up ((Omega). V) implies r * u in Up ((Omega). V) ) by RUSUB_4:def_5; ::_thesis: verum end; theorem :: CIRCLED1:7 for V being RealLinearSpace for M, N being circled Subset of V holds M /\ N is circled proof let V be RealLinearSpace; ::_thesis: for M, N being circled Subset of V holds M /\ N is circled let M, N be circled Subset of V; ::_thesis: M /\ N is circled let x be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & x in M /\ N holds r * x in M /\ N let r be Real; ::_thesis: ( abs r <= 1 & x in M /\ N implies r * x in M /\ N ) assume that A1: abs r <= 1 and A2: x in M /\ N ; ::_thesis: r * x in M /\ N x in N by A2, XBOOLE_0:def_4; then A3: r * x in N by A1, Def1; x in M by A2, XBOOLE_0:def_4; then r * x in M by A1, Def1; hence r * x in M /\ N by A3, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: CIRCLED1:8 for V being RealLinearSpace for M, N being circled Subset of V holds M \/ N is circled proof let V be RealLinearSpace; ::_thesis: for M, N being circled Subset of V holds M \/ N is circled let M, N be circled Subset of V; ::_thesis: M \/ N is circled let x be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & x in M \/ N holds r * x in M \/ N let r be Real; ::_thesis: ( abs r <= 1 & x in M \/ N implies r * x in M \/ N ) assume that A1: abs r <= 1 and A2: x in M \/ N ; ::_thesis: r * x in M \/ N ( x in M or x in N ) by A2, XBOOLE_0:def_3; then ( r * x in M or r * x in N ) by A1, Def1; hence r * x in M \/ N by XBOOLE_0:def_3; ::_thesis: verum end; begin definition let V be non empty RLSStruct ; let M be Subset of V; func Circled-Family M -> Subset-Family of V means :Def2: :: CIRCLED1:def 2 for N being Subset of V holds ( N in it iff ( N is circled & M c= N ) ); existence ex b1 being Subset-Family of V st for N being Subset of V holds ( N in b1 iff ( N is circled & M c= N ) ) proof defpred S1[ Subset of V] means ( \$1 is circled & M c= \$1 ); thus ex F being Subset-Family of V st for N being Subset of V holds ( N in F iff S1[N] ) from SUBSET_1:sch_3(); ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of V st ( for N being Subset of V holds ( N in b1 iff ( N is circled & M c= N ) ) ) & ( for N being Subset of V holds ( N in b2 iff ( N is circled & M c= N ) ) ) holds b1 = b2 proof let SF, SG be Subset-Family of V; ::_thesis: ( ( for N being Subset of V holds ( N in SF iff ( N is circled & M c= N ) ) ) & ( for N being Subset of V holds ( N in SG iff ( N is circled & M c= N ) ) ) implies SF = SG ) assume that A1: for N being Subset of V holds ( N in SF iff ( N is circled & M c= N ) ) and A2: for N being Subset of V holds ( N in SG iff ( N is circled & M c= N ) ) ; ::_thesis: SF = SG for Y being Subset of V holds ( Y in SF iff Y in SG ) proof let Y be Subset of V; ::_thesis: ( Y in SF iff Y in SG ) hereby ::_thesis: ( Y in SG implies Y in SF ) assume Y in SF ; ::_thesis: Y in SG then ( Y is circled & M c= Y ) by A1; hence Y in SG by A2; ::_thesis: verum end; assume Y in SG ; ::_thesis: Y in SF then ( Y is circled & M c= Y ) by A2; hence Y in SF by A1; ::_thesis: verum end; hence SF = SG by SETFAM_1:31; ::_thesis: verum end; end; :: deftheorem Def2 defines Circled-Family CIRCLED1:def_2_:_ for V being non empty RLSStruct for M being Subset of V for b3 being Subset-Family of V holds ( b3 = Circled-Family M iff for N being Subset of V holds ( N in b3 iff ( N is circled & M c= N ) ) ); definition let V be RealLinearSpace; let M be Subset of V; func Cir M -> circled Subset of V equals :: CIRCLED1:def 3 meet (Circled-Family M); coherence meet (Circled-Family M) is circled Subset of V proof for N being Subset of V st N in Circled-Family M holds N is circled by Def2; then Circled-Family M is circled-membered by RLTOPSP1:def_7; hence meet (Circled-Family M) is circled Subset of V by RLTOPSP1:30; ::_thesis: verum end; end; :: deftheorem defines Cir CIRCLED1:def_3_:_ for V being RealLinearSpace for M being Subset of V holds Cir M = meet (Circled-Family M); registration let V be RealLinearSpace; let M be Subset of V; cluster Circled-Family M -> non empty ; coherence not Circled-Family M is empty proof A1: M c= Up ((Omega). V) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in M or u in Up ((Omega). V) ) assume u in M ; ::_thesis: u in Up ((Omega). V) then reconsider u = u as Element of V ; u in the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) ; then u in the carrier of ((Omega). V) by RLSUB_1:def_4; hence u in Up ((Omega). V) by RUSUB_4:def_5; ::_thesis: verum end; Up ((Omega). V) is circled by Th6; hence not Circled-Family M is empty by A1, Def2; ::_thesis: verum end; end; theorem Th9: :: CIRCLED1:9 for V being RealLinearSpace for M1, M2 being Subset of V st M1 c= M2 holds Circled-Family M2 c= Circled-Family M1 proof let V be RealLinearSpace; ::_thesis: for M1, M2 being Subset of V st M1 c= M2 holds Circled-Family M2 c= Circled-Family M1 let M1, M2 be Subset of V; ::_thesis: ( M1 c= M2 implies Circled-Family M2 c= Circled-Family M1 ) assume A1: M1 c= M2 ; ::_thesis: Circled-Family M2 c= Circled-Family M1 let M be set ; :: according to TARSKI:def_3 ::_thesis: ( not M in Circled-Family M2 or M in Circled-Family M1 ) assume A2: M in Circled-Family M2 ; ::_thesis: M in Circled-Family M1 then reconsider M = M as Subset of V ; M2 c= M by A2, Def2; then A3: M1 c= M by A1, XBOOLE_1:1; M is circled by A2, Def2; hence M in Circled-Family M1 by A3, Def2; ::_thesis: verum end; theorem :: CIRCLED1:10 for V being RealLinearSpace for M1, M2 being Subset of V st M1 c= M2 holds Cir M1 c= Cir M2 proof let V be RealLinearSpace; ::_thesis: for M1, M2 being Subset of V st M1 c= M2 holds Cir M1 c= Cir M2 let M1, M2 be Subset of V; ::_thesis: ( M1 c= M2 implies Cir M1 c= Cir M2 ) assume M1 c= M2 ; ::_thesis: Cir M1 c= Cir M2 then Circled-Family M2 c= Circled-Family M1 by Th9; then A1: meet (Circled-Family M1) c= meet (Circled-Family M2) by SETFAM_1:6; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cir M1 or x in Cir M2 ) assume x in Cir M1 ; ::_thesis: x in Cir M2 hence x in Cir M2 by A1; ::_thesis: verum end; theorem Th11: :: CIRCLED1:11 for V being RealLinearSpace for M being Subset of V holds M c= Cir M proof let V be RealLinearSpace; ::_thesis: for M being Subset of V holds M c= Cir M let M be Subset of V; ::_thesis: M c= Cir M let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in M or u in Cir M ) assume A1: u in M ; ::_thesis: u in Cir M for Y being set st Y in Circled-Family M holds u in Y proof let Y be set ; ::_thesis: ( Y in Circled-Family M implies u in Y ) assume A2: Y in Circled-Family M ; ::_thesis: u in Y then reconsider Y = Y as Subset of V ; M c= Y by A2, Def2; hence u in Y by A1; ::_thesis: verum end; hence u in Cir M by SETFAM_1:def_1; ::_thesis: verum end; theorem Th12: :: CIRCLED1:12 for V being RealLinearSpace for M being Subset of V for N being circled Subset of V st M c= N holds Cir M c= N proof let V be RealLinearSpace; ::_thesis: for M being Subset of V for N being circled Subset of V st M c= N holds Cir M c= N let M be Subset of V; ::_thesis: for N being circled Subset of V st M c= N holds Cir M c= N let N be circled Subset of V; ::_thesis: ( M c= N implies Cir M c= N ) assume M c= N ; ::_thesis: Cir M c= N then N in Circled-Family M by Def2; hence Cir M c= N by SETFAM_1:3; ::_thesis: verum end; theorem :: CIRCLED1:13 for V being RealLinearSpace for M being circled Subset of V holds Cir M = M proof let V be RealLinearSpace; ::_thesis: for M being circled Subset of V holds Cir M = M let M be circled Subset of V; ::_thesis: Cir M = M thus Cir M c= M by Th12; :: according to XBOOLE_0:def_10 ::_thesis: M c= Cir M thus M c= Cir M by Th11; ::_thesis: verum end; theorem Th14: :: CIRCLED1:14 for V being RealLinearSpace holds Cir ({} V) = {} proof let V be RealLinearSpace; ::_thesis: Cir ({} V) = {} {} V in Circled-Family ({} V) by Def2; hence Cir ({} V) = {} by SETFAM_1:4; ::_thesis: verum end; theorem :: CIRCLED1:15 for V being RealLinearSpace for M being Subset of V for r being Real holds r * (Cir M) = Cir (r * M) proof let V be RealLinearSpace; ::_thesis: for M being Subset of V for r being Real holds r * (Cir M) = Cir (r * M) let M be Subset of V; ::_thesis: for r being Real holds r * (Cir M) = Cir (r * M) let r be Real; ::_thesis: r * (Cir M) = Cir (r * M) thus r * (Cir M) c= Cir (r * M) :: according to XBOOLE_0:def_10 ::_thesis: Cir (r * M) c= r * (Cir M) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) ) percases ( r = 0 or r <> 0 ) ; supposeA1: r = 0 ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) ) percases ( M = {} or M <> {} ) ; suppose M = {} ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) ) then M = {} V ; then Cir M = {} by Th14; hence ( not x in r * (Cir M) or x in Cir (r * M) ) by CONVEX1:33; ::_thesis: verum end; supposeA2: M <> {} ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) ) then r * M = {(0. V)} by A1, CONVEX1:34; then A3: {(0. V)} c= Cir (r * M) by Th11; Cir M <> {} by A2, Th11, XBOOLE_1:3; then r * (Cir M) = {(0. V)} by A1, CONVEX1:34; hence ( not x in r * (Cir M) or x in Cir (r * M) ) by A3; ::_thesis: verum end; end; end; supposeA4: r <> 0 ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) ) A5: r * (Cir M) = { (r * v) where v is Point of V : v in Cir M } by CONVEX1:def_1; assume x in r * (Cir M) ; ::_thesis: x in Cir (r * M) then consider v being Point of V such that A6: x = r * v and A7: v in Cir M by A5; for W being set st W in Circled-Family (r * M) holds r * v in W proof let W be set ; ::_thesis: ( W in Circled-Family (r * M) implies r * v in W ) assume A8: W in Circled-Family (r * M) ; ::_thesis: r * v in W then reconsider W = W as Subset of V ; r * M c= W by A8, Def2; then (r ") * (r * M) c= (r ") * W by CONVEX1:39; then ((r ") * r) * M c= (r ") * W by CONVEX1:37; then 1 * M c= (r ") * W by A4, XCMPLX_0:def_7; then A9: M c= (r ") * W by CONVEX1:32; W is circled by A8, Def2; then (r ") * W is circled by Th2; then (r ") * W in Circled-Family M by A9, Def2; then ( (r ") * W = { ((r ") * w) where w is Point of V : w in W } & v in (r ") * W ) by A7, CONVEX1:def_1, SETFAM_1:def_1; then consider w being Point of V such that A10: v = (r ") * w and A11: w in W ; r * v = (r * (r ")) * w by A10, RLVECT_1:def_7 .= 1 * w by A4, XCMPLX_0:def_7 .= w by RLVECT_1:def_8 ; hence r * v in W by A11; ::_thesis: verum end; hence x in Cir (r * M) by A6, SETFAM_1:def_1; ::_thesis: verum end; end; end; ( r * M c= r * (Cir M) & r * (Cir M) is circled ) by Th2, Th11, CONVEX1:39; hence Cir (r * M) c= r * (Cir M) by Th12; ::_thesis: verum end; begin definition let V be RealLinearSpace; let L be Linear_Combination of V; attrL is circled means :Def4: :: CIRCLED1:def 4 ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) ); end; :: deftheorem Def4 defines circled CIRCLED1:def_4_:_ for V being RealLinearSpace for L being Linear_Combination of V holds ( L is circled iff ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) ) ); theorem Th16: :: CIRCLED1:16 for V being RealLinearSpace for L being Linear_Combination of V st L is circled holds Carrier L <> {} proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is circled holds Carrier L <> {} let L be Linear_Combination of V; ::_thesis: ( L is circled implies Carrier L <> {} ) assume that A1: L is circled and A2: Carrier L = {} ; ::_thesis: contradiction consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = Carrier L ) and A4: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4; consider f being FinSequence of REAL such that A5: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A4; len F = 0 by A2, A3, CARD_1:27, FINSEQ_4:62; then f = <*> the carrier of V by A5; hence contradiction by A5, RVSUM_1:72; ::_thesis: verum end; theorem Th17: :: CIRCLED1:17 for V being RealLinearSpace for L being Linear_Combination of V for v being VECTOR of V st L is circled & L . v <= 0 holds not v in Carrier L proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for v being VECTOR of V st L is circled & L . v <= 0 holds not v in Carrier L let L be Linear_Combination of V; ::_thesis: for v being VECTOR of V st L is circled & L . v <= 0 holds not v in Carrier L let v be VECTOR of V; ::_thesis: ( L is circled & L . v <= 0 implies not v in Carrier L ) assume that A1: L is circled and A2: L . v <= 0 ; ::_thesis: not v in Carrier L percases ( L . v = 0 or L . v < 0 ) by A2; suppose L . v = 0 ; ::_thesis: not v in Carrier L hence not v in Carrier L by RLVECT_2:19; ::_thesis: verum end; supposeA3: L . v < 0 ; ::_thesis: not v in Carrier L now__::_thesis:_not_v_in_Carrier_L consider F being FinSequence of the carrier of V such that F is one-to-one and A4: rng F = Carrier L and A5: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4; assume v in Carrier L ; ::_thesis: contradiction then consider n being set such that A6: n in dom F and A7: F . n = v by A4, FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; consider f being FinSequence of REAL such that A8: len f = len F and Sum f = 1 and A9: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A5; n in Seg (len F) by A6, FINSEQ_1:def_3; then A10: n in dom f by A8, FINSEQ_1:def_3; then L . v = f . n by A9, A7; hence contradiction by A3, A9, A10; ::_thesis: verum end; hence not v in Carrier L ; ::_thesis: verum end; end; end; theorem :: CIRCLED1:18 for V being RealLinearSpace for L being Linear_Combination of V st L is circled holds L <> ZeroLC V proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is circled holds L <> ZeroLC V let L be Linear_Combination of V; ::_thesis: ( L is circled implies L <> ZeroLC V ) assume that A1: L is circled and A2: L = ZeroLC V ; ::_thesis: contradiction Carrier L <> {} by A1, Th16; hence contradiction by A2, RLVECT_2:def_5; ::_thesis: verum end; registration let V be RealLinearSpace; clusterV10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() circled for Linear_Combination of V; existence ex b1 being Linear_Combination of V st b1 is circled proof set u = the Element of V; consider L being Linear_Combination of { the Element of V} such that A1: L . the Element of V = 1 by RLVECT_4:37; take L ; ::_thesis: L is circled L is circled proof take <* the Element of V*> ; :: according to CIRCLED1:def_4 ::_thesis: ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex f being FinSequence of REAL st ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) ) A2: ex f being FinSequence of REAL st ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) proof reconsider f = <*1*> as FinSequence of REAL ; take f ; ::_thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) A3: for n being Nat st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) assume n in dom f ; ::_thesis: ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) then n in {1} by FINSEQ_1:2, FINSEQ_1:38; then A4: n = 1 by TARSKI:def_1; then f . n = L . the Element of V by A1, FINSEQ_1:40 .= L . (<* the Element of V*> . n) by A4, FINSEQ_1:40 ; hence ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) by A4, FINSEQ_1:40; ::_thesis: verum end; len <*1*> = 1 by FINSEQ_1:39 .= len <* the Element of V*> by FINSEQ_1:39 ; hence ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) by A3, FINSOP_1:11; ::_thesis: verum end; the Element of V in { w where w is Element of V : L . w <> 0 } by A1; then the Element of V in Carrier L by RLVECT_2:def_4; then ( Carrier L c= { the Element of V} & { the Element of V} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31; then Carrier L = { the Element of V} by XBOOLE_0:def_10; hence ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex f being FinSequence of REAL st ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) ) by A2, FINSEQ_1:38, FINSEQ_3:93; ::_thesis: verum end; hence L is circled ; ::_thesis: verum end; end; definition let V be RealLinearSpace; mode circled_Combination of V is circled Linear_Combination of V; end; registration let V be RealLinearSpace; let M be non empty Subset of V; clusterV10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() circled for Linear_Combination of M; existence ex b1 being Linear_Combination of M st b1 is circled proof consider u being set such that A1: u in M by XBOOLE_0:def_1; reconsider u = u as Element of V by A1; consider L being Linear_Combination of {u} such that A2: L . u = 1 by RLVECT_4:37; {u} c= M by A1, ZFMISC_1:31; then reconsider L = L as Linear_Combination of M by RLVECT_2:21; take L ; ::_thesis: L is circled L is circled proof take <*u*> ; :: according to CIRCLED1:def_4 ::_thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) A3: ex f being FinSequence of REAL st ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) proof reconsider f = <*1*> as FinSequence of REAL ; take f ; ::_thesis: ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) A4: for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) assume n in dom f ; ::_thesis: ( f . n = L . (<*u*> . n) & f . n >= 0 ) then n in {1} by FINSEQ_1:2, FINSEQ_1:38; then A5: n = 1 by TARSKI:def_1; then f . n = 1 by FINSEQ_1:40; hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A2, A5, FINSEQ_1:40; ::_thesis: verum end; len <*1*> = 1 by FINSEQ_1:39 .= len <*u*> by FINSEQ_1:39 ; hence ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) by A4, FINSOP_1:11; ::_thesis: verum end; u in { w where w is Element of V : L . w <> 0 } by A2; then u in Carrier L by RLVECT_2:def_4; then ( Carrier L c= {u} & {u} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31; then Carrier L = {u} by XBOOLE_0:def_10; hence ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A3, FINSEQ_1:38, FINSEQ_3:93; ::_thesis: verum end; hence L is circled ; ::_thesis: verum end; end; definition let V be RealLinearSpace; let M be non empty Subset of V; mode circled_Combination of M is circled Linear_Combination of M; end; definition let V be RealLinearSpace; defpred S1[ set ] means \$1 is circled_Combination of V; func circledComb V -> set means :: CIRCLED1:def 5 for L being set holds ( L in it iff L is circled_Combination of V ); existence ex b1 being set st for L being set holds ( L in b1 iff L is circled_Combination of V ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for L being set holds ( L in A iff L is circled_Combination of V ) let L be set ; ::_thesis: ( L in A iff L is circled_Combination of V ) thus ( L in A implies L is circled_Combination of V ) by A1; ::_thesis: ( L is circled_Combination of V implies L in A ) assume L is circled_Combination of V ; ::_thesis: L in A hence L in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for L being set holds ( L in b1 iff L is circled_Combination of V ) ) & ( for L being set holds ( L in b2 iff L is circled_Combination of V ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem defines circledComb CIRCLED1:def_5_:_ for V being RealLinearSpace for b2 being set holds ( b2 = circledComb V iff for L being set holds ( L in b2 iff L is circled_Combination of V ) ); definition let V be RealLinearSpace; let M be non empty Subset of V; defpred S1[ set ] means \$1 is circled_Combination of M; func circledComb M -> set means :: CIRCLED1:def 6 for L being set holds ( L in it iff L is circled_Combination of M ); existence ex b1 being set st for L being set holds ( L in b1 iff L is circled_Combination of M ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for L being set holds ( L in A iff L is circled_Combination of M ) let L be set ; ::_thesis: ( L in A iff L is circled_Combination of M ) thus ( L in A implies L is circled_Combination of M ) by A1; ::_thesis: ( L is circled_Combination of M implies L in A ) assume L is circled_Combination of M ; ::_thesis: L in A hence L in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for L being set holds ( L in b1 iff L is circled_Combination of M ) ) & ( for L being set holds ( L in b2 iff L is circled_Combination of M ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem defines circledComb CIRCLED1:def_6_:_ for V being RealLinearSpace for M being non empty Subset of V for b3 being set holds ( b3 = circledComb M iff for L being set holds ( L in b3 iff L is circled_Combination of M ) ); theorem :: CIRCLED1:19 for V being RealLinearSpace for v being VECTOR of V ex L being circled_Combination of V st ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is circled_Combination of A ) ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V ex L being circled_Combination of V st ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is circled_Combination of A ) ) let v be VECTOR of V; ::_thesis: ex L being circled_Combination of V st ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is circled_Combination of A ) ) consider L being Linear_Combination of {v} such that A1: L . v = 1 by RLVECT_4:37; consider F being FinSequence of the carrier of V such that A2: ( F is one-to-one & rng F = Carrier L ) and Sum L = Sum (L (#) F) by RLVECT_2:def_8; v in Carrier L by A1, RLVECT_2:19; then ( Carrier L c= {v} & {v} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31; then A3: {v} = Carrier L by XBOOLE_0:def_10; then F = <*v*> by A2, FINSEQ_3:97; then A4: F . 1 = v by FINSEQ_1:def_8; deffunc H1( set ) -> set = L . (F . \$1); consider f being FinSequence such that A5: ( len f = len F & ( for n being Nat st n in dom f holds f . n = H1(n) ) ) from FINSEQ_1:sch_2(); A6: len F = 1 by A3, A2, FINSEQ_3:96; then 1 in dom f by A5, FINSEQ_3:25; then A7: f . 1 = L . (F . 1) by A5; then f = <*1*> by A1, A5, A6, A4, FINSEQ_1:40; then reconsider f = f as FinSequence of REAL ; A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A9: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A1, A5, A6, A7, A4, A9, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; f = <*1*> by A1, A5, A6, A7, A4, FINSEQ_1:40; then Sum f = 1 by FINSOP_1:11; then reconsider L = L as circled_Combination of V by A2, A5, A8, Def4; A10: for A being non empty Subset of V st v in A holds L is circled_Combination of A proof let A be non empty Subset of V; ::_thesis: ( v in A implies L is circled_Combination of A ) assume v in A ; ::_thesis: L is circled_Combination of A then {v} c= A by ZFMISC_1:31; hence L is circled_Combination of A by A3, RLVECT_2:def_6; ::_thesis: verum end; take L ; ::_thesis: ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is circled_Combination of A ) ) Sum L = 1 * v by A1, A3, RLVECT_2:35; hence ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is circled_Combination of A ) ) by A10, RLVECT_1:def_8; ::_thesis: verum end; theorem :: CIRCLED1:20 for V being RealLinearSpace for v1, v2 being VECTOR of V st v1 <> v2 holds ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A ) assume A1: v1 <> v2 ; ::_thesis: ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A consider L being Linear_Combination of {v1,v2} such that A2: ( L . v1 = 1 / 2 & L . v2 = 1 / 2 ) by A1, RLVECT_4:38; consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = Carrier L ) and Sum L = Sum (L (#) F) by RLVECT_2:def_8; deffunc H1( set ) -> set = L . (F . \$1); consider f being FinSequence such that A4: ( len f = len F & ( for n being Nat st n in dom f holds f . n = H1(n) ) ) from FINSEQ_1:sch_2(); ( v1 in Carrier L & v2 in Carrier L ) by A2, RLVECT_2:19; then ( Carrier L c= {v1,v2} & {v1,v2} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:32; then A5: {v1,v2} = Carrier L by XBOOLE_0:def_10; then A6: len F = 2 by A1, A3, FINSEQ_3:98; then 2 in dom f by A4, FINSEQ_3:25; then A7: f . 2 = L . (F . 2) by A4; 1 in dom f by A4, A6, FINSEQ_3:25; then A8: f . 1 = L . (F . 1) by A4; now__::_thesis:_ex_L,_L_being_circled_Combination_of_V_st_ for_A_being_non_empty_Subset_of_V_st_{v1,v2}_c=_A_holds_ L_is_circled_Combination_of_A percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A5, A3, FINSEQ_3:99; suppose F = <*v1,v2*> ; ::_thesis: ex L, L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A then A9: ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44; then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44; then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9; then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31 .= {(1 / 2)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A10: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A11: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A9, A11, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum end; f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A9, FINSEQ_1:44; then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77 .= 1 ; then reconsider L = L as circled_Combination of V by A3, A4, A10, Def4; take L = L; ::_thesis: ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A by A5, RLVECT_2:def_6; hence ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A ; ::_thesis: verum end; suppose F = <*v2,v1*> ; ::_thesis: ex L, L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A then A12: ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44; then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44; then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9; then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31 .= {(1 / 2)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A13: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A14: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A12, A14, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum end; f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A12, FINSEQ_1:44; then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77 .= 1 ; then reconsider L = L as circled_Combination of V by A3, A4, A13, Def4; take L = L; ::_thesis: ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A by A5, RLVECT_2:def_6; hence ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A ; ::_thesis: verum end; end; end; hence ex L being circled_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is circled_Combination of A ; ::_thesis: verum end; theorem :: CIRCLED1:21 for V being RealLinearSpace for L1, L2 being circled_Combination of V for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) proof let V be RealLinearSpace; ::_thesis: for L1, L2 being circled_Combination of V for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) let L1, L2 be circled_Combination of V; ::_thesis: for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) let a, b be Real; ::_thesis: ( a * b > 0 implies Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) ) assume a * b > 0 ; ::_thesis: Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) then A1: ( not ( a >= 0 & b <= 0 ) & not ( a <= 0 & b >= 0 ) ) ; then A2: Carrier L2 = Carrier (b * L2) by RLVECT_2:42; A3: Carrier L1 = Carrier (a * L1) by A1, RLVECT_2:42; for x being set st x in (Carrier (a * L1)) \/ (Carrier (b * L2)) holds x in Carrier ((a * L1) + (b * L2)) proof let x be set ; ::_thesis: ( x in (Carrier (a * L1)) \/ (Carrier (b * L2)) implies x in Carrier ((a * L1) + (b * L2)) ) assume A4: x in (Carrier (a * L1)) \/ (Carrier (b * L2)) ; ::_thesis: x in Carrier ((a * L1) + (b * L2)) percases ( x in Carrier (a * L1) or x in Carrier (b * L2) ) by A4, XBOOLE_0:def_3; supposeA5: x in Carrier (a * L1) ; ::_thesis: x in Carrier ((a * L1) + (b * L2)) then x in { v where v is Element of V : (a * L1) . v <> 0 } by RLVECT_2:def_4; then consider v being Element of V such that A6: v = x and A7: (a * L1) . v <> 0 ; A8: L1 . v > 0 by A3, A5, A6, Th17; v in Carrier ((a * L1) + (b * L2)) proof percases ( v in Carrier L2 or not v in Carrier L2 ) ; supposeA9: v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then A10: L2 . v > 0 by Th17; percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1; supposeA11: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then b * (L2 . v) > 0 by A10, XREAL_1:129; then (b * L2) . v > 0 by RLVECT_2:def_11; then A12: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29; a * (L1 . v) > 0 by A8, A11, XREAL_1:129; then (a * L1) . v > 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v > 0 by A12, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; supposeA13: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then a * (L1 . v) < 0 by A3, A5, A6, Th17, XREAL_1:132; then (a * L1) . v < 0 by RLVECT_2:def_11; then A14: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30; b * (L2 . v) < 0 by A9, A13, Th17, XREAL_1:132; then (b * L2) . v < 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v < 0 by A14, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; suppose not v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then L2 . v = 0 by RLVECT_2:19; then b * (L2 . v) = 0 ; then (b * L2) . v = 0 by RLVECT_2:def_11; then ((a * L1) . v) + ((b * L2) . v) = (a * L1) . v ; then ((a * L1) + (b * L2)) . v <> 0 by A7, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; hence x in Carrier ((a * L1) + (b * L2)) by A6; ::_thesis: verum end; supposeA15: x in Carrier (b * L2) ; ::_thesis: x in Carrier ((a * L1) + (b * L2)) then x in { v where v is Element of V : (b * L2) . v <> 0 } by RLVECT_2:def_4; then consider v being Element of V such that A16: v = x and A17: (b * L2) . v <> 0 ; A18: L2 . v > 0 by A2, A15, A16, Th17; v in Carrier ((a * L1) + (b * L2)) proof percases ( v in Carrier L1 or not v in Carrier L1 ) ; supposeA19: v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then A20: L1 . v > 0 by Th17; percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1; supposeA21: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then b * (L2 . v) > 0 by A18, XREAL_1:129; then (b * L2) . v > 0 by RLVECT_2:def_11; then A22: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29; a * (L1 . v) > 0 by A20, A21, XREAL_1:129; then (a * L1) . v > 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v > 0 by A22, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; supposeA23: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then a * (L1 . v) < 0 by A19, Th17, XREAL_1:132; then (a * L1) . v < 0 by RLVECT_2:def_11; then A24: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30; b * (L2 . v) < 0 by A2, A15, A16, A23, Th17, XREAL_1:132; then (b * L2) . v < 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v < 0 by A24, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; suppose not v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then L1 . v = 0 by RLVECT_2:19; then a * (L1 . v) = 0 ; then (a * L1) . v = 0 by RLVECT_2:def_11; then ((a * L1) . v) + ((b * L2) . v) = (b * L2) . v ; then ((a * L1) + (b * L2)) . v <> 0 by A17, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; hence x in Carrier ((a * L1) + (b * L2)) by A16; ::_thesis: verum end; end; end; then A25: (Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2)) by TARSKI:def_3; Carrier ((a * L1) + (b * L2)) c= (Carrier (a * L1)) \/ (Carrier (b * L2)) by RLVECT_2:37; hence Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by A25, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th22: :: CIRCLED1:22 for V being RealLinearSpace for v being VECTOR of V for L being Linear_Combination of V st L is circled & Carrier L = {v} holds ( L . v = 1 & Sum L = (L . v) * v ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L being Linear_Combination of V st L is circled & Carrier L = {v} holds ( L . v = 1 & Sum L = (L . v) * v ) let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V st L is circled & Carrier L = {v} holds ( L . v = 1 & Sum L = (L . v) * v ) let L be Linear_Combination of V; ::_thesis: ( L is circled & Carrier L = {v} implies ( L . v = 1 & Sum L = (L . v) * v ) ) assume that A1: L is circled and A2: Carrier L = {v} ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v ) reconsider L = L as Linear_Combination of {v} by A2, RLVECT_2:def_6; consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = Carrier L ) and A4: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4; A5: F = <*v*> by A2, A3, FINSEQ_3:97; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A4; reconsider r = f /. 1 as Element of REAL ; card (Carrier L) = 1 by A2, CARD_1:30; then len F = 1 by A3, FINSEQ_4:62; then A9: dom f = Seg 1 by A6, FINSEQ_1:def_3; then A10: 1 in dom f by FINSEQ_1:2, TARSKI:def_1; then A11: f . 1 = f /. 1 by PARTFUN1:def_6; then f = <*r*> by A9, FINSEQ_1:def_8; then A12: Sum f = r by FINSOP_1:11; f . 1 = L . (F . 1) by A8, A10; hence ( L . v = 1 & Sum L = (L . v) * v ) by A7, A11, A12, A5, FINSEQ_1:def_8, RLVECT_2:32; ::_thesis: verum end; theorem Th23: :: CIRCLED1:23 for V being RealLinearSpace for v1, v2 being VECTOR of V for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) let v1, v2 be VECTOR of V; ::_thesis: for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) let L be Linear_Combination of V; ::_thesis: ( L is circled & Carrier L = {v1,v2} & v1 <> v2 implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) ) assume that A1: L is circled and A2: Carrier L = {v1,v2} and A3: v1 <> v2 ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) reconsider L = L as Linear_Combination of {v1,v2} by A2, RLVECT_2:def_6; consider F being FinSequence of the carrier of V such that A4: ( F is one-to-one & rng F = Carrier L ) and A5: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A5; len F = card {v1,v2} by A2, A4, FINSEQ_4:62; then A9: len f = 2 by A3, A6, CARD_2:57; then A10: dom f = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; then A11: 1 in dom f by TARSKI:def_2; then A12: f . 1 = L . (F . 1) by A8; then f /. 1 = L . (F . 1) by A11, PARTFUN1:def_6; then reconsider r1 = L . (F . 1) as Element of REAL ; A13: 2 in dom f by A10, TARSKI:def_2; then A14: f . 2 = L . (F . 2) by A8; then f /. 2 = L . (F . 2) by A13, PARTFUN1:def_6; then reconsider r2 = L . (F . 2) as Element of REAL ; A15: f = <*r1,r2*> by A9, A12, A14, FINSEQ_1:44; now__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_) percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:99; suppose F = <*v1,v2*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) then ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A7, A8, A11, A13, A12, A14, A15, RVSUM_1:77; ::_thesis: verum end; suppose F = <*v2,v1*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) then ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A7, A8, A11, A13, A12, A14, A15, RVSUM_1:77; ::_thesis: verum end; end; end; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A3, RLVECT_2:33; ::_thesis: verum end; theorem :: CIRCLED1:24 for V being RealLinearSpace for v being VECTOR of V for L being Linear_Combination of {v} st L is circled holds ( L . v = 1 & Sum L = (L . v) * v ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L being Linear_Combination of {v} st L is circled holds ( L . v = 1 & Sum L = (L . v) * v ) let v be VECTOR of V; ::_thesis: for L being Linear_Combination of {v} st L is circled holds ( L . v = 1 & Sum L = (L . v) * v ) let L be Linear_Combination of {v}; ::_thesis: ( L is circled implies ( L . v = 1 & Sum L = (L . v) * v ) ) Carrier L c= {v} by RLVECT_2:def_6; then A1: ( Carrier L = {} or Carrier L = {v} ) by ZFMISC_1:33; assume L is circled ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v ) hence ( L . v = 1 & Sum L = (L . v) * v ) by A1, Th16, Th22; ::_thesis: verum end; theorem :: CIRCLED1:25 for V being RealLinearSpace for v1, v2 being VECTOR of V for L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V for L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) let v1, v2 be VECTOR of V; ::_thesis: for L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) let L be Linear_Combination of {v1,v2}; ::_thesis: ( v1 <> v2 & L is circled implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) ) assume that A1: v1 <> v2 and A2: L is circled ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) A3: ( Carrier L c= {v1,v2} & Carrier L <> {} ) by A2, Th16, RLVECT_2:def_6; now__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_) percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v1,v2} ) by A3, ZFMISC_1:36; supposeA4: Carrier L = {v1} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) then not v2 in Carrier L by A1, TARSKI:def_1; then not v2 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def_4; then L . v2 = 0 ; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A2, A4, Th22; ::_thesis: verum end; supposeA5: Carrier L = {v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) then not v1 in Carrier L by A1, TARSKI:def_1; then not v1 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def_4; then L . v1 = 0 ; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A2, A5, Th22; ::_thesis: verum end; suppose Carrier L = {v1,v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A1, A2, Th23; ::_thesis: verum end; end; end; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A1, RLVECT_2:33; ::_thesis: verum end;