:: $n$-dimensional Binary Vector Spaces
::  by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 17, 2013
:: Copyright (c) 2013-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 NBVECTSP, DESCIP_1, TARSKI, XBOOLE_0, FINSEQ_1, RELAT_1, FUNCT_1,
      ARYTM_1, FUNCT_2, FINSEQ_2, NAT_1, XBOOLEAN, MARGREL1, ZFMISC_1,
      SUBSET_1, NUMBERS, CARD_1, XXREAL_0, PARTFUN1, ARYTM_3, XCMPLX_0,
      VALUED_1, FUNCOP_1, ALGSTR_0, STRUCT_0, RLVECT_1, SUPINF_2, MESFUNC1,
      BINOP_1, VECTSP_1, RLSUB_1, RLVECT_5, RLVECT_2, CARD_3, FUNCT_4,
      FINSET_1, RLVECT_3, BSPACE;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FINSET_1, CARD_1, NUMBERS,
      XXREAL_0, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCOP_1, XBOOLEAN,
      MARGREL1, BINARITH, DESCIP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
      VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, MATRLIN, VECTSP_9, BSPACE;
 constructors FINSEQ_1, RELSET_1, REAL_1, FINSEQ_4, NAT_D, FINSEQ_6, BINARITH,
      DESCIP_1, BINARI_3, FUNCT_2, EUCLID, BINOP_1, XXREAL_0, NAT_1, RLVECT_1,
      FINSEQ_2, GROUP_1, BINOP_2, MEMBERED, ARMSTRNG, XTUPLE_0, VECTSP_1,
      VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, REALSET1, WAYBEL_4,
      BSPACE;
 registrations FINSEQ_1, RELSET_1, FINSEQ_2, ORDINAL1, FINSET_1, MARGREL1,
      NAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, DESCIP_1, STRUCT_0, VECTSP_1,
      FUNCOP_1, XBOOLEAN, FUNCT_4, VECTSP_9, FINSEQ_3, CARD_1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM;


begin

reserve m,n,s for non zero Element of NAT;

theorem :: NBVECTSP:1
  for u1,v1,w1 be Element of n-tuples_on BOOLEAN
  holds Op-XOR(Op-XOR(u1,v1),w1) = Op-XOR(u1,Op-XOR(v1,w1));

definition
  let n be non zero Element of NAT;
  func XORB n -> BinOp of n-tuples_on BOOLEAN means
:: NBVECTSP:def 1

  for x,y being Element of n-tuples_on BOOLEAN holds it.(x,y) = Op-XOR(x,y);
end;

definition
  let n be non zero Element of NAT;
  func ZeroB n -> Element of n-tuples_on BOOLEAN equals
:: NBVECTSP:def 2
  n |-> 0;
end;

definition
  let n be non zero Element of NAT;
  func n-BinaryGroup -> strict addLoopStr equals
:: NBVECTSP:def 3
  addLoopStr(# n-tuples_on BOOLEAN, XORB n, ZeroB n #);
end;

theorem :: NBVECTSP:2
  for u1 be Element of n-tuples_on BOOLEAN holds Op-XOR(u1,ZeroB n) = u1;

theorem :: NBVECTSP:3
  for u1 be Element of n-tuples_on BOOLEAN holds Op-XOR(u1,u1) = ZeroB n;

registration
  let n be non zero Element of NAT;
  cluster n-BinaryGroup -> add-associative right_zeroed
  right_complementable Abelian non empty;
end;

registration
  cluster -> boolean for Element of Z_2;
end;

registration
  let u,v be Element of Z_2;
  identify u + v with u 'xor' v;
  identify u * v with u '&' v;
end;

definition
  let n be non zero Element of NAT;
  func MLTB n -> Function of [:the carrier of Z_2,
  n-tuples_on BOOLEAN:],n-tuples_on BOOLEAN means
:: NBVECTSP:def 4

  for a be Element of BOOLEAN, x be Element of n-tuples_on BOOLEAN, i be set
  st i in Seg n holds (it.(a,x)).i = a '&' x.i;
end;

definition
  let n be non zero Element of NAT;
  func n-BinaryVectSp -> VectSp of Z_2 equals
:: NBVECTSP:def 5
  ModuleStr(# n-tuples_on BOOLEAN,XORB n,ZeroB n,MLTB n #);
end;

registration
  let n be non zero Element of NAT;
  cluster n-BinaryVectSp -> finite;
end;

registration
  let n be non zero Element of NAT;
  cluster -> finite for Subspace of n-BinaryVectSp;
end;

theorem :: NBVECTSP:4
  for n being Nat holds Sum(n|->0.Z_2) = 0.Z_2;

theorem :: NBVECTSP:5
  for x be FinSequence of Z_2,
      v be Element of Z_2,
      j be Nat
  st len x = m & j in Seg m & for i be Nat st i in Seg m holds
  (i = j implies x.i = v) & (i <> j implies x.i = 0.Z_2)
  holds Sum(x) = v;

theorem :: NBVECTSP:6
  for L be the carrier of (n-BinaryVectSp)-valued FinSequence,
  j be Nat
  st len L = m & m <= n & j in Seg n
  ex x be FinSequence of Z_2 st len x = m &
  for i be Nat st i in Seg m ex K be Element of n-tuples_on BOOLEAN
  st K = L.i & x.i = K.j;

theorem :: NBVECTSP:7
  for L be the carrier of (n-BinaryVectSp)-valued FinSequence,
  Suml be Element of n-tuples_on BOOLEAN,
  j be Nat
  st len L = m & m <= n & Suml = Sum(L) & j in Seg n
  ex x be FinSequence of Z_2 st len x = m & (Suml).j = Sum(x) &
  for i be Nat st i in Seg m ex K be Element of n-tuples_on BOOLEAN
  st K = L.i & x.i = K.j;

theorem :: NBVECTSP:8
  m <= n implies
  ex A be FinSequence of n-tuples_on BOOLEAN st len A = m &
  A is one-to-one & card (rng A) = m & (for i,j be Nat st i in Seg m &
  j in Seg n holds (i = j implies (A.i).j = TRUE) &
  (i <> j implies (A.i).j = FALSE));

theorem :: NBVECTSP:9
  for A be FinSequence of n-tuples_on BOOLEAN,
  B be finite Subset of n-BinaryVectSp,
  l being Linear_Combination of B,
  Suml be Element of n-tuples_on BOOLEAN
  st rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one &
  (for i,j be Nat st i in Seg n & j in Seg m holds
  (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
  holds for j be Nat st j in Seg m holds (Suml).j = l.(A.j);

theorem :: NBVECTSP:10
  for A be FinSequence of n-tuples_on BOOLEAN,
  B be finite Subset of n-BinaryVectSp
  st rng A = B & m <= n & len A = m & A is one-to-one &
  (for i,j be Nat st i in Seg n & j in Seg m holds
  (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
  holds B is linearly-independent;

theorem :: NBVECTSP:11
  for A be FinSequence of n-tuples_on BOOLEAN,
  B be finite Subset of n-BinaryVectSp,
  v be Element of n-tuples_on BOOLEAN
  st rng A = B & len A = n & A is one-to-one
  ex l being Linear_Combination of B st
  for j be Nat st j in Seg n holds v.j = l.(A.j);

theorem :: NBVECTSP:12
  for A be FinSequence of n-tuples_on BOOLEAN,
  B be finite Subset of n-BinaryVectSp
  st rng A = B & len A = n & A is one-to-one &
  (for i,j be Nat st i in Seg n & j in Seg n holds
  (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
  holds Lin B = ModuleStr(# the carrier of n-BinaryVectSp,
  the addF of n-BinaryVectSp, the ZeroF of n-BinaryVectSp,
  the lmult of n-BinaryVectSp #);

theorem :: NBVECTSP:13
  ex B be finite Subset of n-BinaryVectSp
  st B is Basis of n-BinaryVectSp & card B = n &
  ex A be FinSequence of n-tuples_on BOOLEAN st len A = n &
  A is one-to-one & card (rng A) = n & rng A = B &
  (for i,j be Nat st i in Seg n & j in Seg n holds
  (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE));

theorem :: NBVECTSP:14
  n-BinaryVectSp is finite-dimensional & dim (n-BinaryVectSp) = n;

registration
  let n be non zero Element of NAT;
  cluster n-BinaryVectSp -> finite-dimensional;
end;

theorem :: NBVECTSP:15
  for A be FinSequence of n-tuples_on BOOLEAN,
  C be Subset of n-BinaryVectSp
  st len A = n & A is one-to-one & card rng A = n &
  (for i,j be Nat st i in Seg n & j in Seg n holds
  (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE)) &
  C c= rng A
  holds Lin C is Subspace of n-BinaryVectSp & C is Basis of Lin C &
  dim (Lin C) = card C;