:: 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;