let V be RealLinearSpace; :: thesis: for L1, L2 being circled_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 circled_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))

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, Th17;
v in Carrier ((a * L1) + (b * L2))

proof

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

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

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 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, Th17;
v in Carrier ((a * L1) + (b * L2))

proof

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

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

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 x in Carrier ((a * L1) + (b * L2)) by A16; :: thesis: verum

end;

end;

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; :: thesis: verum