let m, n be non zero Element of NAT ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ) ; :: thesis: B is linearly-independent

set V = n -BinaryVectSp ;

for l being Linear_Combination of B st Sum l = 0. (n -BinaryVectSp) holds

Carrier l = {}

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; :: thesis: 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); :: thesis: ( 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 ) ) ; :: thesis: 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

hence
B is linearly-independent
by VECTSP_7:def 1; :: thesis: verum
let l be Linear_Combination of B; :: thesis: ( Sum l = 0. (n -BinaryVectSp) implies Carrier l = {} )

assume A6: Sum l = 0. (n -BinaryVectSp) ; :: thesis: Carrier l = {}

assume Carrier l <> {} ; :: thesis: 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; :: thesis: verum

end;assume A6: Sum l = 0. (n -BinaryVectSp) ; :: thesis: Carrier l = {}

assume Carrier l <> {} ; :: thesis: 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; :: thesis: verum