set C = Complex_of {I};
let A, B be Subset of (); :: 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 () = bool I by SIMPLEX0:4;
A4: B in the topology of () by A2;
A5: A /\ B c= A by XBOOLE_1:17;
A6: @ A is affinely-independent by ;
A7: conv (@ B) c= Affin (@ B) by RLAFFIN1:65;
A8: conv (@ A) c= Affin (@ A) by RLAFFIN1:65;
A9: A in the topology of () by A1;
then A10: Affin (@ A) c= Affin I by ;
A11: @ (A /\ B) is affinely-independent by ;
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
.= 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 ;
x in conv (@ B) by ;
then A16: x |-- (@ B) = x |-- I by ;
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 ;
hence (x |-- I) . y = 0 by ; :: thesis: verum
end;
A20: x in Affin (@ A) by ;
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 ;
hence 0 <= (x |-- (@ (A /\ B))) . v by ; :: thesis: verum
end;
x in Affin (@ (A /\ B)) by ;
hence x in conv (@ (A /\ B)) by ; :: thesis: verum
end;
( conv (@ (A /\ B)) c= conv (@ A) & conv (@ (A /\ B)) c= conv (@ B) ) by ;
hence conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19; :: thesis: verum