:: The Vector Space of Subsets of a Set Based on Symmetric Difference
::  by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-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 NUMBERS, STRUCT_0, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, NAT_1,
      ORDINAL4, VECTSP_1, INT_3, CARD_1, SUPINF_2, MESFUNC1, ARYTM_3, INT_1,
      QC_LANG1, XBOOLE_0, TARSKI, BINOP_1, ZFMISC_1, RLVECT_1, ALGSTR_0,
      GROUP_1, RLVECT_2, XXREAL_0, CARD_3, RLVECT_3, REALSET1, VALUED_1,
      FINSEQ_2, PARTFUN1, FINSET_1, FUNCT_4, RLVECT_5, ORDINAL2, BSPACE;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1,
      FUNCT_1, ORDINAL1, NUMBERS, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1,
      FUNCT_7, XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQOP,
      CARD_2, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6,
      VECTSP_7, MATRLIN, VECTSP_9, INT_3, RANKNULL;
 constructors FINSEQOP, VECTSP_7, VECTSP_9, REALSET1, WELLORD2, NAT_D, FUNCT_7,
      CARD_2, RANKNULL, INT_3, GR_CY_1, RELSET_1, BINOP_2, BINOP_1;
 registrations STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, SUBSET_1, XBOOLE_0,
      VECTSP_1, ORDINAL1, XREAL_0, INT_1, VECTSP_7, RELSET_1;
 requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;


begin

definition
  let S be 1-sorted;
  func <*>S -> FinSequence of S equals
:: BSPACE:def 1
  <*>([#]S);
end;

:: exactly as in FINSEQ_2

reserve S for 1-sorted,
  i for Element of NAT,
  p for FinSequence,
  X for set;

:: copied from FINSEQ_2:13

theorem :: BSPACE:1
  for p being FinSequence of S st i in dom p holds p.i in S;

:: copied from FINSEQ_2:14

theorem :: BSPACE:2
  (for i being Nat st i in dom p holds p.i in S) implies p is FinSequence of S;

scheme :: BSPACE:sch 1
  IndSeqS{S() -> 1-sorted, P[set]}: for p being FinSequence of S() holds P[p]
provided
 P[<*> S()] and
 for p being FinSequence of S() for x being Element of S() st P[p]
holds P[p^<*x*>];

begin :: The two-element field Z_2

definition
  func Z_2 -> Field equals
:: BSPACE:def 2
  INT.Ring(2);
end;

theorem :: BSPACE:3
  [#]Z_2 = {0,1};

theorem :: BSPACE:4
  for a being Element of Z_2 holds a = 0 or a = 1;

theorem :: BSPACE:5
  0.Z_2 = 0;

theorem :: BSPACE:6
  1.Z_2 = 1;

theorem :: BSPACE:7
  1.Z_2 + 1.Z_2 = 0.Z_2;

theorem :: BSPACE:8
  for x being Element of Z_2 holds x = 0.Z_2 iff x <> 1.Z_2;

begin :: Set-theoretical Preliminaries

definition
  let X be set,x be object;
  func X@x -> Element of Z_2 equals
:: BSPACE:def 3

  1.Z_2 if x in X otherwise 0.Z_2;
end;

theorem :: BSPACE:9
  for X,x being set holds X@x = 1.Z_2 iff x in X;

theorem :: BSPACE:10
  for X,x being set holds X@x = 0.Z_2 iff not x in X;

theorem :: BSPACE:11
  for X,x being set holds X@x <> 0.Z_2 iff X@x = 1.Z_2;

theorem :: BSPACE:12
  for X,x,y being set holds X@x = X@y iff (x in X iff y in X);

theorem :: BSPACE:13
  for X,Y,x being set holds X@x = Y@x iff (x in X iff x in Y);

theorem :: BSPACE:14
  for x being set holds {}@x = 0.Z_2;

theorem :: BSPACE:15
  for X being set, u,v being Subset of X, x being Element of X
  holds (u \+\ v)@x = u@x + v@x;

theorem :: BSPACE:16
  for X,Y being set holds X = Y iff for x being object holds X@x = Y@x;

begin :: The Boolean Bector Space of Subsets of a Set

definition
  let X be set, a be Element of Z_2, c be Subset of X;
  func a \*\ c -> Subset of X equals
:: BSPACE:def 4

  c if a = 1.Z_2, {}X if a = 0.Z_2;
end;

definition
  let X be set;
  func bspace-sum(X) -> BinOp of bool X means
:: BSPACE:def 5

  for c,d being Subset of X holds it.(c,d) = c \+\ d;
end;

theorem :: BSPACE:17
  for a being Element of Z_2, c,d being Subset of X holds a \*\ (c
  \+\ d) = (a \*\ c) \+\ (a \*\ d);

theorem :: BSPACE:18
  for a,b being Element of Z_2, c being Subset of X holds (a+b)
  \*\ c = (a \*\ c) \+\ (b \*\ c);

theorem :: BSPACE:19
  for c being Subset of X holds (1.Z_2) \*\ c = c;

theorem :: BSPACE:20
  for a,b being Element of Z_2, c being Subset of X holds a \*\ (b
  \*\ c) = (a*b) \*\ c;

definition
  let X be set;
  func bspace-scalar-mult(X) -> Function of [:the carrier of Z_2,bool X:],bool
  X means
:: BSPACE:def 6

  for a being Element of Z_2, c being Subset of X holds it.(a,c) = a \*\ c;
end;

definition
  let X be set;
  func bspace(X) -> non empty ModuleStr over Z_2 equals
:: BSPACE:def 7
  ModuleStr (# bool X,
    bspace-sum(X), {}X, bspace-scalar-mult(X) #);
end;

theorem :: BSPACE:21
  bspace(X) is Abelian;

theorem :: BSPACE:22
  bspace(X) is add-associative;

theorem :: BSPACE:23
  bspace(X) is right_zeroed;

theorem :: BSPACE:24
  bspace(X) is right_complementable;

theorem :: BSPACE:25
  for a being Element of Z_2, x,y being Element of bspace(X) holds
  a*(x+y) = (a*x)+(a*y);

theorem :: BSPACE:26
  for a,b being Element of Z_2, x being Element of bspace(X) holds
  (a+b)*x = (a*x)+(b*x);

theorem :: BSPACE:27
  for a,b being Element of Z_2, x being Element of bspace(X) holds
  (a*b)*x = a*(b*x);

theorem :: BSPACE:28
  for x being Element of bspace(X) holds (1_Z_2)*x = x;

theorem :: BSPACE:29
  bspace(X) is vector-distributive scalar-distributive
  scalar-associative scalar-unital;

registration
  let X be set;
  cluster bspace(X) -> vector-distributive scalar-distributive
  scalar-associative scalar-unital
   Abelian right_complementable
    add-associative right_zeroed;
end;

begin :: The Linear Independence and Linear Span of 1-element Subsets

definition

  let X be set;
  func singletons(X) -> set equals
:: BSPACE:def 8
  { f where f is Subset of X : f is 1-element };
end;

definition
  let X be set;
  redefine func singletons(X) -> Subset of bspace(X);
end;

registration
  let X be non empty set;
  cluster singletons(X) -> non empty;
end;

theorem :: BSPACE:30
  for X being non empty set, f being Subset of X st f is Element
  of singletons(X) holds f is 1-element;

definition
  let F be Field, V be VectSp of F, l be Linear_Combination of V, x be Element
  of V;
  redefine func l.x -> Element of F;
end;

definition
  let X be non empty set, s be FinSequence of bspace(X), x be Element of X;
  func s@x -> FinSequence of Z_2 means
:: BSPACE:def 9

  len it = len s & for j being Nat st 1 <= j & j <= len s holds it.j = (s.j)@x;
end;

theorem :: BSPACE:31
  for X being non empty set, x being Element of X holds (<*>(
  bspace(X)))@x = <*>Z_2;

theorem :: BSPACE:32
  for X being set, u,v being Element of bspace(X), x being Element
  of X holds (u + v)@x = u@x + v@x;

theorem :: BSPACE:33
  for X being non empty set, s being FinSequence of bspace(X), f
being Element of bspace(X), x being Element of X holds (s ^ <*f*>)@x = (s@x) ^
  <*f@x*>;

theorem :: BSPACE:34
  for X being non empty set, s being FinSequence of bspace(X), x
  being Element of X holds (Sum s)@x = Sum (s@x);

theorem :: BSPACE:35
  for X being non empty set, l being Linear_Combination of bspace(
  X), x being Element of bspace(X) st x in Carrier l holds l.x = 1_Z_2;

registration let X be empty set;
 cluster singletons X -> empty;

end;

theorem :: BSPACE:36
  singletons(X) is linearly-independent;

theorem :: BSPACE:37
  for f being Element of bspace(X) st (ex x being set st x in X & f = {x
  }) holds f in singletons(X);

theorem :: BSPACE:38
  for X being finite set, A being Subset of X ex l being
  Linear_Combination of singletons(X) st Sum l = A;

theorem :: BSPACE:39
  for X being finite set holds Lin(singletons(X)) = bspace(X);

theorem :: BSPACE:40
  for X being finite set holds singletons(X) is Basis of bspace(X);

registration
  let X be finite set;
  cluster singletons(X) -> finite;
end;

registration
  let X be finite set;
  cluster bspace(X) -> finite-dimensional;
end;

theorem :: BSPACE:41
  card (singletons X) = card X;

theorem :: BSPACE:42
  card [#](bspace X) = exp(2,card(X));

theorem :: BSPACE:43
  dim bspace {} = 0;