:: $n$-dimensional Binary Vector Spaces
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 17, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


Lm1: for n being non zero Nat
for D being non empty set
for p being Element of n -tuples_on D holds
( len p = n & p is Element of D * )
proof end;

theorem Th1: :: NBVECTSP:1
for n being non zero Element of NAT
for u1, v1, w1 being Element of n -tuples_on BOOLEAN holds Op-XOR ((Op-XOR (u1,v1)),w1) = Op-XOR (u1,(Op-XOR (v1,w1)))
proof end;

definition
let n be non zero Element of NAT ;
func XORB n -> BinOp of (n -tuples_on BOOLEAN) means :Def1: :: NBVECTSP:def 1
 for x, y being Element of n -tuples_on BOOLEAN holds it . (x,y) = Op-XOR (x,y);
existence
ex b1 being BinOp of (n -tuples_on BOOLEAN) st
for x, y being Element of n -tuples_on BOOLEAN holds b1 . (x,y) = Op-XOR (x,y)
proof end;
uniqueness
for b1, b2 being BinOp of (n -tuples_on BOOLEAN) st ( for x, y being Element of n -tuples_on BOOLEAN holds b1 . (x,y) = Op-XOR (x,y) ) & ( for x, y being Element of n -tuples_on BOOLEAN holds b2 . (x,y) = Op-XOR (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines XORB NBVECTSP:def 1 :
for n being non zero Element of NAT
for b2 being BinOp of (n -tuples_on BOOLEAN) holds
( b2 = XORB n iff for x, y being Element of n -tuples_on BOOLEAN holds b2 . (x,y) = Op-XOR (x,y) );

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

:: deftheorem defines ZeroB NBVECTSP:def 2 :
for n being non zero Element of NAT holds ZeroB n = n |-> 0;

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) #);
correctness
coherence
addLoopStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n) #) is strict addLoopStr ;
;
end;

:: deftheorem defines -BinaryGroup NBVECTSP:def 3 :
for n being non zero Element of NAT holds n -BinaryGroup = addLoopStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n) #);

theorem Th2: :: NBVECTSP:2
for n being non zero Element of NAT
for u1 being Element of n -tuples_on BOOLEAN holds Op-XOR (u1,(ZeroB n)) = u1
proof end;

theorem Th3: :: NBVECTSP:3
for n being non zero Element of NAT
for u1 being Element of n -tuples_on BOOLEAN holds Op-XOR (u1,u1) = ZeroB n
proof end;

registration
let n be non zero Element of NAT ;
cluster n -BinaryGroup -> non empty strict right_complementable Abelian add-associative right_zeroed ;
coherence
( n -BinaryGroup is add-associative & n -BinaryGroup is right_zeroed & n -BinaryGroup is right_complementable & n -BinaryGroup is Abelian & not n -BinaryGroup is empty )
proof end;
end;

registration
cluster -> boolean for Element of the carrier of Z_2;
coherence
for b1 being Element of Z_2 holds b1 is boolean by BSPACE:3;
end;

registration
let u, v be Element of Z_2;
identify u + v with u 'xor' v;
compatibility
u + v = u 'xor' v
proof end;
identify u * v with u '&' v;
compatibility
u * v = u '&' v
proof end;
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 :Def4: :: NBVECTSP:def 4
 for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(it . (a,x)) . i = a '&' (x . i);
existence
ex b1 being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) st
for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(b1 . (a,x)) . i = a '&' (x . i)
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) st ( for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(b1 . (a,x)) . i = a '&' (x . i) ) & ( for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(b2 . (a,x)) . i = a '&' (x . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines MLTB NBVECTSP:def 4 :
for n being non zero Element of NAT
for b2 being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) holds
( b2 = MLTB n iff for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(b2 . (a,x)) . i = a '&' (x . i) );

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) #);
correctness
coherence
ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is VectSp of Z_2 ;
proof end;
end;

:: deftheorem defines -BinaryVectSp NBVECTSP:def 5 :
for n being non zero Element of NAT holds n -BinaryVectSp = ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #);

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

registration
let n be non zero Element of NAT ;
cluster -> finite for Subspace of n -BinaryVectSp ;
coherence
for b1 being Subspace of n -BinaryVectSp holds b1 is finite
proof end;
end;

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

theorem Th5: :: NBVECTSP:5
for m being non zero Element of NAT
for x being FinSequence of Z_2
for v being Element of Z_2
for j being Nat st len x = m & j in Seg m & ( for i being 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
proof end;

theorem Th6: :: NBVECTSP:6
for m, n being non zero Element of NAT
for L being the carrier of (b2 -BinaryVectSp) -valued FinSequence
for j being Nat st len L = m & m <= n & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) )
proof end;

theorem Th7: :: NBVECTSP:7
for m, n being non zero Element of NAT
for L being the carrier of (b2 -BinaryVectSp) -valued FinSequence
for Suml being Element of n -tuples_on BOOLEAN
for j being Nat st len L = m & m <= n & Suml = Sum L & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) )
proof end;

theorem Th8: :: NBVECTSP:8
for m, n being non zero Element of NAT st m <= n holds
ex A being FinSequence of n -tuples_on BOOLEAN st
( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being 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 ) ) ) )
proof end;

theorem Th9: :: NBVECTSP:9
for m, n being non zero Element of NAT
for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of (n -BinaryVectSp)
for l being Linear_Combination of B
for Suml being 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 being 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 being Nat st j in Seg m holds
Suml . j = l . (A . j)
proof end;

theorem Th10: :: NBVECTSP:10
for m, n being non zero Element of NAT
for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of (n -BinaryVectSp) st rng A = B & m <= n & len A = m & A is one-to-one & ( for i, j being 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
proof end;

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

theorem Th12: :: NBVECTSP:12
for n being non zero Element of NAT
for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of (n -BinaryVectSp) st rng A = B & len A = n & A is one-to-one & ( for i, j being 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) #)
proof end;

theorem Th13: :: NBVECTSP:13
for n being non zero Element of NAT ex B being finite Subset of (n -BinaryVectSp) st
( B is Basis of (n -BinaryVectSp) & card B = n & ex A being 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 being 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 ) ) ) ) )
proof end;

theorem Th14: :: NBVECTSP:14
for n being non zero Element of NAT holds
( n -BinaryVectSp is finite-dimensional & dim (n -BinaryVectSp) = n )
proof end;

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

theorem :: NBVECTSP:15
for n being non zero Element of NAT
for A being FinSequence of n -tuples_on BOOLEAN
for C being Subset of (n -BinaryVectSp) st len A = n & A is one-to-one & card (rng A) = n & ( for i, j being 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 )
proof end;