:: by Kenichi Arai and Hiroyuki Okazaki

::

:: Received April 17, 2013

:: Copyright (c) 2013-2016 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)))

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 ;

ex b_{1} being BinOp of (n -tuples_on BOOLEAN) st

for x, y being Element of n -tuples_on BOOLEAN holds b_{1} . (x,y) = Op-XOR (x,y)

for b_{1}, b_{2} being BinOp of (n -tuples_on BOOLEAN) st ( for x, y being Element of n -tuples_on BOOLEAN holds b_{1} . (x,y) = Op-XOR (x,y) ) & ( for x, y being Element of n -tuples_on BOOLEAN holds b_{2} . (x,y) = Op-XOR (x,y) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of n -tuples_on BOOLEAN holds it . (x,y) = Op-XOR (x,y);

ex b

for x, y being Element of n -tuples_on BOOLEAN holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines XORB NBVECTSP:def 1 :

for n being non zero Element of NAT

for b_{2} being BinOp of (n -tuples_on BOOLEAN) holds

( b_{2} = XORB n iff for x, y being Element of n -tuples_on BOOLEAN holds b_{2} . (x,y) = Op-XOR (x,y) );

for n being non zero Element of NAT

for b

( b

definition

let n be non zero Element of NAT ;

correctness

coherence

n |-> 0 is Element of n -tuples_on BOOLEAN;

end;
correctness

coherence

n |-> 0 is Element of n -tuples_on BOOLEAN;

proof end;

:: deftheorem defines ZeroB NBVECTSP:def 2 :

for n being non zero Element of NAT holds ZeroB n = n |-> 0;

for n being non zero Element of NAT holds ZeroB n = n |-> 0;

definition

let n be non zero Element of NAT ;

coherence

addLoopStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n) #) is strict addLoopStr ;

;

end;
func n -BinaryGroup -> strict addLoopStr equals :: NBVECTSP:def 3

addLoopStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n) #);

correctness addLoopStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n) #);

coherence

addLoopStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n) #) is strict addLoopStr ;

;

:: 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) #);

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

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

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 ;

( n -BinaryGroup is add-associative & n -BinaryGroup is right_zeroed & n -BinaryGroup is right_complementable & n -BinaryGroup is Abelian & not n -BinaryGroup is empty )

end;
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;

registration

let u, v be Element of Z_2;

compatibility

u + v = u 'xor' v

u * v = u '&' v

end;
compatibility

u + v = u 'xor' v

proof end;

compatibility u * v = u '&' v

proof end;

definition

let n be non zero Element of NAT ;

ex b_{1} 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_{1} . (a,x)) . i = a '&' (x . i)

for b_{1}, b_{2} 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_{1} . (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_{2} . (a,x)) . i = a '&' (x . i) ) holds

b_{1} = b_{2}

end;
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 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);

ex b

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

proof end;

uniqueness for b

for x being Element of n -tuples_on BOOLEAN

for i being set st i in Seg n holds

(b

for x being Element of n -tuples_on BOOLEAN

for i being set st i in Seg n holds

(b

b

proof end;

:: deftheorem Def4 defines MLTB NBVECTSP:def 4 :

for n being non zero Element of NAT

for b_{2} being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) holds

( b_{2} = 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_{2} . (a,x)) . i = a '&' (x . i) );

for n being non zero Element of NAT

for b

( b

for x being Element of n -tuples_on BOOLEAN

for i being set st i in Seg n holds

(b

definition

let n be non zero Element of NAT ;

coherence

ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is VectSp of Z_2 ;

end;
func n -BinaryVectSp -> VectSp of Z_2 equals :: NBVECTSP:def 5

ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #);

correctness ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #);

coherence

ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #) is VectSp of Z_2 ;

proof 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) #);

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 ;

coherence

for b_{1} being Subspace of n -BinaryVectSp holds b_{1} is finite

end;
coherence

for b

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

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_{2} -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 ) ) )

for L being the carrier of (b

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_{2} -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 ) ) )

for L being the carrier of (b

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 ) ) ) )

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)

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

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)

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) #)

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 ) ) ) ) )

( 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 )

( n -BinaryVectSp is finite-dimensional & dim (n -BinaryVectSp) = n )

proof end;

registration
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 )

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;