let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for A being Subset of V st v in Affin A holds
Affin A = v + (Up (Lin ((- v) + A)))
let v be VECTOR of V; :: thesis: for A being Subset of V st v in Affin A holds
Affin A = v + (Up (Lin ((- v) + A)))
let A be Subset of V; :: thesis: ( v in Affin A implies Affin A = v + (Up (Lin ((- v) + A))) )
set vA = (- v) + A;
set BB = { B where B is Affine Subset of V : (- v) + A c= B } ;
A1: (- v) + A c= Up (Lin ((- v) + A))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- v) + A or x in Up (Lin ((- v) + A)) )
assume x in (- v) + A ; :: thesis: x in Up (Lin ((- v) + A))
then x in Lin ((- v) + A) by RLVECT_3:15;
hence x in Up (Lin ((- v) + A)) ; :: thesis: verum
end;
Up (Lin ((- v) + A)) is Affine by RUSUB_4:24;
then A2: Up (Lin ((- v) + A)) in { B where B is Affine Subset of V : (- v) + A c= B } by A1;
then A3: Affin ((- v) + A) c= Up (Lin ((- v) + A)) by SETFAM_1:3;
assume v in Affin A ; :: thesis: Affin A = v + (Up (Lin ((- v) + A)))
then (- v) + v in (- v) + (Affin A) ;
then A4: 0. V in (- v) + (Affin A) by RLVECT_1:5;
now :: thesis: for Y being set st Y in { B where B is Affine Subset of V : (- v) + A c= B } holds
Up (Lin ((- v) + A)) c= Y
let Y be set ; :: thesis: ( Y in { B where B is Affine Subset of V : (- v) + A c= B } implies Up (Lin ((- v) + A)) c= Y )
A5: Affin ((- v) + A) = (- v) + (Affin A) by Th53;
assume Y in { B where B is Affine Subset of V : (- v) + A c= B } ; :: thesis: Up (Lin ((- v) + A)) c= Y
then consider B being Affine Subset of V such that
A6: Y = B and
A7: (- v) + A c= B ;
A8: Lin ((- v) + A) is Subspace of Lin B by A7, RLVECT_3:20;
Affin ((- v) + A) c= B by A7, Th51;
then B = the carrier of (Lin B) by A4, A5, RUSUB_4:26;
hence Up (Lin ((- v) + A)) c= Y by A6, A8, RLSUB_1:def 2; :: thesis: verum
end;
then Up (Lin ((- v) + A)) c= Affin ((- v) + A) by A2, SETFAM_1:5;
then Up (Lin ((- v) + A)) = Affin ((- v) + A) by A3;
hence v + (Up (Lin ((- v) + A))) = v + ((- v) + (Affin A)) by Th53
.= (v + (- v)) + (Affin A) by Th5
.= (0. V) + (Affin A) by RLVECT_1:5
.= Affin A by Th6 ;
:: thesis: verum