let r be Real; :: thesis: for V being RealLinearSpace

for A being Subset of V holds Affin (r * A) = r * (Affin A)

let V be RealLinearSpace; :: thesis: for A being Subset of V holds Affin (r * A) = r * (Affin A)

let A be Subset of V; :: thesis: Affin (r * A) = r * (Affin A)

for A being Subset of V holds Affin (r * A) = r * (Affin A)

let V be RealLinearSpace; :: thesis: for A being Subset of V holds Affin (r * A) = r * (Affin A)

let A be Subset of V; :: thesis: Affin (r * A) = r * (Affin A)

per cases
( r = 0 or r <> 0 )
;

end;

suppose A1:
r = 0
; :: thesis: Affin (r * A) = r * (Affin A)

then A2:
r * (Affin A) c= {(0. V)}
by Th12;

A3: r * (Affin A) c= r * A

then A7: ( r * A is empty or r * A = {(0. V)} ) by ZFMISC_1:33;

{(0. V)} is Affine by RUSUB_4:23;

then A8: Affin (r * A) = r * A by A7, Lm8;

r * A c= r * (Affin A) by Lm7, Th9;

hence Affin (r * A) = r * (Affin A) by A3, A8; :: thesis: verum

end;A3: r * (Affin A) c= r * A

proof

r * A c= {(0. V)}
by A1, Th12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (Affin A) or x in r * A )

assume A4: x in r * (Affin A) ; :: thesis: x in r * A

then ex v being Element of V st

( x = r * v & v in Affin A ) ;

then not A is empty ;

then consider v being object such that

A5: v in A ;

reconsider v = v as Element of V by A5;

A6: r * v in r * A by A5;

x = 0. V by A2, A4, TARSKI:def 1;

hence x in r * A by A1, A6, RLVECT_1:10; :: thesis: verum

end;assume A4: x in r * (Affin A) ; :: thesis: x in r * A

then ex v being Element of V st

( x = r * v & v in Affin A ) ;

then not A is empty ;

then consider v being object such that

A5: v in A ;

reconsider v = v as Element of V by A5;

A6: r * v in r * A by A5;

x = 0. V by A2, A4, TARSKI:def 1;

hence x in r * A by A1, A6, RLVECT_1:10; :: thesis: verum

then A7: ( r * A is empty or r * A = {(0. V)} ) by ZFMISC_1:33;

{(0. V)} is Affine by RUSUB_4:23;

then A8: Affin (r * A) = r * A by A7, Lm8;

r * A c= r * (Affin A) by Lm7, Th9;

hence Affin (r * A) = r * (Affin A) by A3, A8; :: thesis: verum