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 )

for x being object st x in the carrier of (Lin A) holds

x in 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

( 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

hence
A is Subspace-like
by A1; :: thesis: A = the carrier of (Lin A)
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;( 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

for x being object st x in the carrier of (Lin A) holds

x in A

proof

then A7:
the carrier of (Lin A) c= A
;
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;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

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