:: Affine Independence in Vector Spaces
::  by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ALGSTR_0, ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CONVEX1, CONVEX2,
      CONVEX3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2,
      MONOID_0, ORDERS_1, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3,
      RUSUB_4, SEMI_AF1, SETFAM_1, SUBSET_1, TARSKI, CLASSES1, SUPINF_2,
      RLVECT_5, REAL_1, NUMBERS, NAT_1, CARD_3, XXREAL_0, STRUCT_0, ZFMISC_1,
      RLAFFIN1, ORDINAL1, ORDINAL4, PARTFUN1, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDERS_1, CARD_1, NUMBERS,
      XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FINSET_1, SETFAM_1, DOMAIN_1,
      ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, STRUCT_0,
      FINSEQ_2, FINSEQ_3, FINSEQOP, CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2,
      RLVECT_3, RLVECT_5, RLSUB_1, RLSUB_2, RUSUB_4, CONVEX1, CONVEX2, CONVEX3;
 constructors BINOP_1, BINOP_2, CLASSES1, CONVEX1, CONVEX3, FINSEQOP, FINSOP_1,
      MATRLIN, ORDERS_1, REALSET1, REAL_1, RLVECT_3, RLVECT_5, RVSUM_1,
      RLSUB_2, RUSUB_5, SETWISEO, RELSET_1;
 registrations BINOP_2, CARD_1, CONVEX1, FINSET_1, FINSEQ_2, FUNCT_1, FUNCT_2,
      NAT_1, NUMBERS, RELAT_1, RLVECT_1, RLVECT_3, RUSUB_4, STRUCT_0, SUBSET_1,
      VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, RLVECT_5, RELSET_1, RLVECT_2,
      ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve x,y for set,
        r,s for Real,
        S for non empty addLoopStr,
        LS,LS1,LS2 for Linear_Combination of S,
        G for Abelian add-associative right_zeroed right_complementable
          non empty addLoopStr,
        LG,LG1,LG2 for Linear_Combination of G,
        g,h for Element of G,
        RLS for non empty RLSStruct,
        R for vector-distributive scalar-distributive scalar-associative
        scalar-unitalnon empty RLSStruct,
        AR for Subset of R,
        LR,LR1,LR2 for Linear_Combination of R,
        V for RealLinearSpace,
        v,v1,v2,w,p for VECTOR of V,
        A,B for Subset of V,
        F1,F2 for Subset-Family of V,
        L,L1,L2 for Linear_Combination of V;

registration
  let RLS;
  let A be empty Subset of RLS;
  cluster conv A -> empty;
end;

registration let RLS;
  let A be non empty Subset of RLS;
  cluster conv A -> non empty;
end;

theorem :: RLAFFIN1:1
  for v be Element of R holds conv {v} = {v};

theorem :: RLAFFIN1:2
  for A be Subset of RLS holds A c= conv A;

theorem :: RLAFFIN1:3
  for A,B be Subset of RLS st A c= B holds conv A c= conv B;

theorem :: RLAFFIN1:4
  for S,A be Subset of RLS st A c= conv S holds conv S = conv(S\/A);

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

theorem :: RLAFFIN1:6
  for V be Abelian right_zeroed non empty addLoopStr for A be Subset of V
    holds 0.V + A = A;

theorem :: RLAFFIN1:7
  for A be Subset of G holds card A = card (g+A);

theorem :: RLAFFIN1:8
  for v be Element of S holds v + {}S = {}S;

theorem :: RLAFFIN1:9
  for A,B be Subset of RLS st A c= B holds r*A c= r*B;

theorem :: RLAFFIN1:10
  (r*s)* AR = r * (s*AR);

theorem :: RLAFFIN1:11
  1 * AR = AR;

theorem :: RLAFFIN1:12
  0 * A c= {0.V};

theorem :: RLAFFIN1:13
  for F be FinSequence of S holds (LS1+LS2) * F = (LS1*F) + (LS2*F);

theorem :: RLAFFIN1:14
  for F be FinSequence of V holds (r*L) * F = r * (L*F);

theorem :: RLAFFIN1:15
  A is linearly-independent & A c= B & Lin B = V implies
    ex I be linearly-independent Subset of V st A c= I & I c= B & Lin I = V;

begin :: Two Transformations of Linear Combinations

definition
  let G,LG,g;
  func g + LG -> Linear_Combination of G means
:: RLAFFIN1:def 1
    it.h = LG.(h-g);
end;

theorem :: RLAFFIN1:16
  Carrier (g+LG) = g + Carrier LG;

theorem :: RLAFFIN1:17
  g + (LG1+LG2) = (g+LG1) + (g+LG2);

theorem :: RLAFFIN1:18
  v + (r*L) = r * (v+L);

theorem :: RLAFFIN1:19
  g + (h+LG) = (g+h) + LG;

theorem :: RLAFFIN1:20
  g + ZeroLC G = ZeroLC G;

theorem :: RLAFFIN1:21
  0.G + LG = LG;

definition
  let R,LR; let r be Real;
  func r (*) LR -> Linear_Combination of R means
:: RLAFFIN1:def 2
    for v be Element of R holds it.v = LR.(r"*v) if r<>0 otherwise
   it = ZeroLC R;
end;

theorem :: RLAFFIN1:22
  Carrier (r(*)LR) c= r*Carrier LR;

theorem :: RLAFFIN1:23
  r <> 0 implies Carrier (r(*)LR) = r * Carrier LR;

theorem :: RLAFFIN1:24
  r (*) (LR1+LR2) = (r(*)LR1) + (r(*)LR2);

theorem :: RLAFFIN1:25
  r * (s(*)L) = s (*) (r*L);

theorem :: RLAFFIN1:26
  r (*) ZeroLC(R) = ZeroLC R;

theorem :: RLAFFIN1:27
  r(*)(s(*)LR)=(r*s)(*)LR;

theorem :: RLAFFIN1:28
  1 (*) LR = LR;

begin :: The Sum of Coefficients of a Linear Combination

definition
 let S,LS;
 func sum LS -> Real means
:: RLAFFIN1:def 3
   ex F be FinSequence of S st
      F is one-to-one & rng F = Carrier LS & it = Sum (LS*F);
end;

theorem :: RLAFFIN1:29
  for F be FinSequence of S st Carrier LS misses rng F holds Sum (LS*F) = 0;

theorem :: RLAFFIN1:30
  for F be FinSequence of S st F is one-to-one & Carrier LS c= rng F
    holds sum LS = Sum (LS*F);

theorem :: RLAFFIN1:31
  sum ZeroLC S = 0;

theorem :: RLAFFIN1:32
  for v be Element of S st Carrier LS c= {v} holds sum LS = LS.v;

theorem :: RLAFFIN1:33
  for v1,v2 be Element of S st
      Carrier LS c= {v1,v2} & v1 <> v2 holds sum LS = LS.v1 + LS.v2;

theorem :: RLAFFIN1:34
  sum (LS1+LS2) = sum LS1 + sum LS2;

theorem :: RLAFFIN1:35
  sum (r * L) = r * sum L;

theorem :: RLAFFIN1:36
  sum (L1-L2) =sum L1 - sum L2;

theorem :: RLAFFIN1:37
  sum LG = sum (g+LG);

theorem :: RLAFFIN1:38
  r <> 0 implies sum LR = sum (r(*)LR);

theorem :: RLAFFIN1:39
  Sum (v + L) = (sum L)*v + Sum L;

theorem :: RLAFFIN1:40
  Sum (r(*)L) = r * Sum L;

begin :: Affine Independence of Vectors

definition
  let V,A;
  attr A is affinely-independent means
:: RLAFFIN1:def 4
    A is empty or ex v st v in A & -v + A\{0.V} is linearly-independent;
end;

registration
  let V;
  cluster empty -> affinely-independent for Subset of V;
  let v;
  cluster {v} -> affinely-independent for Subset of V;
  let w;
  cluster {v,w} -> affinely-independent for Subset of V;
end;

registration
  let V;
  cluster 1-element affinely-independent for Subset of V;
end;

theorem :: RLAFFIN1:41
  A is affinely-independent iff for v st v in A holds
                                      -v + A\{0.V} is linearly-independent;

theorem :: RLAFFIN1:42
  A is affinely-independent iff
      for L be Linear_Combination of A st Sum L = 0.V & sum L = 0
        holds Carrier L = {};

theorem :: RLAFFIN1:43
  A is affinely-independent & B c= A implies B is affinely-independent;

registration
  let V;
  cluster linearly-independent -> affinely-independent for Subset of V;
end;

reserve I for affinely-independent Subset of V;

registration
  let V,I,v;
  cluster v + I -> affinely-independent;
end;

theorem :: RLAFFIN1:44
  v+A is affinely-independent implies A is affinely-independent;

registration
  let V,I,r;
  cluster r*I -> affinely-independent;
end;

theorem :: RLAFFIN1:45
  r * A is affinely-independent & r <> 0 implies A is affinely-independent;

theorem :: RLAFFIN1:46
  0.V in A implies
    (A is affinely-independent iff A \ {0.V} is linearly-independent);

definition
  let V;
  let F be Subset-Family of V;
  attr F is affinely-independent means
:: RLAFFIN1:def 5
   A in F implies A is affinely-independent;
end;

registration
  let V;
  cluster empty -> affinely-independent for Subset-Family of V;
  let I;
  cluster {I} -> affinely-independent for Subset-Family of V;
end;

registration
  let V;
  cluster empty affinely-independent for Subset-Family of V;
  cluster non empty affinely-independent for Subset-Family of V;
end;

theorem :: RLAFFIN1:47
  F1 is affinely-independent & F2 is affinely-independent implies
     F1 \/ F2 is affinely-independent;

theorem :: RLAFFIN1:48
  F1 c= F2 & F2 is affinely-independent implies F1 is affinely-independent;

begin :: Affine Hull

definition
  let RLS;
  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};
end;

registration
  let RLS;
  let A be Subset of RLS;
  cluster Affin A -> Affine;
end;

registration
  let RLS;
  let A be empty Subset of RLS;
  cluster Affin A -> empty;
end;

registration
  let RLS;
  let A be non empty Subset of RLS;
  cluster Affin A -> non empty;
end;

theorem :: RLAFFIN1:49
  for A be Subset of RLS holds A c= Affin A;

theorem :: RLAFFIN1:50
  for A be Affine Subset of RLS holds A = Affin A;

theorem :: RLAFFIN1:51
  for A,B be Subset of RLS st A c= B & B is Affine holds Affin A c= B;

theorem :: RLAFFIN1:52
  for A,B be Subset of RLS st A c= B holds Affin A c= Affin B;

theorem :: RLAFFIN1:53
  Affin (v+A) = v + Affin A;

theorem :: RLAFFIN1:54
  AR is Affine implies r * AR is Affine;

theorem :: RLAFFIN1:55
  r <> 0 implies Affin (r*AR) = r * Affin AR;

theorem :: RLAFFIN1:56
  Affin (r*A) = r * Affin A;

theorem :: RLAFFIN1:57
  v in Affin A implies Affin A = v + Up Lin (-v+A);

theorem :: RLAFFIN1:58
  A is affinely-independent iff for B st B c= A & Affin A = Affin B holds A = B
;

theorem :: RLAFFIN1:59
  Affin A = {Sum L where L is Linear_Combination of A : sum L=1};

theorem :: RLAFFIN1:60
  I c=A implies ex Ia be affinely-independent Subset of V st
    I c= Ia & Ia c= A & Affin Ia = Affin A;

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

theorem :: RLAFFIN1:62
  L is convex iff sum L = 1 & for v holds 0 <= L.v;

theorem :: RLAFFIN1:63
  L is convex implies L.x <= 1;

theorem :: RLAFFIN1:64
  L is convex & L.x = 1 implies Carrier L = {x};

theorem :: RLAFFIN1:65
  conv A c= Affin A;

theorem :: RLAFFIN1:66
  x in conv A & (conv A)\{x} is convex implies x in A;

theorem :: RLAFFIN1:67
  Affin conv A = Affin A;

theorem :: RLAFFIN1:68
  conv A c= conv B implies Affin A c= Affin B;

theorem :: RLAFFIN1:69
  for A,B be Subset of RLS st A c= Affin B holds Affin (A\/B) = Affin B;

begin :: Barycentric Coordinates

definition
  let V;
  let A such that
     A is affinely-independent;
  let x be object such that
     x in Affin A;
  func x |-- A -> Linear_Combination of A means
:: RLAFFIN1:def 7
    Sum it = x & sum it = 1;
end;

theorem :: RLAFFIN1:70
  v1 in Affin I & v2 in Affin I implies
  ((1-r)*v1+r*v2) |-- I = (1-r) * (v1|--I) + r * (v2|--I);

theorem :: RLAFFIN1:71
  x in conv I implies x|--I is convex & 0 <= (x|--I).v & (x|--I).v <= 1;

theorem :: RLAFFIN1:72
  x in conv I implies ((x|--I).y = 1 iff x = y & x in I);

theorem :: RLAFFIN1:73
  for I st x in Affin I & for v st v in I holds 0 <= (x|--I).v
    holds x in conv I;

theorem :: RLAFFIN1:74
  x in I implies (conv I)\{x} is convex;

theorem :: RLAFFIN1:75
  for B st x in Affin I & for y st y in B holds (x|--I).y = 0
    holds x in Affin(I\B) & x |-- I = x |-- (I\B);

theorem :: RLAFFIN1:76
  for B st x in conv I & for y st y in B holds (x|--I).y = 0
    holds x in conv (I\B);

theorem :: RLAFFIN1:77
  B c= I & x in Affin B implies x |-- B = x |-- I;

theorem :: RLAFFIN1:78
  v1 in Affin A & v2 in Affin A & r+s = 1 implies r*v1 + s*v2 in Affin A;

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

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

theorem :: RLAFFIN1:81
  L1.v <> L2.v implies ((r*L1+(1-r)*L2).v = s iff r = (L2.v-s)/(L2.v-L1.v));

theorem :: RLAFFIN1:82
  A\/{v} is affinely-independent iff
    A is affinely-independent & (v in A or not v in Affin A);

theorem :: RLAFFIN1:83
  not w in Affin A & v1 in A & v2 in A & r<>1 & r*w + (1-r)*v1 = s*w + (1-s)*v2
    implies r = s & v1 = v2;

theorem :: RLAFFIN1:84
  v in I & w in Affin I & p in Affin(I\{v}) & w = r*v + (1-r)*p
    implies r = (w|--I).v;