:: RLAFFIN2 semantic presentation begin Lm1: for r being Real for V being RealLinearSpace for u, w, v being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) proof let r be Real; ::_thesis: for V being RealLinearSpace for u, w, v being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) let u, w, v be VECTOR of V; ::_thesis: ( r <> 1 & (r * u) + ((1 - r) * w) = v implies w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) ) assume that A1: r <> 1 and A2: (r * u) + ((1 - r) * w) = v ; ::_thesis: w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) A3: (1 - r) * w = v - (r * u) by A2, RLVECT_4:1; A4: 1 - r <> 1 - 1 by A1; then A5: (1 / (1 - r)) * (1 - r) = 1 by XCMPLX_1:106; A6: (1 / (1 - r)) * (r * u) = ((1 / (1 - r)) * r) * u by RLVECT_1:def_7 .= ((1 - (1 - r)) / (1 - r)) * u by XCMPLX_1:99 .= ((1 / (1 - r)) - ((1 - r) / (1 - r))) * u by XCMPLX_1:120 .= ((1 / (1 - r)) - 1) * u by A4, XCMPLX_1:60 ; thus w = 1 * w by RLVECT_1:def_8 .= (1 / (1 - r)) * ((1 - r) * w) by A5, RLVECT_1:def_7 .= ((1 / (1 - r)) * v) - ((1 / (1 - r)) * (r * u)) by A3, RLVECT_1:34 .= ((1 / (1 - r)) * v) + (- (((1 / (1 - r)) - 1) * u)) by A6, RLVECT_1:def_11 .= ((1 / (1 - r)) * v) + (((1 / (1 - r)) - 1) * (- u)) by RLVECT_1:25 .= ((1 / (1 - r)) * v) + ((- ((1 / (1 - r)) - 1)) * u) by RLVECT_1:24 .= ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) ; ::_thesis: verum end; theorem Th1: :: RLAFFIN2:1 for V being RealLinearSpace for v being VECTOR of V for A being Subset of V for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds ex p being VECTOR of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for A being Subset of V for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds ex p being VECTOR of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) let v be VECTOR of V; ::_thesis: for A being Subset of V for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds ex p being VECTOR of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) let A be Subset of V; ::_thesis: for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds ex p being VECTOR of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) let L be Linear_Combination of A; ::_thesis: ( L is convex & v <> Sum L & L . v <> 0 implies ex p being VECTOR of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) ) assume that A1: L is convex and A2: v <> Sum L and A3: L . v <> 0 ; ::_thesis: ex p being VECTOR of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) set Lv = L . v; set 1Lv = 1 - (L . v); A4: Carrier L c= A by RLVECT_2:def_6; Carrier L <> {} by A1, CONVEX1:21; then reconsider A1 = A as non empty Subset of V by A4; consider K being Linear_Combination of {v} such that A5: K . v = L . v by RLVECT_4:37; A6: L . v <> 1 proof assume A7: L . v = 1 ; ::_thesis: contradiction then Carrier L = {v} by A1, RLAFFIN1:64; then Sum L = 1 * v by A7, RLVECT_2:35 .= v by RLVECT_1:def_8 ; hence contradiction by A2; ::_thesis: verum end; L . v <= 1 by A1, RLAFFIN1:63; then L . v < 1 by A6, XXREAL_0:1; then A8: 1 - (L . v) > 1 - 1 by XREAL_1:10; v in Carrier L by A3; then {v} c= A1 by A4, ZFMISC_1:31; then K is Linear_Combination of A1 by RLVECT_2:21; then reconsider LK = L - K as Linear_Combination of A1 by RLVECT_2:56; (1 / (1 - (L . v))) * LK is Linear_Combination of A by RLVECT_2:44; then A9: Carrier ((1 / (1 - (L . v))) * LK) c= A1 by RLVECT_2:def_6; LK . v = (L . v) - (L . v) by A5, RLVECT_2:54; then A10: ((1 / (1 - (L . v))) * LK) . v = (1 / (1 - (L . v))) * ((L . v) - (L . v)) by RLVECT_2:def_11; then not v in Carrier ((1 / (1 - (L . v))) * LK) by RLVECT_2:19; then A11: Carrier ((1 / (1 - (L . v))) * LK) c= A \ {v} by A9, ZFMISC_1:34; A12: Carrier K c= {v} by RLVECT_2:def_6; A13: for w being Element of V holds ((1 / (1 - (L . v))) * LK) . w >= 0 proof let w be Element of V; ::_thesis: ((1 / (1 - (L . v))) * LK) . w >= 0 A14: ((1 / (1 - (L . v))) * LK) . w = (1 / (1 - (L . v))) * (LK . w) by RLVECT_2:def_11 .= (1 / (1 - (L . v))) * ((L . w) - (K . w)) by RLVECT_2:54 ; percases ( w = v or w <> v ) ; suppose w = v ; ::_thesis: ((1 / (1 - (L . v))) * LK) . w >= 0 hence ((1 / (1 - (L . v))) * LK) . w >= 0 by A10; ::_thesis: verum end; suppose w <> v ; ::_thesis: ((1 / (1 - (L . v))) * LK) . w >= 0 then not w in Carrier K by A12, TARSKI:def_1; then A15: K . w = 0 ; L . w >= 0 by A1, RLAFFIN1:62; hence ((1 / (1 - (L . v))) * LK) . w >= 0 by A8, A14, A15; ::_thesis: verum end; end; end; sum LK = (sum L) - (sum K) by RLAFFIN1:36 .= (sum L) - (L . v) by A5, A12, RLAFFIN1:32 .= 1 - (L . v) by A1, RLAFFIN1:62 ; then A16: sum ((1 / (1 - (L . v))) * LK) = (1 / (1 - (L . v))) * (1 - (L . v)) by RLAFFIN1:35 .= 1 by A8, XCMPLX_1:106 ; then (1 / (1 - (L . v))) * LK is convex by A13, RLAFFIN1:62; then Carrier ((1 / (1 - (L . v))) * LK) <> {} by CONVEX1:21; then reconsider Av = A \ {v} as non empty Subset of V by A11; reconsider 1LK = (1 / (1 - (L . v))) * LK as Convex_Combination of Av by A11, A13, A16, RLAFFIN1:62, RLVECT_2:def_6; take p = Sum 1LK; ::_thesis: ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) 1LK in ConvexComb V by CONVEX3:def_1; then p in { (Sum M) where M is Convex_Combination of Av : M in ConvexComb V } ; hence p in conv (A \ {v}) by CONVEX3:5; ::_thesis: ( Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) A17: Sum LK = (Sum L) - (Sum K) by RLVECT_3:4 .= (Sum L) - ((L . v) * v) by A5, RLVECT_2:32 ; then (1 - (L . v)) * p = (1 - (L . v)) * ((1 / (1 - (L . v))) * ((Sum L) - ((L . v) * v))) by RLVECT_3:2 .= ((1 - (L . v)) * (1 / (1 - (L . v)))) * ((Sum L) - ((L . v) * v)) by RLVECT_1:def_7 .= 1 * ((Sum L) - ((L . v) * v)) by A8, XCMPLX_1:106 .= (Sum L) - ((L . v) * v) by RLVECT_1:def_8 ; hence Sum L = ((L . v) * v) + ((1 - (L . v)) * p) by RLVECT_4:1; ::_thesis: ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v 1 - (1 / (L . v)) = ((L . v) / (L . v)) - (1 / (L . v)) by A3, XCMPLX_1:60 .= ((L . v) - 1) / (L . v) by XCMPLX_1:120 .= (- (1 - (L . v))) / (L . v) .= - ((1 - (L . v)) / (L . v)) by XCMPLX_1:187 ; then (1 - (1 / (L . v))) * (Sum 1LK) = (- ((1 - (L . v)) / (L . v))) * ((1 / (1 - (L . v))) * ((Sum L) - ((L . v) * v))) by A17, RLVECT_3:2 .= ((- ((1 - (L . v)) / (L . v))) * (1 / (1 - (L . v)))) * ((Sum L) - ((L . v) * v)) by RLVECT_1:def_7 .= (- (((1 - (L . v)) / (L . v)) * (1 / (1 - (L . v))))) * ((Sum L) - ((L . v) * v)) .= (- (((1 - (L . v)) / (1 - (L . v))) * (1 / (L . v)))) * ((Sum L) - ((L . v) * v)) by XCMPLX_1:85 .= (- (1 * (1 / (L . v)))) * ((Sum L) - ((L . v) * v)) by A8, XCMPLX_1:60 .= ((- (1 / (L . v))) * (Sum L)) - ((- (1 / (L . v))) * ((L . v) * v)) by RLVECT_1:34 .= ((- (1 / (L . v))) * (Sum L)) + (- ((- (1 / (L . v))) * ((L . v) * v))) by RLVECT_1:def_11 .= ((- (1 / (L . v))) * (Sum L)) + ((- (- (1 / (L . v)))) * ((L . v) * v)) by RLVECT_4:3 .= ((- (1 / (L . v))) * (Sum L)) + (((1 / (L . v)) * (L . v)) * v) by RLVECT_1:def_7 .= ((- (1 / (L . v))) * (Sum L)) + (1 * v) by A3, XCMPLX_1:106 .= ((- (1 / (L . v))) * (Sum L)) + v by RLVECT_1:def_8 .= (- ((1 / (L . v)) * (Sum L))) + v by RLVECT_4:3 ; hence ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = (((1 / (L . v)) * (Sum L)) + (- ((1 / (L . v)) * (Sum L)))) + v by RLVECT_1:def_3 .= (((1 / (L . v)) * (Sum L)) - ((1 / (L . v)) * (Sum L))) + v by RLVECT_1:def_11 .= v by RLVECT_4:1 ; ::_thesis: verum end; theorem :: RLAFFIN2:2 for r, s being Real for V being RealLinearSpace for v, u being VECTOR of V for I being affinely-independent Subset of V for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds ( w1 = w2 & r = s ) proof let r, s be Real; ::_thesis: for V being RealLinearSpace for v, u being VECTOR of V for I being affinely-independent Subset of V for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds ( w1 = w2 & r = s ) let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for I being affinely-independent Subset of V for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds ( w1 = w2 & r = s ) let v, u be VECTOR of V; ::_thesis: for I being affinely-independent Subset of V for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds ( w1 = w2 & r = s ) let I be affinely-independent Subset of V; ::_thesis: for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds ( w1 = w2 & r = s ) let p1, p2, w1, w2 be Element of V; ::_thesis: ( v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 implies ( w1 = w2 & r = s ) ) assume that A1: v in conv I and A2: u in conv I and A3: not u in conv (I \ {p1}) and A4: not u in conv (I \ {p2}) and A5: w1 in conv (I \ {p1}) and A6: w2 in conv (I \ {p2}) and A7: (r * u) + ((1 - r) * w1) = v and A8: (s * u) + ((1 - s) * w2) = v and A9: r < 1 and A10: s < 1 ; ::_thesis: ( w1 = w2 & r = s ) set Lu = u |-- I; set Lv = v |-- I; set Lw1 = w1 |-- I; set Lw2 = w2 |-- I; A11: conv I c= Affin I by RLAFFIN1:65; A12: (u |-- I) . p2 > 0 proof assume A13: (u |-- I) . p2 <= 0 ; ::_thesis: contradiction (u |-- I) . p2 >= 0 by A2, RLAFFIN1:71; then for y being set st y in {p2} holds (u |-- I) . y = 0 by A13, TARSKI:def_1; hence contradiction by A2, A4, RLAFFIN1:76; ::_thesis: verum end; conv (I \ {p2}) c= Affin (I \ {p2}) by RLAFFIN1:65; then w2 |-- I = w2 |-- (I \ {p2}) by A6, RLAFFIN1:77, XBOOLE_1:36; then Carrier (w2 |-- I) c= I \ {p2} by RLVECT_2:def_6; then not p2 in Carrier (w2 |-- I) by ZFMISC_1:56; then A14: (w2 |-- I) . p2 = 0 ; A15: (u |-- I) . p1 > 0 proof assume A16: (u |-- I) . p1 <= 0 ; ::_thesis: contradiction (u |-- I) . p1 >= 0 by A2, RLAFFIN1:71; then for y being set st y in {p1} holds (u |-- I) . y = 0 by A16, TARSKI:def_1; hence contradiction by A2, A3, RLAFFIN1:76; ::_thesis: verum end; conv (I \ {p1}) c= Affin (I \ {p1}) by RLAFFIN1:65; then w1 |-- I = w1 |-- (I \ {p1}) by A5, RLAFFIN1:77, XBOOLE_1:36; then Carrier (w1 |-- I) c= I \ {p1} by RLVECT_2:def_6; then not p1 in Carrier (w1 |-- I) by ZFMISC_1:56; then A17: (w1 |-- I) . p1 = 0 ; A18: conv (I \ {p2}) c= conv I by RLAFFIN1:3, XBOOLE_1:36; then w2 in conv I by A6; then (s * (u |-- I)) + ((1 - s) * (w2 |-- I)) = v |-- I by A2, A8, A11, RLAFFIN1:70; then (v |-- I) . p2 = ((s * (u |-- I)) . p2) + (((1 - s) * (w2 |-- I)) . p2) by RLVECT_2:def_10 .= (s * ((u |-- I) . p2)) + (((1 - s) * (w2 |-- I)) . p2) by RLVECT_2:def_11 .= (s * ((u |-- I) . p2)) + ((1 - s) * ((w2 |-- I) . p2)) by RLVECT_2:def_11 .= s * ((u |-- I) . p2) by A14 ; then A19: (v |-- I) . p2 < 1 * ((u |-- I) . p2) by A10, A12, XREAL_1:68; then A20: ((u |-- I) . p2) - ((v |-- I) . p2) >= ((v |-- I) . p2) - ((v |-- I) . p2) by XREAL_1:9; A21: conv (I \ {p1}) c= conv I by RLAFFIN1:3, XBOOLE_1:36; then (w1 |-- I) . p2 >= 0 by A5, RLAFFIN1:71; then A22: (1 / (1 - s)) - 0 >= (1 / (1 - s)) - (((w1 |-- I) . p2) / (((u |-- I) . p2) - ((v |-- I) . p2))) by A20, XREAL_1:10; w1 in conv I by A5, A21; then v |-- I = (r * (u |-- I)) + ((1 - r) * (w1 |-- I)) by A2, A7, A11, RLAFFIN1:70; then (v |-- I) . p1 = ((r * (u |-- I)) . p1) + (((1 - r) * (w1 |-- I)) . p1) by RLVECT_2:def_10 .= (r * ((u |-- I) . p1)) + (((1 - r) * (w1 |-- I)) . p1) by RLVECT_2:def_11 .= (r * ((u |-- I) . p1)) + ((1 - r) * ((w1 |-- I) . p1)) by RLVECT_2:def_11 .= r * ((u |-- I) . p1) by A17 ; then A23: (v |-- I) . p1 < 1 * ((u |-- I) . p1) by A9, A15, XREAL_1:68; then A24: ((u |-- I) . p1) - ((v |-- I) . p1) >= ((v |-- I) . p1) - ((v |-- I) . p1) by XREAL_1:9; w2 = ((1 / (1 - s)) * v) + ((1 - (1 / (1 - s))) * u) by A8, A10, Lm1; then A25: w2 |-- I = ((1 / (1 - s)) * (v |-- I)) + ((1 - (1 / (1 - s))) * (u |-- I)) by A1, A2, A11, RLAFFIN1:70; then A26: 1 / (1 - s) = (((u |-- I) . p2) - 0) / (((u |-- I) . p2) - ((v |-- I) . p2)) by A14, A19, RLAFFIN1:81; A27: w1 = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) by A7, A9, Lm1; then A28: w1 |-- I = ((1 / (1 - r)) * (v |-- I)) + ((1 - (1 / (1 - r))) * (u |-- I)) by A1, A2, A11, RLAFFIN1:70; then A29: 1 / (1 - r) = (((u |-- I) . p2) - ((w1 |-- I) . p2)) / (((u |-- I) . p2) - ((v |-- I) . p2)) by A19, RLAFFIN1:81 .= (1 / (1 - s)) - (((w1 |-- I) . p2) / (((u |-- I) . p2) - ((v |-- I) . p2))) by A26, XCMPLX_1:120 ; (w2 |-- I) . p1 >= 0 by A6, A18, RLAFFIN1:71; then A30: (1 / (1 - r)) - 0 >= (1 / (1 - r)) - (((w2 |-- I) . p1) / (((u |-- I) . p1) - ((v |-- I) . p1))) by A24, XREAL_1:10; A31: 1 / (1 - r) = (((u |-- I) . p1) - 0) / (((u |-- I) . p1) - ((v |-- I) . p1)) by A17, A23, A28, RLAFFIN1:81; 1 / (1 - s) = (((u |-- I) . p1) - ((w2 |-- I) . p1)) / (((u |-- I) . p1) - ((v |-- I) . p1)) by A23, A25, RLAFFIN1:81 .= (1 / (1 - r)) - (((w2 |-- I) . p1) / (((u |-- I) . p1) - ((v |-- I) . p1))) by A31, XCMPLX_1:120 ; then 1 - r = 1 - s by A30, A22, A29, XCMPLX_1:59, XXREAL_0:1; hence ( w1 = w2 & r = s ) by A8, A10, A27, Lm1; ::_thesis: verum end; theorem Th3: :: RLAFFIN2:3 for V being RealLinearSpace for Af being finite Subset of V for If being finite affinely-independent Subset of V for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) proof let V be RealLinearSpace; ::_thesis: for Af being finite Subset of V for If being finite affinely-independent Subset of V for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) let Af be finite Subset of V; ::_thesis: for If being finite affinely-independent Subset of V for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) let If be finite affinely-independent Subset of V; ::_thesis: for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) defpred S1[ Nat] means for B being finite Subset of V st card B = $1 & B c= conv If holds for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ); A1: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: S1[m] ; ::_thesis: S1[m + 1] let B be finite Subset of V; ::_thesis: ( card B = m + 1 & B c= conv If implies for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) ) assume that A3: card B = m + 1 and A4: B c= conv If ; ::_thesis: for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) conv If c= Affin If by RLAFFIN1:65; then A5: B c= Affin If by A4, XBOOLE_1:1; then A6: Affin B c= Affin If by RLAFFIN1:51; let L be Linear_Combination of B; ::_thesis: ( Carrier L = B & sum L = 1 implies ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) ) assume that A7: Carrier L = B and A8: sum L = 1 ; ::_thesis: ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) Sum L in { (Sum K) where K is Linear_Combination of B : sum K = 1 } by A8; then Sum L in Affin B by RLAFFIN1:59; hence Sum L in Affin If by A6; ::_thesis: for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) percases ( m = 0 or m > 0 ) ; supposeA9: m = 0 ; ::_thesis: for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) let x be Element of V; ::_thesis: ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) consider b being set such that A10: B = {b} by A3, A9, CARD_2:42; b in B by A10, TARSKI:def_1; then reconsider b = b as Element of V ; A11: sum L = L . b by A7, A10, RLAFFIN1:32; set F = <*((b |-- If) . x)*>; set G = <*b*>; take <*((b |-- If) . x)*> ; ::_thesis: ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len G = len <*((b |-- If) . x)*> & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds <*((b |-- If) . x)*> . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) take <*b*> ; ::_thesis: ( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len <*b*> = len <*((b |-- If) . x)*> & <*b*> is one-to-one & rng <*b*> = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) ) ) Sum L = (L . b) * b by A10, RLVECT_2:32; then ( len <*b*> = 1 & Sum L = b ) by A8, A11, FINSEQ_1:39, RLVECT_1:def_8; hence ( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len <*b*> = len <*((b |-- If) . x)*> & <*b*> is one-to-one & rng <*b*> = Carrier L ) by A7, A10, FINSEQ_1:39, FINSEQ_3:93, RVSUM_1:73; ::_thesis: for n being Nat st n in dom <*((b |-- If) . x)*> holds <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) let n be Nat; ::_thesis: ( n in dom <*((b |-- If) . x)*> implies <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) ) assume n in dom <*((b |-- If) . x)*> ; ::_thesis: <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) then n in Seg 1 by FINSEQ_1:38; then A12: n = 1 by FINSEQ_1:2, TARSKI:def_1; then <*b*> . n = b by FINSEQ_1:40; hence <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) by A8, A11, A12, FINSEQ_1:40; ::_thesis: verum end; supposeA13: m > 0 ; ::_thesis: for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ex v being Element of V st ( L . v <> 1 & v in Carrier L ) proof consider F being FinSequence of V such that A14: F is one-to-one and A15: rng F = Carrier L and A16: 1 = Sum (L * F) by A8, RLAFFIN1:def_3; dom F,B are_equipotent by A7, A14, A15, WELLORD2:def_4; then A17: card B = card (dom F) by CARD_1:5 .= card (Seg (len F)) by FINSEQ_1:def_3 .= len F by FINSEQ_1:57 ; A18: ( len F = len (L * F) & len ((len F) |-> 1) = len F ) by CARD_1:def_7, FINSEQ_2:33; Sum ((len F) |-> 1) = (len F) * 1 by RVSUM_1:80; then (len F) |-> 1 <> L * F by A3, A13, A16, A17; then consider k being Nat such that A19: ( 1 <= k & k <= len F ) and A20: ((len F) |-> 1) . k <> (L * F) . k by A18, FINSEQ_1:14; A21: k in Seg (len F) by A19, FINSEQ_1:1; A22: k in dom F by A19, FINSEQ_3:25; then A23: F . k in Carrier L by A15, FUNCT_1:def_3; L . (F . k) = (L * F) . k by A22, FUNCT_1:13; then L . (F . k) <> 1 by A20, A21, FINSEQ_2:57; hence ex v being Element of V st ( L . v <> 1 & v in Carrier L ) by A23; ::_thesis: verum end; then consider v being Element of V such that A24: L . v <> 1 and A25: v in Carrier L ; set 1Lv = 1 - (L . v); consider K being Linear_Combination of {v} such that A26: K . v = L . v by RLVECT_4:37; set LK = L - K; A27: 1 - (L . v) <> 0 by A24; set 1LK = (1 / (1 - (L . v))) * (L - K); A28: Carrier K c= {v} by RLVECT_2:def_6; then sum K = K . v by RLAFFIN1:32; then sum (L - K) = 1 - (L . v) by A8, A26, RLAFFIN1:36; then A29: sum ((1 / (1 - (L . v))) * (L - K)) = (1 / (1 - (L . v))) * (1 - (L . v)) by RLAFFIN1:35; (L - K) . v = (L . v) - (K . v) by RLVECT_2:54; then A30: not v in Carrier (L - K) by A26, RLVECT_2:19; A31: card (B \ {v}) = m by A3, A7, A25, STIRL2_1:55; A32: Sum K = (L . v) * v by A26, RLVECT_2:32; B \ {v} c= B by XBOOLE_1:36; then A33: B \ {v} c= conv If by A4, XBOOLE_1:1; L . v <> 0 by A25, RLVECT_2:19; then v in Carrier K by A26; then A34: Carrier K = {v} by A28, ZFMISC_1:33; A35: B \ {v} c= Carrier (L - K) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B \ {v} or x in Carrier (L - K) ) assume A36: x in B \ {v} ; ::_thesis: x in Carrier (L - K) then reconsider u = x as Element of V ; u in B by A36, ZFMISC_1:56; then A37: L . u <> 0 by A7, RLVECT_2:19; ( (L - K) . u = (L . u) - (K . u) & not u in {v} ) by A36, RLVECT_2:54, XBOOLE_0:def_5; then (L - K) . u <> 0 by A34, A37; hence x in Carrier (L - K) ; ::_thesis: verum end; let x be Element of V; ::_thesis: ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) A38: (1 / (1 - (L . v))) * (1 - (L . v)) = (1 * (1 - (L . v))) / (1 - (L . v)) by XCMPLX_1:74 .= 1 by A27, XCMPLX_1:60 ; Sum ((1 / (1 - (L . v))) * (L - K)) = (1 / (1 - (L . v))) * (Sum (L - K)) by RLVECT_3:2; then (1 - (L . v)) * (Sum ((1 / (1 - (L . v))) * (L - K))) = ((1 - (L . v)) * (1 / (1 - (L . v)))) * (Sum (L - K)) by RLVECT_1:def_7 .= Sum (L - K) by A38, RLVECT_1:def_8 ; then A39: ((1 - (L . v)) * (Sum ((1 / (1 - (L . v))) * (L - K)))) + ((L . v) * v) = ((Sum L) - ((L . v) * v)) + ((L . v) * v) by A32, RLVECT_3:4 .= Sum L by RLVECT_4:1 ; B \/ {v} = B by A7, A25, ZFMISC_1:40; then Carrier (L - K) c= B \ {v} by A7, A34, A30, RLVECT_2:55, ZFMISC_1:34; then B \ {v} = Carrier (L - K) by A35, XBOOLE_0:def_10; then A40: Carrier ((1 / (1 - (L . v))) * (L - K)) = B \ {v} by A27, RLVECT_2:42; then A41: (1 / (1 - (L . v))) * (L - K) is Linear_Combination of B \ {v} by RLVECT_2:def_6; then consider F being FinSequence of REAL , G being FinSequence of V such that A42: ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If) . x = Sum F and A43: len G = len F and A44: G is one-to-one and A45: rng G = Carrier ((1 / (1 - (L . v))) * (L - K)) and A46: for n being Nat st n in dom F holds F . n = (((1 / (1 - (L . v))) * (L - K)) . (G . n)) * (((G . n) |-- If) . x) by A2, A29, A38, A31, A33, A40; Sum ((1 / (1 - (L . v))) * (L - K)) in Affin If by A2, A29, A38, A31, A33, A40, A41; then A47: (Sum L) |-- If = ((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) + ((L . v) * (v |-- If)) by A5, A7, A25, A39, RLAFFIN1:70; take F1 = ((1 - (L . v)) * F) ^ <*((L . v) * ((v |-- If) . x))*>; ::_thesis: ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F1 & len G = len F1 & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F1 holds F1 . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) take G1 = G ^ <*v*>; ::_thesis: ( ((Sum L) |-- If) . x = Sum F1 & len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) ) thus Sum F1 = (Sum ((1 - (L . v)) * F)) + ((L . v) * ((v |-- If) . x)) by RVSUM_1:74 .= ((1 - (L . v)) * (((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If) . x)) + ((L . v) * ((v |-- If) . x)) by A42, RVSUM_1:87 .= (((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) . x) + ((L . v) * ((v |-- If) . x)) by RLVECT_2:def_11 .= (((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) . x) + (((L . v) * (v |-- If)) . x) by RLVECT_2:def_11 .= ((Sum L) |-- If) . x by A47, RLVECT_2:def_10 ; ::_thesis: ( len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) ) reconsider f = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92; A48: len F = len ((1 - (L . v)) * f) by CARD_1:def_7; then A49: len F1 = (len F) + 1 by FINSEQ_2:16; hence len F1 = len G1 by A43, FINSEQ_2:16; ::_thesis: ( G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) ) A50: rng <*v*> = {v} by FINSEQ_1:38; then ( <*v*> is one-to-one & rng G misses rng <*v*> ) by A40, A45, FINSEQ_3:93, XBOOLE_1:79; hence G1 is one-to-one by A44, FINSEQ_3:91; ::_thesis: ( rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) ) thus rng G1 = (B \ {v}) \/ {v} by A40, A45, A50, FINSEQ_1:31 .= Carrier L by A7, A25, ZFMISC_1:116 ; ::_thesis: for n being Nat st n in dom F1 holds F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) let n be Nat; ::_thesis: ( n in dom F1 implies F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) assume A51: n in dom F1 ; ::_thesis: F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) then A52: n <= len F1 by FINSEQ_3:25; percases ( ( 1 <= n & n <= len F ) or n = (len F) + 1 ) by A49, A51, A52, FINSEQ_3:25, NAT_1:8; supposeA53: ( 1 <= n & n <= len F ) ; ::_thesis: F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) then n in dom F by FINSEQ_3:25; then A54: ( ((1 - (L . v)) * f) . n = (1 - (L . v)) * (f . n) & F . n = (((1 / (1 - (L . v))) * (L - K)) . (G . n)) * (((G . n) |-- If) . x) ) by A46, RVSUM_1:45; A55: n in dom G by A43, A53, FINSEQ_3:25; then A56: G1 . n = G . n by FINSEQ_1:def_7; A57: G . n in B \ {v} by A40, A45, A55, FUNCT_1:def_3; then not G . n in {v} by XBOOLE_0:def_5; then K . (G . n) = 0 by A34, A57; then (L - K) . (G . n) = (L . (G . n)) - 0 by A57, RLVECT_2:54; then ((1 / (1 - (L . v))) * (L - K)) . (G . n) = (1 / (1 - (L . v))) * (L . (G . n)) by A57, RLVECT_2:def_11; then (1 - (L . v)) * (((1 / (1 - (L . v))) * (L - K)) . (G1 . n)) = ((1 - (L . v)) * (1 / (1 - (L . v)))) * (L . (G . n)) by A56; then A58: (1 - (L . v)) * (((1 / (1 - (L . v))) * (L - K)) . (G1 . n)) = L . (G . n) by A38; n in dom ((1 - (L . v)) * F) by A48, A53, FINSEQ_3:25; hence F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) by A54, A56, A58, FINSEQ_1:def_7; ::_thesis: verum end; supposeA59: n = (len F) + 1 ; ::_thesis: F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) then G1 . n = v by A43, FINSEQ_1:42; hence F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) by A48, A59, FINSEQ_1:42; ::_thesis: verum end; end; end; end; end; let L be Linear_Combination of Af; ::_thesis: ( Af c= conv If & sum L = 1 implies ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) ) assume that A60: Af c= conv If and A61: sum L = 1 ; ::_thesis: ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) set C = Carrier L; Carrier L c= Af by RLVECT_2:def_6; then A62: Carrier L c= conv If by A60, XBOOLE_1:1; reconsider L1 = L as Linear_Combination of Carrier L by RLVECT_2:def_6; A63: S1[ 0 ] proof let B be finite Subset of V; ::_thesis: ( card B = 0 & B c= conv If implies for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) ) assume that A64: card B = 0 and B c= conv If ; ::_thesis: for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) let L be Linear_Combination of B; ::_thesis: ( Carrier L = B & sum L = 1 implies ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) ) assume that Carrier L = B and A65: sum L = 1 ; ::_thesis: ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) B = {} the carrier of V by A64; then L = ZeroLC V by RLVECT_2:23; hence ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) by A65, RLAFFIN1:31; ::_thesis: verum end; for m being Nat holds S1[m] from NAT_1:sch_2(A63, A1); then ( sum L = sum L1 & S1[ card (Carrier L)] ) ; hence ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st ( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) by A61, A62; ::_thesis: verum end; theorem :: RLAFFIN2:4 for V being RealLinearSpace for v being VECTOR of V for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B) let v be VECTOR of V; ::_thesis: for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B) let A, B, Aff be Subset of V; ::_thesis: ( Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff implies (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B) ) assume that A1: Aff is Affine and A2: (conv A) /\ (conv B) c= Aff and A3: conv (A \ {v}) c= Aff and A4: not v in Aff ; ::_thesis: (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B) conv (A \ {v}) c= conv A by RLTOPSP1:20, XBOOLE_1:36; hence (conv (A \ {v})) /\ (conv B) c= (conv A) /\ (conv B) by XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: (conv A) /\ (conv B) c= (conv (A \ {v})) /\ (conv B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (conv A) /\ (conv B) or x in (conv (A \ {v})) /\ (conv B) ) assume A5: x in (conv A) /\ (conv B) ; ::_thesis: x in (conv (A \ {v})) /\ (conv B) then reconsider A1 = A as non empty Subset of V by XBOOLE_0:def_4; A6: x in Aff by A2, A5; ( conv A = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } & x in conv A ) by A5, CONVEX3:5, XBOOLE_0:def_4; then consider L being Convex_Combination of A1 such that A7: x = Sum L and L in ConvexComb V ; set Lv = L . v; A8: Carrier L c= A by RLVECT_2:def_6; A9: x in conv B by A5, XBOOLE_0:def_4; percases ( L . v = 0 or L . v <> 0 ) ; suppose L . v = 0 ; ::_thesis: x in (conv (A \ {v})) /\ (conv B) then not v in Carrier L by RLVECT_2:19; then A10: Carrier L c= A \ {v} by A8, ZFMISC_1:34; then reconsider K = L as Linear_Combination of A \ {v} by RLVECT_2:def_6; Carrier L <> {} by CONVEX1:21; then reconsider Av = A \ {v} as non empty Subset of V by A10; K in ConvexComb V by CONVEX3:def_1; then Sum K in { (Sum M) where M is Convex_Combination of Av : M in ConvexComb V } ; then x in conv Av by A7, CONVEX3:5; hence x in (conv (A \ {v})) /\ (conv B) by A9, XBOOLE_0:def_4; ::_thesis: verum end; suppose L . v <> 0 ; ::_thesis: x in (conv (A \ {v})) /\ (conv B) then ex p being Element of V st ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) by A4, A6, A7, Th1; hence x in (conv (A \ {v})) /\ (conv B) by A1, A2, A3, A4, A5, A7, RUSUB_4:def_4; ::_thesis: verum end; end; end; begin definition let V be non empty RLSStruct ; let A be Subset of V; func Int A -> Subset of V means :Def1: :: RLAFFIN2:def 1 for x being set holds ( x in it iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ); existence ex b1 being Subset of V st for x being set holds ( x in b1 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) proof set I = { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) } ; now__::_thesis:_for_x_being_set_st_x_in__{__x_where_x_is_Element_of_V_:_(_x_in_conv_A_&_(_for_B_being_Subset_of_V_holds_ (_not_B_c<_A_or_not_x_in_conv_B_)_)_)__}__holds_ x_in_the_carrier_of_V let x be set ; ::_thesis: ( x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) } implies x in the carrier of V ) assume x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) } ; ::_thesis: x in the carrier of V then ex y being Element of V st ( x = y & y in conv A & ( for B being Subset of V holds ( not B c< A or not y in conv B ) ) ) ; hence x in the carrier of V ; ::_thesis: verum end; then reconsider I = { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) } as Subset of V by TARSKI:def_3; take I ; ::_thesis: for x being set holds ( x in I iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) let x be set ; ::_thesis: ( x in I iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) hereby ::_thesis: ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) implies x in I ) assume x in I ; ::_thesis: ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) then ex y being Element of V st ( x = y & y in conv A & ( for B being Subset of V holds ( not B c< A or not y in conv B ) ) ) ; hence ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ; ::_thesis: verum end; assume ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ; ::_thesis: x in I hence x in I ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of V st ( for x being set holds ( x in b1 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) ) holds b1 = b2 proof let I1, I2 be Subset of V; ::_thesis: ( ( for x being set holds ( x in I1 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) ) & ( for x being set holds ( x in I2 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) ) implies I1 = I2 ) assume that A1: for x being set holds ( x in I1 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) and A2: for x being set holds ( x in I2 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) ; ::_thesis: I1 = I2 now__::_thesis:_for_x_being_set_holds_ (_x_in_I1_iff_x_in_I2_) let x be set ; ::_thesis: ( x in I1 iff x in I2 ) ( x in I1 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) by A1; hence ( x in I1 iff x in I2 ) by A2; ::_thesis: verum end; hence I1 = I2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines Int RLAFFIN2:def_1_:_ for V being non empty RLSStruct for A, b3 being Subset of V holds ( b3 = Int A iff for x being set holds ( x in b3 iff ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) ) ); Lm2: for V being non empty RLSStruct for A being Subset of V holds Int A c= conv A proof let V be non empty RLSStruct ; ::_thesis: for A being Subset of V holds Int A c= conv A let A be Subset of V; ::_thesis: Int A c= conv A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int A or x in conv A ) assume x in Int A ; ::_thesis: x in conv A hence x in conv A by Def1; ::_thesis: verum end; registration let V be non empty RLSStruct ; let A be empty Subset of V; cluster Int A -> empty ; coherence Int A is empty proof Int A c= conv A by Lm2; hence Int A is empty ; ::_thesis: verum end; end; theorem :: RLAFFIN2:5 for V being non empty RLSStruct for A being Subset of V holds Int A c= conv A by Lm2; theorem :: RLAFFIN2:6 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for A being Subset of V holds ( Int A = A iff A is trivial ) proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for A being Subset of V holds ( Int A = A iff A is trivial ) let A be Subset of V; ::_thesis: ( Int A = A iff A is trivial ) percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: ( Int A = A iff A is trivial ) hence ( Int A = A iff A is trivial ) ; ::_thesis: verum end; supposeA1: not A is empty ; ::_thesis: ( Int A = A iff A is trivial ) hereby ::_thesis: ( A is trivial implies Int A = A ) assume A2: Int A = A ; ::_thesis: A is trivial now__::_thesis:_for_x,_y_being_set_st_x_in_A_&_y_in_A_holds_ x_=_y let x, y be set ; ::_thesis: ( x in A & y in A implies x = y ) assume that A3: x in A and A4: y in A ; ::_thesis: x = y ( A \ {x} c= A & A \ {x} <> A ) by A3, XBOOLE_1:36, ZFMISC_1:56; then ( A \ {x} c= conv (A \ {x}) & A \ {x} c< A ) by RLAFFIN1:2, XBOOLE_0:def_8; then not y in A \ {x} by A2, A4, Def1; hence x = y by A4, ZFMISC_1:56; ::_thesis: verum end; hence A is trivial by ZFMISC_1:def_10; ::_thesis: verum end; assume A is trivial ; ::_thesis: Int A = A then consider v being Element of V such that A5: A = {v} by A1, SUBSET_1:47; A6: for B being Subset of V holds ( not B c< A or not v in conv B ) proof let B be Subset of V; ::_thesis: ( not B c< A or not v in conv B ) assume A7: B c< A ; ::_thesis: not v in conv B then B c= A by XBOOLE_0:def_8; then B is empty by A5, A7, ZFMISC_1:33; hence not v in conv B ; ::_thesis: verum end; A8: conv A = A by A5, RLAFFIN1:1; then A9: Int A c= A by Lm2; v in A by A5, TARSKI:def_1; then v in Int A by A6, A8, Def1; hence Int A = A by A5, A9, ZFMISC_1:33; ::_thesis: verum end; end; end; theorem :: RLAFFIN2:7 for V being RealLinearSpace for A, B being Subset of V st A c< B holds conv A misses Int B proof let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st A c< B holds conv A misses Int B let A, B be Subset of V; ::_thesis: ( A c< B implies conv A misses Int B ) assume A1: A c< B ; ::_thesis: conv A misses Int B assume conv A meets Int B ; ::_thesis: contradiction then ex x being set st ( x in conv A & x in Int B ) by XBOOLE_0:3; hence contradiction by A1, Def1; ::_thesis: verum end; theorem Th8: :: RLAFFIN2:8 for V being RealLinearSpace for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A } proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A } let A be Subset of V; ::_thesis: conv A = union { (Int B) where B is Subset of V : B c= A } defpred S1[ Nat] means for S being finite Subset of V st card S <= $1 holds conv S = union { (Int B) where B is Subset of V : B c= S } ; set I = { (Int B) where B is Subset of V : B c= A } ; A1: for A being Subset of V holds union { (Int B) where B is Subset of V : B c= A } c= conv A proof let A be Subset of V; ::_thesis: union { (Int B) where B is Subset of V : B c= A } c= conv A set I = { (Int B) where B is Subset of V : B c= A } ; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union { (Int B) where B is Subset of V : B c= A } or y in conv A ) assume y in union { (Int B) where B is Subset of V : B c= A } ; ::_thesis: y in conv A then consider x being set such that A2: y in x and A3: x in { (Int B) where B is Subset of V : B c= A } by TARSKI:def_4; consider B being Subset of V such that A4: x = Int B and A5: B c= A by A3; A6: conv B c= conv A by A5, RLAFFIN1:3; y in conv B by A2, A4, Def1; hence y in conv A by A6; ::_thesis: verum end; A7: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A8: S1[n] ; ::_thesis: S1[n + 1] let S be finite Subset of V; ::_thesis: ( card S <= n + 1 implies conv S = union { (Int B) where B is Subset of V : B c= S } ) assume A9: card S <= n + 1 ; ::_thesis: conv S = union { (Int B) where B is Subset of V : B c= S } percases ( card S <= n or card S = n + 1 ) by A9, NAT_1:8; suppose card S <= n ; ::_thesis: conv S = union { (Int B) where B is Subset of V : B c= S } hence conv S = union { (Int B) where B is Subset of V : B c= S } by A8; ::_thesis: verum end; supposeA10: card S = n + 1 ; ::_thesis: conv S = union { (Int B) where B is Subset of V : B c= S } set I = { (Int B) where B is Subset of V : B c= S } ; A11: conv S c= union { (Int B) where B is Subset of V : B c= S } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in conv S or x in union { (Int B) where B is Subset of V : B c= S } ) assume A12: x in conv S ; ::_thesis: x in union { (Int B) where B is Subset of V : B c= S } percases ( for A being Subset of V st A c< S holds not x in conv A or ex A being Subset of V st ( A c< S & x in conv A ) ) ; suppose for A being Subset of V st A c< S holds not x in conv A ; ::_thesis: x in union { (Int B) where B is Subset of V : B c= S } then ( Int S in { (Int B) where B is Subset of V : B c= S } & x in Int S ) by A12, Def1; hence x in union { (Int B) where B is Subset of V : B c= S } by TARSKI:def_4; ::_thesis: verum end; suppose ex A being Subset of V st ( A c< S & x in conv A ) ; ::_thesis: x in union { (Int B) where B is Subset of V : B c= S } then consider A being Subset of V such that A13: A c< S and A14: x in conv A ; A15: A c= S by A13, XBOOLE_0:def_8; then reconsider A = A as finite Subset of V ; card A < n + 1 by A10, A13, CARD_2:48; then card A <= n by NAT_1:13; then conv A = union { (Int B) where B is Subset of V : B c= A } by A8; then consider Y being set such that A16: x in Y and A17: Y in { (Int B) where B is Subset of V : B c= A } by A14, TARSKI:def_4; consider B being Subset of V such that A18: Y = Int B and A19: B c= A by A17; B c= S by A15, A19, XBOOLE_1:1; then Int B in { (Int B) where B is Subset of V : B c= S } ; hence x in union { (Int B) where B is Subset of V : B c= S } by A16, A18, TARSKI:def_4; ::_thesis: verum end; end; end; union { (Int B) where B is Subset of V : B c= S } c= conv S by A1; hence conv S = union { (Int B) where B is Subset of V : B c= S } by A11, XBOOLE_0:def_10; ::_thesis: verum end; end; end; A20: S1[ 0 ] proof let A be finite Subset of V; ::_thesis: ( card A <= 0 implies conv A = union { (Int B) where B is Subset of V : B c= A } ) set I = { (Int B) where B is Subset of V : B c= A } ; assume card A <= 0 ; ::_thesis: conv A = union { (Int B) where B is Subset of V : B c= A } then A is empty ; then A21: conv A is empty ; union { (Int B) where B is Subset of V : B c= A } c= conv A by A1; hence conv A = union { (Int B) where B is Subset of V : B c= A } by A21; ::_thesis: verum end; A22: for n being Nat holds S1[n] from NAT_1:sch_2(A20, A7); hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (Int B) where B is Subset of V : B c= A } c= conv A let x be set ; ::_thesis: ( x in conv A implies x in union { (Int B) where B is Subset of V : B c= A } ) assume A23: x in conv A ; ::_thesis: x in union { (Int B) where B is Subset of V : B c= A } reconsider A1 = A as non empty Subset of V by A23; conv A = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5; then consider L being Convex_Combination of A1 such that A24: ( x = Sum L & L in ConvexComb V ) by A23; reconsider C = Carrier L as non empty finite Subset of V by CONVEX1:21; reconsider K = L as Linear_Combination of C by RLVECT_2:def_6; K is convex ; then x in { (Sum M) where M is Convex_Combination of C : M in ConvexComb V } by A24; then A25: x in conv C by CONVEX3:5; S1[ card C] by A22; then x in union { (Int B) where B is Subset of V : B c= C } by A25; then consider y being set such that A26: x in y and A27: y in { (Int B) where B is Subset of V : B c= C } by TARSKI:def_4; consider B being Subset of V such that A28: y = Int B and A29: B c= C by A27; C c= A by RLVECT_2:def_6; then B c= A by A29, XBOOLE_1:1; then Int B in { (Int B) where B is Subset of V : B c= A } ; hence x in union { (Int B) where B is Subset of V : B c= A } by A26, A28, TARSKI:def_4; ::_thesis: verum end; thus union { (Int B) where B is Subset of V : B c= A } c= conv A by A1; ::_thesis: verum end; theorem :: RLAFFIN2:9 for V being RealLinearSpace for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) let A be Subset of V; ::_thesis: conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) set I = { (conv (A \ {v})) where v is VECTOR of V : v in A } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) c= conv A let x be set ; ::_thesis: ( x in conv A implies b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 in A } ) ) assume x in conv A ; ::_thesis: b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 in A } ) then x in union { (Int B) where B is Subset of V : B c= A } by Th8; then consider y being set such that A1: x in y and A2: y in { (Int B) where B is Subset of V : B c= A } by TARSKI:def_4; consider B being Subset of V such that A3: y = Int B and A4: B c= A by A2; percases ( A = B or B <> A ) ; suppose A = B ; ::_thesis: b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 in A } ) hence x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by A1, A3, XBOOLE_0:def_3; ::_thesis: verum end; suppose B <> A ; ::_thesis: b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 in A } ) then B c< A by A4, XBOOLE_0:def_8; then consider y being set such that A5: y in A and A6: not y in B by XBOOLE_0:6; reconsider y = y as Element of V by A5; A7: conv (A \ {y}) in { (conv (A \ {v})) where v is VECTOR of V : v in A } by A5; B c= A \ {y} by A4, A6, ZFMISC_1:34; then A8: conv B c= conv (A \ {y}) by RLAFFIN1:3; x in conv B by A1, A3, Def1; then x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } by A7, A8, TARSKI:def_4; hence x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) or x in conv A ) A9: now__::_thesis:_(_x_in_union__{__(conv_(A_\_{v}))_where_v_is_VECTOR_of_V_:_v_in_A__}__implies_x_in_conv_A_) assume x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } ; ::_thesis: x in conv A then consider y being set such that A10: x in y and A11: y in { (conv (A \ {v})) where v is VECTOR of V : v in A } by TARSKI:def_4; consider v being VECTOR of V such that A12: y = conv (A \ {v}) and v in A by A11; conv (A \ {v}) c= conv A by RLAFFIN1:3, XBOOLE_1:36; hence x in conv A by A10, A12; ::_thesis: verum end; assume x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) ; ::_thesis: x in conv A then A13: ( x in Int A or x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by XBOOLE_0:def_3; Int A c= conv A by Lm2; hence x in conv A by A9, A13; ::_thesis: verum end; theorem Th10: :: RLAFFIN2:10 for x being set for V being RealLinearSpace for A being Subset of V st x in Int A holds ex L being Linear_Combination of A st ( L is convex & x = Sum L ) proof let x be set ; ::_thesis: for V being RealLinearSpace for A being Subset of V st x in Int A holds ex L being Linear_Combination of A st ( L is convex & x = Sum L ) let V be RealLinearSpace; ::_thesis: for A being Subset of V st x in Int A holds ex L being Linear_Combination of A st ( L is convex & x = Sum L ) let A be Subset of V; ::_thesis: ( x in Int A implies ex L being Linear_Combination of A st ( L is convex & x = Sum L ) ) assume A1: x in Int A ; ::_thesis: ex L being Linear_Combination of A st ( L is convex & x = Sum L ) then reconsider A1 = A as non empty Subset of V ; x in conv A by A1, Def1; then x in { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5; then ex L being Convex_Combination of A1 st ( x = Sum L & L in ConvexComb V ) ; hence ex L being Linear_Combination of A st ( L is convex & x = Sum L ) ; ::_thesis: verum end; theorem Th11: :: RLAFFIN2:11 for V being RealLinearSpace for A being Subset of V for L being Linear_Combination of A st L is convex & Sum L in Int A holds Carrier L = A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for L being Linear_Combination of A st L is convex & Sum L in Int A holds Carrier L = A let A be Subset of V; ::_thesis: for L being Linear_Combination of A st L is convex & Sum L in Int A holds Carrier L = A let L be Linear_Combination of A; ::_thesis: ( L is convex & Sum L in Int A implies Carrier L = A ) assume that A1: L is convex and A2: Sum L in Int A ; ::_thesis: Carrier L = A reconsider C = Carrier L as non empty Subset of V by A1, CONVEX1:21; reconsider LC = L as Linear_Combination of C by RLVECT_2:def_6; LC in ConvexComb V by A1, CONVEX3:def_1; then Sum LC in { (Sum M) where M is Convex_Combination of C : M in ConvexComb V } by A1; then A3: Sum L in conv C by CONVEX3:5; A4: Carrier L c= A by RLVECT_2:def_6; assume Carrier L <> A ; ::_thesis: contradiction then Carrier L c< A by A4, XBOOLE_0:def_8; hence contradiction by A2, A3, Def1; ::_thesis: verum end; theorem Th12: :: RLAFFIN2:12 for V being RealLinearSpace for I being affinely-independent Subset of V for L being Linear_Combination of I st L is convex & Carrier L = I holds Sum L in Int I proof let V be RealLinearSpace; ::_thesis: for I being affinely-independent Subset of V for L being Linear_Combination of I st L is convex & Carrier L = I holds Sum L in Int I let I be affinely-independent Subset of V; ::_thesis: for L being Linear_Combination of I st L is convex & Carrier L = I holds Sum L in Int I let L be Linear_Combination of I; ::_thesis: ( L is convex & Carrier L = I implies Sum L in Int I ) assume that A1: L is convex and A2: Carrier L = I ; ::_thesis: Sum L in Int I reconsider I1 = I as non empty Subset of V by A1, A2, CONVEX1:21; reconsider K = L as Linear_Combination of I1 ; K in ConvexComb V by A1, CONVEX3:def_1; then Sum K in { (Sum M) where M is Convex_Combination of I1 : M in ConvexComb V } by A1; then A3: Sum K in conv I1 by CONVEX3:5; A4: ( conv I1 c= Affin I1 & sum L = 1 ) by A1, RLAFFIN1:62, RLAFFIN1:65; for A being Subset of V st A c< I holds not Sum K in conv A proof let A be Subset of V; ::_thesis: ( A c< I implies not Sum K in conv A ) assume A5: A c< I ; ::_thesis: not Sum K in conv A assume A6: Sum K in conv A ; ::_thesis: contradiction ( conv A c= Affin A & A c= I ) by A5, RLAFFIN1:65, XBOOLE_0:def_8; then (Sum K) |-- A = (Sum K) |-- I by A6, RLAFFIN1:77 .= K by A3, A4, RLAFFIN1:def_7 ; then I c= A by A2, RLVECT_2:def_6; hence contradiction by A5, XBOOLE_0:def_8; ::_thesis: verum end; hence Sum L in Int I by A3, Def1; ::_thesis: verum end; theorem :: RLAFFIN2:13 for V being RealLinearSpace for A being Subset of V st not Int A is empty holds A is finite proof let V be RealLinearSpace; ::_thesis: for A being Subset of V st not Int A is empty holds A is finite let A be Subset of V; ::_thesis: ( not Int A is empty implies A is finite ) assume not Int A is empty ; ::_thesis: A is finite then consider x being set such that A1: x in Int A by XBOOLE_0:def_1; consider L being Linear_Combination of A such that A2: ( L is convex & x = Sum L ) by A1, Th10; Carrier L = A by A1, A2, Th11; hence A is finite ; ::_thesis: verum end; theorem :: RLAFFIN2:14 for r being Real for V being RealLinearSpace for v, u, p being VECTOR of V for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds p in Int (I \ {v}) proof let r be Real; ::_thesis: for V being RealLinearSpace for v, u, p being VECTOR of V for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds p in Int (I \ {v}) let V be RealLinearSpace; ::_thesis: for v, u, p being VECTOR of V for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds p in Int (I \ {v}) let v, u, p be VECTOR of V; ::_thesis: for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds p in Int (I \ {v}) let I be affinely-independent Subset of V; ::_thesis: ( v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u implies p in Int (I \ {v}) ) assume that A1: v in I and A2: u in Int I and A3: p in conv (I \ {v}) and A4: (r * v) + ((1 - r) * p) = u ; ::_thesis: p in Int (I \ {v}) A5: conv I c= Affin I by RLAFFIN1:65; I c= conv I by RLAFFIN1:2; then A6: v in conv I by A1; conv (I \ {v}) c= conv I by RLAFFIN1:3, XBOOLE_1:36; then p in conv I by A3; then A7: u |-- I = ((1 - r) * (p |-- I)) + (r * (v |-- I)) by A4, A5, A6, RLAFFIN1:70; A8: Carrier (v |-- {v}) c= {v} by RLVECT_2:def_6; A9: u in conv I by A2, Def1; then Sum (u |-- I) = u by A5, RLAFFIN1:def_7; then A10: Carrier (u |-- I) = I by A2, A9, Th11, RLAFFIN1:71; A11: ( {v} c= Affin {v} & v in {v} ) by RLAFFIN1:49, TARSKI:def_1; {v} c= I by A1, ZFMISC_1:31; then A12: v |-- I = v |-- {v} by A11, RLAFFIN1:77; A13: conv (I \ {v}) c= Affin (I \ {v}) by RLAFFIN1:65; then A14: p |-- I = p |-- (I \ {v}) by A3, RLAFFIN1:77, XBOOLE_1:36; A15: I \ {v} c= Carrier (p |-- (I \ {v})) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I \ {v} or x in Carrier (p |-- (I \ {v})) ) assume A16: x in I \ {v} ; ::_thesis: x in Carrier (p |-- (I \ {v})) then reconsider w = x as Element of V ; A17: w in I by A16, ZFMISC_1:56; w <> v by A16, ZFMISC_1:56; then not w in Carrier (v |-- {v}) by A8, TARSKI:def_1; then A18: (v |-- I) . w = 0 by A12; (u |-- I) . w = (((1 - r) * (p |-- I)) . w) + ((r * (v |-- I)) . w) by A7, RLVECT_2:def_10 .= (((1 - r) * (p |-- I)) . w) + (r * ((v |-- I) . w)) by RLVECT_2:def_11 .= (1 - r) * ((p |-- I) . w) by A18, RLVECT_2:def_11 ; then (p |-- I) . w <> 0 by A10, A17, RLVECT_2:19; hence x in Carrier (p |-- (I \ {v})) by A14; ::_thesis: verum end; Carrier (p |-- (I \ {v})) c= I \ {v} by RLVECT_2:def_6; then A19: I \ {v} = Carrier (p |-- (I \ {v})) by A15, XBOOLE_0:def_10; A20: I \ {v} is affinely-independent by RLAFFIN1:43, XBOOLE_1:36; then Sum (p |-- (I \ {v})) = p by A3, A13, RLAFFIN1:def_7; hence p in Int (I \ {v}) by A3, A19, A20, Th12, RLAFFIN1:71; ::_thesis: verum end; begin definition let V be RealLinearSpace; func center_of_mass V -> Function of (BOOL the carrier of V), the carrier of V means :Def2: :: RLAFFIN2:def 2 ( ( for A being non empty finite Subset of V holds it . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds it . A = 0. V ) ); existence ex b1 being Function of (BOOL the carrier of V), the carrier of V st ( ( for A being non empty finite Subset of V holds b1 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds b1 . A = 0. V ) ) proof defpred S1[ set , set ] means ( ( for A being non empty finite Subset of V st A = $1 holds $2 = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite & A = $1 holds $2 = 0. V ) ); set cV = the carrier of V; A1: for x being set st x in BOOL the carrier of V holds ex y being set st ( y in the carrier of V & S1[x,y] ) proof let x be set ; ::_thesis: ( x in BOOL the carrier of V implies ex y being set st ( y in the carrier of V & S1[x,y] ) ) assume x in BOOL the carrier of V ; ::_thesis: ex y being set st ( y in the carrier of V & S1[x,y] ) then reconsider A = x as Subset of V ; percases ( A is finite or A is infinite ) ; suppose A is finite ; ::_thesis: ex y being set st ( y in the carrier of V & S1[x,y] ) then reconsider A1 = A as finite Subset of V ; take (1 / (card A1)) * (Sum A1) ; ::_thesis: ( (1 / (card A1)) * (Sum A1) in the carrier of V & S1[x,(1 / (card A1)) * (Sum A1)] ) thus ( (1 / (card A1)) * (Sum A1) in the carrier of V & S1[x,(1 / (card A1)) * (Sum A1)] ) ; ::_thesis: verum end; supposeA2: A is infinite ; ::_thesis: ex y being set st ( y in the carrier of V & S1[x,y] ) take 0. V ; ::_thesis: ( 0. V in the carrier of V & S1[x, 0. V] ) thus ( 0. V in the carrier of V & S1[x, 0. V] ) by A2; ::_thesis: verum end; end; end; consider f being Function of (BOOL the carrier of V), the carrier of V such that A3: for x being set st x in BOOL the carrier of V holds S1[x,f . x] from FUNCT_2:sch_1(A1); take f ; ::_thesis: ( ( for A being non empty finite Subset of V holds f . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds f . A = 0. V ) ) hereby ::_thesis: for A being Subset of V st A is infinite holds f . A = 0. V let A be non empty finite Subset of V; ::_thesis: f . A = (1 / (card A)) * (Sum A) A in BOOL the carrier of V by ZFMISC_1:56; hence f . A = (1 / (card A)) * (Sum A) by A3; ::_thesis: verum end; let A be Subset of V; ::_thesis: ( A is infinite implies f . A = 0. V ) assume A4: A is infinite ; ::_thesis: f . A = 0. V then A in (bool the carrier of V) \ {{}} by ZFMISC_1:56; hence f . A = 0. V by A3, A4; ::_thesis: verum end; uniqueness for b1, b2 being Function of (BOOL the carrier of V), the carrier of V st ( for A being non empty finite Subset of V holds b1 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds b1 . A = 0. V ) & ( for A being non empty finite Subset of V holds b2 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds b2 . A = 0. V ) holds b1 = b2 proof set cV = the carrier of V; let F1, F2 be Function of (BOOL the carrier of V), the carrier of V; ::_thesis: ( ( for A being non empty finite Subset of V holds F1 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds F1 . A = 0. V ) & ( for A being non empty finite Subset of V holds F2 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds F2 . A = 0. V ) implies F1 = F2 ) assume that A5: for A being non empty finite Subset of V holds F1 . A = (1 / (card A)) * (Sum A) and A6: for A being Subset of V st A is infinite holds F1 . A = 0. V and A7: for A being non empty finite Subset of V holds F2 . A = (1 / (card A)) * (Sum A) and A8: for A being Subset of V st A is infinite holds F2 . A = 0. V ; ::_thesis: F1 = F2 for x being set st x in BOOL the carrier of V holds F1 . x = F2 . x proof let x be set ; ::_thesis: ( x in BOOL the carrier of V implies F1 . x = F2 . x ) assume x in BOOL the carrier of V ; ::_thesis: F1 . x = F2 . x then reconsider A = x as non empty Subset of V by ZFMISC_1:56; percases ( A is finite or A is infinite ) ; suppose A is finite ; ::_thesis: F1 . x = F2 . x then reconsider A1 = A as non empty finite Subset of V ; thus F1 . x = (1 / (card A1)) * (Sum A1) by A5 .= F2 . x by A7 ; ::_thesis: verum end; supposeA9: A is infinite ; ::_thesis: F1 . x = F2 . x hence F1 . x = 0. V by A6 .= F2 . x by A8, A9 ; ::_thesis: verum end; end; end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def2 defines center_of_mass RLAFFIN2:def_2_:_ for V being RealLinearSpace for b2 being Function of (BOOL the carrier of V), the carrier of V holds ( b2 = center_of_mass V iff ( ( for A being non empty finite Subset of V holds b2 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds b2 . A = 0. V ) ) ); theorem Th15: :: RLAFFIN2:15 for r being Real for V being RealLinearSpace for Af being finite Subset of V ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) proof let r be Real; ::_thesis: for V being RealLinearSpace for Af being finite Subset of V ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) let V be RealLinearSpace; ::_thesis: for Af being finite Subset of V ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) let Af be finite Subset of V; ::_thesis: ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) set cV = the carrier of V; set Ar = (ZeroLC V) +* (Af --> r); A1: dom (Af --> r) = Af by FUNCOP_1:13; dom (ZeroLC V) = the carrier of V by FUNCT_2:def_1; then dom ((ZeroLC V) +* (Af --> r)) = the carrier of V \/ Af by A1, FUNCT_4:def_1; then ( rng ((ZeroLC V) +* (Af --> r)) c= (rng (Af --> r)) \/ (rng (ZeroLC V)) & dom ((ZeroLC V) +* (Af --> r)) = the carrier of V ) by FUNCT_4:17, XBOOLE_1:12; then (ZeroLC V) +* (Af --> r) is Function of the carrier of V,REAL by FUNCT_2:2; then reconsider Ar = (ZeroLC V) +* (Af --> r) as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_ex_Af_being_finite_Subset_of_V_st_ for_v_being_VECTOR_of_V_st_not_v_in_Af_holds_ Ar_._v_=_0 take Af = Af; ::_thesis: for v being VECTOR of V st not v in Af holds Ar . v = 0 let v be VECTOR of V; ::_thesis: ( not v in Af implies Ar . v = 0 ) assume not v in Af ; ::_thesis: Ar . v = 0 hence Ar . v = (ZeroLC V) . v by A1, FUNCT_4:11 .= 0 by RLVECT_2:20 ; ::_thesis: verum end; then reconsider Ar = Ar as Linear_Combination of V by RLVECT_2:def_3; Carrier Ar c= Af proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier Ar or x in Af ) assume A2: x in Carrier Ar ; ::_thesis: x in Af then reconsider v = x as Element of V ; assume not x in Af ; ::_thesis: contradiction then Ar . x = (ZeroLC V) . v by A1, FUNCT_4:11 .= 0 by RLVECT_2:20 ; hence contradiction by A2, RLVECT_2:19; ::_thesis: verum end; then reconsider Ar = (ZeroLC V) +* (Af --> r) as Linear_Combination of Af by RLVECT_2:def_6; A3: Carrier Ar c= Af by RLVECT_2:def_6; percases ( r = 0 or r <> 0 ) ; supposeA4: r = 0 ; ::_thesis: ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) Carrier Ar = {} proof assume Carrier Ar <> {} ; ::_thesis: contradiction then consider x being set such that A5: x in Carrier Ar by XBOOLE_0:def_1; ( Ar . x = (Af --> r) . x & (Af --> r) . x = 0 ) by A1, A3, A4, A5, FUNCOP_1:7, FUNCT_4:13; hence contradiction by A5, RLVECT_2:19; ::_thesis: verum end; then Ar = ZeroLC V by RLVECT_2:def_5; then A6: ( Sum Ar = 0. V & sum Ar = 0 ) by RLAFFIN1:31, RLVECT_2:30; r * (Sum Af) = 0. V by A4, RLVECT_1:10; hence ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) by A4, A6; ::_thesis: verum end; supposeA7: r <> 0 ; ::_thesis: ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) consider F being FinSequence of V such that A8: F is one-to-one and A9: rng F = Carrier Ar and A10: Sum Ar = Sum (Ar (#) F) by RLVECT_2:def_8; Af c= Carrier Ar proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Af or x in Carrier Ar ) assume A11: x in Af ; ::_thesis: x in Carrier Ar then Ar . x = (Af --> r) . x by A1, FUNCT_4:13; hence x in Carrier Ar by A7, A11; ::_thesis: verum end; then A12: Af = Carrier Ar by A3, XBOOLE_0:def_10; then dom F,Af are_equipotent by A8, A9, WELLORD2:def_4; then A13: card Af = card (dom F) by CARD_1:5 .= card (Seg (len F)) by FINSEQ_1:def_3 .= len F by FINSEQ_1:57 ; set L = (len F) |-> r; A14: len (Ar * F) = len F by FINSEQ_2:33; then reconsider ArF = Ar * F as Element of (len F) -tuples_on REAL by FINSEQ_2:92; now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_F)_holds_ ArF_._i_=_((len_F)_|->_r)_._i let i be Nat; ::_thesis: ( i in Seg (len F) implies ArF . i = ((len F) |-> r) . i ) assume A15: i in Seg (len F) ; ::_thesis: ArF . i = ((len F) |-> r) . i then i in dom F by FINSEQ_1:def_3; then A16: F . i in rng F by FUNCT_1:def_3; then A17: (Af --> r) . (F . i) = r by A3, A9, FUNCOP_1:7; i in dom ArF by A14, A15, FINSEQ_1:def_3; then ArF . i = Ar . (F . i) by FUNCT_1:12; then ArF . i = (Af --> r) . (F . i) by A1, A3, A9, A16, FUNCT_4:13; hence ArF . i = ((len F) |-> r) . i by A15, A17, FINSEQ_2:57; ::_thesis: verum end; then ArF = (len F) |-> r by FINSEQ_2:119; then A18: sum Ar = Sum ((len F) |-> r) by A8, A9, RLAFFIN1:def_3 .= (len F) * r by RVSUM_1:80 ; set AF = Ar (#) F; A19: len (Ar (#) F) = len F by RLVECT_2:def_7; then A20: dom (Ar (#) F) = dom F by FINSEQ_3:29; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_F_holds_ (Ar_(#)_F)_._i_=_r_*_(F_/._i) let i be Element of NAT ; ::_thesis: ( i in dom F implies (Ar (#) F) . i = r * (F /. i) ) assume A21: i in dom F ; ::_thesis: (Ar (#) F) . i = r * (F /. i) then ( F /. i = F . i & F . i in rng F ) by FUNCT_1:def_3, PARTFUN1:def_6; then ( Ar . (F /. i) = (Af --> r) . (F /. i) & (Af --> r) . (F /. i) = r ) by A1, A3, A9, FUNCOP_1:7, FUNCT_4:13; hence (Ar (#) F) . i = r * (F /. i) by A20, A21, RLVECT_2:def_7; ::_thesis: verum end; then Sum Ar = r * (Sum F) by A10, A19, RLVECT_2:3 .= r * (Sum Af) by A8, A9, A12, RLVECT_2:def_2 ; hence ex L being Linear_Combination of Af st ( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) by A13, A18; ::_thesis: verum end; end; end; theorem Th16: :: RLAFFIN2:16 for V being RealLinearSpace for Af being finite Subset of V st not Af is empty holds (center_of_mass V) . Af in conv Af proof let V be RealLinearSpace; ::_thesis: for Af being finite Subset of V st not Af is empty holds (center_of_mass V) . Af in conv Af let Af be finite Subset of V; ::_thesis: ( not Af is empty implies (center_of_mass V) . Af in conv Af ) assume not Af is empty ; ::_thesis: (center_of_mass V) . Af in conv Af then reconsider a = Af as non empty finite Subset of V ; consider L being Linear_Combination of Af such that A1: Sum L = (1 / (card a)) * (Sum a) and A2: sum L = (1 / (card a)) * (card a) and A3: L = (ZeroLC V) +* (Af --> (1 / (card a))) by Th15; A4: dom (Af --> (1 / (card a))) = Af by FUNCOP_1:13; A5: for v being VECTOR of V holds 0 <= L . v proof let v be VECTOR of V; ::_thesis: 0 <= L . v percases ( v in Af or not v in Af ) ; supposeA6: v in Af ; ::_thesis: 0 <= L . v then L . v = (Af --> (1 / (card a))) . v by A3, A4, FUNCT_4:13 .= 1 / (card a) by A6, FUNCOP_1:7 ; hence 0 <= L . v ; ::_thesis: verum end; suppose not v in Af ; ::_thesis: 0 <= L . v then L . v = (ZeroLC V) . v by A3, A4, FUNCT_4:11 .= 0 by RLVECT_2:20 ; hence 0 <= L . v ; ::_thesis: verum end; end; end; sum L = 1 by A2, XCMPLX_1:87; then A7: L is convex by A5, RLAFFIN1:62; then L in ConvexComb V by CONVEX3:def_1; then Sum L in { (Sum K) where K is Convex_Combination of a : K in ConvexComb V } by A7; then Sum L in conv Af by CONVEX3:5; hence (center_of_mass V) . Af in conv Af by A1, Def2; ::_thesis: verum end; theorem Th17: :: RLAFFIN2:17 for V being RealLinearSpace for F being Subset-Family of V st union F is finite holds (center_of_mass V) .: F c= conv (union F) proof let V be RealLinearSpace; ::_thesis: for F being Subset-Family of V st union F is finite holds (center_of_mass V) .: F c= conv (union F) let F be Subset-Family of V; ::_thesis: ( union F is finite implies (center_of_mass V) .: F c= conv (union F) ) set B = center_of_mass V; assume A1: union F is finite ; ::_thesis: (center_of_mass V) .: F c= conv (union F) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (center_of_mass V) .: F or y in conv (union F) ) assume y in (center_of_mass V) .: F ; ::_thesis: y in conv (union F) then consider x being set such that A2: x in dom (center_of_mass V) and A3: x in F and A4: (center_of_mass V) . x = y by FUNCT_1:def_6; reconsider x = x as non empty Subset of V by A2, ZFMISC_1:56; x c= union F by A3, ZFMISC_1:74; then A5: y in conv x by A1, A4, Th16; conv x c= conv (union F) by A3, RLTOPSP1:20, ZFMISC_1:74; hence y in conv (union F) by A5; ::_thesis: verum end; theorem Th18: :: RLAFFIN2:18 for V being RealLinearSpace for v being VECTOR of V for If being finite affinely-independent Subset of V st v in If holds (((center_of_mass V) . If) |-- If) . v = 1 / (card If) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for If being finite affinely-independent Subset of V st v in If holds (((center_of_mass V) . If) |-- If) . v = 1 / (card If) let v be VECTOR of V; ::_thesis: for If being finite affinely-independent Subset of V st v in If holds (((center_of_mass V) . If) |-- If) . v = 1 / (card If) let If be finite affinely-independent Subset of V; ::_thesis: ( v in If implies (((center_of_mass V) . If) |-- If) . v = 1 / (card If) ) consider L being Linear_Combination of If such that A1: ( Sum L = (1 / (card If)) * (Sum If) & sum L = (1 / (card If)) * (card If) ) and A2: L = (ZeroLC V) +* (If --> (1 / (card If))) by Th15; assume A3: v in If ; ::_thesis: (((center_of_mass V) . If) |-- If) . v = 1 / (card If) then A4: ( conv If c= Affin If & (center_of_mass V) . If in conv If ) by Th16, RLAFFIN1:65; ( (center_of_mass V) . If = Sum L & sum L = 1 ) by A1, A3, Def2, XCMPLX_1:87; then ( dom (If --> (1 / (card If))) = If & L = ((center_of_mass V) . If) |-- If ) by A4, FUNCOP_1:13, RLAFFIN1:def_7; hence (((center_of_mass V) . If) |-- If) . v = (If --> (1 / (card If))) . v by A2, A3, FUNCT_4:13 .= 1 / (card If) by A3, FUNCOP_1:7 ; ::_thesis: verum end; theorem Th19: :: RLAFFIN2:19 for V being RealLinearSpace for If being finite affinely-independent Subset of V holds ( (center_of_mass V) . If in If iff card If = 1 ) proof let V be RealLinearSpace; ::_thesis: for If being finite affinely-independent Subset of V holds ( (center_of_mass V) . If in If iff card If = 1 ) let If be finite affinely-independent Subset of V; ::_thesis: ( (center_of_mass V) . If in If iff card If = 1 ) set B = center_of_mass V; hereby ::_thesis: ( card If = 1 implies (center_of_mass V) . If in If ) assume A1: (center_of_mass V) . If in If ; ::_thesis: 1 = card If then reconsider BA = (center_of_mass V) . If as Element of V ; (center_of_mass V) . If in conv If by A1, Th16; then 1 = (BA |-- If) . BA by A1, RLAFFIN1:72 .= 1 / (card If) by A1, Th18 ; hence 1 = card If by XCMPLX_1:58; ::_thesis: verum end; assume A2: card If = 1 ; ::_thesis: (center_of_mass V) . If in If then consider x being set such that A3: {x} = If by CARD_2:42; x in If by A3, TARSKI:def_1; then reconsider x = x as Element of V ; (center_of_mass V) . If = (1 / (card If)) * (Sum If) by A3, Def2 .= (1 / 1) * x by A2, A3, RLVECT_2:9 .= x by RLVECT_1:def_8 ; hence (center_of_mass V) . If in If by A3, TARSKI:def_1; ::_thesis: verum end; theorem Th20: :: RLAFFIN2:20 for V being RealLinearSpace for If being finite affinely-independent Subset of V st not If is empty holds (center_of_mass V) . If in Int If proof let V be RealLinearSpace; ::_thesis: for If being finite affinely-independent Subset of V st not If is empty holds (center_of_mass V) . If in Int If let If be finite affinely-independent Subset of V; ::_thesis: ( not If is empty implies (center_of_mass V) . If in Int If ) set BA = ((center_of_mass V) . If) |-- If; A1: If c= Carrier (((center_of_mass V) . If) |-- If) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in If or x in Carrier (((center_of_mass V) . If) |-- If) ) assume A2: x in If ; ::_thesis: x in Carrier (((center_of_mass V) . If) |-- If) then (((center_of_mass V) . If) |-- If) . x = 1 / (card If) by Th18; hence x in Carrier (((center_of_mass V) . If) |-- If) by A2; ::_thesis: verum end; assume not If is empty ; ::_thesis: (center_of_mass V) . If in Int If then A3: (center_of_mass V) . If in conv If by Th16; Carrier (((center_of_mass V) . If) |-- If) c= If by RLVECT_2:def_6; then ( Carrier (((center_of_mass V) . If) |-- If) = If & ((center_of_mass V) . If) |-- If is convex ) by A1, A3, RLAFFIN1:71, XBOOLE_0:def_10; then ( conv If c= Affin If & Sum (((center_of_mass V) . If) |-- If) in Int If ) by Th12, RLAFFIN1:65; hence (center_of_mass V) . If in Int If by A3, RLAFFIN1:def_7; ::_thesis: verum end; theorem :: RLAFFIN2:21 for V being RealLinearSpace for A being Subset of V for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds If = A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds If = A let A be Subset of V; ::_thesis: for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds If = A let If be finite affinely-independent Subset of V; ::_thesis: ( A c= If & (center_of_mass V) . If in Affin A implies If = A ) set B = center_of_mass V; assume that A1: A c= If and A2: (center_of_mass V) . If in Affin A ; ::_thesis: If = A A3: ((center_of_mass V) . If) |-- If = ((center_of_mass V) . If) |-- A by A1, A2, RLAFFIN1:77; reconsider i = If as finite set ; assume If <> A ; ::_thesis: contradiction then not If c= A by A1, XBOOLE_0:def_10; then consider x being set such that A4: x in If and A5: not x in A by TARSKI:def_3; reconsider x = x as Element of V by A4; A6: (((center_of_mass V) . If) |-- If) . x = 1 / (card i) by A4, Th18; Carrier (((center_of_mass V) . If) |-- A) c= A by RLVECT_2:def_6; then not x in Carrier (((center_of_mass V) . If) |-- A) by A5; hence contradiction by A3, A4, A6; ::_thesis: verum end; theorem Th22: :: RLAFFIN2:22 for V being RealLinearSpace for v being VECTOR of V for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) let v be VECTOR of V; ::_thesis: for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) let Af be finite Subset of V; ::_thesis: ( v in Af & not Af \ {v} is empty implies (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) ) set Av = Af \ {v}; assume that A1: v in Af and A2: not Af \ {v} is empty ; ::_thesis: (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) consider L3 being Linear_Combination of {v} such that A3: L3 . v = 1 / (card Af) by RLVECT_4:37; consider L1 being Linear_Combination of Af \ {v} such that A4: Sum L1 = (1 / (card (Af \ {v}))) * (Sum (Af \ {v})) and sum L1 = (1 / (card (Af \ {v}))) * (card (Af \ {v})) and A5: L1 = (ZeroLC V) +* ((Af \ {v}) --> (1 / (card (Af \ {v})))) by Th15; consider L2 being Linear_Combination of Af such that A6: Sum L2 = (1 / (card Af)) * (Sum Af) and sum L2 = (1 / (card Af)) * (card Af) and A7: L2 = (ZeroLC V) +* (Af --> (1 / (card Af))) by Th15; A8: Sum L1 = (center_of_mass V) . (Af \ {v}) by A2, A4, Def2; for u being Element of V holds L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u proof let u be Element of V; ::_thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u A9: ( (((1 - (1 / (card Af))) * L1) + L3) . u = (((1 - (1 / (card Af))) * L1) . u) + (L3 . u) & ((1 - (1 / (card Af))) * L1) . u = (1 - (1 / (card Af))) * (L1 . u) ) by RLVECT_2:def_10, RLVECT_2:def_11; A10: (ZeroLC V) . u = 0 by RLVECT_2:20; A11: Carrier L3 c= {v} by RLVECT_2:def_6; A12: dom (Af --> (1 / (card Af))) = Af by FUNCOP_1:13; A13: dom ((Af \ {v}) --> (1 / (card (Af \ {v})))) = Af \ {v} by FUNCOP_1:13; percases ( not u in Af or v = u or ( u in Af & u <> v ) ) ; supposeA14: not u in Af ; ::_thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u then not u in Carrier L3 by A1, A11, TARSKI:def_1; then A15: L3 . u = 0 ; not u in Af \ {v} by A14, ZFMISC_1:56; then L1 . u = 0 by A5, A10, A13, FUNCT_4:11; hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A7, A9, A10, A12, A14, A15, FUNCT_4:11; ::_thesis: verum end; supposeA16: v = u ; ::_thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u then not u in Af \ {v} by ZFMISC_1:56; then A17: L1 . u = 0 by A5, A10, A13, FUNCT_4:11; L2 . u = (Af --> (1 / (card Af))) . v by A1, A7, A12, A16, FUNCT_4:13; hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A1, A3, A9, A16, A17, FUNCOP_1:7; ::_thesis: verum end; supposeA18: ( u in Af & u <> v ) ; ::_thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u then L2 . u = (Af --> (1 / (card Af))) . u by A7, A12, FUNCT_4:13; then A19: L2 . u = 1 / (card Af) by A18, FUNCOP_1:7; not u in Carrier L3 by A11, A18, TARSKI:def_1; then A20: L3 . u = 0 ; ( not v in Af \ {v} & (Af \ {v}) \/ {v} = Af ) by A1, ZFMISC_1:56, ZFMISC_1:116; then A21: card Af = (card (Af \ {v})) + 1 by CARD_2:41; 1 - (1 / (card Af)) = ((card Af) / (card Af)) - (1 / (card Af)) by A1, XCMPLX_1:60 .= ((card Af) - 1) / (card Af) by XCMPLX_1:120 .= (card (Af \ {v})) / (card Af) by A21 ; then A22: (1 - (1 / (card Af))) * (1 / (card (Af \ {v}))) = ((card (Af \ {v})) / (card Af)) / (card (Af \ {v})) by XCMPLX_1:99 .= ((card (Af \ {v})) / (card (Af \ {v}))) / (card Af) by XCMPLX_1:48 .= 1 / (card Af) by A2, XCMPLX_1:60 ; A23: u in Af \ {v} by A18, ZFMISC_1:56; then L1 . u = ((Af \ {v}) --> (1 / (card (Af \ {v})))) . u by A5, A13, FUNCT_4:13; hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A9, A19, A20, A22, A23, FUNCOP_1:7; ::_thesis: verum end; end; end; then A24: L2 = ((1 - (1 / (card Af))) * L1) + L3 by RLVECT_2:def_9; dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def_1; then A25: Af \ {v} in dom (center_of_mass V) by A2, ZFMISC_1:56; Sum L2 = (center_of_mass V) . Af by A1, A6, Def2; hence (center_of_mass V) . Af = (Sum ((1 - (1 / (card Af))) * L1)) + (Sum L3) by A24, RLVECT_3:1 .= ((1 - (1 / (card Af))) * (Sum L1)) + (Sum L3) by RLVECT_3:2 .= ((1 - (1 / (card Af))) * (Sum L1)) + ((1 / (card Af)) * v) by A3, RLVECT_2:32 .= ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) by A8, A25, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: RLAFFIN2:23 for V being RealLinearSpace for A being Subset of V for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds ex B being Subset of V st ( B c< If & conv A c= conv B ) proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds ex B being Subset of V st ( B c< If & conv A c= conv B ) let A be Subset of V; ::_thesis: for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds ex B being Subset of V st ( B c< If & conv A c= conv B ) let If be finite affinely-independent Subset of V; ::_thesis: ( conv A c= conv If & not If is empty & conv A misses Int If implies ex B being Subset of V st ( B c< If & conv A c= conv B ) ) assume that A1: conv A c= conv If and A2: not If is empty and A3: conv A misses Int If ; ::_thesis: ex B being Subset of V st ( B c< If & conv A c= conv B ) reconsider If = If as non empty finite affinely-independent Subset of V by A2; set YY = { B where B is Subset of V : ( B c= If & ex x being set st ( x in conv A & x in Int B ) ) } ; { B where B is Subset of V : ( B c= If & ex x being set st ( x in conv A & x in Int B ) ) } c= bool the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of V : ( B c= If & ex x being set st ( x in conv A & x in Int B ) ) } or x in bool the carrier of V ) assume x in { B where B is Subset of V : ( B c= If & ex x being set st ( x in conv A & x in Int B ) ) } ; ::_thesis: x in bool the carrier of V then ex B being Subset of V st ( B = x & B c= If & ex y being set st ( y in conv A & y in Int B ) ) ; hence x in bool the carrier of V ; ::_thesis: verum end; then reconsider YY = { B where B is Subset of V : ( B c= If & ex x being set st ( x in conv A & x in Int B ) ) } as Subset-Family of V ; take U = union YY; ::_thesis: ( U c< If & conv A c= conv U ) A4: conv A c= conv U proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in conv A or v in conv U ) assume A5: v in conv A ; ::_thesis: v in conv U then v in conv If by A1; then v in union { (Int B) where B is Subset of V : B c= If } by Th8; then consider IB being set such that A6: v in IB and A7: IB in { (Int B) where B is Subset of V : B c= If } by TARSKI:def_4; consider B being Subset of V such that A8: IB = Int B and A9: B c= If by A7; Int B c= conv B by Lm2; then A10: v in conv B by A6, A8; B in YY by A5, A6, A8, A9; then conv B c= conv U by RLAFFIN1:3, ZFMISC_1:74; hence v in conv U by A10; ::_thesis: verum end; A11: U c= If proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U or x in If ) assume x in U ; ::_thesis: x in If then consider b being set such that A12: x in b and A13: b in YY by TARSKI:def_4; ex B being Subset of V st ( b = B & B c= If & ex y being set st ( y in conv A & y in Int B ) ) by A13; hence x in If by A12; ::_thesis: verum end; U <> If proof defpred S1[ set , set ] means for B being Subset of V st B = $2 holds ( $1 in B & ex x being set st ( x in conv A & x in Int B ) ); assume A14: U = If ; ::_thesis: contradiction A15: for x being set st x in If holds ex y being set st ( y in bool If & S1[x,y] ) proof let x be set ; ::_thesis: ( x in If implies ex y being set st ( y in bool If & S1[x,y] ) ) assume x in If ; ::_thesis: ex y being set st ( y in bool If & S1[x,y] ) then consider b being set such that A16: x in b and A17: b in YY by A14, TARSKI:def_4; consider B being Subset of V such that A18: ( b = B & B c= If & ex y being set st ( y in conv A & y in Int B ) ) by A17; take B ; ::_thesis: ( B in bool If & S1[x,B] ) thus ( B in bool If & S1[x,B] ) by A16, A18; ::_thesis: verum end; consider p being Function of If,(bool If) such that A19: for x being set st x in If holds S1[x,p . x] from FUNCT_2:sch_1(A15); defpred S2[ set , set ] means for B being Subset of V st B = p . $1 holds ( $2 in conv A & $2 in Int B ); A20: dom p = If by FUNCT_2:def_1; A21: for x being set st x in If holds ex y being set st ( y in the carrier of V & S2[x,y] ) proof let x be set ; ::_thesis: ( x in If implies ex y being set st ( y in the carrier of V & S2[x,y] ) ) assume A22: x in If ; ::_thesis: ex y being set st ( y in the carrier of V & S2[x,y] ) then p . x in rng p by A20, FUNCT_1:def_3; then reconsider px = p . x as Subset of V by XBOOLE_1:1; consider y being set such that A23: ( y in conv A & y in Int px ) by A19, A22; take y ; ::_thesis: ( y in the carrier of V & S2[x,y] ) thus ( y in the carrier of V & S2[x,y] ) by A23; ::_thesis: verum end; consider q being Function of If,V such that A24: for x being set st x in If holds S2[x,q . x] from FUNCT_2:sch_1(A21); reconsider R = rng q as non empty finite Subset of V ; A25: R c= conv A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R or y in conv A ) assume y in R ; ::_thesis: y in conv A then consider x being set such that A26: x in dom q and A27: y = q . x by FUNCT_1:def_3; p . x in rng p by A20, A26, FUNCT_1:def_3; then reconsider px = p . x as Subset of V by XBOOLE_1:1; px = p . x ; hence y in conv A by A24, A26, A27; ::_thesis: verum end; then A28: R c= conv U by A4, XBOOLE_1:1; A29: conv R c= conv A by A25, CONVEX1:30; A30: dom q = If by FUNCT_2:def_1; A31: (1 / (card R)) * (card R) = (card R) / (card R) by XCMPLX_1:99 .= 1 by XCMPLX_1:60 ; consider L being Linear_Combination of R such that A32: Sum L = (1 / (card R)) * (Sum R) and A33: sum L = (1 / (card R)) * (card R) and A34: L = (ZeroLC V) +* (R --> (1 / (card R))) by Th15; set SL = Sum L; set SLIf = (Sum L) |-- If; Sum L = (center_of_mass V) . R by A32, Def2; then A35: Sum L in conv R by Th16; A36: dom (R --> (1 / (card R))) = R by FUNCOP_1:13; A37: now__::_thesis:_for_x_being_set_st_x_in_R_holds_ L_._x_=_1_/_(card_R) let x be set ; ::_thesis: ( x in R implies L . x = 1 / (card R) ) assume A38: x in R ; ::_thesis: L . x = 1 / (card R) hence L . x = (R --> (1 / (card R))) . x by A34, A36, FUNCT_4:13 .= 1 / (card R) by A38, FUNCOP_1:7 ; ::_thesis: verum end; A39: R c= Carrier L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in Carrier L ) assume A40: x in R ; ::_thesis: x in Carrier L then L . x <> 0 by A37; hence x in Carrier L by A40; ::_thesis: verum end; A41: conv U c= conv If by A11, RLAFFIN1:3; then A42: R c= conv If by A28, XBOOLE_1:1; then A43: conv R c= conv If by CONVEX1:30; then A44: Sum L in conv If by A35; A45: R c= conv If by A28, A41, XBOOLE_1:1; Carrier L c= R by RLVECT_2:def_6; then A46: R = Carrier L by A39, XBOOLE_0:def_10; A47: If c= Carrier ((Sum L) |-- If) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in If or x in Carrier ((Sum L) |-- If) ) assume A48: x in If ; ::_thesis: x in Carrier ((Sum L) |-- If) then consider F being FinSequence of REAL , G being FinSequence of V such that A49: ((Sum L) |-- If) . x = Sum F and A50: len G = len F and G is one-to-one and A51: rng G = Carrier L and A52: for n being Nat st n in dom F holds F . n = (L . (G . n)) * (((G . n) |-- If) . x) by A31, A33, A42, Th3; A53: p . x in rng p by A20, A48, FUNCT_1:def_3; then reconsider px = p . x as Subset of V by XBOOLE_1:1; A54: Int px c= conv px by Lm2; A55: q . x in Int px by A24, A48; then A56: q . x in conv px by A54; A57: x in px by A19, A48; A58: conv px c= Affin px by RLAFFIN1:65; A59: px is affinely-independent by A53, RLAFFIN1:43; then Sum ((q . x) |-- px) = q . x by A56, A58, RLAFFIN1:def_7; then A60: Carrier ((q . x) |-- px) = px by A54, A55, A59, Th11, RLAFFIN1:71; (q . x) |-- px = (q . x) |-- If by A53, A56, A58, RLAFFIN1:77; then A61: ((q . x) |-- If) . x <> 0 by A57, A60, RLVECT_2:19; conv px c= conv If by A53, RLAFFIN1:3; then A62: ((q . x) |-- If) . x >= 0 by A48, A56, RLAFFIN1:71; A63: q . x in R by A30, A48, FUNCT_1:def_3; then A64: L . (q . x) = 1 / (card R) by A37; A65: dom G = dom F by A50, FINSEQ_3:29; A66: now__::_thesis:_for_m_being_Nat_st_m_in_dom_F_holds_ 0_<=_F_._m let m be Nat; ::_thesis: ( m in dom F implies 0 <= F . m ) assume A67: m in dom F ; ::_thesis: 0 <= F . m then G . m in R by A46, A51, A65, FUNCT_1:def_3; then A68: ( L . (G . m) > 0 & ((G . m) |-- If) . x >= 0 ) by A37, A45, A48, RLAFFIN1:71; F . m = (L . (G . m)) * (((G . m) |-- If) . x) by A52, A67; hence 0 <= F . m by A68; ::_thesis: verum end; consider n being set such that A69: n in dom G and A70: G . n = q . x by A39, A51, A63, FUNCT_1:def_3; F . n = (L . (q . x)) * (((q . x) |-- If) . x) by A52, A65, A69, A70; then ((Sum L) |-- If) . x > 0 by A49, A61, A62, A64, A65, A66, A69, RVSUM_1:85; hence x in Carrier ((Sum L) |-- If) by A48; ::_thesis: verum end; Carrier ((Sum L) |-- If) c= If by RLVECT_2:def_6; then ( Carrier ((Sum L) |-- If) = If & (Sum L) |-- If is convex ) by A47, A35, A43, RLAFFIN1:71, XBOOLE_0:def_10; then ( conv If c= Affin If & Sum ((Sum L) |-- If) in Int If ) by Th12, RLAFFIN1:65; then Sum L in Int If by A44, RLAFFIN1:def_7; hence contradiction by A3, A29, A35, XBOOLE_0:3; ::_thesis: verum end; hence ( U c< If & conv A c= conv U ) by A4, A11, XBOOLE_0:def_8; ::_thesis: verum end; theorem Th24: :: RLAFFIN2:24 for V being RealLinearSpace for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds ex v being VECTOR of V st L1 . v > L2 . v proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds ex v being VECTOR of V st L1 . v > L2 . v let L1, L2 be Linear_Combination of V; ::_thesis: ( Sum L1 <> Sum L2 & sum L1 = sum L2 implies ex v being VECTOR of V st L1 . v > L2 . v ) assume that A1: Sum L1 <> Sum L2 and A2: sum L1 = sum L2 ; ::_thesis: ex v being VECTOR of V st L1 . v > L2 . v consider F being FinSequence such that A3: rng F = (Carrier L1) \/ (Carrier L2) and A4: F is one-to-one by FINSEQ_4:58; reconsider F = F as FinSequence of V by A3, FINSEQ_1:def_4; A5: len (L2 * F) = len F by FINSEQ_2:33; A6: len (L1 * F) = len F by FINSEQ_2:33; then reconsider L1F = L1 * F, L2F = L2 * F as Element of (len F) -tuples_on REAL by A5, FINSEQ_2:92; A7: len (L2F - L1F) = len F by CARD_1:def_7; assume A8: for v being Element of V holds L1 . v <= L2 . v ; ::_thesis: contradiction A9: for i being Nat st i in dom (L2F - L1F) holds 0 <= (L2F - L1F) . i proof let i be Nat; ::_thesis: ( i in dom (L2F - L1F) implies 0 <= (L2F - L1F) . i ) L2 . (F /. i) >= L1 . (F /. i) by A8; then A10: (L2 . (F /. i)) - (L1 . (F /. i)) >= (L1 . (F /. i)) - (L1 . (F /. i)) by XREAL_1:9; assume A11: i in dom (L2F - L1F) ; ::_thesis: 0 <= (L2F - L1F) . i then i in dom F by A7, FINSEQ_3:29; then A12: F /. i = F . i by PARTFUN1:def_6; i in dom L2F by A5, A7, A11, FINSEQ_3:29; then A13: L2F . i = L2 . (F . i) by FUNCT_1:12; i in dom L1F by A6, A7, A11, FINSEQ_3:29; then L1F . i = L1 . (F . i) by FUNCT_1:12; hence 0 <= (L2F - L1F) . i by A10, A12, A13, RVSUM_1:27; ::_thesis: verum end; A14: Sum (L2F - L1F) = (Sum L2F) - (Sum L1F) by RVSUM_1:90 .= (sum L2) - (Sum L1F) by A3, A4, RLAFFIN1:30, XBOOLE_1:7 .= (sum L2) - (sum L1) by A3, A4, RLAFFIN1:30, XBOOLE_1:7 .= 0 by A2 ; now__::_thesis:_for_v_being_Element_of_V_holds_L1_._v_=_L2_._v let v be Element of V; ::_thesis: L1 . v = L2 . v now__::_thesis:_L1_._v_=_L2_._v percases ( ( not v in Carrier L1 & not v in Carrier L2 ) or v in rng F ) by A3, XBOOLE_0:def_3; supposeA15: ( not v in Carrier L1 & not v in Carrier L2 ) ; ::_thesis: L1 . v = L2 . v then L1 . v = 0 ; hence L1 . v = L2 . v by A15; ::_thesis: verum end; suppose v in rng F ; ::_thesis: L1 . v = L2 . v then consider i being set such that A16: i in dom F and A17: F . i = v by FUNCT_1:def_3; reconsider i = i as Nat by A16; i in dom L2F by A5, A16, FINSEQ_3:29; then A18: ( (L2F - L1F) . i = (L2F . i) - (L1F . i) & L2F . i = L2 . v ) by A17, FUNCT_1:12, RVSUM_1:27; i in dom L1F by A6, A16, FINSEQ_3:29; then A19: L1F . i = L1 . v by A17, FUNCT_1:12; A20: i in dom (L2F - L1F) by A7, A16, FINSEQ_3:29; then (L2 . v) - (L1 . v) <= 0 by A9, A14, A18, A19, RVSUM_1:85; then (L2 . v) - (L1 . v) = 0 by A9, A18, A19, A20; hence L1 . v = L2 . v ; ::_thesis: verum end; end; end; hence L1 . v = L2 . v ; ::_thesis: verum end; hence contradiction by A1, RLVECT_2:def_9; ::_thesis: verum end; Lm3: for r, s being Real for V being RealLinearSpace for v being VECTOR of V for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) proof let r, s be Real; ::_thesis: for V being RealLinearSpace for v being VECTOR of V for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) let v be VECTOR of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 . v <> L2 . v implies ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) ) set u1 = L1 . v; set u2 = L2 . v; A1: ((r * L1) + ((1 - r) * L2)) . v = ((r * L1) . v) + (((1 - r) * L2) . v) by RLVECT_2:def_10 .= (r * (L1 . v)) + (((1 - r) * L2) . v) by RLVECT_2:def_11 .= (r * (L1 . v)) + (((- r) + 1) * (L2 . v)) by RLVECT_2:def_11 .= (r * ((L1 . v) - (L2 . v))) + (L2 . v) ; assume A2: L1 . v <> L2 . v ; ::_thesis: ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) then A3: (L1 . v) - (L2 . v) <> 0 ; A4: (L2 . v) - (L1 . v) <> 0 by A2; hereby ::_thesis: ( r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) implies ((r * L1) + ((1 - r) * L2)) . v = s ) assume ((r * L1) + ((1 - r) * L2)) . v = s ; ::_thesis: r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) then r * ((L2 . v) - (L1 . v)) = ((L2 . v) - s) * 1 by A1; then r / 1 = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) by A4, XCMPLX_1:94; hence r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ; ::_thesis: verum end; assume r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ; ::_thesis: ((r * L1) + ((1 - r) * L2)) . v = s hence ((r * L1) + ((1 - r) * L2)) . v = ((((L2 . v) - s) / (- ((L1 . v) - (L2 . v)))) * ((L1 . v) - (L2 . v))) + (L2 . v) by A1 .= (((- ((L2 . v) - s)) / ((L1 . v) - (L2 . v))) * ((L1 . v) - (L2 . v))) + (L2 . v) by XCMPLX_1:192 .= (- ((L2 . v) - s)) + (L2 . v) by A3, XCMPLX_1:87 .= s ; ::_thesis: verum end; theorem Th25: :: RLAFFIN2:25 for r, s being Real for V being RealLinearSpace for v being VECTOR of V for L1, L2 being Linear_Combination of V for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) proof let r, s be Real; ::_thesis: for V being RealLinearSpace for v being VECTOR of V for L1, L2 being Linear_Combination of V for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L1, L2 being Linear_Combination of V for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) let v be VECTOR of V; ::_thesis: for L1, L2 being Linear_Combination of V for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) let L1, L2 be Linear_Combination of V; ::_thesis: for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) let p be Real; ::_thesis: ( ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v implies ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) ) set rv = ((r * L1) + ((1 - r) * L2)) . v; set sv = ((s * L1) + ((1 - s) * L2)) . v; set v1 = L1 . v; set v2 = L2 . v; A1: ((r * L1) + ((1 - r) * L2)) . v = ((r * L1) . v) + (((1 - r) * L2) . v) by RLVECT_2:def_10 .= (r * (L1 . v)) + (((1 - r) * L2) . v) by RLVECT_2:def_11 .= (r * (L1 . v)) + ((1 - r) * (L2 . v)) by RLVECT_2:def_11 ; A2: ((s * L1) + ((1 - s) * L2)) . v = ((s * L1) . v) + (((1 - s) * L2) . v) by RLVECT_2:def_10 .= (s * (L1 . v)) + (((1 - s) * L2) . v) by RLVECT_2:def_11 .= (s * (L1 . v)) + ((1 - s) * (L2 . v)) by RLVECT_2:def_11 ; assume that A3: ((r * L1) + ((1 - r) * L2)) . v <= p and A4: p <= ((s * L1) + ((1 - s) * L2)) . v ; ::_thesis: ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) percases ( ((r * L1) + ((1 - r) * L2)) . v = ((s * L1) + ((1 - s) * L2)) . v or ((r * L1) + ((1 - r) * L2)) . v <> ((s * L1) + ((1 - s) * L2)) . v ) ; supposeA5: ((r * L1) + ((1 - r) * L2)) . v = ((s * L1) + ((1 - s) * L2)) . v ; ::_thesis: ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) take r ; ::_thesis: ( ((r * L1) + ((1 - r) * L2)) . v = p & ( r <= s implies ( r <= r & r <= s ) ) & ( s <= r implies ( s <= r & r <= r ) ) ) thus ( ((r * L1) + ((1 - r) * L2)) . v = p & ( r <= s implies ( r <= r & r <= s ) ) & ( s <= r implies ( s <= r & r <= r ) ) ) by A3, A4, A5, XXREAL_0:1; ::_thesis: verum end; suppose ((r * L1) + ((1 - r) * L2)) . v <> ((s * L1) + ((1 - s) * L2)) . v ; ::_thesis: ex rs being Real st ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) then A6: (((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) <> 0 ; set y = (p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)); set x = ((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)); take rs = (r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))); ::_thesis: ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) A7: ( (r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) = r * ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) & (s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) = s * ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) ) ; A8: (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) = (((((s * L1) + ((1 - s) * L2)) . v) - p) + (p - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)) by XCMPLX_1:62 .= 1 by A6, XCMPLX_1:60 ; A9: p - (((r * L1) + ((1 - r) * L2)) . v) >= (((r * L1) + ((1 - r) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) by A3, XREAL_1:9; thus p = (p * ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)) by A6, XCMPLX_1:89 .= (((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) + ((((s * L1) + ((1 - s) * L2)) . v) * (p - (((r * L1) + ((1 - r) * L2)) . v)))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)) .= (((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + (((((s * L1) + ((1 - s) * L2)) . v) * (p - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) by XCMPLX_1:62 .= (((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + (((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * (((s * L1) + ((1 - s) * L2)) . v)) by XCMPLX_1:74 .= ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * ((r * (L1 . v)) + ((1 - r) * (L2 . v)))) + (((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * ((s * (L1 . v)) + ((1 - s) * (L2 . v)))) by A1, A2, XCMPLX_1:74 .= ((rs * (L1 . v)) + (((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) * (L2 . v))) - (rs * (L2 . v)) .= ((rs * (L1 . v)) + (1 * (L2 . v))) - (rs * (L2 . v)) by A8 .= (rs * (L1 . v)) + ((1 - rs) * (L2 . v)) .= (rs * (L1 . v)) + (((1 - rs) * L2) . v) by RLVECT_2:def_11 .= ((rs * L1) . v) + (((1 - rs) * L2) . v) by RLVECT_2:def_11 .= ((rs * L1) + ((1 - rs) * L2)) . v by RLVECT_2:def_10 ; ::_thesis: ( ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) A10: ( (((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) >= (((s * L1) + ((1 - s) * L2)) . v) - p & (((s * L1) + ((1 - s) * L2)) . v) - p >= p - p ) by A3, A4, XREAL_1:9, XREAL_1:10; hereby ::_thesis: ( s <= r implies ( s <= rs & rs <= r ) ) assume r <= s ; ::_thesis: ( r <= rs & rs <= s ) then ( r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) <= s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) & r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) <= s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) ) by A9, A10, XREAL_1:64; hence ( r <= rs & rs <= s ) by A7, A8, XREAL_1:6; ::_thesis: verum end; assume A11: s <= r ; ::_thesis: ( s <= rs & rs <= r ) then A12: r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) >= s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) by A10, XREAL_1:64; (((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) >= p - (((r * L1) + ((1 - r) * L2)) . v) by A4, XREAL_1:9; then r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) >= s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) by A9, A11, XREAL_1:64; hence ( s <= rs & rs <= r ) by A7, A8, A12, XREAL_1:6; ::_thesis: verum end; end; end; theorem :: RLAFFIN2:26 for V being RealLinearSpace for v, u being VECTOR of V for A being Subset of V st v in conv A & u in conv A & v <> u holds ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) proof let V be RealLinearSpace; ::_thesis: for v, u being VECTOR of V for A being Subset of V st v in conv A & u in conv A & v <> u holds ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) let v, u be VECTOR of V; ::_thesis: for A being Subset of V st v in conv A & u in conv A & v <> u holds ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) let A be Subset of V; ::_thesis: ( v in conv A & u in conv A & v <> u implies ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) ) reconsider Z = 0 as Real by XREAL_0:def_1; assume that A1: v in conv A and A2: u in conv A and A3: v <> u ; ::_thesis: ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) reconsider A1 = A as non empty Subset of V by A1; A4: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5; then consider Lv being Convex_Combination of A1 such that A5: v = Sum Lv and A6: Lv in ConvexComb V by A1; set Cv = Carrier Lv; A7: Carrier Lv c= A by RLVECT_2:def_6; consider Lu being Convex_Combination of A1 such that A8: u = Sum Lu and Lu in ConvexComb V by A2, A4; set Cu = Carrier Lu; A9: Carrier Lu c= A by RLVECT_2:def_6; then A10: (Carrier Lv) \/ (Carrier Lu) c= A by A7, XBOOLE_1:8; percases ( not Carrier Lu c= Carrier Lv or Carrier Lu c= Carrier Lv ) ; suppose not Carrier Lu c= Carrier Lv ; ::_thesis: ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) then consider p being set such that A11: p in Carrier Lu and A12: not p in Carrier Lv by TARSKI:def_3; reconsider p = p as Element of V by A11; ( Carrier Lv <> {} & Carrier Lv c= A \ {p} ) by A7, A12, CONVEX1:21, ZFMISC_1:34; then reconsider Ap = A \ {p} as non empty Subset of V ; Carrier Lv c= Ap by A7, A12, ZFMISC_1:34; then reconsider LV = Lv as Linear_Combination of Ap by RLVECT_2:def_6; take p ; ::_thesis: ex w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) take w = v; ::_thesis: ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) take Z ; ::_thesis: ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v ) A13: (Z * u) + ((1 - Z) * w) = (0. V) + (1 * w) by RLVECT_1:10 .= (0. V) + w by RLVECT_1:def_8 .= v by RLVECT_1:4 ; Sum LV in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A6; hence ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v ) by A5, A9, A11, A13, CONVEX3:5; ::_thesis: verum end; supposeA14: Carrier Lu c= Carrier Lv ; ::_thesis: ex p, w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) defpred S1[ set , set ] means for r being Real for p being Element of V st r = $2 & p = $1 holds ( r < 0 & Lv . p <> Lu . p & ((r * Lu) + ((1 - r) * Lv)) . p = 0 ); set P = { r where r is Element of REAL : ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } ; A15: now__::_thesis:_for_x_being_set_st_x_in__{__r_where_r_is_Element_of_REAL_:_ex_p_being_Element_of_V_st_ (_S1[p,r]_&_p_in_(Carrier_Lv)_\/_(Carrier_Lu)_)__}__holds_ x_is_real let x be set ; ::_thesis: ( x in { r where r is Element of REAL : ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } implies x is real ) assume x in { r where r is Element of REAL : ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } ; ::_thesis: x is real then ex r being Element of REAL st ( r = x & ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) ) ; hence x is real ; ::_thesis: verum end; A16: for p being Element of V for r, s being Element of REAL st S1[p,r] & S1[p,s] holds r = s proof let p be Element of V; ::_thesis: for r, s being Element of REAL st S1[p,r] & S1[p,s] holds r = s let r, s be Element of REAL ; ::_thesis: ( S1[p,r] & S1[p,s] implies r = s ) assume A17: S1[p,r] ; ::_thesis: ( not S1[p,s] or r = s ) then A18: ((r * Lu) + ((1 - r) * Lv)) . p = 0 ; A19: Lv . p <> Lu . p by A17; assume S1[p,s] ; ::_thesis: r = s then ((s * Lu) + ((1 - s) * Lv)) . p = 0 ; then s = ((Lv . p) - 0) / ((Lv . p) - (Lu . p)) by A19, Lm3 .= r by A18, A19, Lm3 ; hence r = s ; ::_thesis: verum end; ( sum Lu = 1 & sum Lv = 1 ) by RLAFFIN1:62; then consider p being Element of V such that A20: Lu . p > Lv . p by A3, A5, A8, Th24; A21: Lv . p <> 0 proof assume A22: Lv . p = 0 ; ::_thesis: contradiction then not p in Carrier Lu by A14, RLVECT_2:19; hence contradiction by A20, A22; ::_thesis: verum end; then p in Carrier Lv ; then A23: p in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def_3; set r = (Lv . p) / ((Lv . p) - (Lu . p)); A24: ( (Lv . p) / ((Lv . p) - (Lu . p)) = ((Lv . p) - Z) / ((Lv . p) - (Lu . p)) & (Lv . p) - (Lu . p) < (Lu . p) - (Lu . p) ) by A20, XREAL_1:9; Lv . p > 0 by A21, RLAFFIN1:62; then S1[p,(Lv . p) / ((Lv . p) - (Lu . p))] by A24, Lm3; then A25: (Lv . p) / ((Lv . p) - (Lu . p)) in { r where r is Element of REAL : ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } by A23; A26: (Carrier Lv) \/ (Carrier Lu) is finite ; { r where r is Element of REAL : ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } is finite from FRAENKEL:sch_28(A26, A16); then reconsider P = { r where r is Element of REAL : ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } as non empty finite real-membered set by A15, A25, MEMBERED:def_3; set M = max P; max P in P by XXREAL_2:def_8; then consider r being Element of REAL such that A27: max P = r and A28: ex p being Element of V st ( S1[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) ; set Lw = (r * Lu) + ((1 - r) * Lv); consider p being Element of V such that A29: S1[p,r] and A30: p in (Carrier Lv) \/ (Carrier Lu) by A28; set w = (r * u) + ((1 - r) * v); set R = (- r) / (1 - r); A31: Sum ((r * Lu) + ((1 - r) * Lv)) = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1 .= (r * u) + (Sum ((1 - r) * Lv)) by A8, RLVECT_3:2 .= (r * u) + ((1 - r) * v) by A5, RLVECT_3:2 ; A32: for z being Element of V holds 0 <= ((r * Lu) + ((1 - r) * Lv)) . z proof let z be Element of V; ::_thesis: 0 <= ((r * Lu) + ((1 - r) * Lv)) . z A33: ((Z * Lu) + ((1 - Z) * Lv)) . z = ((Z * Lu) . z) + (((1 - Z) * Lv) . z) by RLVECT_2:def_10 .= (Z * (Lu . z)) + (((1 - Z) * Lv) . z) by RLVECT_2:def_11 .= (Z * (Lu . z)) + ((1 - 0) * (Lv . z)) by RLVECT_2:def_11 .= Lv . z ; assume A34: 0 > ((r * Lu) + ((1 - r) * Lv)) . z ; ::_thesis: contradiction A35: ((r * Lu) + ((1 - r) * Lv)) . z = ((r * Lu) . z) + (((1 - r) * Lv) . z) by RLVECT_2:def_10 .= (r * (Lu . z)) + (((1 - r) * Lv) . z) by RLVECT_2:def_11 .= (r * (Lu . z)) + ((1 - r) * (Lv . z)) by RLVECT_2:def_11 ; A36: Lv . z <> 0 proof assume A37: Lv . z = 0 ; ::_thesis: contradiction then not z in Carrier Lu by A14, RLVECT_2:19; then Lu . z = 0 ; hence contradiction by A34, A35, A37; ::_thesis: verum end; then z in Carrier Lv ; then A38: z in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def_3; Lv . z >= 0 by RLAFFIN1:62; then consider rs being Real such that A39: ((rs * Lu) + ((1 - rs) * Lv)) . z = 0 and A40: ( r <= 0 implies ( r <= rs & rs <= 0 ) ) and ( 0 <= r implies ( 0 <= rs & rs <= r ) ) by A33, A34, Th25; rs <> 0 by A33, A36, A39; then S1[z,rs] by A29, A34, A35, A39, A40, RLAFFIN1:62; then rs in P by A38; then rs <= r by A27, XXREAL_2:def_8; then rs = r by A28, A40, XXREAL_0:1; hence contradiction by A34, A39; ::_thesis: verum end; ( r * Lu is Linear_Combination of A & (1 - r) * Lv is Linear_Combination of A ) by RLVECT_2:44; then (r * Lu) + ((1 - r) * Lv) is Linear_Combination of A by RLVECT_2:38; then A41: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A by RLVECT_2:def_6; ((r * Lu) + ((1 - r) * Lv)) . p = 0 by A29; then not p in Carrier ((r * Lu) + ((1 - r) * Lv)) by RLVECT_2:19; then A42: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A \ {p} by A41, ZFMISC_1:34; A43: sum ((r * Lu) + ((1 - r) * Lv)) = (sum (r * Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:34 .= (r * (sum Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:35 .= (r * 1) + (sum ((1 - r) * Lv)) by RLAFFIN1:62 .= (r * 1) + ((1 - r) * (sum Lv)) by RLAFFIN1:35 .= (r * 1) + ((1 - r) * 1) by RLAFFIN1:62 .= 1 ; then (r * Lu) + ((1 - r) * Lv) is convex by A32, RLAFFIN1:62; then Carrier ((r * Lu) + ((1 - r) * Lv)) <> {} by CONVEX1:21; then reconsider Ap = A \ {p} as non empty Subset of V by A42; reconsider LW = (r * Lu) + ((1 - r) * Lv) as Linear_Combination of Ap by A42, RLVECT_2:def_6; A44: LW is convex by A32, A43, RLAFFIN1:62; then LW in ConvexComb V by CONVEX3:def_1; then A45: Sum LW in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A44; take p ; ::_thesis: ex w being VECTOR of V ex r being Real st ( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) take (r * u) + ((1 - r) * v) ; ::_thesis: ex r being Real st ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * ((r * u) + ((1 - r) * v))) = v ) take (- r) / (1 - r) ; ::_thesis: ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v ) A46: 0 > r by A29; then A47: ( 1 + (- r) > 0 + (- r) & (1 + (- r)) / (1 + (- r)) = 1 ) by XCMPLX_1:60, XREAL_1:6; (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = (((- r) / (1 - r)) * u) + ((((1 - r) / (1 - r)) - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) by A46, XCMPLX_1:60 .= (((- r) / (1 - r)) * u) + ((((1 - r) - (- r)) / (1 - r)) * ((r * u) + ((1 - r) * v))) by XCMPLX_1:120 .= (((- r) / (1 - r)) * u) + (((1 / (1 - r)) * (r * u)) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def_5 .= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def_7 .= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by RLVECT_1:def_7 .= (((- r) / (1 - r)) * u) + ((((r / (1 - r)) * 1) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by XCMPLX_1:75 .= (((- r) / (1 - r)) * u) + (((r / (1 - r)) * u) + (1 * v)) by A46, XCMPLX_1:87 .= ((((- r) / (1 - r)) * u) + ((r / (1 - r)) * u)) + (1 * v) by RLVECT_1:def_3 .= ((((- r) / (1 - r)) + (r / (1 - r))) * u) + (1 * v) by RLVECT_1:def_6 .= ((((- r) + r) / (1 - r)) * u) + (1 * v) by XCMPLX_1:62 .= ((0 / (1 - r)) * u) + v by RLVECT_1:def_8 .= (0. V) + v by RLVECT_1:10 .= v by RLVECT_1:def_4 ; hence ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v ) by A10, A30, A31, A45, A46, A47, CONVEX3:5, XREAL_1:74; ::_thesis: verum end; end; end; theorem Th27: :: RLAFFIN2:27 for V being RealLinearSpace for v being VECTOR of V for A being Subset of V holds ( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) ) by RLAFFIN1:82; theorem Th28: :: RLAFFIN2:28 for V being RealLinearSpace for v being VECTOR of V for Af being finite Subset of V for I being affinely-independent Subset of V st Af c= I & v in Af holds (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for Af being finite Subset of V for I being affinely-independent Subset of V st Af c= I & v in Af holds (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V let v be VECTOR of V; ::_thesis: for Af being finite Subset of V for I being affinely-independent Subset of V st Af c= I & v in Af holds (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V let Af be finite Subset of V; ::_thesis: for I being affinely-independent Subset of V st Af c= I & v in Af holds (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V let I be affinely-independent Subset of V; ::_thesis: ( Af c= I & v in Af implies (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V ) assume that A1: Af c= I and A2: v in Af ; ::_thesis: (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V set Iv = I \ {v}; set Av = Af \ {v}; A3: (I \ {v}) \/ {v} = I by A1, A2, ZFMISC_1:116; set BA = (center_of_mass V) /. Af; A4: (center_of_mass V) . Af = (1 / (card Af)) * (Sum Af) by A2, Def2; A5: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def_1; then Af in dom (center_of_mass V) by A2, ZFMISC_1:56; then A6: (center_of_mass V) . Af = (center_of_mass V) /. Af by PARTFUN1:def_6; percases ( Af = {v} or Af <> {v} ) ; suppose Af = {v} ; ::_thesis: (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V then ( Sum Af = v & card Af = 1 ) by CARD_1:30, RLVECT_2:9; hence (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V by A3, A4, RLVECT_1:def_8; ::_thesis: verum end; supposeA7: Af <> {v} ; ::_thesis: (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V A8: not (center_of_mass V) /. Af in Affin (I \ {v}) proof A9: not Af \ {v} is empty proof assume Af \ {v} is empty ; ::_thesis: contradiction then Af c= {v} by XBOOLE_1:37; hence contradiction by A2, A7, ZFMISC_1:33; ::_thesis: verum end; then Af \ {v} in dom (center_of_mass V) by A5, ZFMISC_1:56; then A10: (center_of_mass V) . (Af \ {v}) = (center_of_mass V) /. (Af \ {v}) by PARTFUN1:def_6; Af \ {v} c= I \ {v} by A1, XBOOLE_1:33; then A11: Affin (Af \ {v}) c= Affin (I \ {v}) by RLAFFIN1:52; reconsider c = card Af as Real by XREAL_0:def_1; A12: c / c = c * (1 / c) by XCMPLX_1:99; ( conv (Af \ {v}) c= Affin (Af \ {v}) & (center_of_mass V) . (Af \ {v}) in conv (Af \ {v}) ) by A9, Th16, RLAFFIN1:65; then A13: (center_of_mass V) . (Af \ {v}) in Affin (Af \ {v}) ; assume (center_of_mass V) /. Af in Affin (I \ {v}) ; ::_thesis: contradiction then A14: ( not v in I \ {v} & ((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)) in Affin (I \ {v}) ) by A10, A11, A13, RUSUB_4:def_4, ZFMISC_1:56; ((center_of_mass V) /. Af) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) = (((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / c) * v)) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) by A2, A6, A9, Th22; then A15: (1 / c) * v = ((center_of_mass V) /. Af) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) by RLVECT_4:1 .= ((center_of_mass V) /. Af) + (- ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v})))) by RLVECT_1:def_11 .= ((- (1 - (1 / c))) * ((center_of_mass V) /. (Af \ {v}))) + ((center_of_mass V) /. Af) by RLVECT_4:3 ; A16: 1 = c / c by A2, XCMPLX_1:60; ((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)) = 1 * (((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af))) by RLVECT_1:def_8 .= c * ((1 / c) * (((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)))) by A12, A16, RLVECT_1:def_7 .= c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + ((1 / c) * (c * ((center_of_mass V) /. Af)))) by RLVECT_1:def_5 .= c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + (1 * ((center_of_mass V) /. Af))) by A12, A16, RLVECT_1:def_7 .= c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + ((center_of_mass V) /. Af)) by RLVECT_1:def_8 .= c * ((((1 / c) * (1 - c)) * ((center_of_mass V) /. (Af \ {v}))) + ((center_of_mass V) /. Af)) by RLVECT_1:def_7 .= 1 * v by A16, A15, A12, RLVECT_1:def_7 .= v by RLVECT_1:def_8 ; hence contradiction by A3, A14, Th27; ::_thesis: verum end; I \ {v} is affinely-independent by RLAFFIN1:43, XBOOLE_1:36; hence (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V by A6, A8, Th27; ::_thesis: verum end; end; end; theorem Th29: :: RLAFFIN2:29 for V being RealLinearSpace for F being c=-linear Subset-Family of V st union F is finite & union F is affinely-independent holds (center_of_mass V) .: F is affinely-independent Subset of V proof let V be RealLinearSpace; ::_thesis: for F being c=-linear Subset-Family of V st union F is finite & union F is affinely-independent holds (center_of_mass V) .: F is affinely-independent Subset of V set B = center_of_mass V; defpred S1[ Nat] means for k being Nat st k <= $1 holds for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V; let S be c=-linear Subset-Family of V; ::_thesis: ( union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V ) A1: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def_1; A2: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] let k be Nat; ::_thesis: ( k <= n + 1 implies for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V ) assume A4: k <= n + 1 ; ::_thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V percases ( k <= n or k = n + 1 ) by A4, NAT_1:8; suppose k <= n ; ::_thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V hence for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V by A3; ::_thesis: verum end; supposeA5: k = n + 1 ; ::_thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V let S be c=-linear Subset-Family of V; ::_thesis: ( card (union S) = k & union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V ) assume that A6: card (union S) = k and A7: ( union S is finite & union S is affinely-independent ) ; ::_thesis: (center_of_mass V) .: S is affinely-independent Subset of V set U = union S; A8: S c= bool (union S) by ZFMISC_1:82; set SU = S \ {(union S)}; A9: union (S \ {(union S)}) c= union S by XBOOLE_1:36, ZFMISC_1:77; then reconsider Usu = union (S \ {(union S)}) as finite set by A7; A10: S \ {(union S)} c= S by XBOOLE_1:36; A11: union (S \ {(union S)}) <> union S proof assume A12: union (S \ {(union S)}) = union S ; ::_thesis: contradiction then not S \ {(union S)} is empty by A5, A6, ZFMISC_1:2; then union (S \ {(union S)}) in S \ {(union S)} by A7, A10, A8, SIMPLEX0:9; hence contradiction by A12, ZFMISC_1:56; ::_thesis: verum end; then union (S \ {(union S)}) c< union S by A9, XBOOLE_0:def_8; then consider v being set such that A13: v in union S and A14: not v in union (S \ {(union S)}) by XBOOLE_0:6; reconsider v = v as Element of V by A13; A15: ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} is affinely-independent Subset of V by A7, A13, Th28; not union S is empty by A5, A6; then A16: union S in dom (center_of_mass V) by A1, ZFMISC_1:56; (center_of_mass V) . (union S) in {((center_of_mass V) . (union S))} by TARSKI:def_1; then (center_of_mass V) . (union S) in ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} by XBOOLE_0:def_3; then reconsider BU = (center_of_mass V) . (union S) as Element of V by A15; not S is empty by A5, A6, ZFMISC_1:2; then (S \ {(union S)}) \/ {(union S)} = S by A7, A8, SIMPLEX0:9, ZFMISC_1:116; then A17: (center_of_mass V) .: S = ((center_of_mass V) .: (S \ {(union S)})) \/ ((center_of_mass V) .: {(union S)}) by RELAT_1:120 .= ((center_of_mass V) .: (S \ {(union S)})) \/ (Im ((center_of_mass V),(union S))) by RELAT_1:def_16 .= ((center_of_mass V) .: (S \ {(union S)})) \/ {BU} by A16, FUNCT_1:59 ; A18: {v} c= union S by A13, ZFMISC_1:31; A19: card {v} = 1 by CARD_1:30; percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: (center_of_mass V) .: S is affinely-independent Subset of V then A20: union S = {v} by A5, A6, A7, A18, A19, CARD_FIN:1; (S \ {(union S)}) /\ (dom (center_of_mass V)) = {} proof assume (S \ {(union S)}) /\ (dom (center_of_mass V)) <> {} ; ::_thesis: contradiction then consider x being set such that A21: x in (S \ {(union S)}) /\ (dom (center_of_mass V)) by XBOOLE_0:def_1; x in S \ {(union S)} by A21, XBOOLE_0:def_4; then A22: x c= union (S \ {(union S)}) by ZFMISC_1:74; then x c= union S by A9, XBOOLE_1:1; then A23: ( x = union S or x = {} ) by A20, ZFMISC_1:33; not v in x by A14, A22; hence contradiction by A20, A21, A23, TARSKI:def_1, ZFMISC_1:56; ::_thesis: verum end; then (center_of_mass V) .: (S \ {(union S)}) = (center_of_mass V) .: {} by RELAT_1:112 .= {} ; hence (center_of_mass V) .: S is affinely-independent Subset of V by A17; ::_thesis: verum end; supposeA24: n > 0 ; ::_thesis: (center_of_mass V) .: S is affinely-independent Subset of V reconsider u = union S as finite set by A7; A25: Usu c= u by XBOOLE_1:36, ZFMISC_1:77; then card Usu <= n + 1 by A5, A6, NAT_1:43; then card Usu < n + 1 by A5, A6, A11, A25, CARD_FIN:1, XXREAL_0:1; then A26: card Usu <= n by NAT_1:13; ( union (S \ {(union S)}) c= (union S) \ {v} & (union S) \ {v} c= ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} ) by A9, A14, XBOOLE_1:7, ZFMISC_1:34; then union (S \ {(union S)}) is affinely-independent by A15, RLAFFIN1:43, XBOOLE_1:1; then reconsider BSU = (center_of_mass V) .: (S \ {(union S)}) as affinely-independent Subset of V by A3, A10, A26; BSU c= Affin ((union S) \ {v}) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in BSU or y in Affin ((union S) \ {v}) ) assume y in BSU ; ::_thesis: y in Affin ((union S) \ {v}) then consider x being set such that A27: x in dom (center_of_mass V) and A28: x in S \ {(union S)} and A29: (center_of_mass V) . x = y by FUNCT_1:def_6; reconsider x = x as non empty Subset of V by A27, ZFMISC_1:56; x in S by A28, XBOOLE_0:def_5; then A30: x c= union S by ZFMISC_1:74; x c= union (S \ {(union S)}) by A28, ZFMISC_1:74; then not v in x by A14; then x c= (union S) \ {v} by A30, ZFMISC_1:34; then A31: conv x c= conv ((union S) \ {v}) by RLTOPSP1:20; y in conv x by A7, A29, A30, Th16; then A32: y in conv ((union S) \ {v}) by A31; conv ((union S) \ {v}) c= Affin ((union S) \ {v}) by RLAFFIN1:65; hence y in Affin ((union S) \ {v}) by A32; ::_thesis: verum end; then A33: Affin BSU c= Affin ((union S) \ {v}) by RLAFFIN1:51; card (union S) <> 1 by A5, A6, A24; then not BU in union S by A7, Th19; then not BU in (union S) \ {v} by XBOOLE_0:def_5; then not BU in Affin BSU by A15, A33, Th27; hence (center_of_mass V) .: S is affinely-independent Subset of V by A17, Th27; ::_thesis: verum end; end; end; end; end; A34: S1[ 0 ] proof let k be Nat; ::_thesis: ( k <= 0 implies for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V ) assume A35: k <= 0 ; ::_thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds (center_of_mass V) .: S is affinely-independent Subset of V let S be c=-linear Subset-Family of V; ::_thesis: ( card (union S) = k & union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V ) assume that A36: card (union S) = k and ( union S is finite & union S is affinely-independent ) ; ::_thesis: (center_of_mass V) .: S is affinely-independent Subset of V A37: union S = {} by A35, A36; S /\ (dom (center_of_mass V)) = {} proof assume S /\ (dom (center_of_mass V)) <> {} ; ::_thesis: contradiction then consider x being set such that A38: x in S /\ (dom (center_of_mass V)) by XBOOLE_0:def_1; x in S by A38, XBOOLE_0:def_4; then A39: x c= {} by A37, ZFMISC_1:74; x <> {} by A38, ZFMISC_1:56; hence contradiction by A39; ::_thesis: verum end; then (center_of_mass V) .: S = (center_of_mass V) .: {} by RELAT_1:112 .= {} ; hence (center_of_mass V) .: S is affinely-independent Subset of V ; ::_thesis: verum end; A40: for n being Nat holds S1[n] from NAT_1:sch_2(A34, A2); assume A41: ( union S is finite & union S is affinely-independent ) ; ::_thesis: (center_of_mass V) .: S is affinely-independent Subset of V then card (union S) is Nat ; hence (center_of_mass V) .: S is affinely-independent Subset of V by A40, A41; ::_thesis: verum end; theorem :: RLAFFIN2:30 for V being RealLinearSpace for F being c=-linear Subset-Family of V st union F is affinely-independent & union F is finite holds Int ((center_of_mass V) .: F) c= Int (union F) proof let V be RealLinearSpace; ::_thesis: for F being c=-linear Subset-Family of V st union F is affinely-independent & union F is finite holds Int ((center_of_mass V) .: F) c= Int (union F) set B = center_of_mass V; let S be c=-linear Subset-Family of V; ::_thesis: ( union S is affinely-independent & union S is finite implies Int ((center_of_mass V) .: S) c= Int (union S) ) assume A1: ( union S is affinely-independent & union S is finite ) ; ::_thesis: Int ((center_of_mass V) .: S) c= Int (union S) reconsider BS = (center_of_mass V) .: S as affinely-independent Subset of V by A1, Th29; set U = union S; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int ((center_of_mass V) .: S) or x in Int (union S) ) assume A2: x in Int ((center_of_mass V) .: S) ; ::_thesis: x in Int (union S) not BS is empty by A2; then consider y being set such that A3: y in BS by XBOOLE_0:def_1; consider X being set such that A4: X in dom (center_of_mass V) and A5: X in S and (center_of_mass V) . X = y by A3, FUNCT_1:def_6; ( X c= union S & not X is empty ) by A4, A5, ZFMISC_1:56, ZFMISC_1:74; then reconsider U = union S as non empty finite Subset of V by A1; set xBS = x |-- BS; A6: Int BS c= conv BS by Lm2; then A7: x |-- BS is convex by A2, RLAFFIN1:71; S c= bool U proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in S or s in bool U ) assume s in S ; ::_thesis: s in bool U then s c= U by ZFMISC_1:74; hence s in bool U ; ::_thesis: verum end; then A8: U in S by A5, SIMPLEX0:9; dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def_1; then U in dom (center_of_mass V) by ZFMISC_1:56; then A9: (center_of_mass V) . U in BS by A8, FUNCT_1:def_6; then reconsider BU = (center_of_mass V) . U as Element of V ; conv BS c= Affin BS by RLAFFIN1:65; then A10: Int BS c= Affin BS by A6, XBOOLE_1:1; then A11: Sum (x |-- BS) = x by A2, RLAFFIN1:def_7; then Carrier (x |-- BS) = BS by A2, A6, Th11, RLAFFIN1:71; then A12: (x |-- BS) . BU <> 0 by A9, RLVECT_2:19; then A13: (x |-- BS) . BU > 0 by A2, A6, RLAFFIN1:71; set xU = x |-- U; A14: conv U c= Affin U by RLAFFIN1:65; A15: conv ((center_of_mass V) .: S) c= conv U by Th17, CONVEX1:30; then A16: Int BS c= conv U by A6, XBOOLE_1:1; then Int BS c= Affin U by A14, XBOOLE_1:1; then A17: Sum (x |-- U) = x by A1, A2, RLAFFIN1:def_7; BS c= conv BS by RLAFFIN1:2; then A18: (center_of_mass V) . U in conv BS by A9; percases ( x = (center_of_mass V) . U or x <> BU ) ; suppose x = (center_of_mass V) . U ; ::_thesis: x in Int (union S) hence x in Int (union S) by A1, Th20; ::_thesis: verum end; suppose x <> BU ; ::_thesis: x in Int (union S) then consider p being Element of V such that A19: p in conv (BS \ {BU}) and A20: Sum (x |-- BS) = (((x |-- BS) . BU) * BU) + ((1 - ((x |-- BS) . BU)) * p) and ((1 / ((x |-- BS) . BU)) * (Sum (x |-- BS))) + ((1 - (1 / ((x |-- BS) . BU))) * p) = BU by A7, A11, A12, Th1; A21: x = ((1 - ((x |-- BS) . BU)) * p) + (((x |-- BS) . BU) * BU) by A2, A10, A20, RLAFFIN1:def_7; (x |-- BS) . BU <= 1 by A2, A6, RLAFFIN1:71; then A22: 1 - ((x |-- BS) . BU) >= 1 - 1 by XREAL_1:10; A23: BU in conv U by A15, A18; conv (BS \ {BU}) c= conv BS by RLAFFIN1:3, XBOOLE_1:36; then A24: p in conv BS by A19; then p in conv U by A15; then A25: x |-- U = ((1 - ((x |-- BS) . BU)) * (p |-- U)) + (((x |-- BS) . BU) * (BU |-- U)) by A1, A14, A21, A23, RLAFFIN1:70; A26: U c= Carrier (x |-- U) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in U or u in Carrier (x |-- U) ) assume A27: u in U ; ::_thesis: u in Carrier (x |-- U) then A28: (x |-- U) . u = (((1 - ((x |-- BS) . BU)) * (p |-- U)) . u) + ((((x |-- BS) . BU) * (BU |-- U)) . u) by A25, RLVECT_2:def_10 .= (((1 - ((x |-- BS) . BU)) * (p |-- U)) . u) + (((x |-- BS) . BU) * ((BU |-- U) . u)) by A27, RLVECT_2:def_11 .= ((1 - ((x |-- BS) . BU)) * ((p |-- U) . u)) + (((x |-- BS) . BU) * ((BU |-- U) . u)) by A27, RLVECT_2:def_11 ; ( (BU |-- U) . u = 1 / (card U) & (p |-- U) . u >= 0 ) by A1, A15, A24, A27, Th18, RLAFFIN1:71; hence u in Carrier (x |-- U) by A13, A22, A27, A28; ::_thesis: verum end; Carrier (x |-- U) c= U by RLVECT_2:def_6; then Carrier (x |-- U) = U by A26, XBOOLE_0:def_10; hence x in Int (union S) by A1, A2, A16, A17, Th12, RLAFFIN1:71; ::_thesis: verum end; end; end;