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))
proof
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
proof
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;
A20: x in Affin (@ A) by A8, A14;
A21: now :: thesis: for v being Element of V st v in @ (A /\ B) holds
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;
x in Affin (@ (A /\ B)) by A10, A12, A18, A20, RLAFFIN1:75;
hence x in conv (@ (A /\ B)) by A11, A21, RLAFFIN1:73; :: thesis: verum
end;
( conv (@ (A /\ B)) c= conv (@ A) & conv (@ (A /\ B)) c= conv (@ B) ) by RLTOPSP1:20, XBOOLE_1:17;
hence conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19; :: thesis: verum