let X be set ; singletons X is linearly-independent
per cases
( X is empty or not X is empty )
;
suppose
not
X is
empty
;
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;
( Sum l = 0. (bspace X) implies Carrier l = {} )
assume A1:
Sum l = 0. (bspace X)
;
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 <> {}
;
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;
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
A13:
t @ x = 0
proof
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)
proof
let F be
FinSequence of
(bspace X);
( 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
;
(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
let k be
Nat;
( 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) )
;
((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;
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
((m (#) F) @ x) . k =
((m (#) F) . k) @ x
by A18, A19, A21, Def9
.=
0. Z_2
by A9, A27, A30, A29
;
hence
((m (#) F) @ x) . k = ((len F) |-> (0. Z_2)) . k
by A22, FUNCOP_1:7;
verum
end;
dom ((len F) |-> (0. Z_2)) = Seg (len F)
by FUNCOP_1:13;
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;
verum
end;
then
(m (#) F) @ x = (len F) |-> (0. Z_2)
by A14;
hence
t @ x = 0
by A15, A16, Th5, MATRIX_3:11;
verum
end;
l = n + m
by A4, RANKNULL:27;
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;
verum
end; hence
singletons X is
linearly-independent
by VECTSP_7:def 1;
verum end;