let V be non empty Abelian add-associative RealLinearSpace-like RLSStruct ; :: thesis: for M, N being Affine Subset of V holds M + N is Affine
let M, N be Affine Subset of V; :: thesis: M + N is Affine
for x, y being VECTOR of V
for a being Real st x in M + N & y in M + N holds
((1 - a) * x) + (a * y) in M + N
proof
let x,
y be
VECTOR of
V;
:: thesis: for a being Real st x in M + N & y in M + N holds
((1 - a) * x) + (a * y) in M + Nlet a be
Real;
:: thesis: ( x in M + N & y in M + N implies ((1 - a) * x) + (a * y) in M + N )
assume A1:
(
x in M + N &
y in M + N )
;
:: thesis: ((1 - a) * x) + (a * y) in M + N
then consider u1,
v1 being
Element of
V such that A2:
(
x = u1 + v1 &
u1 in M &
v1 in N )
;
consider u2,
v2 being
Element of
V such that A3:
(
y = u2 + v2 &
u2 in M &
v2 in N )
by A1;
A4:
((1 - a) * u1) + (a * u2) in M
by A2, A3, Def5;
A5:
((1 - a) * v1) + (a * v2) in N
by A2, A3, Def5;
((1 - a) * x) + (a * y) =
(((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2))
by A2, A3, RLVECT_1:def 9
.=
(((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2))
by RLVECT_1:def 9
.=
((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2)
by RLVECT_1:def 6
.=
(((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2)
by RLVECT_1:def 6
.=
(((1 - a) * u1) + (a * u2)) + (((1 - a) * v1) + (a * v2))
by RLVECT_1:def 6
;
hence
((1 - a) * x) + (a * y) in M + N
by A4, A5;
:: thesis: verum
end;
hence
M + N is Affine
by Def5; :: thesis: verum