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

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

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

thus singletons X is linearly-independent by A1, Th36; :: thesis: verum

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 = {}

proof

let l be Linear_Combination of singletons X; :: thesis: ( Sum l = 0. (bspace X) implies Carrier l = {} )
assume A2: Sum l = 0. (bspace X) ; :: thesis: Carrier l = {}
set C = Carrier l;
reconsider s = Sum l as Subset of X ;
assume Carrier l <> {} ; :: thesis: contradiction
then consider f being Element of (bspace X) such that
A3: f in Carrier l by SUBSET_1:10;
reconsider f = f as Subset of X ;
Carrier l c= singletons X by VECTSP_6:def 7;
then f is Singleton by A3, Th30;
then consider x being set such that
A4: x in X and
A5: f = {x} by Def9;
x in f by A5, TARSKI:def 1;
then A6: f @ x = 1. Z_2 by Def3;
reconsider x = x as Element of X by A4;
A7: s @ x = 0. Z_2 by A2, Def3;
A8: for g being Subset of X st g <> f & g in Carrier l holds
g @ x = 0. Z_2

proof

let g be Subset of X; :: thesis: ( g <> f & g in Carrier l implies g @ x = 0. Z_2 )
assume that
A9: g <> f and
A10: g in Carrier l ; :: thesis: g @ x = 0. Z_2
Carrier l c= singletons X by VECTSP_6:def 7;
then g is Singleton by A10, Th30;
then consider y being set such that
A11: y in X and
A12: g = {y} by Def9;
reconsider y = y as Element of X by A11;

now

assume g @ x <> 0. Z_2 ; :: thesis: contradiction
then x in {y} by A12, Def3;
hence contradiction by A5, A9, A12, TARSKI:def 1; :: thesis: verum

end;

hence g @ x = 0. Z_2 ; :: thesis: verum

end;

reconsider g = f as Element of (bspace X) ;
reconsider m = l ! ((Carrier l) \ {g}) as Linear_Combination of (Carrier l) \ {g} ;
reconsider n = l ! {g} as Linear_Combination of {g} ;
reconsider t = Sum m, u = Sum n as Subset of X ;
A13: l ! (Carrier l) = l by RANKNULL:24;
A14: {g} c= Carrier l by A3, ZFMISC_1:37;
reconsider l = l as Linear_Combination of Carrier l by A13;
l = n + m by A14, RANKNULL:27;
then Sum l = (Sum m) + (Sum n) by VECTSP_6:77;
then s = t \+\ u by Def5;
then A15: s @ x = (t @ x) + (u @ x) by Th15;
A16: t @ x = 0

proof

A17: 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

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
A18: rng F = Carrier m ; :: thesis: (m (#) F) @ x = (len F) |-> (0. Z_2 )
set L = (m (#) F) @ x;
set R = (len F) |-> (0. Z_2 );
A19: len (m (#) F) = len F by VECTSP_6:def 8;
then A20: len ((m (#) F) @ x) = len F by Def11;
dom ((len F) |-> (0. Z_2 )) = Seg (len F) by FUNCOP_1:19;
then A21: len ((m (#) F) @ x) = len ((len F) |-> (0. Z_2 )) by A20, FINSEQ_1:def 3;
for k being Nat st 1 <= k & k <= len ((m (#) F) @ x) holds
((m (#) F) @ x) . k = ((len F) |-> (0. Z_2 )) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((m (#) F) @ x) implies ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2 )) . k )
assume that
A22: 1 <= k and
A23: k <= len ((m (#) F) @ x) ; :: thesis: ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2 )) . k
len (m (#) F) = len F by VECTSP_6:def 8;
then A24: dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;
A25: k in NAT by ORDINAL1:def 13;
then k in dom (m (#) F) by A20, A22, A23, A24;
then A26: (m (#) F) . k = (m . (F /. k)) * (F /. k) by VECTSP_6:def 8;
dom F = Seg (len F) by FINSEQ_1:def 3;
then A27: k in dom F by A20, A22, A23, A25;
then A28: F /. k = F . k by PARTFUN1:def 8;
then A29: F /. k in Carrier m by A18, A27, FUNCT_1:12;
reconsider Fk = F /. k as Subset of X ;
m . (F /. k) = 1_ Z_2 by A18, A27, A28, Th35, FUNCT_1:12;
then A30: (m (#) F) . k = Fk by A26, VECTSP_1:def 26;
A31: Carrier m = (Carrier l) \ {f}

proof

thus Carrier m c= (Carrier l) \ {f} by VECTSP_6:def 7; :: according to XBOOLE_0:def 10 :: thesis: (Carrier l) \ {f} c= Carrier m
thus (Carrier l) \ {f} c= Carrier m :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Carrier l) \ {f} or y in Carrier m )
assume A32: y in (Carrier l) \ {f} ; :: thesis: y in Carrier m
A33: y in Carrier l by A32, XBOOLE_0:def 5;
reconsider y = y as Element of (bspace X) by A32;

now

assume A34: not y in Carrier m ; :: thesis: contradiction
m . y = l . y by A32, RANKNULL:25;
then l . y = 0. Z_2 by A34;
hence contradiction by A33, VECTSP_6:20; :: thesis: verum

end;

hence y in Carrier m ; :: thesis: verum

end;

end;

A35: Fk <> f

proof

assume Fk = f ; :: thesis: contradiction
then not f in {f} by A29, A31, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

A36: Fk in Carrier l by A29, A31, XBOOLE_0:def 5;
A37: ((m (#) F) @ x) . k = ((m (#) F) . k) @ x by A19, A20, A22, A23, Def11
.= 0. Z_2 by A8, A30, A35, A36 ;
k in Seg (len F) by A20, A22, A23, A25;
hence ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2 )) . k by A37, FUNCOP_1:13; :: thesis: verum

end;

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

end;

consider F being FinSequence of (bspace X) such that
A38: F is one-to-one and
A39: rng F = Carrier m and
A40: t = Sum (m (#) F) by VECTSP_6:def 9;
A41: (Sum (m (#) F)) @ x = Sum ((m (#) F) @ x) by Th34;
(m (#) F) @ x = (len F) |-> (0. Z_2 ) by A17, A38, A39;
hence t @ x = 0 by A40, A41, Th5, MATRIX_3:13; :: thesis: verum

end;

u = f

proof

A42: Sum n = (n . g) * g by VECTSP_6:43;
g in {g} by TARSKI:def 1;
then A43: n . g = l . g by RANKNULL:25;
l . g <> 0. Z_2 by A3, VECTSP_6:20;
then A44: l . g = 1_ Z_2 by Th5, Th6, CARD_1:88, TARSKI:def 2;
thus u = f by A42, A43, A44, VECTSP_1:def 26; :: thesis: verum

end;

hence contradiction by A6, A7, A15, A16, Th5, RLVECT_1:10; :: thesis: verum

end;

hence singletons X is linearly-independent by VECTSP_7:def 1; :: thesis: verum

end;

end;