let K be Ring; :: thesis: for V being LeftMod of K
for b being FinSequence of V st b is one-to-one holds
( rng b is linearly-independent iff for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) )

let V be LeftMod of K; :: thesis: for b being FinSequence of V st b is one-to-one holds
( rng b is linearly-independent iff for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) )

let b be FinSequence of V; :: thesis: ( b is one-to-one implies ( rng b is linearly-independent iff for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) ) )

assume AS: b is one-to-one ; :: thesis: ( rng b is linearly-independent iff for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) )

hereby :: thesis: ( ( for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) ) implies rng b is linearly-independent )
assume AS1: rng b is linearly-independent ; :: thesis: for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K)

let r be FinSequence of K; :: thesis: for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K)

let rb be FinSequence of V; :: thesis: ( len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V implies r = (Seg (len r)) --> (0. K) )

assume that
A1: ( len r = len b & len rb = len b ) and
A2: for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) and
A3: Sum rb = 0. V ; :: thesis: r = (Seg (len r)) --> (0. K)
DRB: dom r = dom b by ;
defpred S1[ object , object ] means ( ( \$1 in rng b & \$2 = (r * (b ")) . \$1 ) or ( not \$1 in rng b & \$2 = 0. K ) );
XA2: for x being object st x in the carrier of V holds
ex y being object st
( y in the carrier of K & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of K & S1[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S1[x,y] )

then reconsider x = x as Vector of V ;
per cases ( x in rng b or not x in rng b ) ;
suppose XA3: x in rng b ; :: thesis: ex y being object st
( y in the carrier of K & S1[x,y] )

then XA31: x in dom (b ") by ;
(b ") . x in rng (b ") by ;
then (b ") . x in dom r by ;
then r . ((b ") . x) in rng r by FUNCT_1:3;
then reconsider y = (r * (b ")) . x as Element of K by ;
S1[x,y] by XA3;
hence ex y being object st
( y in the carrier of K & S1[x,y] ) ; :: thesis: verum
end;
suppose not x in rng b ; :: thesis: ex y being object st
( y in the carrier of K & S1[x,y] )

hence ex y being object st
( y in the carrier of K & S1[x,y] ) ; :: thesis: verum
end;
end;
end;
consider L being Function of the carrier of V, the carrier of K such that
XA5: for x being object st x in the carrier of V holds
S1[x,L . x] from XA6: for v being Vector of V st not v in rng b holds
L . v = 0. K by XA5;
L is Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by ;
now :: thesis: for x being object st x in Carrier L holds
x in rng b
let x be object ; :: thesis: ( x in Carrier L implies x in rng b )
assume that
XA7: x in Carrier L and
XA8: not x in rng b ; :: thesis: contradiction
consider v being Vector of V such that
XA9: x = v and
XA10: L . v <> 0. K by XA7;
thus contradiction by XA5, XA8, XA9, XA10; :: thesis: verum
end;
then Carrier L c= rng b ;
then reconsider L = L as Linear_Combination of rng b by VECTSP_6:def 4;
XA41: dom L = the carrier of V by FUNCT_2:def 1;
rng (b ") = dom r by ;
then XA43: dom (r * (b ")) = dom (b ") by RELAT_1:27
.= rng b by ;
for i being object st i in dom (L | (rng b)) holds
(L | (rng b)) . i = (r * (b ")) . i
proof
let i be object ; :: thesis: ( i in dom (L | (rng b)) implies (L | (rng b)) . i = (r * (b ")) . i )
assume ASXA: i in dom (L | (rng b)) ; :: thesis: (L | (rng b)) . i = (r * (b ")) . i
then XA45: i in rng b ;
(L | (rng b)) . i = L . i by ;
hence (L | (rng b)) . i = (r * (b ")) . i by ; :: thesis: verum
end;
then A4: L | (rng b) = r * (b ") by ;
ZA2: dom rb = Seg (len b) by ;
ZA3: dom (L (#) b) = Seg (len (L (#) b)) by FINSEQ_1:def 3
.= Seg (len b) by VECTSP_6:def 5 ;
for i being Nat st i in dom (L (#) b) holds
(L (#) b) . i = rb . i
proof
let i be Nat; :: thesis: ( i in dom (L (#) b) implies (L (#) b) . i = rb . i )
assume ZA40: i in dom (L (#) b) ; :: thesis: (L (#) b) . i = rb . i
then ZA41: (L (#) b) . i = (L . (b /. i)) * (b /. i) by VECTSP_6:def 5;
ZA42: i in dom b by ;
then ZA45: b . i in rng b by FUNCT_1:3;
then ZA49: b . i in dom (b ") by ;
L . (b . i) = (r * (b ")) . (b . i) by
.= r . ((b ") . (b . i)) by
.= r . i by
.= r /. i by ;
then L . (b /. i) = r /. i by ;
hence (L (#) b) . i = rb . i by A2, ZA2, ZA3, ZA40, ZA41; :: thesis: verum
end;
then ZA1: rb = L (#) b by ;
reconsider B = Carrier L as finite Subset of V ;
set F0 = canFS B;
BS3: rng () = B by FUNCT_2:def 3;
rng () c= the carrier of V by TARSKI:def 3;
then reconsider F0 = canFS B as FinSequence of V by FINSEQ_1:def 4;
reconsider C = (rng b) \ B as finite Subset of V ;
set G0 = canFS C;
BS4: rng () = C by FUNCT_2:def 3;
rng () c= the carrier of V by TARSKI:def 3;
then reconsider G0 = canFS C as FinSequence of V by FINSEQ_1:def 4;
BS5: (rng F0) /\ (rng G0) = B /\ ((rng b) \ B) by
.= (B /\ (rng b)) \ B by XBOOLE_1:49
.= {} by ;
then BS6: F0 ^ G0 is one-to-one by LMBASE2A;
BS7: rng (F0 ^ G0) = B \/ ((rng b) \ B) by
.= (rng b) \/ B by XBOOLE_1:39
.= rng b by ;
BS10: L (#) G0 = (dom G0) --> (0. V) by ;
then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
A51: Sum (L (#) b) = Sum (L (#) (F0 ^ G0)) by
.= 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
.= Sum L by ;
A6: Carrier L = {} by ;
set N = { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ;
for z being object st z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } holds
z in Carrier L
proof
let z be object ; :: thesis: ( z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } implies z in Carrier L )
assume z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis:
then consider x being object such that
D70: ( x in dom b & x in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } & z = b . x ) by FUNCT_1:def 6;
reconsider x = x as Nat by D70;
consider i being Nat such that
A80: ( x = i & i in dom r & r . i <> 0. K ) by D70;
A81: b . i in rng b by ;
then A86: b . i in dom (b ") by ;
A83: L . (b . i) = (L | (rng b)) . (b . i) by
.= r . ((b ") . (b . i)) by
.= r . i by ;
reconsider bi = b . i as Element of V by A81;
L . bi <> 0. K by ;
hence z in Carrier L by ; :: thesis: verum
end;
then A8: b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= Carrier L ;
for z being object st z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } holds
z in dom b
proof
let z be object ; :: thesis: ( z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } implies z in dom b )
assume z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis: z in dom b
then consider i being Nat such that
A80: ( z = i & i in dom r & r . i <> 0. K ) ;
thus z in dom b by ; :: thesis: verum
end;
then A9: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= dom b ;
A7: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {}
proof
per cases ( rng b = {} or rng b <> {} ) ;
suppose rng b = {} ; :: thesis: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {}
then dom b = {} by RELAT_1:42;
then Y2: Seg (len r) = {} by ;
thus { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {} :: thesis: verum
proof
assume { i where i is Nat : ( i in dom r & r . i <> 0. K ) } <> {} ; :: thesis: contradiction
then consider z being object such that
Y3: z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } by XBOOLE_0:def 1;
ex i being Nat st
( z = i & i in dom r & r . i <> 0. K ) by Y3;
hence contradiction by Y2, FINSEQ_1:def 3; :: thesis: verum
end;
end;
suppose Y1: rng b <> {} ; :: thesis: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {}
b is Function of (dom b),(rng b) by FUNCT_2:1;
then { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= {} by A6, A8, A9, Y1;
hence { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {} ; :: thesis: verum
end;
end;
end;
for z being object st z in dom r holds
r . z = 0. K
proof
let z be object ; :: thesis: ( z in dom r implies r . z = 0. K )
assume X1: z in dom r ; :: thesis: r . z = 0. K
assume X2: r . z <> 0. K ; :: thesis: contradiction
reconsider i = z as Nat by X1;
i in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } by X1, X2;
hence contradiction by A7; :: thesis: verum
end;
then r = (dom r) --> (0. K) by FUNCOP_1:11;
hence r = (Seg (len r)) --> (0. K) by FINSEQ_1:def 3; :: thesis: verum
end;
assume AS2: for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) ; :: thesis:
for L being Linear_Combination of rng b st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = rng b & Sum (L (#) F) = 0. V ) holds
Carrier L = {}
proof
let L be Linear_Combination of rng b; :: thesis: ( ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = rng b & Sum (L (#) F) = 0. V ) implies Carrier L = {} )

given F being FinSequence of the carrier of V such that A4: F is one-to-one and
A5: rng F = rng b and
A6: Sum (L (#) F) = 0. V ; :: thesis:
reconsider rb = L (#) b as FinSequence of V ;
rng (L * b) c= the carrier of K ;
then reconsider r = L * b as FinSequence of K by FINSEQ_1:def 4;
B24: len rb = len b by VECTSP_6:def 5;
( rng b c= the carrier of V & dom L = the carrier of V ) by FUNCT_2:def 1;
then X2: dom r = dom b by RELAT_1:27;
then B21: len r = len b by FINSEQ_3:29;
B23: for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i)
proof
let i be Nat; :: thesis: ( i in dom rb implies rb . i = (r /. i) * (b /. i) )
assume B231: i in dom rb ; :: thesis: rb . i = (r /. i) * (b /. i)
then B233: i in dom b by ;
i in dom r by ;
then r /. i = r . i by PARTFUN1:def 6
.= L . (b . i) by
.= L . (b /. i) by ;
hence rb . i = (r /. i) * (b /. i) by ; :: thesis: verum
end;
Sum rb = Sum (L (#) F) by ;
then A5: r = (Seg (len r)) --> (0. K) by A6, AS2, B21, B23, B24;
A6: Carrier L c= rng b by VECTSP_6:def 4;
assume Carrier L <> {} ; :: thesis: contradiction
then consider x being object such that
A7: x in Carrier L by XBOOLE_0:def 1;
consider v being Element of V such that
A8: ( x = v & L . v <> 0. K ) by A7;
consider i being object such that
A9: ( i in dom b & v = b . i ) by ;
A10: r . i <> 0. K by ;
i in Seg (len r) by ;
hence contradiction by A5, A10, FUNCOP_1:7; :: thesis: verum
end;
hence rng b is linearly-independent by LMBASE2X; :: thesis: verum