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))

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

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

then A25:
(Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2))
;
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))

end;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))end;

hence
x in Carrier ((a * L1) + (b * L2))
; :: thesis: verumper cases
( x in Carrier (a * L1) or x in Carrier (b * L2) )
by A4, XBOOLE_0:def 3;

end;

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))

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

end;

hence
x in Carrier ((a * L1) + (b * L2))
by A6; :: thesis: verumnow :: thesis: v in Carrier ((a * L1) + (b * L2))end;

hence
v in Carrier ((a * L1) + (b * L2))
; :: thesis: verumper cases
( v in Carrier L2 or not v in Carrier L2 )
;

end;

suppose A9:
v in Carrier L2
; :: thesis: v in Carrier ((a * L1) + (b * L2))

then A10:
L2 . v > 0
by CONVEX1:22;

end;now :: thesis: v in Carrier ((a * L1) + (b * L2))end;

hence
v in Carrier ((a * L1) + (b * L2))
; :: thesis: verumper cases
( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )
by A1;

end;

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

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

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

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))

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

end;

hence
x in Carrier ((a * L1) + (b * L2))
by A16; :: thesis: verumnow :: thesis: v in Carrier ((a * L1) + (b * L2))end;

hence
v in Carrier ((a * L1) + (b * L2))
; :: thesis: verumper cases
( v in Carrier L1 or not v in Carrier L1 )
;

end;

suppose A19:
v in Carrier L1
; :: thesis: v in Carrier ((a * L1) + (b * L2))

then A20:
L1 . v > 0
by CONVEX1:22;

end;now :: thesis: v in Carrier ((a * L1) + (b * L2))end;

hence
v in Carrier ((a * L1) + (b * L2))
; :: thesis: verumper cases
( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )
by A1;

end;

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

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

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

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