:: by Karol P\c{a}k

::

:: Received December 18, 2009

:: Copyright (c) 2009-2018 Association of Mizar Users

registration
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;

coherence

not conv A is empty

end;
let A be non empty Subset of RLS;

coherence

not conv A is empty

proof 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}

for v being Element of R holds conv {v} = {v}

proof end;

theorem :: RLAFFIN1:2

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)

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)

for A being Subset of V

for v, w being Element of V holds (v + w) + A = v + (w + 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)

for g being Element of G

for A being Subset of G holds card A = card (g + A)

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

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)

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

for AR being Subset of R holds 1 * AR = AR

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)

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)

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 )

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;

ex b_{1} being Linear_Combination of G st

for h being Element of G holds b_{1} . h = LG . (h - g)

for b_{1}, b_{2} being Linear_Combination of G st ( for h being Element of G holds b_{1} . h = LG . (h - g) ) & ( for h being Element of G holds b_{2} . h = LG . (h - g) ) holds

b_{1} = b_{2}

end;
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 for h being Element of G holds it . h = LG . (h - g);

ex b

for h being Element of G holds b

proof end;

uniqueness for b

b

proof 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_{4} being Linear_Combination of G holds

( b_{4} = g + LG iff for h being Element of G holds b_{4} . h = LG . (h - g) );

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

( b

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)

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)

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)

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

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

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

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;

( ( r <> 0 implies ex b_{1} being Linear_Combination of R st

for v being Element of R holds b_{1} . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b_{1} being Linear_Combination of R st b_{1} = ZeroLC R ) )

for b_{1}, b_{2} being Linear_Combination of R holds

( ( r <> 0 & ( for v being Element of R holds b_{1} . v = LR . ((r ") * v) ) & ( for v being Element of R holds b_{2} . v = LR . ((r ") * v) ) implies b_{1} = b_{2} ) & ( not r <> 0 & b_{1} = ZeroLC R & b_{2} = ZeroLC R implies b_{1} = b_{2} ) )

for b_{1} being Linear_Combination of R holds verum
;

end;
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 for v being Element of R holds it . v = LR . ((r ") * v) if r <> 0

otherwise it = ZeroLC R;

( ( r <> 0 implies ex b

for v being Element of R holds b

proof end;

uniqueness for b

( ( r <> 0 & ( for v being Element of R holds b

proof end;

consistency for b

:: 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_{4} being Linear_Combination of R holds

( ( r <> 0 implies ( b_{4} = r (*) LR iff for v being Element of R holds b_{4} . v = LR . ((r ") * v) ) ) & ( not r <> 0 implies ( b_{4} = r (*) LR iff b_{4} = ZeroLC R ) ) );

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

( ( r <> 0 implies ( b

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)

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)

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)

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)

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

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

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

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;

ex b_{1} being Real ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & b_{1} = Sum (LS * F) )

for b_{1}, b_{2} being Real st ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & b_{1} = Sum (LS * F) ) & ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & b_{2} = Sum (LS * F) ) holds

b_{1} = b_{2}

end;
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 F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & it = Sum (LS * F) );

ex b

( F is one-to-one & rng F = Carrier LS & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier LS & b

( F is one-to-one & rng F = Carrier LS & b

b

proof end;

:: deftheorem Def3 defines sum RLAFFIN1:def 3 :

for S being non empty addLoopStr

for LS being Linear_Combination of S

for b_{3} being Real holds

( b_{3} = sum LS iff ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & b_{3} = Sum (LS * F) ) );

for S being non empty addLoopStr

for LS being Linear_Combination of S

for b

( b

( F is one-to-one & rng F = Carrier LS & b

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

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)

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 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

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)

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)

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)

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)

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)

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)

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)

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)

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;

end;
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 ) );

( A is empty or ex v being VECTOR of V st

( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) );

:: 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 ) ) );

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;

coherence

for b_{1} being Subset of V st b_{1} is empty holds

b_{1} is affinely-independent
;

let v be VECTOR of V;

coherence

for b_{1} being Subset of V st b_{1} = {v} holds

b_{1} is affinely-independent

coherence

for b_{1} being Subset of V st b_{1} = {v,w} holds

b_{1} is affinely-independent

end;
coherence

for b

b

let v be VECTOR of V;

coherence

for b

b

proof end;

let w be VECTOR of V;coherence

for b

b

proof end;

registration

let V be RealLinearSpace;

existence

ex b_{1} being Subset of V st

( b_{1} is 1 -element & b_{1} is affinely-independent )

end;
existence

ex b

( b

proof 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 )

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 = {} )

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

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;

coherence

for b_{1} being Subset of V st b_{1} is linearly-independent holds

b_{1} is affinely-independent

end;
coherence

for b

b

proof end;

registration

let V be RealLinearSpace;

let I be affinely-independent Subset of V;

let v be VECTOR of V;

coherence

v + I is affinely-independent

end;
let I be affinely-independent Subset of V;

let v be VECTOR of V;

coherence

v + I is affinely-independent

proof 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

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;

coherence

r * I is affinely-independent

end;
let I be affinely-independent Subset of V;

let r be Real;

coherence

r * I is affinely-independent

proof 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

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 )

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;

end;
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 ;

for A being Subset of V st A in F holds

A is affinely-independent ;

:: 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 );

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;

coherence

for b_{1} being Subset-Family of V st b_{1} is empty holds

b_{1} is affinely-independent
;

let I be affinely-independent Subset of V;

coherence

for b_{1} being Subset-Family of V st b_{1} = {I} holds

b_{1} is affinely-independent
by TARSKI:def 1;

end;
coherence

for b

b

let I be affinely-independent Subset of V;

coherence

for b

b

registration

let V be RealLinearSpace;

existence

ex b_{1} being Subset-Family of V st

( b_{1} is empty & b_{1} is affinely-independent )

ex b_{1} being Subset-Family of V st

( not b_{1} is empty & b_{1} is affinely-independent )

end;
existence

ex b

( b

proof end;

existence ex b

( not b

proof 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

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 ;

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;

meet { B where B is Affine Subset of RLS : A c= B } is Subset of RLS

end;
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 } ;

meet { B where B is Affine Subset of RLS : A c= B } is Subset of RLS

proof 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 } ;

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
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
end;

registration

let RLS be non empty RLSStruct ;

let A be non empty Subset of RLS;

coherence

not Affin A is empty

end;
let A be non empty Subset of RLS;

coherence

not Affin A is empty

proof end;

theorem :: RLAFFIN1:49

theorem :: RLAFFIN1:50

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

for A, B being Subset of RLS st A c= B & B is Affine holds

Affin A c= 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)

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

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)

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)

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)))

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 )

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 }

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 )

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

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 ) ) )

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

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}

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 :: 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

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 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

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 ;

existence

ex b_{1} being Linear_Combination of A st

( Sum b_{1} = x & sum b_{1} = 1 )

for b_{1}, b_{2} being Linear_Combination of A st Sum b_{1} = x & sum b_{1} = 1 & Sum b_{2} = x & sum b_{2} = 1 holds

b_{1} = b_{2}

end;
let A be Subset of V;

assume A1: A is affinely-independent ;

let x be object ;

assume A2: x in Affin A ;

existence

ex b

( Sum b

proof end;

uniqueness for b

b

proof 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_{4} being Linear_Combination of A holds

( b_{4} = x |-- A iff ( Sum b_{4} = x & sum b_{4} = 1 ) );

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

( b

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))

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 )

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 ) )

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

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

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) )

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)

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

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

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

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

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)) )

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 ) ) )

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 )

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

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;