:: Affine Independence in Vector Spaces
:: by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users


registration
let RLS be non empty RLSStruct ;
let A be empty Subset of RLS;
cluster conv A -> empty ;
coherence
conv A is empty
proof end;
end;

Lm1: for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A
proof end;

registration
let RLS be non empty RLSStruct ;
let A be non empty Subset of RLS;
cluster conv A -> non empty ;
coherence
not conv A is empty
proof end;
end;

theorem :: RLAFFIN1:1
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v being Element of R holds conv {v} = {v}
proof end;

theorem :: RLAFFIN1:2
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A by Lm1;

theorem Th3: :: RLAFFIN1:3
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
conv A c= conv B
proof end;

theorem :: RLAFFIN1:4
for RLS being non empty RLSStruct
for S, A being Subset of RLS st A c= conv S holds
conv S = conv (S \/ A)
proof end;

Lm2: for V being non empty right_complementable add-associative right_zeroed addLoopStr
for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
proof end;

Lm3: for S being non empty addLoopStr
for v, w being Element of S holds {(v + w)} = v + {w}
proof end;

theorem Th5: :: RLAFFIN1:5
for V being non empty add-associative addLoopStr
for A being Subset of V
for v, w being Element of V holds (v + w) + A = v + (w + A)
proof end;

theorem Th6: :: RLAFFIN1:6
for V being non empty Abelian right_zeroed addLoopStr
for A being Subset of V holds (0. V) + A = A
proof end;

Lm4: for V being non empty addLoopStr
for A being Subset of V
for v being Element of V holds card (v + A) c= card A
proof end;

theorem Th7: :: RLAFFIN1:7
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for g being Element of G
for A being Subset of G holds card A = card (g + A)
proof end;

theorem Th8: :: RLAFFIN1:8
for S being non empty addLoopStr
for v being Element of S holds v + ({} S) = {} S
proof end;

theorem Th9: :: RLAFFIN1:9
for r being Real
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
r * A c= r * B
proof end;

theorem Th10: :: RLAFFIN1:10
for r, s being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R holds (r * s) * AR = r * (s * AR)
proof end;

theorem Th11: :: RLAFFIN1:11
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R holds 1 * AR = AR
proof end;

theorem Th12: :: RLAFFIN1:12
for V being RealLinearSpace
for A being Subset of V holds 0 * A c= {(0. V)}
proof end;

theorem Th13: :: RLAFFIN1:13
for S being non empty addLoopStr
for LS1, LS2 being Linear_Combination of S
for F being FinSequence of S holds (LS1 + LS2) * F = (LS1 * F) + (LS2 * F)
proof end;

theorem Th14: :: RLAFFIN1:14
for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V
for F being FinSequence of V holds (r * L) * F = r * (L * F)
proof end;

theorem Th15: :: RLAFFIN1:15
for V being RealLinearSpace
for A, B being Subset of V st A is linearly-independent & A c= B & Lin B = V holds
ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V )
proof end;

definition
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let LG be Linear_Combination of G;
let g be Element of G;
func g + LG -> Linear_Combination of G means :Def1: :: RLAFFIN1:def 1
 for h being Element of G holds it . h = LG . (h - g);
existence
ex b1 being Linear_Combination of G st
for h being Element of G holds b1 . h = LG . (h - g)
proof end;
uniqueness
for b1, b2 being Linear_Combination of G st ( for h being Element of G holds b1 . h = LG . (h - g) ) & ( for h being Element of G holds b2 . h = LG . (h - g) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines + RLAFFIN1:def 1 :
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G
for b4 being Linear_Combination of G holds
( b4 = g + LG iff for h being Element of G holds b4 . h = LG . (h - g) );

theorem Th16: :: RLAFFIN1:16
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G holds Carrier (g + LG) = g + (Carrier LG)
proof end;

theorem Th17: :: RLAFFIN1:17
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG1, LG2 being Linear_Combination of G
for g being Element of G holds g + (LG1 + LG2) = (g + LG1) + (g + LG2)
proof end;

theorem :: RLAFFIN1:18
for r being Real
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
proof end;

theorem Th19: :: RLAFFIN1:19
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g, h being Element of G holds g + (h + LG) = (g + h) + LG
proof end;

theorem Th20: :: RLAFFIN1:20
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for g being Element of G holds g + (ZeroLC G) = ZeroLC G
proof end;

theorem Th21: :: RLAFFIN1:21
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G holds (0. G) + LG = LG
proof end;

definition
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
let LR be Linear_Combination of R;
let r be Real;
func r (*) LR -> Linear_Combination of R means :Def2: :: RLAFFIN1:def 2
 for v being Element of R holds it . v = LR . ((r ") * v) if r <> 0
otherwise it = ZeroLC R;
existence
( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) )
proof end;
uniqueness
for b1, b2 being Linear_Combination of R holds
( ( r <> 0 & ( for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds b2 . v = LR . ((r ") * v) ) implies b1 = b2 ) & ( not r <> 0 & b1 = ZeroLC R & b2 = ZeroLC R implies b1 = b2 ) )
proof end;
consistency
for b1 being Linear_Combination of R holds verum ;
end;

:: deftheorem Def2 defines (*) RLAFFIN1:def 2 :
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R
for r being Real
for b4 being Linear_Combination of R holds
( ( r <> 0 implies ( b4 = r (*) LR iff for v being Element of R holds b4 . v = LR . ((r ") * v) ) ) & ( not r <> 0 implies ( b4 = r (*) LR iff b4 = ZeroLC R ) ) );

theorem Th22: :: RLAFFIN1:22
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds Carrier (r (*) LR) c= r * (Carrier LR)
proof end;

theorem Th23: :: RLAFFIN1:23
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R st r <> 0 holds
Carrier (r (*) LR) = r * (Carrier LR)
proof end;

theorem Th24: :: RLAFFIN1:24
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
proof end;

theorem :: RLAFFIN1:25
for r, s being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)
proof end;

theorem Th26: :: RLAFFIN1:26
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds r (*) (ZeroLC R) = ZeroLC R
proof end;

theorem Th27: :: RLAFFIN1:27
for r, s being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds r (*) (s (*) LR) = (r * s) (*) LR
proof end;

theorem Th28: :: RLAFFIN1:28
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds 1 (*) LR = LR
proof end;

definition
let S be non empty addLoopStr ;
let LS be Linear_Combination of S;
func sum LS -> Real means :Def3: :: RLAFFIN1:def 3
 ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & it = Sum (LS * F) );
existence
ex b1 being Real ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b1 = Sum (LS * F) )
proof end;
uniqueness
for b1, b2 being Real st ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b1 = Sum (LS * F) ) & ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b2 = Sum (LS * F) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines sum RLAFFIN1:def 3 :
for S being non empty addLoopStr
for LS being Linear_Combination of S
for b3 being Real holds
( b3 = sum LS iff ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b3 = Sum (LS * F) ) );

theorem Th29: :: RLAFFIN1:29
for S being non empty addLoopStr
for LS being Linear_Combination of S
for F being FinSequence of S st Carrier LS misses rng F holds
Sum (LS * F) = 0
proof end;

theorem Th30: :: RLAFFIN1:30
for S being non empty addLoopStr
for LS being Linear_Combination of S
for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds
sum LS = Sum (LS * F)
proof end;

theorem Th31: :: RLAFFIN1:31
for S being non empty addLoopStr holds sum (ZeroLC S) = 0
proof end;

theorem Th32: :: RLAFFIN1:32
for S being non empty addLoopStr
for LS being Linear_Combination of S
for v being Element of S st Carrier LS c= {v} holds
sum LS = LS . v
proof end;

theorem :: RLAFFIN1:33
for S being non empty addLoopStr
for LS being Linear_Combination of S
for v1, v2 being Element of S st Carrier LS c= {v1,v2} & v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
proof end;

theorem Th34: :: RLAFFIN1:34
for S being non empty addLoopStr
for LS1, LS2 being Linear_Combination of S holds sum (LS1 + LS2) = (sum LS1) + (sum LS2)
proof end;

theorem Th35: :: RLAFFIN1:35
for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds sum (r * L) = r * (sum L)
proof end;

theorem Th36: :: RLAFFIN1:36
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds sum (L1 - L2) = (sum L1) - (sum L2)
proof end;

theorem Th37: :: RLAFFIN1:37
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G holds sum LG = sum (g + LG)
proof end;

theorem Th38: :: RLAFFIN1:38
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R st r <> 0 holds
sum LR = sum (r (*) LR)
proof end;

theorem Th39: :: RLAFFIN1:39
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)
proof end;

theorem Th40: :: RLAFFIN1:40
for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)
proof end;

definition
let V be RealLinearSpace;
let A be Subset of V;
attr A is affinely-independent means :: RLAFFIN1:def 4
( A is empty or ex v being VECTOR of V st
( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) );
end;

:: deftheorem defines affinely-independent RLAFFIN1:def 4 :
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff ( A is empty or ex v being VECTOR of V st
( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) ) );

registration
let V be RealLinearSpace;
cluster empty -> affinely-independent for Element of K19( the carrier of V);
coherence
for b1 being Subset of V st b1 is empty holds
b1 is affinely-independent ;
let v be VECTOR of V;
cluster {v} -> affinely-independent for Subset of V;
coherence
for b1 being Subset of V st b1 = {v} holds
b1 is affinely-independent
proof end;
let w be VECTOR of V;
cluster {v,w} -> affinely-independent for Subset of V;
coherence
for b1 being Subset of V st b1 = {v,w} holds
b1 is affinely-independent
proof end;
end;

registration
let V be RealLinearSpace;
cluster 1 -element affinely-independent for Element of K19( the carrier of V);
existence
ex b1 being Subset of V st
( b1 is 1 -element & b1 is affinely-independent )
proof end;
end;

Lm5: for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
proof end;

Lm6: for V being RealLinearSpace
for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) holds
for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
proof end;

theorem Th41: :: RLAFFIN1:41
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent )
proof end;

theorem Th42: :: RLAFFIN1:42
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
proof end;

theorem Th43: :: RLAFFIN1:43
for V being RealLinearSpace
for A, B being Subset of V st A is affinely-independent & B c= A holds
B is affinely-independent
proof end;

registration
let V be RealLinearSpace;
cluster linearly-independent -> affinely-independent for Element of K19( the carrier of V);
coherence
for b1 being Subset of V st b1 is linearly-independent holds
b1 is affinely-independent
proof end;
end;

registration
let V be RealLinearSpace;
let I be affinely-independent Subset of V;
let v be VECTOR of V;
cluster v + I -> affinely-independent ;
coherence
v + I is affinely-independent
proof end;
end;

theorem :: RLAFFIN1:44
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v + A is affinely-independent holds
A is affinely-independent
proof end;

registration
let V be RealLinearSpace;
let I be affinely-independent Subset of V;
let r be Real;
cluster r * I -> affinely-independent ;
coherence
r * I is affinely-independent
proof end;
end;

theorem :: RLAFFIN1:45
for r being Real
for V being RealLinearSpace
for A being Subset of V st r * A is affinely-independent & r <> 0 holds
A is affinely-independent
proof end;

theorem Th46: :: RLAFFIN1:46
for V being RealLinearSpace
for A being Subset of V st 0. V in A holds
( A is affinely-independent iff A \ {(0. V)} is linearly-independent )
proof end;

definition
let V be RealLinearSpace;
let F be Subset-Family of V;
attr F is affinely-independent means :: RLAFFIN1:def 5
 for A being Subset of V st A in F holds
A is affinely-independent ;
end;

:: deftheorem defines affinely-independent RLAFFIN1:def 5 :
for V being RealLinearSpace
for F being Subset-Family of V holds
( F is affinely-independent iff for A being Subset of V st A in F holds
A is affinely-independent );

registration
let V be RealLinearSpace;
cluster empty -> affinely-independent for Element of K19(K19( the carrier of V));
coherence
for b1 being Subset-Family of V st b1 is empty holds
b1 is affinely-independent ;
let I be affinely-independent Subset of V;
cluster {I} -> affinely-independent for Subset-Family of V;
coherence
for b1 being Subset-Family of V st b1 = {I} holds
b1 is affinely-independent by TARSKI:def 1;
end;

registration
let V be RealLinearSpace;
cluster empty affinely-independent for Element of K19(K19( the carrier of V));
existence
ex b1 being Subset-Family of V st
( b1 is empty & b1 is affinely-independent )
proof end;
cluster non empty affinely-independent for Element of K19(K19( the carrier of V));
existence
ex b1 being Subset-Family of V st
( not b1 is empty & b1 is affinely-independent )
proof end;
end;

theorem :: RLAFFIN1:47
for V being RealLinearSpace
for F1, F2 being Subset-Family of V st F1 is affinely-independent & F2 is affinely-independent holds
F1 \/ F2 is affinely-independent
proof end;

theorem :: RLAFFIN1:48
for V being RealLinearSpace
for F1, F2 being Subset-Family of V st F1 c= F2 & F2 is affinely-independent holds
F1 is affinely-independent ;

definition
let RLS be non empty RLSStruct ;
let A be Subset of RLS;
func Affin A -> Subset of RLS equals :: RLAFFIN1:def 6
 meet { B where B is Affine Subset of RLS : A c= B } ;
coherence
meet { B where B is Affine Subset of RLS : A c= B } is Subset of RLS
proof end;
end;

:: deftheorem defines Affin RLAFFIN1:def 6 :
for RLS being non empty RLSStruct
for A being Subset of RLS holds Affin A = meet { B where B is Affine Subset of RLS : A c= B } ;

registration
let RLS be non empty RLSStruct ;
let A be Subset of RLS;
cluster Affin A -> Affine ;
coherence
Affin A is Affine
proof end;
end;

Lm7: for V being non empty RLSStruct
for A being Subset of V holds A c= Affin A
proof end;

Lm8: for V being non empty RLSStruct
for A being Affine Subset of V holds A = Affin A
proof end;

registration
let RLS be non empty RLSStruct ;
let A be empty Subset of RLS;
cluster Affin A -> empty ;
coherence
Affin A is empty
proof end;
end;

registration
let RLS be non empty RLSStruct ;
let A be non empty Subset of RLS;
cluster Affin A -> non empty ;
coherence
not Affin A is empty
proof end;
end;

theorem :: RLAFFIN1:49
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= Affin A by Lm7;

theorem :: RLAFFIN1:50
for RLS being non empty RLSStruct
for A being Affine Subset of RLS holds A = Affin A by Lm8;

theorem Th51: :: RLAFFIN1:51
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B & B is Affine holds
Affin A c= B
proof end;

theorem Th52: :: RLAFFIN1:52
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
Affin A c= Affin B
proof end;

theorem Th53: :: RLAFFIN1:53
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V holds Affin (v + A) = v + (Affin A)
proof end;

theorem Th54: :: RLAFFIN1:54
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R st AR is Affine holds
r * AR is Affine
proof end;

theorem Th55: :: RLAFFIN1:55
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R st r <> 0 holds
Affin (r * AR) = r * (Affin AR)
proof end;

theorem :: RLAFFIN1:56
for r being Real
for V being RealLinearSpace
for A being Subset of V holds Affin (r * A) = r * (Affin A)
proof end;

theorem Th57: :: RLAFFIN1:57
for V being RealLinearSpace
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)))
proof end;

Lm9: for V being RealLinearSpace
for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
proof end;

theorem Th58: :: RLAFFIN1:58
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds
A = B )
proof end;

theorem Th59: :: RLAFFIN1:59
for V being RealLinearSpace
for A being Subset of V holds Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 }
proof end;

theorem Th60: :: RLAFFIN1:60
for V being RealLinearSpace
for A being Subset of V
for I being affinely-independent Subset of V st I c= A holds
ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
proof end;

theorem :: RLAFFIN1:61
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent & Affin A = Affin B & card B <= card A holds
B is affinely-independent
proof end;

theorem Th62: :: RLAFFIN1:62
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )
proof end;

theorem Th63: :: RLAFFIN1:63
for x being set
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
L . x <= 1
proof end;

reconsider jj = 1 as Real ;

theorem Th64: :: RLAFFIN1:64
for x being set
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex & L . x = 1 holds
Carrier L = {x}
proof end;

theorem Th65: :: RLAFFIN1:65
for V being RealLinearSpace
for A being Subset of V holds conv A c= Affin A
proof end;

theorem :: RLAFFIN1:66
for x being set
for V being RealLinearSpace
for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds
x in A
proof end;

theorem Th67: :: RLAFFIN1:67
for V being RealLinearSpace
for A being Subset of V holds Affin (conv A) = Affin A
proof end;

theorem :: RLAFFIN1:68
for V being RealLinearSpace
for A, B being Subset of V st conv A c= conv B holds
Affin A c= Affin B
proof end;

theorem Th69: :: RLAFFIN1:69
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= Affin B holds
Affin (A \/ B) = Affin B
proof end;

definition
let V be RealLinearSpace;
let A be Subset of V;
assume A1: A is affinely-independent ;
let x be object ;
assume A2: x in Affin A ;
func x |-- A -> Linear_Combination of A means :Def7: :: RLAFFIN1:def 7
( Sum it = x & sum it = 1 );
existence
ex b1 being Linear_Combination of A st
( Sum b1 = x & sum b1 = 1 )
proof end;
uniqueness
for b1, b2 being Linear_Combination of A st Sum b1 = x & sum b1 = 1 & Sum b2 = x & sum b2 = 1 holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines |-- RLAFFIN1:def 7 :
for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for x being object st x in Affin A holds
for b4 being Linear_Combination of A holds
( b4 = x |-- A iff ( Sum b4 = x & sum b4 = 1 ) );

theorem Th70: :: RLAFFIN1:70
for r being Real
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
proof end;

theorem Th71: :: RLAFFIN1:71
for x being set
for V being RealLinearSpace
for v being VECTOR of V
for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
proof end;

theorem Th72: :: RLAFFIN1:72
for x, y being set
for V being RealLinearSpace
for I being affinely-independent Subset of V st x in conv I holds
( (x |-- I) . y = 1 iff ( x = y & x in I ) )
proof end;

theorem Th73: :: RLAFFIN1:73
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ) holds
x in conv I
proof end;

theorem :: RLAFFIN1:74
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V st x in I holds
(conv I) \ {x} is convex
proof end;

theorem Th75: :: RLAFFIN1:75
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
proof end;

theorem :: RLAFFIN1:76
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
proof end;

theorem Th77: :: RLAFFIN1:77
for x being set
for V being RealLinearSpace
for B being Subset of V
for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
proof end;

theorem Th78: :: RLAFFIN1:78
for r, s being Real
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for A being Subset of V st v1 in Affin A & v2 in Affin A & r + s = 1 holds
(r * v1) + (s * v2) in Affin A
proof end;

theorem Th79: :: RLAFFIN1:79
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B holds
card A <= card B
proof end;

theorem :: RLAFFIN1:80
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B & card A = card B holds
B is affinely-independent
proof end;

theorem :: RLAFFIN1:81
for r, s being Real
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
proof end;

theorem :: RLAFFIN1:82
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
proof end;

theorem :: RLAFFIN1:83
for r, s being Real
for V being RealLinearSpace
for v1, v2, w being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
proof end;

theorem :: RLAFFIN1:84
for r being Real
for V being RealLinearSpace
for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
proof end;