let K be Ring; for V being LeftMod of K
for A being finite Subset of V holds
( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} )
let V be LeftMod of K; for A being finite Subset of V holds
( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} )
let A be finite Subset of V; ( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} )
hereby ( ( for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} ) implies A is linearly-independent )
assume BS:
A is
linearly-independent
;
for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} let L be
Linear_Combination of
A;
( ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) implies Carrier L = {} )given F being
FinSequence of the
carrier of
V such that BS2:
(
F is
one-to-one &
rng F = A &
Sum (L (#) F) = 0. V )
;
Carrier L = {} reconsider B =
Carrier L as
finite Subset of
V ;
set F0 =
canFS B;
BS3:
rng (canFS B) = B
by FUNCT_2:def 3;
rng (canFS B) c= the
carrier of
V
by TARSKI:def 3;
then reconsider F0 =
canFS B as
FinSequence of the
carrier of
V by FINSEQ_1:def 4;
reconsider C =
A \ B as
finite Subset of
V ;
set G0 =
canFS C;
BS4:
rng (canFS C) = C
by FUNCT_2:def 3;
rng (canFS C) c= the
carrier of
V
by TARSKI:def 3;
then reconsider G0 =
canFS C as
FinSequence of the
carrier of
V by FINSEQ_1:def 4;
BS5:
(rng F0) /\ (rng G0) =
B /\ (A \ B)
by BS3, FUNCT_2:def 3
.=
(B /\ A) \ B
by XBOOLE_1:49
.=
{}
by XBOOLE_1:37, XBOOLE_1:17
;
then BS6:
F0 ^ G0 is
one-to-one
by LMBASE2A;
BS7:
rng (F0 ^ G0) =
B \/ (A \ B)
by BS3, BS4, BS5, LMBASE2A
.=
A \/ B
by XBOOLE_1:39
.=
A
by VECTSP_6:def 4, XBOOLE_1:12
;
(rng G0) /\ (Carrier L) = {}
by BS5, FUNCT_2:def 3;
then BS10:
L (#) G0 = (dom G0) --> (0. V)
by LMBASE2C;
then aa:
dom (L (#) G0) = dom G0
by FUNCOP_1:13;
BS12:
Sum (L (#) F) =
Sum (L (#) (F0 ^ G0))
by EQSUMLF, BS6, BS7, BS2
.=
Sum ((L (#) F0) ^ (L (#) G0))
by VECTSP_6:13
.=
(Sum (L (#) F0)) + (Sum (L (#) G0))
by RLVECT_1:41
.=
(Sum (L (#) F0)) + (0. V)
by BS10, LMBASE2D, aa
.=
Sum (L (#) F0)
;
Sum L = 0. V
by BS2, BS3, BS12, VECTSP_6:def 6;
hence
Carrier L = {}
by VECTSP_7:def 1, BS;
verum
end;
assume AS:
for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {}
; A is linearly-independent
for L being Linear_Combination of A st Sum L = 0. V holds
Carrier L = {}
proof
let L be
Linear_Combination of
A;
( Sum L = 0. V implies Carrier L = {} )
assume BS:
Sum L = 0. V
;
Carrier L = {}
consider F0 being
FinSequence of the
carrier of
V such that P3:
(
F0 is
one-to-one &
rng F0 = Carrier L &
Sum L = Sum (L (#) F0) )
by VECTSP_6:def 6;
reconsider B =
Carrier L as
finite Subset of
V ;
reconsider C =
A \ B as
finite Subset of
V ;
set G0 =
canFS C;
BS4:
rng (canFS C) = C
by FUNCT_2:def 3;
rng (canFS C) c= the
carrier of
V
by TARSKI:def 3;
then reconsider G0 =
canFS C as
FinSequence of the
carrier of
V by FINSEQ_1:def 4;
set F =
F0 ^ G0;
BS5:
(rng F0) /\ (rng G0) =
B /\ (A \ B)
by P3, FUNCT_2:def 3
.=
(B /\ A) \ B
by XBOOLE_1:49
.=
{}
by XBOOLE_1:37, XBOOLE_1:17
;
then BS6:
F0 ^ G0 is
one-to-one
by LMBASE2A, P3;
BS7:
rng (F0 ^ G0) =
B \/ (A \ B)
by P3, BS4, BS5, LMBASE2A
.=
A \/ B
by XBOOLE_1:39
.=
A
by VECTSP_6:def 4, XBOOLE_1:12
;
BS10:
L (#) G0 = (dom G0) --> (0. V)
by BS5, P3, LMBASE2C;
then aa:
dom (L (#) G0) = dom G0
by FUNCOP_1:13;
Sum (L (#) (F0 ^ G0)) =
Sum ((L (#) F0) ^ (L (#) G0))
by VECTSP_6:13
.=
(Sum (L (#) F0)) + (Sum (L (#) G0))
by RLVECT_1:41
.=
(Sum (L (#) F0)) + (0. V)
by BS10, LMBASE2D, aa
.=
Sum (L (#) F0)
;
hence
Carrier L = {}
by AS, BS, BS6, BS7, P3;
verum
end;
hence
A is linearly-independent
by VECTSP_7:def 1; verum