let V be RealLinearSpace; :: thesis: for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let L1, L2 be Convex_Combination of V; :: thesis: for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let a, b be Real; :: thesis: ( a * b > 0 implies Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) )
assume a * b > 0 ; :: thesis: Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
then A1: ( not ( a >= 0 & b <= 0 ) & not ( a <= 0 & b >= 0 ) ) ;
then A2: Carrier L2 = Carrier (b * L2) by RLVECT_2:42;
A3: Carrier L1 = Carrier (a * L1) by A1, RLVECT_2:42;
for x being object st x in (Carrier (a * L1)) \/ (Carrier (b * L2)) holds
x in Carrier ((a * L1) + (b * L2))
proof
let x be object ; :: thesis: ( x in (Carrier (a * L1)) \/ (Carrier (b * L2)) implies x in Carrier ((a * L1) + (b * L2)) )
assume A4: x in (Carrier (a * L1)) \/ (Carrier (b * L2)) ; :: thesis: x in Carrier ((a * L1) + (b * L2))
now :: thesis: x in Carrier ((a * L1) + (b * L2))
per cases ( x in Carrier (a * L1) or x in Carrier (b * L2) ) by A4, XBOOLE_0:def 3;
suppose A5: x in Carrier (a * L1) ; :: thesis: x in Carrier ((a * L1) + (b * L2))
then x in { v where v is Element of V : (a * L1) . v <> 0 } by RLVECT_2:def 4;
then consider v being Element of V such that
A6: v = x and
A7: (a * L1) . v <> 0 ;
A8: L1 . v > 0 by A3, A5, A6, CONVEX1:22;
v in Carrier ((a * L1) + (b * L2))
proof
now :: thesis: v in Carrier ((a * L1) + (b * L2))
per cases ( v in Carrier L2 or not v in Carrier L2 ) ;
suppose A9: v in Carrier L2 ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then A10: L2 . v > 0 by CONVEX1:22;
now :: thesis: v in Carrier ((a * L1) + (b * L2))
per cases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;
suppose A11: ( a > 0 & b > 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then b * (L2 . v) > 0 by A10, XREAL_1:129;
then (b * L2) . v > 0 by RLVECT_2:def 11;
then A12: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29;
a * (L1 . v) > 0 by A8, A11, XREAL_1:129;
then (a * L1) . v > 0 by RLVECT_2:def 11;
then ((a * L1) + (b * L2)) . v > 0 by A12, RLVECT_2:def 10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; :: thesis: verum
end;
suppose A13: ( a < 0 & b < 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then a * (L1 . v) < 0 by A3, A5, A6, CONVEX1:22, XREAL_1:132;
then (a * L1) . v < 0 by RLVECT_2:def 11;
then A14: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30;
b * (L2 . v) < 0 by A9, A13, CONVEX1:22, XREAL_1:132;
then (b * L2) . v < 0 by RLVECT_2:def 11;
then ((a * L1) + (b * L2)) . v < 0 by A14, RLVECT_2:def 10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; :: thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; :: thesis: verum
end;
suppose not v in Carrier L2 ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then L2 . v = 0 by RLVECT_2:19;
then b * (L2 . v) = 0 ;
then (b * L2) . v = 0 by RLVECT_2:def 11;
then ((a * L1) . v) + ((b * L2) . v) = (a * L1) . v ;
then ((a * L1) + (b * L2)) . v <> 0 by A7, RLVECT_2:def 10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; :: thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; :: thesis: verum
end;
hence x in Carrier ((a * L1) + (b * L2)) by A6; :: thesis: verum
end;
suppose A15: x in Carrier (b * L2) ; :: thesis: x in Carrier ((a * L1) + (b * L2))
then x in { v where v is Element of V : (b * L2) . v <> 0 } by RLVECT_2:def 4;
then consider v being Element of V such that
A16: v = x and
A17: (b * L2) . v <> 0 ;
A18: L2 . v > 0 by A2, A15, A16, CONVEX1:22;
v in Carrier ((a * L1) + (b * L2))
proof
now :: thesis: v in Carrier ((a * L1) + (b * L2))
per cases ( v in Carrier L1 or not v in Carrier L1 ) ;
suppose A19: v in Carrier L1 ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then A20: L1 . v > 0 by CONVEX1:22;
now :: thesis: v in Carrier ((a * L1) + (b * L2))
per cases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;
suppose A21: ( a > 0 & b > 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then b * (L2 . v) > 0 by A18, XREAL_1:129;
then (b * L2) . v > 0 by RLVECT_2:def 11;
then A22: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29;
a * (L1 . v) > 0 by A20, A21, XREAL_1:129;
then (a * L1) . v > 0 by RLVECT_2:def 11;
then ((a * L1) + (b * L2)) . v > 0 by A22, RLVECT_2:def 10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; :: thesis: verum
end;
suppose A23: ( a < 0 & b < 0 ) ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then a * (L1 . v) < 0 by A19, CONVEX1:22, XREAL_1:132;
then (a * L1) . v < 0 by RLVECT_2:def 11;
then A24: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30;
b * (L2 . v) < 0 by A2, A15, A16, A23, CONVEX1:22, XREAL_1:132;
then (b * L2) . v < 0 by RLVECT_2:def 11;
then ((a * L1) + (b * L2)) . v < 0 by A24, RLVECT_2:def 10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; :: thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; :: thesis: verum
end;
suppose not v in Carrier L1 ; :: thesis: v in Carrier ((a * L1) + (b * L2))
then L1 . v = 0 by RLVECT_2:19;
then a * (L1 . v) = 0 ;
then (a * L1) . v = 0 by RLVECT_2:def 11;
then ((a * L1) . v) + ((b * L2) . v) = (b * L2) . v ;
then ((a * L1) + (b * L2)) . v <> 0 by A17, RLVECT_2:def 10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; :: thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; :: thesis: verum
end;
hence x in Carrier ((a * L1) + (b * L2)) by A16; :: thesis: verum
end;
end;
end;
hence x in Carrier ((a * L1) + (b * L2)) ; :: thesis: verum
end;
then A25: (Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2)) ;
Carrier ((a * L1) + (b * L2)) c= (Carrier (a * L1)) \/ (Carrier (b * L2)) by RLVECT_2:37;
hence Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by A25, XBOOLE_0:def 10; :: thesis: verum