let V be RealLinearSpace; 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; 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 )
;
suppose
not
A is
empty
;
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 }
XBOOLE_0:def 10 { (Sum L) where L is Linear_Combination of A : sum L = 1 } c= Affin Aproof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end; let x be
object ;
TARSKI:def 3 ( not x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } or x in Affin A )assume
x in { (Sum L) where L is Linear_Combination of A : sum L = 1 }
;
x in Affin Athen 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;
verum end;