:: 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 b₁ being Linear_Combination of G st
for h being Element of G holds b₁ . h = LG . (h - g)

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of G st ( for h being Element of G holds b₁ . h = LG . (h - g) ) & ( for h being Element of G holds b₂ . h = LG . (h - g) ) holds
b₁ = b₂

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 b₄ being Linear_Combination of G holds
( b₄ = g + LG iff for h being Element of G holds b₄ . 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 b₁ being Linear_Combination of R st
for v being Element of R holds b₁ . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b₁ being Linear_Combination of R st b₁ = ZeroLC R ) )

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of R holds
( ( r <> 0 & ( for v being Element of R holds b₁ . v = LR . ((r ") * v) ) & ( for v being Element of R holds b₂ . v = LR . ((r ") * v) ) implies b₁ = b₂ ) & ( not r <> 0 & b₁ = ZeroLC R & b₂ = ZeroLC R implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₄ being Linear_Combination of R holds
( ( r <> 0 implies ( b₄ = r (*) LR iff for v being Element of R holds b₄ . v = LR . ((r ") * v) ) ) & ( not r <> 0 implies ( b₄ = r (*) LR iff b₄ = 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 b₁ being Real ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b₁ = Sum (LS * F) )

proof end;

uniqueness
for b₁, b₂ being Real st ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b₁ = Sum (LS * F) ) & ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b₂ = Sum (LS * F) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines sum RLAFFIN1:def 3 :
for S being non empty addLoopStr
for LS being Linear_Combination of S
for b₃ being Real holds
( b₃ = sum LS iff ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b₃ = 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 b₁ being Subset of V st b₁ is empty holds
b₁ is affinely-independent ;
let v be VECTOR of V;

cluster {v} -> affinely-independent for Subset of V;

coherence
for b₁ being Subset of V st b₁ = {v} holds
b₁ is affinely-independent

proof end;

let w be VECTOR of V;

cluster {v,w} -> affinely-independent for Subset of V;

coherence
for b₁ being Subset of V st b₁ = {v,w} holds
b₁ 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 b₁ being Subset of V st
( b₁ is 1 -element & b₁ 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 b₁ being Subset of V st b₁ is linearly-independent holds
b₁ 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 b₁ being Subset-Family of V st b₁ is empty holds
b₁ is affinely-independent ;
let I be affinely-independent Subset of V;

cluster {I} -> affinely-independent for Subset-Family of V;

coherence
for b₁ being Subset-Family of V st b₁ = {I} holds
b₁ 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 b₁ being Subset-Family of V st
( b₁ is empty & b₁ is affinely-independent )

proof end;

cluster non empty affinely-independent for Element of K19(K19( the carrier of V));

existence
ex b₁ being Subset-Family of V st
( not b₁ is empty & b₁ 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 b₁ being Linear_Combination of A st
( Sum b₁ = x & sum b₁ = 1 )

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of A st Sum b₁ = x & sum b₁ = 1 & Sum b₂ = x & sum b₂ = 1 holds
b₁ = b₂

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 b₄ being Linear_Combination of A holds
( b₄ = x |-- A iff ( Sum b₄ = x & sum b₄ = 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;