let V be RealLinearSpace; :: thesis: for A being Subset of V holds Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 }

let A be Subset of V; :: thesis: Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 }

set S = { (Sum L) where L is Linear_Combination of A : sum L = 1 } ;

let A be Subset of V; :: thesis: Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 }

set S = { (Sum L) where L is Linear_Combination of A : sum L = 1 } ;

per cases
( A is empty or not A is empty )
;

end;

suppose A1:
A is empty
; :: thesis: Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 }

assume
Affin A <> { (Sum L) where L is Linear_Combination of A : sum L = 1 }
; :: thesis: contradiction

then not { (Sum L) where L is Linear_Combination of A : sum L = 1 } is empty by A1;

then consider x being object such that

A2: x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } ;

consider L being Linear_Combination of A such that

x = Sum L and

A3: sum L = 1 by A2;

A = {} the carrier of V by A1;

then L = ZeroLC V by RLVECT_2:23;

hence contradiction by A3, Th31; :: thesis: verum

end;then not { (Sum L) where L is Linear_Combination of A : sum L = 1 } is empty by A1;

then consider x being object such that

A2: x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } ;

consider L being Linear_Combination of A such that

x = Sum L and

A3: sum L = 1 by A2;

A = {} the carrier of V by A1;

then L = ZeroLC V by RLVECT_2:23;

hence contradiction by A3, Th31; :: thesis: verum

suppose
not A is empty
; :: thesis: Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 }

then consider p being object such that

A4: p in A ;

reconsider p = p as Element of V by A4;

A c= Affin A by Lm7;

then A5: Affin A = p + (Up (Lin ((- p) + A))) by A4, Th57;

thus Affin A c= { (Sum L) where L is Linear_Combination of A : sum L = 1 } :: according to XBOOLE_0:def 10 :: thesis: { (Sum L) where L is Linear_Combination of A : sum L = 1 } c= Affin A

assume x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } ; :: thesis: x in Affin A

then consider L being Linear_Combination of A such that

A18: Sum L = x and

A19: sum L = 1 ;

set pL = (- p) + L;

Carrier L c= A by RLVECT_2:def 6;

then A20: (- p) + (Carrier L) c= (- p) + A by RLTOPSP1:8;

(- p) + (Carrier L) = Carrier ((- p) + L) by Th16;

then (- p) + L is Linear_Combination of (- p) + A by A20, RLVECT_2:def 6;

then Sum ((- p) + L) in Lin ((- p) + A) by RLVECT_3:14;

then A21: Sum ((- p) + L) in Up (Lin ((- p) + A)) ;

p + (Sum ((- p) + L)) = p + ((1 * (- p)) + (Sum L)) by A19, Th39

.= p + ((- p) + (Sum L)) by RLVECT_1:def 8

.= (p + (- p)) + (Sum L) by RLVECT_1:def 3

.= (0. V) + (Sum L) by RLVECT_1:5

.= x by A18 ;

hence x in Affin A by A5, A21; :: thesis: verum

end;A4: p in A ;

reconsider p = p as Element of V by A4;

A c= Affin A by Lm7;

then A5: Affin A = p + (Up (Lin ((- p) + A))) by A4, Th57;

thus Affin A c= { (Sum L) where L is Linear_Combination of A : sum L = 1 } :: according to XBOOLE_0:def 10 :: thesis: { (Sum L) where L is Linear_Combination of A : sum L = 1 } c= Affin A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } or x in Affin A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Affin A or x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } )

assume x in Affin A ; :: thesis: x in { (Sum L) where L is Linear_Combination of A : sum L = 1 }

then consider v being VECTOR of V such that

A6: x = p + v and

A7: v in Up (Lin ((- p) + A)) by A5;

v in Lin ((- p) + A) by A7;

then consider L being Linear_Combination of (- p) + A such that

A8: Sum L = v by RLVECT_3:14;

set pL = p + L;

consider Lp being Linear_Combination of {(0. V)} such that

A9: Lp . (0. V) = 1 - (sum L) by RLVECT_4:37;

set pLL = p + (L + Lp);

set pLp = p + Lp;

A10: Carrier Lp c= {(0. V)} by RLVECT_2:def 6;

then A11: p + (Carrier Lp) c= p + {(0. V)} by RLTOPSP1:8;

A12: ( Carrier (p + L) = p + (Carrier L) & Carrier L c= (- p) + A ) by Th16, RLVECT_2:def 6;

p + ((- p) + A) = (p + (- p)) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

then A13: Carrier (p + L) c= A by A12, RLTOPSP1:8;

A14: ( Carrier ((p + L) + (p + Lp)) c= (Carrier (p + L)) \/ (Carrier (p + Lp)) & p + (L + Lp) = (p + L) + (p + Lp) ) by Th17, RLVECT_2:37;

( Carrier (p + Lp) = p + (Carrier Lp) & p + {(0. V)} = {(p + (0. V))} ) by Lm3, Th16;

then Carrier (p + Lp) c= {p} by A11;

then (Carrier (p + L)) \/ (Carrier (p + Lp)) c= A \/ {p} by A13, XBOOLE_1:13;

then Carrier (p + (L + Lp)) c= A \/ {p} by A14;

then Carrier (p + (L + Lp)) c= A by A4, ZFMISC_1:40;

then A15: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def 6;

A16: sum (p + (L + Lp)) = sum (L + Lp) by Th37;

A17: sum (L + Lp) = (sum L) + (sum Lp) by Th34

.= (sum L) + (1 - (sum L)) by A9, A10, Th32

.= 1 ;

then Sum (p + (L + Lp)) = (1 * p) + (Sum (L + Lp)) by Th39

.= (1 * p) + (v + (Sum Lp)) by A8, RLVECT_3:1

.= (1 * p) + (v + ((Lp . (0. V)) * (0. V))) by RLVECT_2:32

.= (1 * p) + (v + (0. V))

.= p + (v + (0. V)) by RLVECT_1:def 8

.= x by A6 ;

hence x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } by A15, A16, A17; :: thesis: verum

end;assume x in Affin A ; :: thesis: x in { (Sum L) where L is Linear_Combination of A : sum L = 1 }

then consider v being VECTOR of V such that

A6: x = p + v and

A7: v in Up (Lin ((- p) + A)) by A5;

v in Lin ((- p) + A) by A7;

then consider L being Linear_Combination of (- p) + A such that

A8: Sum L = v by RLVECT_3:14;

set pL = p + L;

consider Lp being Linear_Combination of {(0. V)} such that

A9: Lp . (0. V) = 1 - (sum L) by RLVECT_4:37;

set pLL = p + (L + Lp);

set pLp = p + Lp;

A10: Carrier Lp c= {(0. V)} by RLVECT_2:def 6;

then A11: p + (Carrier Lp) c= p + {(0. V)} by RLTOPSP1:8;

A12: ( Carrier (p + L) = p + (Carrier L) & Carrier L c= (- p) + A ) by Th16, RLVECT_2:def 6;

p + ((- p) + A) = (p + (- p)) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

then A13: Carrier (p + L) c= A by A12, RLTOPSP1:8;

A14: ( Carrier ((p + L) + (p + Lp)) c= (Carrier (p + L)) \/ (Carrier (p + Lp)) & p + (L + Lp) = (p + L) + (p + Lp) ) by Th17, RLVECT_2:37;

( Carrier (p + Lp) = p + (Carrier Lp) & p + {(0. V)} = {(p + (0. V))} ) by Lm3, Th16;

then Carrier (p + Lp) c= {p} by A11;

then (Carrier (p + L)) \/ (Carrier (p + Lp)) c= A \/ {p} by A13, XBOOLE_1:13;

then Carrier (p + (L + Lp)) c= A \/ {p} by A14;

then Carrier (p + (L + Lp)) c= A by A4, ZFMISC_1:40;

then A15: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def 6;

A16: sum (p + (L + Lp)) = sum (L + Lp) by Th37;

A17: sum (L + Lp) = (sum L) + (sum Lp) by Th34

.= (sum L) + (1 - (sum L)) by A9, A10, Th32

.= 1 ;

then Sum (p + (L + Lp)) = (1 * p) + (Sum (L + Lp)) by Th39

.= (1 * p) + (v + (Sum Lp)) by A8, RLVECT_3:1

.= (1 * p) + (v + ((Lp . (0. V)) * (0. V))) by RLVECT_2:32

.= (1 * p) + (v + (0. V))

.= p + (v + (0. V)) by RLVECT_1:def 8

.= x by A6 ;

hence x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } by A15, A16, A17; :: thesis: verum

assume x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } ; :: thesis: x in Affin A

then consider L being Linear_Combination of A such that

A18: Sum L = x and

A19: sum L = 1 ;

set pL = (- p) + L;

Carrier L c= A by RLVECT_2:def 6;

then A20: (- p) + (Carrier L) c= (- p) + A by RLTOPSP1:8;

(- p) + (Carrier L) = Carrier ((- p) + L) by Th16;

then (- p) + L is Linear_Combination of (- p) + A by A20, RLVECT_2:def 6;

then Sum ((- p) + L) in Lin ((- p) + A) by RLVECT_3:14;

then A21: Sum ((- p) + L) in Up (Lin ((- p) + A)) ;

p + (Sum ((- p) + L)) = p + ((1 * (- p)) + (Sum L)) by A19, Th39

.= p + ((- p) + (Sum L)) by RLVECT_1:def 8

.= (p + (- p)) + (Sum L) by RLVECT_1:def 3

.= (0. V) + (Sum L) by RLVECT_1:5

.= x by A18 ;

hence x in Affin A by A5, A21; :: thesis: verum