:: $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 b₁ being BinOp of (n -tuples_on BOOLEAN) st
for x, y being Element of n -tuples_on BOOLEAN holds b₁ . (x,y) = Op-XOR (x,y)

proof end;

uniqueness
for b₁, b₂ being BinOp of (n -tuples_on BOOLEAN) st ( for x, y being Element of n -tuples_on BOOLEAN holds b₁ . (x,y) = Op-XOR (x,y) ) & ( for x, y being Element of n -tuples_on BOOLEAN holds b₂ . (x,y) = Op-XOR (x,y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines XORB NBVECTSP:def 1 :
for n being non zero Element of NAT
for b₂ being BinOp of (n -tuples_on BOOLEAN) holds
( b₂ = XORB n iff for x, y being Element of n -tuples_on BOOLEAN holds b₂ . (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 b₁ being Element of Z_2 holds b₁ 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 b₁ 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
(b₁ . (a,x)) . i = a '&' (x . i)

proof end;

uniqueness
for b₁, b₂ 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
(b₁ . (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
(b₂ . (a,x)) . i = a '&' (x . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines MLTB NBVECTSP:def 4 :
for n being non zero Element of NAT
for b₂ being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) holds
( b₂ = 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
(b₂ . (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 b₁ being Subspace of n -BinaryVectSp holds b₁ 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 (b₂ -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 (b₂ -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;