:: $n$-dimensional Binary Vector Spaces
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 17, 2013
:: Copyright (c) 2013 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, ORDINAL1,
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, 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,
FRAENKEL, FUNCOP_1, XBOOLEAN, FUNCT_4, VECTSP_9, INT_3, GR_CY_1,
STIRL2_1, XCMPLX_0, FINSEQ_3;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1,
GROUP_1, VECTSP_6, MARGREL1, XBOOLEAN;
equalities FINSEQ_1, FINSEQ_2, VECTSP_1, VECTSP_6, ALGSTR_0, STRUCT_0,
MARGREL1, XBOOLEAN, ORDINAL1;
expansions XBOOLEAN, MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FUNCT_2, XXREAL_0, NAT_1, FINSEQ_1,
CARD_1, BINOP_1, FINSEQ_2, XBOOLEAN, XBOOLE_0, XBOOLE_1, DESCIP_1,
WELLORD2, RLVECT_2, FUNCOP_1, MARGREL1, RLVECT_1, ALGSTR_0, STRUCT_0,
VECTSP_4, VECTSP_6, MATRLIN, VECTSP_7, VECTSP_9, FUNCT_4, ORDINAL1,
BSPACE, VECTSP_1;
schemes FUNCT_1, FUNCT_2, FINSEQ_1, NAT_1, BINOP_1;
begin
reserve m,n,s for non zero Element of NAT;
LM00:
for n be non zero Nat,
D be non empty set,
p be Element of n-tuples_on D
holds len p = n & p is Element of D*
proof
let n be non zero Nat,
D be non empty set,
p be Element of n-tuples_on D;
p in n-tuples_on D;
then ex s be Element of D* st p = s & len s = n;
hence thesis;
end;
theorem LM01:
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))
proof
let u1,v1,w1 be Element of n-tuples_on BOOLEAN;
B1: len Op-XOR(Op-XOR(u1,v1),w1) = n by LM00;
B2: len Op-XOR(u1,Op-XOR(v1,w1)) = n by LM00;
now let i be Nat;
assume 1 <= i & i <= len Op-XOR(Op-XOR(u1,v1),w1);
then
A1: i in Seg n by B1;
thus (Op-XOR(Op-XOR(u1,v1),w1)).i
= (Op-XOR(u1,v1)).i 'xor' w1.i by DESCIP_1:def 4,A1
.= (u1.i 'xor' v1.i) 'xor' w1.i by DESCIP_1:def 4,A1
.= u1.i 'xor' (v1.i 'xor' w1.i) by XBOOLEAN:73
.= u1.i 'xor' (Op-XOR(v1,w1)).i by DESCIP_1:def 4,A1
.= (Op-XOR(u1,Op-XOR(v1,w1))).i by DESCIP_1:def 4,A1;
end;
hence thesis by LM00,B2,FINSEQ_1:14;
end;
definition
let n be non zero Element of NAT;
func XORB n -> BinOp of n-tuples_on BOOLEAN means
:defXORn:
for x,y being Element of n-tuples_on BOOLEAN holds it.(x,y) = Op-XOR(x,y);
existence
proof
deffunc F(Element of n-tuples_on BOOLEAN,Element of n-tuples_on BOOLEAN)
= Op-XOR($1,$2);
consider f being Function of [:n-tuples_on BOOLEAN,n-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN such that
P1: for x,y being Element of n-tuples_on BOOLEAN
holds f.(x,y) = F(x,y) from BINOP_1:sch 4;
take f;
thus thesis by P1;
end;
uniqueness
proof
let H1,H2 be BinOp of n-tuples_on BOOLEAN;
assume
A1: for x,y be Element of n-tuples_on BOOLEAN
holds H1.(x,y) = Op-XOR(x,y);
assume
A2: for x,y be Element of n-tuples_on BOOLEAN
holds H2.(x,y) = Op-XOR(x,y);
for x,y be Element of n-tuples_on BOOLEAN
holds H1.(x,y) = H2.(x,y)
proof
let x,y be Element of n-tuples_on BOOLEAN;
thus H1.(x,y) = Op-XOR(x,y) by A1
.= H2.(x,y) by A2;
end;
hence H1 = H2 by BINOP_1:2;
end;
end;
definition
let n be non zero Element of NAT;
func ZeroB n -> Element of n-tuples_on BOOLEAN equals
n |-> 0;
correctness
proof
reconsider o = 0 as Element of BOOLEAN by TARSKI:def 2;
n |-> o in n-tuples_on BOOLEAN;
hence thesis;
end;
end;
definition
let n be non zero Element of NAT;
func n-BinaryGroup -> strict addLoopStr equals
addLoopStr(# n-tuples_on BOOLEAN, XORB n, ZeroB n #);
correctness;
end;
theorem LM02:
for u1 be Element of n-tuples_on BOOLEAN holds Op-XOR(u1,ZeroB n) = u1
proof
let u1 be Element of n-tuples_on BOOLEAN;
B1: len Op-XOR(u1,ZeroB n) = n by LM00;
B2: len u1 = n by LM00;
now let i be Nat;
assume 1 <= i & i <= len Op-XOR(u1,ZeroB n);
then
A1: i in Seg n by B1;
thus (Op-XOR(u1,ZeroB n)).i
= u1.i 'xor' (ZeroB n).i by DESCIP_1:def 4,A1
.= u1.i 'xor' FALSE
.= u1.i;
end;
hence thesis by LM00,B2,FINSEQ_1:14;
end;
theorem LM03:
for u1 be Element of n-tuples_on BOOLEAN holds Op-XOR(u1,u1) = ZeroB n
proof
let u1 be Element of n-tuples_on BOOLEAN;
B1: len Op-XOR(u1,u1) = n by LM00;
B2: len ZeroB n = n by LM00;
now let i be Nat;
assume 1 <= i & i <= len Op-XOR(u1,u1); then
A1: i in Seg n by B1;
thus (Op-XOR(u1,u1)).i = u1.i 'xor' u1.i by DESCIP_1:def 4,A1
.= FALSE by XBOOLEAN:147
.= (ZeroB n).i;
end;
hence thesis by LM00,B2,FINSEQ_1:14;
end;
registration
let n be non zero Element of NAT;
cluster n-BinaryGroup -> add-associative right_zeroed
right_complementable Abelian non empty;
coherence
proof
set IT = n-BinaryGroup;
hereby
let u,v,w be Element of IT;
reconsider u1 = u,v1 = v,w1 = w as Element of n-tuples_on BOOLEAN;
Q1: u + v = Op-XOR(u1,v1) by defXORn;
Q2: v + w = Op-XOR(v1,w1) by defXORn;
thus (u + v) + w = Op-XOR(Op-XOR(u1,v1),w1) by Q1,defXORn
.=Op-XOR(u1,Op-XOR(v1,w1)) by LM01
.=u + (v + w) by Q2,defXORn;
end;
hereby
let v be Element of IT;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
thus v + 0.IT = Op-XOR(v1,(ZeroB n)) by defXORn
.=v by LM02;
end;
hereby
let v be Element of IT;
thus v is right_complementable
proof
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
take v;
thus v + v = Op-XOR(v1,v1) by defXORn
.= 0.IT by LM03;
end;
end;
hereby
let u,v be Element of IT;
reconsider u1 = u,v1 = v as Element of n-tuples_on BOOLEAN;
thus u + v = Op-XOR(v1,u1) by defXORn
.= v + u by defXORn;
end;
thus thesis;
end;
end;
registration
cluster -> boolean for Element of Z_2;
coherence by BSPACE:3;
end;
registration
let u,v be Element of Z_2;
identify u + v with u 'xor' v;
compatibility
proof
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose u = 0.Z_2;
hence thesis by RLVECT_1:4,BSPACE:5;
end;
suppose
A1: u = 1.Z_2;
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose v = 0.Z_2;
hence thesis by RLVECT_1:4,BSPACE:5;
end;
suppose v = 1.Z_2;
hence thesis by A1,BSPACE:5,BSPACE:7,XBOOLEAN:147;
end;
end;
end;
identify u * v with u '&' v;
compatibility
proof
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose
A1: u = 0.Z_2;
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose v = 0.Z_2;
then u*v = (0.Z_2)*(0.Z_2) by A1
.= 0 by BSPACE:5;
hence thesis by A1,BSPACE:5;
end;
suppose v = 1.Z_2;
then u*v = (0.Z_2)*(1.Z_2) by A1
.= 0 by BSPACE:5;
hence thesis by A1,BSPACE:5;
end;
end;
suppose
A4: u = 1.Z_2;
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose
A5: v = 0.Z_2;
then u*v = (1.Z_2)*(0.Z_2) by A4
.= 0 by BSPACE:5;
hence thesis by A5,BSPACE:5;
end;
suppose v = 1.Z_2;
hence thesis by A4,VECTSP_1:def 6;
end;
end;
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
:defMLTB:
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;
existence
proof
defpred P1[boolean number,boolean-valued Function,
boolean-valued Function] means
for i be set st i in Seg n holds $3.i = $1 '&' $2.i;
A1: for a being Element of BOOLEAN
for x being Element of n-tuples_on BOOLEAN
ex z being Element of n-tuples_on BOOLEAN st P1[a,x,z]
proof
let a be Element of BOOLEAN,
x be Element of n-tuples_on BOOLEAN;
deffunc H1(element) = a '&' (x.$1);
consider s being Function such that
A13: dom s = Seg n and
A14: for i being element st i in Seg n
holds s.i = H1(i) from FUNCT_1:sch 3;
X1: now let y be element;
assume y in rng s;
then consider i being element such that
A15: i in dom s and
A16: y = s.i by FUNCT_1:def 3;
y = a '&' (x.i) by A13, A14, A15, A16;
then (y = FALSE or y = TRUE) by XBOOLEAN:def 3;
hence y in BOOLEAN;
end;
reconsider s as boolean-valued Function by X1,TARSKI:def 3,
MARGREL1:def 16;
s is Function of Seg n,BOOLEAN by A13,FUNCT_2:2,TARSKI:def 3,X1;
then s is Element of Funcs ((Seg n),BOOLEAN) by FUNCT_2:8;
then reconsider s as Element of n-tuples_on BOOLEAN by FINSEQ_2:93;
for i being set st i in Seg n holds s.i = a '&' x.i by A14;
hence thesis;
end;
ex f being Function of [:BOOLEAN,n-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN st for a being Element of BOOLEAN
for x being Element of n-tuples_on BOOLEAN
holds P1[a,x,f.(a,x)] from BINOP_1:sch 3(A1);
hence thesis by BSPACE:3;
end;
uniqueness
proof
let f1,f2 be Function of [:the carrier of Z_2,
n-tuples_on BOOLEAN:],n-tuples_on BOOLEAN;
assume
A1: for a be Element of BOOLEAN,x be Element of n-tuples_on BOOLEAN
holds for i be set st i in Seg n holds (f1.(a,x)).i = a '&' x.i;
assume
A2: for a be Element of BOOLEAN, x be Element of n-tuples_on BOOLEAN
holds for i be set st i in Seg n
holds (f2.(a,x)).i = a '&' x.i;
now let a be Element of the carrier of Z_2,
x be Element of n-tuples_on BOOLEAN;
A5: len (f1.(a,x)) = n by CARD_1:def 7;
A6: len (f2.(a,x)) = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len (f1.(a,x)); then
A7: i in Seg n by A5;
thus (f1.(a,x)).i = a '&' x.i by A1,A7,BSPACE:3
.= (f2.(a,x)).i by A2,A7,BSPACE:3;
end;
hence f1.(a,x) = f2.(a,x) by FINSEQ_1:14,CARD_1:def 7,A6;
end;
hence f1 = f2 by BINOP_1:2;
end;
end;
definition
let n be non zero Element of NAT;
func n-BinaryVectSp -> VectSp of Z_2 equals
VectSpStr(# n-tuples_on BOOLEAN,XORB n,ZeroB n,MLTB n #);
correctness
proof
set X = Z_2;
set X0 = n-tuples_on BOOLEAN;
set Z0 = ZeroB n;
set ADD = XORB n;
set LMLT = MLTB n;
set XP = VectSpStr(# X0, ADD,Z0,LMLT #);
reconsider 1X = TRUE as Element of Z_2 by BSPACE:6;
Q1: XP is scalar-distributive vector-distributive scalar-associative
scalar-unital
proof
thus XP is scalar-distributive
proof
let x,y be Element of X;
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider xyv1 = (x + y) * v as Element of n-tuples_on BOOLEAN;
reconsider xv = x * v as Element of n-tuples_on BOOLEAN;
reconsider yv = y * v as Element of n-tuples_on BOOLEAN;
reconsider xyv2 = x * v + y * v as Element of n-tuples_on BOOLEAN;
A4: len xyv1 = n by CARD_1:def 7;
A5: len xyv2 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len xyv1;
then
A7: i in Seg n by A4;
A8: xv.i = x '&' (v1.i) by defMLTB,A7,BSPACE:3;
A9: yv.i = y '&' (v1.i) by defMLTB,A7,BSPACE:3;
thus xyv1.i = (x 'xor' y) '&' (v1.i) by defMLTB,A7,BSPACE:3
.= xv.i 'xor' yv.i by XBOOLEAN:75,A8,A9
.= (Op-XOR(xv,yv)).i by DESCIP_1:def 4,A7
.= xyv2.i by defXORn;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A5;
end;
thus XP is vector-distributive
proof
let x be Element of X;
let v,w be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider w1 = w as Element of n-tuples_on BOOLEAN;
reconsider xvw1 = x * (v + w) as Element of n-tuples_on BOOLEAN;
reconsider vw = v + w as Element of n-tuples_on BOOLEAN;
reconsider xv = x * v as Element of n-tuples_on BOOLEAN;
reconsider xw = x * w as Element of n-tuples_on BOOLEAN;
reconsider xvw2 = x * v + x * w as Element of n-tuples_on BOOLEAN;
A4: len xvw1 = n by CARD_1:def 7;
A5: len xvw2 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len xvw1;
then
A7: i in Seg n by A4;
A8: xv.i = x '&' (v1.i) by defMLTB,A7,BSPACE:3;
A9: xw.i = x '&' (w1.i) by defMLTB,A7,BSPACE:3;
A10: vw.i = (Op-XOR(v1,w1)).i by defXORn
.= v1.i 'xor' w1.i by DESCIP_1:def 4,A7;
thus xvw2.i = (Op-XOR(xv,xw)).i by defXORn
.= (x '&' (v1.i)) 'xor' (x '&' (w1.i)) by DESCIP_1:def 4,A7,A8,A9
.= x '&' (vw.i) by XBOOLEAN:75,A10
.= xvw1.i by defMLTB,A7,BSPACE:3;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A5;
end;
thus XP is scalar-associative
proof
let x,y be Element of X;
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider xyv1 = (x*y)*v as Element of n-tuples_on BOOLEAN;
reconsider yv1 = y*v as Element of n-tuples_on BOOLEAN;
reconsider xyv2 = x*(y*v) as Element of n-tuples_on BOOLEAN;
A4: len xyv1 = n by CARD_1:def 7;
A5: len xyv2 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len xyv1; then
A7: i in Seg n by A4;
A8: (yv1.i) = y '&' (v1.i) by defMLTB,A7,BSPACE:3;
thus xyv2.i = x '&' (yv1.i) by defMLTB,A7,BSPACE:3
.= (x '&' y) '&' (v1.i) by A8
.= xyv1.i by defMLTB,A7,BSPACE:3;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A5;
end;
thus XP is scalar-unital
proof
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider w1 = (MLTB n).(1X,v1) as Element of n-tuples_on BOOLEAN;
A4: len v1 = n by CARD_1:def 7;
A5: len w1 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len v1;
then i in Seg n by A4;
hence w1.i = TRUE '&' v1.i by defMLTB
.= v1.i;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A5,BSPACE:6;
end;
end;
Q2: XP is add-associative
proof
for u,v,w being Element of XP holds (u + v) + w = u + (v + w)
proof
let u,v,w be Element of XP;
reconsider u1 = u,v1 = v,w1 = w as Element of n-tuples_on BOOLEAN;
Q11: u + v = Op-XOR(u1,v1) by defXORn;
Q12: v + w = Op-XOR(v1,w1) by defXORn;
thus (u + v) + w = Op-XOR(Op-XOR(u1,v1),w1) by Q11,defXORn
.= Op-XOR(u1,Op-XOR(v1,w1)) by LM01
.= u + (v + w) by Q12,defXORn;
end;
hence thesis by RLVECT_1:def 3;
end;
Q3: XP is right_zeroed
proof
for v being Element of XP holds v + 0.XP = v
proof
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
thus v + 0.XP = Op-XOR(v1,(ZeroB n)) by defXORn
.= v by LM02;
end;
hence thesis by RLVECT_1:def 4;
end;
Q4: XP is right_complementable
proof
for x being Element of XP holds x is right_complementable
proof
let v be Element of XP;
ex y be Element of XP st v + y = 0.XP
proof
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
take v;
thus v + v = Op-XOR(v1,v1) by defXORn
.= 0.XP by LM03;
end;
hence thesis by ALGSTR_0:def 11;
end;
hence thesis by ALGSTR_0:def 16;
end;
XP is Abelian
proof
for v,w being Element of XP holds v + w = w + v
proof
let u,v be Element of XP;
reconsider u1 = u,v1 = v as Element of n-tuples_on BOOLEAN;
thus (u + v) = Op-XOR(v1,u1) by defXORn
.= v + u by defXORn;
end;
hence thesis by RLVECT_1:def 2;
end;
hence thesis by Q1,Q2,Q3,Q4;
end;
end;
registration
let n be non zero Element of NAT;
cluster n-BinaryVectSp -> finite;
coherence;
end;
registration
let n be non zero Element of NAT;
cluster -> finite for Subspace of n-BinaryVectSp;
coherence
proof
let V be Subspace of n-BinaryVectSp;
the carrier of V c= the carrier of n-BinaryVectSp by VECTSP_4:def 2;
hence thesis;
end;
end;
theorem VLM0302A:
for n being Nat holds Sum(n|->0.Z_2) = 0.Z_2
proof
let n be Nat;
set x = n|->0.Z_2;
A0: len x = len x;
now let k be Nat;
assume k in dom x;
then x/.k = x.k by PARTFUN1:def 6
.= 0.Z_2 by BSPACE:5;
hence x.k = x/.k + x/.k by BSPACE:5;
end;
then
A4:Sum(x) - Sum(x) = Sum(x) + Sum(x) - Sum(x) by A0,RLVECT_2:2;
Sum(x) + Sum(x) - Sum(x) = Sum(x) + (Sum(x) - Sum(x)) by RLVECT_1:28
.= Sum(x) + 0.Z_2 by RLVECT_1:15
.= Sum(x) by BSPACE:5;
hence thesis by A4,RLVECT_1:15;
end;
theorem VLM0302:
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
proof
defpred P[Nat] means
for m be non zero Element of NAT,
x be FinSequence of Z_2,
v be Element of Z_2,
j be Nat
st $1 = m & 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;
P0: P[0];
PN: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A1: P[k];
for m be non zero Element of NAT, x be FinSequence of Z_2,
v be Element of Z_2, j be Nat
st k + 1 = m & 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
proof
let m be non zero Element of NAT, x be FinSequence of Z_2,
v be Element of Z_2, j be Nat;
assume
A2: k + 1 = m & 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);
reconsider xk = x|k as FinSequence of Z_2;
W9: k <= k + 1 by NAT_1:11;
W0: len xk = k by A2,NAT_1:11,FINSEQ_1:59;
W1: len x = len xk + 1 by A2,NAT_1:11,FINSEQ_1:59;
W3: xk = x | dom xk by W0,FINSEQ_1:def 3;
AA: len ((len xk)|->0.Z_2) = len xk by CARD_1:def 7;
per cases;
suppose
A21: j = m;
then
A23: x.(len x) = v by A2;
for i be Nat st i in dom xk holds xk.i = ((len xk)|->0.Z_2).i
proof
let i be Nat;
assume
A230: i in dom xk;
then
A232: i in Seg k by W0,FINSEQ_1:def 3;
then
A231: i in Seg m by A2,W9,FINSEQ_1:5,TARSKI:def 3;
1 <= i & i <= k by FINSEQ_1:1,A232;
then i <> j by A2,A21,NAT_1:13;
then x.i = 0.Z_2 by A2,A231;
then xk.i = 0.Z_2 by A230,W3,FUNCT_1:49;
hence thesis by BSPACE:5;
end; then
BBB: xk = (len xk)|->0.Z_2 by AA,FINSEQ_2:9;
thus Sum(x) = Sum(xk) + v by RLVECT_1:38,W1,W3,A23
.= v + 0.Z_2 by BBB,VLM0302A
.= v by BSPACE:5;
end;
suppose
A22: j <> m;
A221: 1 <= j & j <= m by A2,FINSEQ_1:1;
then j < m by A22,XXREAL_0:1;
then j <= k by A2,NAT_1:13;
then
A224: j in Seg k by A221;
A226: k <> 0 by A2,A22,XXREAL_0:1,A221;
for i be Nat st i in Seg k holds (i = j implies xk.i = v) &
(i <> j implies xk.i = 0.Z_2)
proof
let i be Nat;
assume
A228: i in Seg k;
A229: Seg k c= Seg m by A2,NAT_1:11,FINSEQ_1:5;
xk.i = x.i by A228,FUNCT_1:49;
hence (i = j implies xk.i = v) &
(i <> j implies xk.i = 0.Z_2) by A2,A228,A229;
end;
then
A225: Sum(xk) = v by W0,A1,A224,A226;
A226: m in Seg m by FINSEQ_1:3;
A23: x.(len x) = 0.Z_2 by A2,A226,A22;
thus Sum(x) = v + 0.Z_2 by RLVECT_1:38,W1,W3,A23,A225
.= v by BSPACE:5;
end;
end;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(P0,PN);
hence thesis;
end;
theorem VLM0303A:
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
proof
let L be the carrier of (n-BinaryVectSp)-valued FinSequence,
j be Nat;
assume
A1: len L = m & m <= n & j in Seg n;
defpred P1[Nat,set] means ex K be Element of n-tuples_on BOOLEAN
st K = L.$1 & $2 = K.j;
A11: for i be Nat st i in Seg m ex y being Element of BOOLEAN st P1[i,y]
proof
let i be Nat;
assume i in Seg m;
then i in dom L by A1,FINSEQ_1:def 3;
then L/.i = L.i by PARTFUN1:def 6;
then reconsider K = L.i as Element of n-tuples_on BOOLEAN;
take K.j;
thus P1[i,K.j];
end;
consider x being FinSequence of BOOLEAN such that
A12: dom x = Seg m & for i be Nat st i in Seg m holds P1[i,x.i]
from FINSEQ_1:sch 5 (A11);
len x = m by FINSEQ_1:def 3, A12;
hence thesis by A12,BSPACE:3;
end;
theorem VLM0303B:
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
proof
let L be the carrier of (n-BinaryVectSp)-valued FinSequence,
Suml be Element of n-tuples_on BOOLEAN,
j be Nat;
assume
A1: len L = m & m <= n & Suml = Sum(L) & j in Seg n;
then consider x be FinSequence of Z_2 such that
P1: 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 by VLM0303A;
consider f being Function of NAT, n-BinaryVectSp such that
P2: Sum(L) = f.(len L) & f.0 = 0.(n-BinaryVectSp) &
(for j being Nat for v being Element of (n-BinaryVectSp)
st j < len L & v = L.(j + 1) holds f.(j + 1) = (f.j) + v)
by RLVECT_1:def 12;
defpred P1[Nat,set] means ex K be Element of n-tuples_on BOOLEAN
st K = f.$1 & $2 = K.j;
A11: for i be Element of NAT ex y being Element of the carrier of Z_2
st P1[i,y]
proof
let i be Element of NAT;
reconsider K = f.i as Element of n-tuples_on BOOLEAN;
reconsider y = K.j as Element of Z_2 by BSPACE:3;
take y;
thus P1[i,y];
end;
consider g being Function of NAT, Z_2 such that
P2J: for i be Element of NAT holds P1[i,g.i] from FUNCT_2:sch 3 (A11);
set Sumlj = Suml.j;
P3: Sumlj = g.(len x)
proof
ex K be Element of n-tuples_on BOOLEAN st K = f.(len L) & g.(len L) = K.j
by P2J;
hence Sumlj = g.(len x) by A1,P2,P1;
end;
P4: g.0 = 0.Z_2
proof
ex K be Element of n-tuples_on BOOLEAN st K = f.0 & g.0 = K.j by P2J;
hence g.0 = 0.Z_2 by P2,BSPACE:5;
end;
P5: for k being Nat for vj being Element of Z_2
st k < len x & vj = x.(k + 1) holds g.(k + 1) = (g.k) + vj
proof
let k be Nat, vj be Element of Z_2;
assume
P51: k < len x & vj = x.(k + 1);
then 1 <= k + 1 & k + 1 <= len x by NAT_1:11,NAT_1:13;
then k + 1 in Seg m by P1;
then consider LVn be Element of n-tuples_on BOOLEAN such that
P52: LVn = L.(k + 1) & x.(k + 1) = LVn.j by P1;
reconsider Vn = LVn as Element of (n-BinaryVectSp);
consider K1 be Element of n-tuples_on BOOLEAN such that
P55: K1 = f.(k + 1) & g.(k + 1) = K1.j by P2J;
reconsider VK1 = K1 as Element of (n-BinaryVectSp);
for i be Nat holds P1[i,g.i]
proof
let i be Nat;
i is Element of NAT by ORDINAL1:def 12;
hence thesis by P2J;
end; then
consider K0 be Element of n-tuples_on BOOLEAN such that
P56: K0 = f.k & g.k = K0.j;
reconsider VK0 = K0 as Element of (n-BinaryVectSp);
VK0 + Vn = Op-XOR(K0,LVn) by defXORn;
hence g.(k + 1) = (g.k) + vj by P55,P2,P51,P52,A1,P1,P56,DESCIP_1:def 4;
end;
(Suml).j = Sum(x) by P3,P4,P5,RLVECT_1:def 12;
hence thesis by P1;
end;
theorem VLM0300:
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))
proof
assume
A0: m <= n;
defpred P[Nat,Function] means for j be Nat st j in Seg n
holds ($1 = j implies $2.j = TRUE) & ($1 <> j implies $2.j = FALSE);
A1: for k be Nat st k in Seg m ex x being Element of n-tuples_on BOOLEAN
st P[k,x]
proof
let k be Nat;
assume k in Seg m;
defpred P1[Nat,set] means (k = $1 implies $2 = TRUE) &
(k <> $1 implies $2 = FALSE);
A11: for j be Nat st j in Seg n ex y being Element of BOOLEAN st P1[j,y]
proof
let j be Nat;
assume j in Seg n;
per cases;
suppose
C1: k = j;
take TRUE;
thus P1[j,TRUE] by C1;
end;
suppose
C2: k <> j;
take FALSE;
thus P1[j,FALSE] by C2;
end;
end;
consider x being FinSequence of BOOLEAN such that
A12: dom x = Seg n & for j be Nat st j in Seg n holds P1[j,x.j]
from FINSEQ_1:sch 5 (A11);
reconsider x as Element of (BOOLEAN)* by FINSEQ_1:def 11;
len x = n by A12,FINSEQ_1:def 3;
then x in {s where s is Element of BOOLEAN*: len s = n};
then reconsider x as Element of n-tuples_on BOOLEAN;
take x;
thus P[k,x] by A12;
end;
consider A being FinSequence of n-tuples_on BOOLEAN such that
A2: dom A = Seg m &
for k be Nat st k in Seg m holds P[k,A.k] from FINSEQ_1:sch 5 (A1);
take A;
thus len A = m by A2,FINSEQ_1:def 3;
A3: for x,y be element st x in dom A & y in dom A & A.x = A.y holds x = y
proof
let x,y be element;
assume
AA1: x in dom A & y in dom A & A.x = A.y;
then reconsider i1 = x, i2 = y as Nat;
assume
XX1: x <> y;
YY1: Seg m c= Seg n by A0,FINSEQ_1:5;
(A.i2).i1 = FALSE by XX1,AA1,A2,YY1;
hence contradiction by AA1,A2,YY1;
end;
hence A is one-to-one by FUNCT_1:def 4;
A5: card (dom A) = m by FINSEQ_1:57,A2;
dom A, rng A are_equipotent by A3,FUNCT_1:def 4,WELLORD2:def 4;
hence card (rng A) = m by A5,CARD_1:5;
thus thesis by A2;
end;
theorem VLM0301:
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)
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp,
l be Linear_Combination of B,
Suml be Element of n-tuples_on BOOLEAN;
assume that
A1: rng A = B and
A2: m <= n and
A3: len A = m and
A4: Suml = Sum l and
A5: A is one-to-one and
A6: 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);
set V = n-BinaryVectSp;
let j be Nat;
assume
P1: j in Seg m;
reconsider FA = A as FinSequence of V;
P1X: j in Seg n by P1,A2,FINSEQ_1:5,TARSKI:def 3;
A7: Carrier l c= rng FA by A1,VECTSP_6:def 4;
Z1: len (l (#) FA) = m by A3,VECTSP_6:def 5;
Suml = Sum (l (#) FA) by VECTSP_9:3,A5,A7,A4;
then consider x be FinSequence of Z_2 such that
P2: 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 (#) FA).i &
x.i = K.j by VLM0303B,A2,P1X,Z1;
P3: for i be Nat st i in Seg m holds (i = j implies x.i = l.(A.j)) &
(i <> j implies x.i = 0.Z_2)
proof
let i be Nat;
assume
PX1: i in Seg m;
then consider K be Element of n-tuples_on BOOLEAN such that
PX2: K = (l (#) FA).i & x.i = K.j by P2;
P2X: i in Seg n by PX1,A2,FINSEQ_1:5,TARSKI:def 3;
PX5: i in dom (l (#) FA) by FINSEQ_1:def 3,PX1,Z1;
PX3: K = (l.(FA/.i)) * (FA/.i) by PX2,PX5,VECTSP_6:def 5;
reconsider FAi = (FA/.i) as Element of n-tuples_on BOOLEAN;
set lFAi = l.(FA/.i);
PX8: K.j = lFAi '&' (FAi.j) by defMLTB,P1X,PX3,BSPACE:3;
PX10: i in dom A by A3,FINSEQ_1:def 3,PX1;
then
PX7: FAi.j = (A.i).j by PARTFUN1:def 6;
thus i = j implies x.i = l.(A.j)
proof
assume
XX: i = j;
then K.j = lFAi '&' TRUE by A6,P1X,PX1,PX8,PX7;
hence x.i = l.(A.j) by XX,PX2,PX10,PARTFUN1:def 6;
end;
assume i <> j;
then K.j = lFAi '&' FALSE by A6,P1,P2X,PX8,PX7;
hence x.i = 0.Z_2 by PX2,BSPACE:5;
end;
j in dom A by A3,P1,FINSEQ_1:def 3;
then l.(A.j) is Element of Z_2 by PARTFUN1:4,FUNCT_2:5;
hence thesis by VLM0302,P1,P2,P3;
end;
theorem VLM0302X:
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
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp;
assume that
A1: rng A = B and
A2: m <= n and
A3: len A = m and
A4: A is one-to-one and
A5: 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);
set V = n-BinaryVectSp;
for l being Linear_Combination of B st Sum l = 0.V
holds Carrier l = {}
proof
let l be Linear_Combination of B;
assume
P1: Sum l = 0.V;
assume Carrier l <> {};
then consider x be element such that
P3: x in Carrier l by XBOOLE_0:def 1;
consider v be Element of V such that
P4: x = v & l.v <> 0.Z_2 by P3;
P2: Carrier l c= B by VECTSP_6:def 4;
reconsider Suml = Sum l as Element of n-tuples_on BOOLEAN;
consider j be element such that
P7: j in dom A & v = A.j by A1,P2,P3,P4,FUNCT_1:def 3;
P8: j in Seg m by A3,P7,FINSEQ_1:def 3;
reconsider j as Nat by P7;
(Suml).j = l.(A.j) by VLM0301,A1,A2,A3,A4,A5,P8;
hence contradiction by P1,P4,P7,BSPACE:5;
end;
hence thesis by VECTSP_7:def 1;
end;
theorem VLM0303X:
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)
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp,
v be Element of n-tuples_on BOOLEAN;
assume that
A1: rng A = B and
A2: len A = n and
A3: A is one-to-one;
set V = n-BinaryVectSp;
defpred P1[element,element] means ex j be Nat st j in Seg n &
$1 = A.j & $2 = v.j;
B1: for x being element st x in B ex y being element st
y in the carrier of Z_2 & P1[x,y]
proof
let x be element;
assume
P2: x in B;
consider j be element such that
P3: j in dom A & x = A.j by A1,P2,FUNCT_1:def 3;
P4: j in Seg n by A2,P3,FINSEQ_1:def 3;
reconsider j as Nat by P3;
v.j in the carrier of Z_2 by BSPACE:3;
hence thesis by P3,P4;
end;
consider l0 being Function of B,the carrier of Z_2 such that
B2: for x being element st x in B holds P1[x,l0.x] from FUNCT_2:sch 1(B1);
B3: for j be Nat st j in Seg n holds l0.(A.j) = v.j
proof
let j be Nat;
assume j in Seg n;
then
B31: j in dom A by A2,FINSEQ_1:def 3;
then consider i be Nat such that
B32: i in Seg n & A.j = A.i & l0.(A.j) = v.i by A1,FUNCT_1:3,B2;
i in dom A by A2,B32,FINSEQ_1:def 3;
hence l0.(A.j) = v.j by A3,B31,B32,FUNCT_1:def 4;
end;
set f = (the carrier of V) --> 0.Z_2;
set l = f +* l0;
B5: dom l = (dom f) \/ (dom l0) by FUNCT_4:def 1
.= (the carrier of V) \/ (dom l0) by FUNCT_2:def 1
.= (the carrier of V) \/ B by FUNCT_2:def 1
.= (the carrier of V) by XBOOLE_1:12;
rng l c= the carrier of Z_2;
then l is Function of (the carrier of V),the carrier of Z_2
by FUNCT_2:2,B5;
then reconsider l as Element of Funcs (the carrier of V,
the carrier of Z_2) by FUNCT_2:8;
X0: for v being Element of V st not v in B holds l.v = 0.Z_2
proof
let v be Element of V;
v in dom l by B5;
then
B71: v in (dom f) \/ (dom l0) by FUNCT_4:def 1;
assume not v in B;
then not v in dom l0;
then l.v = f.v by B71,FUNCT_4:def 1;
hence l.v = 0.Z_2 by FUNCOP_1:7;
end;
then reconsider l as Linear_Combination of V by VECTSP_6:def 1;
for x be element st x in Carrier l holds x in B
proof
let x be element;
assume x in Carrier l;
then ex v be Element of V st x = v & l.v <> 0.Z_2;
hence x in B by X0;
end;
then
B8: l is Linear_Combination of B by TARSKI:def 3,VECTSP_6:def 4;
for j be Nat st j in Seg n holds v.j = l.(A.j)
proof
let j be Nat;
assume
B9: j in Seg n;
then j in dom A by A2,FINSEQ_1:def 3;
then
B92: A.j in B by A1,FUNCT_1:3;
then reconsider x = A.j as Element of V;
B93: x in dom l0 by FUNCT_2:def 1,B92;
x in dom l by B5;
then
B94: x in (dom f) \/ (dom l0) by FUNCT_4:def 1;
thus l.(A.j) = l0.x by B93,B94,FUNCT_4:def 1
.= v.j by B3,B9;
end;
hence thesis by B8;
end;
theorem VLM0303:
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 = VectSpStr(# the carrier of n-BinaryVectSp,
the addF of n-BinaryVectSp, the ZeroF of n-BinaryVectSp,
the lmult of n-BinaryVectSp #)
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp;
assume that
A1: rng A = B and
A2: len A = n and
A3: A is one-to-one and
A4: 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);
set V = n-BinaryVectSp;
for x be element holds x in the carrier of (Lin B) iff x in the carrier of V
proof
let x be element;
hereby assume
X1: x in the carrier of Lin B;
the carrier of (Lin B) c= the carrier of V by VECTSP_4:def 2;
hence x in the carrier of V by X1;
end;
assume x in the carrier of V;
then reconsider v = x as Element of n-tuples_on BOOLEAN;
consider l being Linear_Combination of B such that
X3: for j be Nat st j in Seg n holds v.j = l.(A.j) by VLM0303X,A1,A2,A3;
reconsider Suml = Sum l as Element of n-tuples_on BOOLEAN;
X50: len v = n by LM00;
X51: len Suml = n by LM00;
X5: dom v = Seg n by FINSEQ_1:def 3,X50
.= dom Suml by FINSEQ_1:def 3,X51;
for j be Nat st j in dom v holds v.j = Suml.j
proof
let j be Nat;
assume j in dom v;
then
X4: j in Seg n by FINSEQ_1:def 3,X50;
thus v.j = l.(A.j) by X3,X4
.= Suml.j by VLM0301,A1,A2,A3,A4,X4;
end;
then x in Lin B by FINSEQ_1:13,X5,VECTSP_7:7;
hence x in the carrier of (Lin B) by STRUCT_0:def 5;
end;
hence thesis by TARSKI:2,VECTSP_4:31;
end;
theorem VLM03A:
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))
proof
set V = n-BinaryVectSp;
consider A be FinSequence of n-tuples_on BOOLEAN such that
P1: 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))
by VLM0300;
reconsider B = rng A as finite Subset of n-BinaryVectSp;
P2: B is linearly-independent by P1,VLM0302X;
Lin B = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V,
the lmult of V #) by P1,VLM0303;
then B is Basis of V by VECTSP_7:def 3,P2;
hence thesis by P1;
end;
theorem VLM03:
n-BinaryVectSp is finite-dimensional & dim (n-BinaryVectSp) = n
proof
set V = n-BinaryVectSp;
consider B be finite Subset of n-BinaryVectSp such that
P1: 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)
by VLM03A;
thus V is finite-dimensional by P1,MATRLIN:def 1;
hence dim V = n by P1,VECTSP_9:def 1;
end;
registration
let n be non zero Element of NAT;
cluster n-BinaryVectSp -> finite-dimensional;
coherence by VLM03;
end;
theorem
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
proof
let A be FinSequence of n-tuples_on BOOLEAN,
C be Subset of n-BinaryVectSp;
assume
P1: 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));
assume
P2: C c= rng A;
reconsider B = rng A as finite Subset of n-BinaryVectSp;
B is linearly-independent by P1,VLM0302X;
then
P3: C is linearly-independent by P2,VECTSP_7:1;
for x be element st x in C holds x in the carrier of Lin C
by VECTSP_7:8,STRUCT_0:def 5;
then reconsider C0 = C as Subset of (Lin C) by TARSKI:def 3;
Lin C0 = the VectSpStr of (Lin C) by VECTSP_9:17;
then C0 is Basis of Lin C by VECTSP_7:def 3,P3,VECTSP_9:12;
hence thesis by VECTSP_9:def 1;
end;