let m, n be 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
let A be 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
let B be finite Subset of (n -BinaryVectSp); ( 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 ) ) ) implies B is linearly-independent )
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 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 ) )
; B is linearly-independent
set V = n -BinaryVectSp ;
for l being Linear_Combination of B st Sum l = 0. (n -BinaryVectSp) holds
Carrier l = {}
proof
let l be
Linear_Combination of
B;
( Sum l = 0. (n -BinaryVectSp) implies Carrier l = {} )
assume A6:
Sum l = 0. (n -BinaryVectSp)
;
Carrier l = {}
assume
Carrier l <> {}
;
contradiction
then consider x being
object such that A7:
x in Carrier l
by XBOOLE_0:def 1;
consider v being
Element of
(n -BinaryVectSp) such that A8:
(
x = v &
l . v <> 0. Z_2 )
by A7;
A9:
Carrier l c= B
by VECTSP_6:def 4;
reconsider Suml =
Sum l as
Element of
n -tuples_on BOOLEAN ;
consider j being
object such that A10:
(
j in dom A &
v = A . j )
by A1, A9, A7, A8, FUNCT_1:def 3;
A11:
j in Seg m
by A3, A10, FINSEQ_1:def 3;
reconsider j =
j as
Nat by A10;
Suml . j = l . (A . j)
by Th9, A1, A2, A3, A4, A5, A11;
hence
contradiction
by A6, A8, A10, BSPACE:5;
verum
end;
hence
B is linearly-independent
by VECTSP_7:def 1; verum