set C = Complex_of {I};

let A, B be Subset of (Complex_of {I}); :: according to SIMPLEX1:def 8 :: thesis: ( A is simplex-like & B is simplex-like implies (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) )

assume that

A1: A is simplex-like and

A2: B is simplex-like ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))

A3: the topology of (Complex_of {I}) = bool I by SIMPLEX0:4;

A4: B in the topology of (Complex_of {I}) by A2;

A5: A /\ B c= A by XBOOLE_1:17;

A6: @ A is affinely-independent by A1, Def7;

A7: conv (@ B) c= Affin (@ B) by RLAFFIN1:65;

A8: conv (@ A) c= Affin (@ A) by RLAFFIN1:65;

A9: A in the topology of (Complex_of {I}) by A1;

then A10: Affin (@ A) c= Affin I by A3, RLAFFIN1:52;

A11: @ (A /\ B) is affinely-independent by A1, Def7;

thus (conv (@ A)) /\ (conv (@ B)) c= conv (@ (A /\ B)) :: according to XBOOLE_0:def 10 :: thesis: conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B))

hence conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19; :: thesis: verum

let A, B be Subset of (Complex_of {I}); :: according to SIMPLEX1:def 8 :: thesis: ( A is simplex-like & B is simplex-like implies (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) )

assume that

A1: A is simplex-like and

A2: B is simplex-like ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))

A3: the topology of (Complex_of {I}) = bool I by SIMPLEX0:4;

A4: B in the topology of (Complex_of {I}) by A2;

A5: A /\ B c= A by XBOOLE_1:17;

A6: @ A is affinely-independent by A1, Def7;

A7: conv (@ B) c= Affin (@ B) by RLAFFIN1:65;

A8: conv (@ A) c= Affin (@ A) by RLAFFIN1:65;

A9: A in the topology of (Complex_of {I}) by A1;

then A10: Affin (@ A) c= Affin I by A3, RLAFFIN1:52;

A11: @ (A /\ B) is affinely-independent by A1, Def7;

thus (conv (@ A)) /\ (conv (@ B)) c= conv (@ (A /\ B)) :: according to XBOOLE_0:def 10 :: thesis: conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B))

proof

( conv (@ (A /\ B)) c= conv (@ A) & conv (@ (A /\ B)) c= conv (@ B) )
by RLTOPSP1:20, XBOOLE_1:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (conv (@ A)) /\ (conv (@ B)) or x in conv (@ (A /\ B)) )

set IAB = I \ (@ (A /\ B));

A12: @ (A /\ B) = I /\ (@ (A /\ B)) by A3, A5, A9, XBOOLE_1:1, XBOOLE_1:28

.= I \ (I \ (@ (A /\ B))) by XBOOLE_1:48 ;

assume A13: x in (conv (@ A)) /\ (conv (@ B)) ; :: thesis: x in conv (@ (A /\ B))

then A14: x in conv (@ A) by XBOOLE_0:def 4;

then A15: x |-- (@ A) = x |-- I by A3, A8, A9, RLAFFIN1:77;

x in conv (@ B) by A13, XBOOLE_0:def 4;

then A16: x |-- (@ B) = x |-- I by A3, A4, A7, RLAFFIN1:77;

A17: ( Carrier (x |-- (@ A)) c= A & Carrier (x |-- (@ B)) c= B ) by RLVECT_2:def 6;

A18: for y being set st y in I \ (@ (A /\ B)) holds

(x |-- I) . y = 0

hence x in conv (@ (A /\ B)) by A11, A21, RLAFFIN1:73; :: thesis: verum

end;set IAB = I \ (@ (A /\ B));

A12: @ (A /\ B) = I /\ (@ (A /\ B)) by A3, A5, A9, XBOOLE_1:1, XBOOLE_1:28

.= I \ (I \ (@ (A /\ B))) by XBOOLE_1:48 ;

assume A13: x in (conv (@ A)) /\ (conv (@ B)) ; :: thesis: x in conv (@ (A /\ B))

then A14: x in conv (@ A) by XBOOLE_0:def 4;

then A15: x |-- (@ A) = x |-- I by A3, A8, A9, RLAFFIN1:77;

x in conv (@ B) by A13, XBOOLE_0:def 4;

then A16: x |-- (@ B) = x |-- I by A3, A4, A7, RLAFFIN1:77;

A17: ( Carrier (x |-- (@ A)) c= A & Carrier (x |-- (@ B)) c= B ) by RLVECT_2:def 6;

A18: for y being set st y in I \ (@ (A /\ B)) holds

(x |-- I) . y = 0

proof

A20:
x in Affin (@ A)
by A8, A14;
let y be set ; :: thesis: ( y in I \ (@ (A /\ B)) implies (x |-- I) . y = 0 )

assume A19: y in I \ (@ (A /\ B)) ; :: thesis: (x |-- I) . y = 0

then not y in A /\ B by XBOOLE_0:def 5;

then ( not y in Carrier (x |-- (@ A)) or not y in Carrier (x |-- (@ B)) ) by A17, XBOOLE_0:def 4;

hence (x |-- I) . y = 0 by A15, A16, A19; :: thesis: verum

end;assume A19: y in I \ (@ (A /\ B)) ; :: thesis: (x |-- I) . y = 0

then not y in A /\ B by XBOOLE_0:def 5;

then ( not y in Carrier (x |-- (@ A)) or not y in Carrier (x |-- (@ B)) ) by A17, XBOOLE_0:def 4;

hence (x |-- I) . y = 0 by A15, A16, A19; :: thesis: verum

A21: now :: thesis: for v being Element of V st v in @ (A /\ B) holds

0 <= (x |-- (@ (A /\ B))) . v

x in Affin (@ (A /\ B))
by A10, A12, A18, A20, RLAFFIN1:75;0 <= (x |-- (@ (A /\ B))) . v

let v be Element of V; :: thesis: ( v in @ (A /\ B) implies 0 <= (x |-- (@ (A /\ B))) . v )

assume v in @ (A /\ B) ; :: thesis: 0 <= (x |-- (@ (A /\ B))) . v

0 <= (x |-- (@ A)) . v by A6, A14, RLAFFIN1:71;

hence 0 <= (x |-- (@ (A /\ B))) . v by A10, A12, A15, A18, A20, RLAFFIN1:75; :: thesis: verum

end;assume v in @ (A /\ B) ; :: thesis: 0 <= (x |-- (@ (A /\ B))) . v

0 <= (x |-- (@ A)) . v by A6, A14, RLAFFIN1:71;

hence 0 <= (x |-- (@ (A /\ B))) . v by A10, A12, A15, A18, A20, RLAFFIN1:75; :: thesis: verum

hence x in conv (@ (A /\ B)) by A11, A21, RLAFFIN1:73; :: thesis: verum

hence conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19; :: thesis: verum