let X be set ; :: thesis: singletons X is linearly-independent

per cases
( X is empty or not X is empty )
;

end;

suppose
not X is empty
; :: thesis: singletons X is linearly-independent

then reconsider X = X as non empty set ;

set V = bspace X;

set S = singletons X;

for l being Linear_Combination of singletons X st Sum l = 0. (bspace X) holds

Carrier l = {}

end;set V = bspace X;

set S = singletons X;

for l being Linear_Combination of singletons X st Sum l = 0. (bspace X) holds

Carrier l = {}

proof

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

assume A1: Sum l = 0. (bspace X) ; :: thesis: Carrier l = {}

reconsider s = Sum l as Subset of X ;

set C = Carrier l;

A2: l ! (Carrier l) = l by RANKNULL:24;

assume Carrier l <> {} ; :: thesis: contradiction

then consider f being Element of (bspace X) such that

A3: f in Carrier l by SUBSET_1:4;

reconsider f = f as Subset of X ;

reconsider g = f as Element of (bspace X) ;

A4: {g} c= Carrier l by A3, ZFMISC_1:31;

reconsider n = l ! {g} as Linear_Combination of {g} ;

reconsider m = l ! ((Carrier l) \ {g}) as Linear_Combination of (Carrier l) \ {g} ;

reconsider l = l as Linear_Combination of Carrier l by A2;

reconsider t = Sum m, u = Sum n as Subset of X ;

g in {g} by TARSKI:def 1;

then A5: ( Sum n = (n . g) * g & n . g = l . g ) by RANKNULL:25, VECTSP_6:17;

l . g <> 0. Z_2 by A3, VECTSP_6:2;

then l . g = 1_ Z_2 by Th5, Th6, CARD_1:50, TARSKI:def 2;

then A6: u = f by A5, VECTSP_1:def 17;

Carrier l c= singletons X by VECTSP_6:def 4;

then f is 1 -element by A3, Th30;

then consider x being Element of X such that

A7: f = {x} by CARD_1:65;

x in f by A7, TARSKI:def 1;

then A8: f @ x = 1. Z_2 by Def3;

A9: for g being Subset of X st g <> f & g in Carrier l holds

g @ x = 0. Z_2

then Sum l = (Sum m) + (Sum n) by VECTSP_6:44;

then s = t \+\ u by Def5;

then A31: s @ x = (t @ x) + (u @ x) by Th15;

s @ x = 0. Z_2 by A1, Def3;

hence contradiction by A8, A31, A13, A6, RLVECT_1:4; :: thesis: verum

end;assume A1: Sum l = 0. (bspace X) ; :: thesis: Carrier l = {}

reconsider s = Sum l as Subset of X ;

set C = Carrier l;

A2: l ! (Carrier l) = l by RANKNULL:24;

assume Carrier l <> {} ; :: thesis: contradiction

then consider f being Element of (bspace X) such that

A3: f in Carrier l by SUBSET_1:4;

reconsider f = f as Subset of X ;

reconsider g = f as Element of (bspace X) ;

A4: {g} c= Carrier l by A3, ZFMISC_1:31;

reconsider n = l ! {g} as Linear_Combination of {g} ;

reconsider m = l ! ((Carrier l) \ {g}) as Linear_Combination of (Carrier l) \ {g} ;

reconsider l = l as Linear_Combination of Carrier l by A2;

reconsider t = Sum m, u = Sum n as Subset of X ;

g in {g} by TARSKI:def 1;

then A5: ( Sum n = (n . g) * g & n . g = l . g ) by RANKNULL:25, VECTSP_6:17;

l . g <> 0. Z_2 by A3, VECTSP_6:2;

then l . g = 1_ Z_2 by Th5, Th6, CARD_1:50, TARSKI:def 2;

then A6: u = f by A5, VECTSP_1:def 17;

Carrier l c= singletons X by VECTSP_6:def 4;

then f is 1 -element by A3, Th30;

then consider x being Element of X such that

A7: f = {x} by CARD_1:65;

x in f by A7, TARSKI:def 1;

then A8: f @ x = 1. Z_2 by Def3;

A9: for g being Subset of X st g <> f & g in Carrier l holds

g @ x = 0. Z_2

proof

A13:
t @ x = 0
let g be Subset of X; :: thesis: ( g <> f & g in Carrier l implies g @ x = 0. Z_2 )

assume that

A10: g <> f and

A11: g in Carrier l ; :: thesis: g @ x = 0. Z_2

Carrier l c= singletons X by VECTSP_6:def 4;

then g is 1 -element by A11, Th30;

then consider y being Element of X such that

A12: g = {y} by CARD_1:65;

end;assume that

A10: g <> f and

A11: g in Carrier l ; :: thesis: g @ x = 0. Z_2

Carrier l c= singletons X by VECTSP_6:def 4;

then g is 1 -element by A11, Th30;

then consider y being Element of X such that

A12: g = {y} by CARD_1:65;

now :: thesis: not g @ x <> 0. Z_2

hence
g @ x = 0. Z_2
; :: thesis: verumassume
g @ x <> 0. Z_2
; :: thesis: contradiction

then x in {y} by A12, Def3;

hence contradiction by A7, A10, A12, TARSKI:def 1; :: thesis: verum

end;then x in {y} by A12, Def3;

hence contradiction by A7, A10, A12, TARSKI:def 1; :: thesis: verum

proof

l = n + m
by A4, RANKNULL:27;
consider F being FinSequence of (bspace X) such that

A14: ( F is one-to-one & rng F = Carrier m ) and

A15: t = Sum (m (#) F) by VECTSP_6:def 6;

A16: (Sum (m (#) F)) @ x = Sum ((m (#) F) @ x) by Th34;

for F being FinSequence of (bspace X) st F is one-to-one & rng F = Carrier m holds

(m (#) F) @ x = (len F) |-> (0. Z_2)

hence t @ x = 0 by A15, A16, Th5, MATRIX_3:11; :: thesis: verum

end;A14: ( F is one-to-one & rng F = Carrier m ) and

A15: t = Sum (m (#) F) by VECTSP_6:def 6;

A16: (Sum (m (#) F)) @ x = Sum ((m (#) F) @ x) by Th34;

for F being FinSequence of (bspace X) st F is one-to-one & rng F = Carrier m holds

(m (#) F) @ x = (len F) |-> (0. Z_2)

proof

then
(m (#) F) @ x = (len F) |-> (0. Z_2)
by A14;
let F be FinSequence of (bspace X); :: thesis: ( F is one-to-one & rng F = Carrier m implies (m (#) F) @ x = (len F) |-> (0. Z_2) )

assume that

F is one-to-one and

A17: rng F = Carrier m ; :: thesis: (m (#) F) @ x = (len F) |-> (0. Z_2)

set R = (len F) |-> (0. Z_2);

set L = (m (#) F) @ x;

A18: len (m (#) F) = len F by VECTSP_6:def 5;

then A19: len ((m (#) F) @ x) = len F by Def9;

A20: for k being Nat st 1 <= k & k <= len ((m (#) F) @ x) holds

((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k

then len ((m (#) F) @ x) = len ((len F) |-> (0. Z_2)) by A19, FINSEQ_1:def 3;

hence (m (#) F) @ x = (len F) |-> (0. Z_2) by A20; :: thesis: verum

end;assume that

F is one-to-one and

A17: rng F = Carrier m ; :: thesis: (m (#) F) @ x = (len F) |-> (0. Z_2)

set R = (len F) |-> (0. Z_2);

set L = (m (#) F) @ x;

A18: len (m (#) F) = len F by VECTSP_6:def 5;

then A19: len ((m (#) F) @ x) = len F by Def9;

A20: for k being Nat st 1 <= k & k <= len ((m (#) F) @ x) holds

((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k

proof

dom ((len F) |-> (0. Z_2)) = Seg (len F)
by FUNCOP_1:13;
let k be Nat; :: thesis: ( 1 <= k & k <= len ((m (#) F) @ x) implies ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k )

assume A21: ( 1 <= k & k <= len ((m (#) F) @ x) ) ; :: thesis: ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k

A22: k in Seg (len F) by A19, A21;

len (m (#) F) = len F by VECTSP_6:def 5;

then dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;

then k in dom (m (#) F) by A19, A21;

then A23: (m (#) F) . k = (m . (F /. k)) * (F /. k) by VECTSP_6:def 5;

reconsider Fk = F /. k as Subset of X ;

A24: Carrier m c= (Carrier l) \ {f} by VECTSP_6:def 4;

dom F = Seg (len F) by FINSEQ_1:def 3;

then A25: k in dom F by A19, A21;

then A26: F /. k = F . k by PARTFUN1:def 6;

then m . (F /. k) = 1_ Z_2 by A17, A25, Th35, FUNCT_1:3;

then A27: (m (#) F) . k = Fk by A23, VECTSP_1:def 17;

A28: F /. k in Carrier m by A17, A25, A26, FUNCT_1:3;

then A29: Fk in Carrier l by A24, XBOOLE_0:def 5;

A30: Fk <> f

.= 0. Z_2 by A9, A27, A30, A29 ;

hence ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k by A22, FUNCOP_1:7; :: thesis: verum

end;assume A21: ( 1 <= k & k <= len ((m (#) F) @ x) ) ; :: thesis: ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k

A22: k in Seg (len F) by A19, A21;

len (m (#) F) = len F by VECTSP_6:def 5;

then dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;

then k in dom (m (#) F) by A19, A21;

then A23: (m (#) F) . k = (m . (F /. k)) * (F /. k) by VECTSP_6:def 5;

reconsider Fk = F /. k as Subset of X ;

A24: Carrier m c= (Carrier l) \ {f} by VECTSP_6:def 4;

dom F = Seg (len F) by FINSEQ_1:def 3;

then A25: k in dom F by A19, A21;

then A26: F /. k = F . k by PARTFUN1:def 6;

then m . (F /. k) = 1_ Z_2 by A17, A25, Th35, FUNCT_1:3;

then A27: (m (#) F) . k = Fk by A23, VECTSP_1:def 17;

A28: F /. k in Carrier m by A17, A25, A26, FUNCT_1:3;

then A29: Fk in Carrier l by A24, XBOOLE_0:def 5;

A30: Fk <> f

proof

((m (#) F) @ x) . k =
((m (#) F) . k) @ x
by A18, A19, A21, Def9
assume
Fk = f
; :: thesis: contradiction

then not f in {f} by A28, A24, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not f in {f} by A28, A24, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

.= 0. Z_2 by A9, A27, A30, A29 ;

hence ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k by A22, FUNCOP_1:7; :: thesis: verum

then len ((m (#) F) @ x) = len ((len F) |-> (0. Z_2)) by A19, FINSEQ_1:def 3;

hence (m (#) F) @ x = (len F) |-> (0. Z_2) by A20; :: thesis: verum

hence t @ x = 0 by A15, A16, Th5, MATRIX_3:11; :: thesis: verum

then Sum l = (Sum m) + (Sum n) by VECTSP_6:44;

then s = t \+\ u by Def5;

then A31: s @ x = (t @ x) + (u @ x) by Th15;

s @ x = 0. Z_2 by A1, Def3;

hence contradiction by A8, A31, A13, A6, RLVECT_1:4; :: thesis: verum