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

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

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

hence singletons X is linearly-independent by 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 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:10;
reconsider f = f as Subset of X ;
reconsider g = f as Element of (bspace X) ;
A4: {g} c= Carrier l by A3, ZFMISC_1:37;
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:43;
l . g <> 0. Z_2 by A3, VECTSP_6:20;
then l . g = 1_ Z_2 by Th5, Th6, CARD_1:88, TARSKI:def 2;
then A6: u = f by A5, VECTSP_1:def 29;
Carrier l c= singletons X by VECTSP_6:def 7;
then f is Singleton by A3, Th30;
then consider x being set such that
A7: x in X and
A8: f = {x} by Def9;
x in f by A8, TARSKI:def 1;
then A9: f @ x = 1. Z_2 by Def3;
reconsider x = x as Element of X by A7;
A10: 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
A11: g <> f and
A12: 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 A12, Th30;
then consider y being set such that
A13: y in X and
A14: g = {y} by Def9;
reconsider y = y as Element of X by A13;

now

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

end;

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

end;

A15: t @ x = 0

proof

consider F being FinSequence of (bspace X) such that
A16: ( F is one-to-one & rng F = Carrier m ) and
A17: t = Sum (m (#) F) by VECTSP_6:def 9;
A18: (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

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
A19: 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;
A20: len (m (#) F) = len F by VECTSP_6:def 8;
then A21: len ((m (#) F) @ x) = len F by Def11;
A22: 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 A23: ( 1 <= k & k <= len ((m (#) F) @ x) ) ; :: thesis: ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2 )) . k
A24: k in NAT by ORDINAL1:def 13;
then A25: k in Seg (len F) by A21, A23;
len (m (#) F) = len F by VECTSP_6:def 8;
then dom (m (#) F) = Seg (len F) by FINSEQ_1:def 3;
then k in dom (m (#) F) by A21, A23, A24;
then A26: (m (#) F) . k = (m . (F /. k)) * (F /. k) by VECTSP_6:def 8;
reconsider Fk = F /. k as Subset of X ;
A27: Carrier m c= (Carrier l) \ {f} by VECTSP_6:def 7;
dom F = Seg (len F) by FINSEQ_1:def 3;
then A28: k in dom F by A21, A23, A24;
then A29: F /. k = F . k by PARTFUN1:def 8;
then m . (F /. k) = 1_ Z_2 by A19, A28, Th35, FUNCT_1:12;
then A30: (m (#) F) . k = Fk by A26, VECTSP_1:def 29;
A31: F /. k in Carrier m by A19, A28, A29, FUNCT_1:12;
then A32: Fk in Carrier l by A27, XBOOLE_0:def 5;
A33: Fk <> f

proof

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

end;

((m (#) F) @ x) . k = ((m (#) F) . k) @ x by A20, A21, A23, Def11
.= 0. Z_2 by A10, A30, A33, A32 ;
hence ((m (#) F) @ x) . k = ((len F) |-> (0. Z_2 )) . k by A25, FUNCOP_1:13; :: thesis: verum

end;

dom ((len F) |-> (0. Z_2 )) = Seg (len F) by FUNCOP_1:19;
then len ((m (#) F) @ x) = len ((len F) |-> (0. Z_2 )) by A21, FINSEQ_1:def 3;
hence (m (#) F) @ x = (len F) |-> (0. Z_2 ) by A22, FINSEQ_1:18; :: thesis: verum

end;

then (m (#) F) @ x = (len F) |-> (0. Z_2 ) by A16;
hence t @ x = 0 by A17, A18, Th5, MATRIX_3:13; :: thesis: verum

end;

l = n + m by A4, RANKNULL:27;
then Sum l = (Sum m) + (Sum n) by VECTSP_6:77;
then s = t \+\ u by Def5;
then A34: s @ x = (t @ x) + (u @ x) by Th15;
s @ x = 0. Z_2 by A1, Def3;
hence contradiction by A9, A34, A15, A6, Th5, RLVECT_1:10; :: thesis: verum

end;

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

end;

end;