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

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

per cases
( L . v = 0 or L . v <> 0 )
;

end;

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

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