let V be RealLinearSpace; :: thesis: for A being non empty Affine Subset of V st 0. V in A holds
( A is Subspace-like & A = the carrier of (Lin A) )
let A be non empty Affine Subset of V; :: thesis: ( 0. V in A implies ( A is Subspace-like & A = the carrier of (Lin A) ) )
assume A1: 0. V in A ; :: thesis: ( A is Subspace-like & A = the carrier of (Lin A) )
A2: for x, y being Element of V
for a being Real st x in A & y in A holds
( x + y in A & a * x in A )
proof
let x, y be Element of V; :: thesis: for a being Real st x in A & y in A holds
( x + y in A & a * x in A )
let a be Real; :: thesis: ( x in A & y in A implies ( x + y in A & a * x in A ) )
assume that
A3: x in A and
A4: y in A ; :: thesis: ( x + y in A & a * x in A )
reconsider x = x, y = y as VECTOR of V ;
A5: 2 * (((1 - (1 / 2)) * x) + ((1 / 2) * y)) = (2 * ((1 - (1 / 2)) * x)) + (2 * ((1 / 2) * y)) by RLVECT_1:def 5
.= ((2 * (1 - (1 / 2))) * x) + (2 * ((1 / 2) * y)) by RLVECT_1:def 7
.= ((2 - 1) * x) + ((2 * (1 / 2)) * y) by RLVECT_1:def 7
.= x + (1 * y) by RLVECT_1:def 8
.= x + y by RLVECT_1:def 8 ;
((1 - (1 / 2)) * x) + ((1 / 2) * y) in A by A3, A4, Def4;
hence ( x + y in A & a * x in A ) by A1, A3, A5, Th25; :: thesis: verum
end;
hence A is Subspace-like by A1; :: thesis: A = the carrier of (Lin A)
for x being object st x in the carrier of (Lin A) holds
x in A
proof
let x be object ; :: thesis: ( x in the carrier of (Lin A) implies x in A )
assume x in the carrier of (Lin A) ; :: thesis: x in A
then x in Lin A ;
then A6: ex l being Linear_Combination of A st x = Sum l by RLVECT_3:14;
( ( for v, u being VECTOR of V st v in A & u in A holds
v + u in A ) & ( for a being Real
for v being VECTOR of V st v in A holds
a * v in A ) ) by A2;
then A is linearly-closed by RLSUB_1:def 1;
hence x in A by A6, RLVECT_2:29; :: thesis: verum
end;
then A7: the carrier of (Lin A) c= A ;
for x being object st x in A holds
x in the carrier of (Lin A) by RLVECT_3:15, STRUCT_0:def 5;
then A c= the carrier of (Lin A) ;
hence A = the carrier of (Lin A) by A7; :: thesis: verum